• The hypothesis.
  
  

After metallurgical examination of the two fan
blade fractures suffered by G-BNNL and G-OBMG..
it became clear that there was a generic
problem affecting the -3C-1 variant of the
CFM56... The position of the fracture origin
was in the region of the blade where the
highest vibratory stresses were expected

(Page 144 from UK Air Accident Investigation Branch
report on the accident to Boeing 737-400 G-OBME near
Kegworth, Leicestershire on January 8th 1989.

• The formalisation.
  
  

forall e : fatigue(fan_blade(e)) <= 
   type(fan_blade(e), -3c-1_CFM56), 
   second_order_vibrations(e). [2]