Proof step 105 from proof BFS-correct-if-reachable (previous step)

User applied rule if right

And obtained the following new goals

• Proof step 96:

  〈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), ∀ S2, m, n1, n2, S3, S4, source0, dest0, done. m1 = # S2 ∧ (∀ n, n0, S0, S, S1, source, dest, done0. m = 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)) ∧ m + 1 = n1 - n2 ∧ INVR(S2, S3, S4, n2, n1, source0, dest0) ∧ INV(S2, S3, S4, n2, source0) ∧ (done → dest0 ∈ S2) ∧ (S2 = ∅ → S3 = ∅) → ⟪while S2 ≠ ∅ ∧ ¬ done do { choose v with v ∈ S2 in if v = dest0 then done := true else { S2 := S2 -- v ; ADD(succ(v); S4, S3) } ; if S2 = ∅ then S2 := S3, S3 := ∅, n2 := n2 + 1 }⟫ ⟪norfail0 := (done ⊃ some(n2); fail)⟫ norfail0 = some(n1), m0 + 1 = n - n0, m1 + 1 = # S0, S2 = S0 -- v, S0 ≠ ∅, v ≠ dest, 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), S0 = ∅ ++ v ⊦ ⟪S2 := s0, s0 := ∅, n0 := n0 + 1⟫ ⟪done0 := false ; while S2 ≠ ∅ ∧ ¬ done0 do { choose v with v ∈ S2 in if v = dest then done0 := true else { S2 := S2 -- v ; ADD(succ(v); s, s0) } ; if S2 = ∅ then S2 := s0, s0 := ∅, n0 := n0 + 1 }⟫ ⟪norfail0 := (done0 ⊃ some(n0); fail)⟫ norfail0 = some(n)

• Proof step 104:

  〈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), ∀ S2, m, n1, n2, S3, S4, source0, dest0, done. m1 = # S2 ∧ (∀ n, n0, S0, S, S1, source, dest, done0. m = 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)) ∧ m + 1 = n1 - n2 ∧ INVR(S2, S3, S4, n2, n1, source0, dest0) ∧ INV(S2, S3, S4, n2, source0) ∧ (done → dest0 ∈ S2) ∧ (S2 = ∅ → S3 = ∅) → ⟪while S2 ≠ ∅ ∧ ¬ done do { choose v with v ∈ S2 in if v = dest0 then done := true else { S2 := S2 -- v ; ADD(succ(v); S4, S3) } ; if S2 = ∅ then S2 := S3, S3 := ∅, n2 := n2 + 1 }⟫ ⟪norfail0 := (done ⊃ some(n2); fail)⟫ norfail0 = some(n1), m0 + 1 = n - n0, m1 + 1 = # S0, S2 = S0 -- v, S0 ≠ ∅, v ≠ dest, 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), S0 ≠ ∅ ++ v ⊦ ⟪skip⟫ ⟪done0 := false ; while S2 ≠ ∅ ∧ ¬ done0 do { choose v with v ∈ S2 in if v = dest then done0 := true else { S2 := S2 -- v ; ADD(succ(v); s, s0) } ; if S2 = ∅ then S2 := s0, s0 := ∅, n0 := n0 + 1 }⟫ ⟪norfail0 := (done0 ⊃ some(n0); fail)⟫ norfail0 = some(n)

Rule argument

Additional information

[[CONCRETESIMPRULES : ()]]