| ⟪while S2 ≠ ∅ ∧ ¬ done do { choose v with v ∈ S2 in if v = dest1 then done := true else { S2 := S2 -- v ; ADD(succ(v); S5, S6) } ; if S2 = ∅ then S2 := S6, S6 := ∅, n1 := n1 + 1 }⟫ ⟪norfail0 := (done ⊃ some(n1); fail)⟫ norfail0 = some(n), 〈ADD(succ(v); S1, S)〉 (S1 = s ∧ S = s0), ⟪ADD(succ(v); S1, S)⟫ (INV(S0 -- v, S, S1, n0, source) ∧ INVR(S0 -- v, S, S1, n0, n, source, dest)), ∀ n, n0, S0, S, S1, source, dest, done0. m0 = n - n0 ∧ INVR(S0, S, S1, n0, n, source, dest) ∧ INV(S0, S, S1, n0, source) ∧ (done0 → dest ∈ S0) ∧ (S0 = ∅ → S = ∅) → ⟪while S0 ≠ ∅ ∧ ¬ done0 do { choose v with v ∈ S0 in if v = dest then done0 := true else { S0 := S0 -- v ; ADD(succ(v); S1, S) } ; if S0 = ∅ then S0 := S, S := ∅, n0 := n0 + 1 }⟫ ⟪norfail0 := (done0 ⊃ some(n0); fail)⟫ norfail0 = some(n), ¬ done, m0 + 1 = n - n0, m1 + 1 = # S0, S2 = S0 -- v, S0 ≠ ∅, v ≠ dest, S0 ≠ ∅ ++ v, INVR(S0, S, S1, n0, n, source, dest), INV(S0, S, S1, n0, source), v ∈ S0, INV(S0 -- v, s0, s, n0, source), INVR(S0 -- v, s0, s, n0, n, source, dest), dest1 = dest ∧ S5 = s ∧ S6 = s0 ∧ n1 = n0 ⊦ ⟪while S2 ≠ ∅ ∧ ¬ done do { choose v with v ∈ S2 in if v = dest then done := true else { S2 := S2 -- v ; ADD(succ(v); s, s0) } ; if S2 = ∅ then S2 := s0, s0 := ∅, n0 := n0 + 1 }⟫ ⟪norfail0 := (done ⊃ some(n0); fail)⟫ norfail0 = some(n) |
[[CONCRETESIMPRULES : ()]]