|I don't really understand in which sense you say that your proposed approach reuses (T1) since SpecWeak (or its next-state relation) doesn't occur in T4. It sounds to me that really your inductive invariant should be|
IC /\ Safety
By (T4) it remains to prove
IC /\ Safety /\ SpecStrongNext => Safety'
Now, assuming that the proof of (T2) is a standard invariance proof, it will include a step
Safety /\ C /\ C' /\ SpecWeakNext => Safety'
and if we also have
SpecStrongNext => SpecWeakNext
then we are done, using the fact that IC => C. If however for proving (T1), you needed an additional invariant, you'd want to conjoin that predicate to IC /\ Safety.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/FFB7E75E-1ED9-40A2-B8DF-821CEAB201EF%40gmail.com.