| R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')), \A ∀ N0, R2, pm, S, Post2, s, G2, Pre2, Pre1, R1, G1, Post1, I, N. N0 < m → R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ Pre2(pm, s) ∧ Pre1(pm, s) ∧ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ I(pm, S) ∧ Post1(pm, s, S) → ((R1(pm, S', S'') ∧ R2(pm, S', S'') ∧ N = N'' + 1) ∧ N0 = N0'' +1) -+-> (last ⊃ Post1(pm, s, S) ∧ Post2(pm, s, S);G1(pm, S, S') ∨ G2(pm, S, S')), m = N0, Pre2(pm, s), Pre1(pm, s), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), I(pm, S), Post1(pm, s, S) ⊦ ((R1(pm, S', S'') ∧ R2(pm, S', S'') ∧ N = N'' + 1) ∧ N0 = N0'' +1) -+-> (last ⊃ Post1(pm, s, S) ∧ Post2(pm, s, S);G1(pm, S, S') ∨ G2(pm, S, S')) |
R2(pm, s1, S) → R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')), \A ∀ N0, R2, pm, S, Post2, s, G2, Pre2, Pre1, R1, G1, Post1, I, N. N0 < m → R2(pm, S', S'') -+-> (last ⊃ Post2(pm, s, S);G2(pm, S, S')) ∧ Pre2(pm, s) ∧ Pre1(pm, s) ∧ RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2) ∧ I(pm, S) ∧ Post1(pm, s, S) → ((R1(pm, S', S'') ∧ R2(pm, S', S'') ∧ N = N'' + 1) ∧ N0 = N0'' +1) -+-> (last ⊃ Post1(pm, s, S) ∧ Post2(pm, s, S);G1(pm, S, S') ∨ G2(pm, S, S')), m = n, Pre2(pm, s), Pre1(pm, s), RG-restr(pm, R1, G1, Pre1, Post1, I, R2, G2, Pre2, Post2), I(pm, s0), Post1(pm, s, s0), ¬ false, boolvar → s0 = s1 ∧ n = n1 ∧ n0 = n2, (false ⊃ Post2(pm, s, s0);G2(pm, s0, s1)) ⊦ (false ⊃ Post1(pm, s, s0) ∧ Post2(pm, s, s0);G1(pm, s0, s1) ∨ G2(pm, s0, s1)) ∧ ( (R1(pm, s1, S) ∧ R2(pm, s1, S) ∧ n0 = N + 1) ∧ n = N0 +1 → ((R1(pm, S', S'') ∧ R2(pm, S', S'') ∧ N = N'' + 1) ∧ N0 = N0'' +1) -+-> (last ⊃ Post1(pm, s, S) ∧ Post2(pm, s, S);G1(pm, S, S') ∨ G2(pm, S, S')))