theory ind2_rest
begin

/* the restriction 'once' will bind the possible traces only to traces having at most one event 'Bigger'  */
/* Hence, we do not need to use induction in order to prove the lemma Origin this time! */ 

functions: z/0, succ/1

rule Start:
[  ]  --[ Start() ]-> [ Nat(z) ]

rule Out_pk:
[ Nat(n) ] --[ Bigger() ]-> [ Nat(succ(n)) ]

restriction once:
" 
All #i #j. Bigger()@i & Bigger()@j ==> #i=#j 
"


//Properties
lemma Origin:
"
  All #i. Bigger()@i ==> Ex #j. Start()@j 
"



end