theory simple1
begin

functions: a/0

/* without '!' before,  facts are linear. But the  rule GenA allows to  generate facts of the form A(x) with the same value 'x' infinitely times */
/* So both events of the form Ba(x) and Ca(x) can occur  */
/* moreover, each event of the form Ba(x) should be preceded by an event of the form Aa(x) */

rule GenA:
[]--[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
    "
/* an  event of type Ca(x) can occur */
   
lemma exC:
  exists-trace
    "Ex x #i. Ca(x) @i
    "

/* 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