theory simple6
begin

/* for each  generated fact A(x) by the rule GenA, the rule Rev will send it to the adversary which cand send it back. Moreover, since f and g are public, he can use them in order to compute new messages  */
/* So both events of the form  Ba(x) and  Ca(x) can occur */
/* lemma  Ba_Rev ensures that the adversary can learn an 'x' generated by the rule GenA, only if it was "revealed" before using the rule Rev  */

functions: a/0, g/1, f/2
equations: f(x,x) = g(x)

/*
rule GenA:
[Fr(~y)]--[Aa(~y)]->[A(~y)]

rule Rev:
[A(x)]--[Rev(x)]->[Out(x)]
*/
rule GenB:
[In(x)]--[Ba(x)]->[B(x)]


rule GenC:
[In(g(x))]--[Ca(x)]->[C(x)]


lemma exB:
  exists-trace
    "Ex x #i. Ba(x) @i
    "
lemma exC:
  exists-trace
    "Ex x #i. Ca(x) @i
    "
/*  
lemma Ba_Rev:
    "All x #i #k. (Ba(x) @i) & (Aa(x)@k)   ==> Ex #j. Rev(x)@j & j<i
    "
   
lemma Ca_Rev:
    "All x #i #k. (Ca(x) @i) & (Aa(x)@k)   ==> Ex #j. Rev(x)@j & j<i
    "
*/
end