| □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), [:S | Boolvar ::- [PL ¬ Pre1(pm, S)] ∥nf false ::- [PL S = s5 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ¬ □ R2(pm, S', S'')]], N = N'' + 1 until Boolvar, INDHYP-nat(N + 1), R1(pm, s1, S), Pre1(pm, s2), I(pm, s2), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s1), Pre2(pm, s), R1(pm, s2, S), R2(pm, s2, S), I(pm, s1), I(pm, s), G2(pm, s1, s2), R2(pm, s2, s5), R1(pm, s1, s2), I(pm, S), I(pm, s5), Pre1(pm, S) ⊦ ◇ last |
boolvar ∨ n = N + 1 ∧ N = N'' + 1 until Boolvar, ( ( ( ((s3 = s5 ∧ (false ⊃ Post2(pm, s, s3);G2(pm, s3, s4))) ∧ ¬ Pre1(pm, s3)) ∧ ¬ R2(pm, s4, S) ∨ (((s3 = s5 ∧ (false ⊃ Post2(pm, s, s3);G2(pm, s3, s4))) ∧ ¬ Pre1(pm, s3)) ∧ ¬ R2(pm, s4, S)) ∧ ¬ □ R2(pm, S', S'')) ∨ false ∨ ((s3 = s5 ∧ (false ⊃ Post2(pm, s, s3);G2(pm, s3, s4)) ∧ R2(pm, s4, S)) ∧ ¬ Pre1(pm, s3)) ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ¬ □ R2(pm, S', S'')) ∨ (¬ false ∧ ¬ Pre1(pm, s3)) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL true ∧ true] ∥nf false ::- [PL S = s5 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ¬ □ R2(pm, S', S'')] ] ∨ ( (∃ s0. (((s3 = s5 ∧ (false ⊃ Post2(pm, s, s3);G2(pm, s3, s4))) ∧ ¬ Pre1(pm, s3)) ∧ ¬ R2(pm, s4, s0)) ∧ [:S | Boolvar ::- [PL true ∧ true] ∥nf false ::- [PL S = s0 ∧ true]]) ∨ (∃ s0. (((s3 = s5 ∧ (false ⊃ Post2(pm, s, s3);G2(pm, s3, s4))) ∧ ¬ Pre1(pm, s3)) ∧ ¬ R2(pm, s4, s0)) ∧ [:S | Boolvar ::- [PL true ∧ true] ∥nf false ::- [PL S = s0 ∧ ¬ □ R2(pm, S', S'')]])) ∨ false ∨ (∃ s0. ((s3 = s5 ∧ (false ⊃ Post2(pm, s, s3);G2(pm, s3, s4)) ∧ R2(pm, s4, s0)) ∧ ¬ Pre1(pm, s3)) ∧ [:S | Boolvar ::- [PL true ∧ true] ∥nf false ::- [PL S = s0 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ¬ □ R2(pm, S', S'')] ])) ∨ ( ( ((s3 = s5 ∧ (true ⊃ Post2(pm, s, s3);G2(pm, s3, s3))) ∧ ¬ R2(pm, s3, s3)) ∧ ¬ Pre1(pm, s3) ∨ (∃ s0. (¬ boolvar ∧ (s3 = s5 ∧ (false ⊃ Post2(pm, s, s3);G2(pm, s3, s4))) ∧ ¬ R2(pm, s4, s0)) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL ¬ Pre1(pm, S)] ∥nf false ::- [PL S = s0 ∧ true]]) ∨ (∃ s0. (((s3 = s5 ∧ (false ⊃ Post2(pm, s, s3);G2(pm, s3, s3))) ∧ ¬ R2(pm, s3, s0)) ∧ ¬ Pre1(pm, s3)) ∧ [:S | Boolvar ::- [PL true ∧ true] ∥nf false ::- [PL S = s0 ∧ true]])) ∨ (∃ s0. (¬ boolvar ∧ (s3 = s5 ∧ (false ⊃ Post2(pm, s, s3);G2(pm, s3, s4))) ∧ ¬ R2(pm, s4, s0)) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL ¬ Pre1(pm, S)] ∥nf false ::- [PL S = s0 ∧ ¬ □ R2(pm, S', S'')]]) ∨ (∃ s0. (((s3 = s5 ∧ (false ⊃ Post2(pm, s, s3);G2(pm, s3, s3))) ∧ ¬ R2(pm, s3, s0)) ∧ ¬ Pre1(pm, s3)) ∧ [:S | Boolvar ::- [PL true ∧ true] ∥nf false ::- [PL S = s0 ∧ ¬ □ R2(pm, S', S'')]])) ∨ ( false ∨ (¬ boolvar ∧ false) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL ¬ Pre1(pm, S)] ∥nf false ::- [PL true ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S'))]]) ∨ (∃ s0. (¬ boolvar ∧ s3 = s5 ∧ (false ⊃ Post2(pm, s, s3);G2(pm, s3, s4)) ∧ R2(pm, s4, s0)) ∧ ¬ boolvar1 ∧ [:S | Boolvar ::- [PL ¬ Pre1(pm, S)] ∥nf false ::- [PL S = s0 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ¬ □ R2(pm, S', S'')] ]) ∨ (∃ s0. ((s3 = s5 ∧ (false ⊃ Post2(pm, s, s3);G2(pm, s3, s3)) ∧ R2(pm, s3, s0)) ∧ ¬ Pre1(pm, s3)) ∧ [:S | Boolvar ::- [PL true ∧ true] ∥nf false ::- [PL S = s0 ∧ R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ ¬ □ R2(pm, S', S'')] ]), □ (R1(pm, S', S'') ∧ R2(pm, S', S'')), INDHYP-nat(n + 1), R1(pm, s1, s3), Pre1(pm, s2), I(pm, s2), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), Pre1(pm, s1), Pre2(pm, s), R1(pm, s2, s3), R2(pm, s2, s3), I(pm, s1), I(pm, s), G2(pm, s1, s2), R2(pm, s2, s5), R1(pm, s1, s2), I(pm, s3), I(pm, s5), Pre1(pm, s3), ¬ false, boolvar1 → s3 = s4 ∧ (boolvar ↔ boolvar0) ∧ n = n0, R1(pm, s4, S), R2(pm, s4, S) ⊦ ◇ last