theory ind1
begin

/* in order to prove the lemma Origin, you have to use induction */ 

functions: z/0, succ/1

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

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




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



end