theory simple2
begin

functions: a/0

/* without '!' before,  facts are linear. Fresh rule ensures that rule GenA will always generate facts of the form A(x) with a new 'x' value each time*/
/* So an event of the form Ba(x) can occur, but not an  event of type Ca(x) */
/* moreover, each event of the form Ba(x) should be preceded by an event of the form Aa(x) */

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

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

rule GenC:
[A(x), B(x)]--[Ca(x)]->[C(x)]

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

lemma exB:
  exists-trace
    "Ex x #i. Ba(x) @i
    "
/* no  event of type Ca(x) can occur */
   
lemma n_exC:
    "All x #i. Ca(x) @i ==> F"
 
/* each event of the form Ba(x) should be preceded by an event of the form Aa(x) */   

lemma A_b_C:
  "All x #i. Ba(x) @i ==> Ex #j. Aa(x)@j & j<i"

end