| [:Inpf, S, Outf | [PL ¬ GInv(S) ∨ ¬ Pr(n0 + 1)(S)] ∥ [PL ¬ GInv(S) ∨ ¬ Prton(n0)(S)]], ∀ m. m ≤ n0 + 1 → Pr(m)(S), GInv(S) ⊦ (Rton(n0 + 1)(S', S'') ∧ (GInv(S') → GInv(S''))) -+-> (last ⊃ Poton(n0 + 1)(S) ∧ GInv(S);Gton(n0 + 1)(S, S') ∧ ¬ blocked ∧ (GInv(S) → GInv(S'))) |
∀ m0. m0 ≤ n0 + 1 → Pr(m0)(s), GInv(s), true, (¬(GInv(s) ∧ Pr(n0 + 1)(s)) ∧ ¬(GInv(s) ∧ Prton(n0)(s)) ∨ false ∨ false) ∨ ¬(GInv(s) ∧ Prton(n0)(s)) ∧ ¬(GInv(s) ∧ Pr(n0 + 1)(s)) ∨ false ∨ false, (true ⊃ ¬ Poton(n0 + 1)(s) ∨ ¬ GInv(s);¬ Gton(n0 + 1)(s, s) ∨ false ∨ ¬(GInv(s) → GInv(s))) ⊦
( ¬(GInv(s) ∧ Pr(n0 + 1)(s)) ∧ ¬(GInv(s) ∧ Prton(n0)(s)) ∨ (¬ false ∧ (¬ GInv(s) ∨ ¬ Pr(n0 + 1)(s))) ∧ ¬ boolvar ∧ [:Inpf, S, Outf | [PL true ∧ true] ∥ [PL ¬ GInv(S) ∨ ¬ Prton(n0)(S)]] ∨ (¬(GInv(s) ∧ Pr(n0 + 1)(s)) ∧ ¬(GInv(s) ∧ Prton(n0)(s))) ∧ [:Inpf, S, Outf | [PL true ∧ true] ∥ [PL true ∧ true]]) ∨ ¬(GInv(s) ∧ Prton(n0)(s)) ∧ ¬(GInv(s) ∧ Pr(n0 + 1)(s)) ∨ (¬ false ∧ (¬ GInv(s) ∨ ¬ Prton(n0)(s))) ∧ ¬ boolvar ∧ [:Inpf, S, Outf | [PL ¬ GInv(S) ∨ ¬ Pr(n0 + 1)(S)] ∥ [PL true ∧ true]] ∨ (¬(GInv(s) ∧ Prton(n0)(s)) ∧ ¬(GInv(s) ∧ Pr(n0 + 1)(s))) ∧ [:Inpf, S, Outf | [PL true ∧ true] ∥ [PL true ∧ true]], ∀ m0. m0 ≤ n0 + 1 → Pr(m0)(s), GInv(s), ¬ false, boolvar → s = s0 ∧ inpf = inpf0 ∧ outf = outf0 ⊦ (false ⊃ Poton(n0 + 1)(s) ∧ GInv(s);Gton(n0 + 1)(s, s0) ∧ ¬ boolvar ∧ (GInv(s) → GInv(s0))) ∧ ( Rton(n0 + 1)(s0, S) ∧ (GInv(s0) → GInv(S)) → (Rton(n0 + 1)(S', S'') ∧ (GInv(S') → GInv(S''))) -+-> (last ⊃ Poton(n0 + 1)(S) ∧ GInv(S);Gton(n0 + 1)(S, S') ∧ ¬ blocked ∧ (GInv(S) → GInv(S'))))