theory simple4
begin

functions: a/0, b/0



rule GenA:
[Fr(~r)]--[Aa(~r)]->[A(~r)]

rule GenB:
[A(x)]--[Bs(x)]->[B(x)]

rule GenB2:
[B(x)]--[Ba(x)]->[B(x)]

/* an event of the form Ba(x) can occur */

lemma exB:
  exists-trace
    "Ex x #i. Ba(x) @i "

/* each event of the form Ba(x) should be preceded by an event of the form Bs(x) */   
/* but now we need to prove it by induction! */
    
lemma Bs_Ba:
    "All x #i. Ba(x) @i ==> Ex #j. Bs(x)@j & j<i
    "

end