theory Minimal_Loop_Example begin



/*
  Author: Simon Meier <simon.meier@inf.ethz.ch>
  Date:   2012 06 10
  Status: Working

  A minimal example that is looping and satisfies a property cannot be proven
  without inductive strengthening.

*/

rule Start: [ Fr(x) ] --[ Start(x) ]-> [ A(x) ]

rule Loop:  [ A(x) ]  --[ Loop(x)  ]-> [ A(x) ]

rule Stop:  [ A(x) ]  --[ Stop(x)  ]-> [ ]

lemma Start_before_Loop [reuse, use_induction]:
  "All x #j. Loop(x) @ j ==> (Ex #i. Start(x) @ i & i < j)"

lemma Start_before_Stop:
  "All x #j. Stop(x) @ j ==> (Ex #i. Start(x) @ i & i < j)"

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

lemma Stop_unique [reuse]:
  "All x #i #j. Stop(x) @ j & Stop(x) @ i ==> #i = #j"

lemma Satisfied_by_empty_trace_only [use_induction]:
  exists-trace
  "All x #j. Loop(x) @ j ==> F"

end