Bug.spthy

theory Bug begin

builtins: multiset


rule Start: [ Fr(~x) ] --[ Start(<x,'1'>), C(x,'1'), IsFresh(x) ]-> [ A(x,'1') ]

rule Loop:  [ A(x,n) ] --[ Loop(<x,n>), C(x,n)  ]-> [ A(x,n) ]

rule Stop:  [ A(x,n) ] --[ Stop(<x,n>), C(x,'1'+n) ]-> [ A(x,'1'+n) ]


lemma Blub [use_induction, reuse]:
  "All x #i n. C(x,n)@i ==> (Ex #j u. IsFresh(u)@j & x = u)"

lemma Loop_before_Stop [use_induction]:
  "All x #i #j. Stop(x) @ j & Loop(x) @ i ==> #i < #j"

end