| Here is a concrete, though somewhat silly example of what (I believe) Tomer means. Note that steps <1>1 and the sub-step <2>3 of <1>2 cannot currently be proved: step <1>1 requires invoking a well-founded ordering and is therefore essentially non-propositional, and step <2>3 requires proving an ENABLED predicate. VARIABLE a Init == a \in Nat Next == a'=a+1 Spec == Init /\ [][Next]_a /\ WF_a(Next) LEMMA Spec => \A n \in Nat : <>[](a > n) <1>0. Spec => [](a \in Nat) <2>1. a \in Nat /\ [Next]_a => (a \in Nat)' BY DEF Next <2>. QED BY <2>1, PTL DEF Spec, Init <1>. SUFFICES ASSUME NEW n \in Nat PROVE Spec => <>[](a > n) OBVIOUS <1>1. Spec /\ [](a \in Nat) => <>(a = n) OMITTED <1>2. Spec => [](a=n => <>(a > n)) <2>1. a=n /\ <<Next>>_a => (a>n)' BY DEF Next <2>2. a=n /\ UNCHANGED a => (a=n)' OBVIOUS <2>3. a=n => ENABLED <<Next>>_a OMITTED <2>. QED BY <2>1, <2>2, <2>3, PTL DEF Spec <1>3. Spec /\ [](a \in Nat) => [](a>n => [](a>n)) <2>1. a \in Nat /\ a>n /\ [Next]_a => (a \in Nat /\ a>n)' BY DEF Next <2>. QED BY <2>1, PTL DEF Spec <1>. QED BY <1>0, <1>1, <1>2, <1>3, PTL Best, Stephan
|