Proof step 18 from proof replay-lpt-at (previous step)

User applied rule case distinction

And obtained the following new goals

• Proof step 19:

  replay-lpt(lpt, nx, n0)[m] = (lpf = LP_FREE ∨ m ∈ nx ⊃ mklp(m0, m1, lpf, m2) ;(lpf = LP_INDEX_NODES ∧ m0 ≠ 0 ⊃ mklp(m0, LEB_SIZE, LP_INDEX_NODES, m2);(m0 = 0 ⊃ mklp(0, 0, LP_FREE, m2);mklp(m0, m1, lpf, m2))) ), lpt[m] = mklp(m0, m1, lpf, m2), lpt[n0] = mklp(m3, m4, lpf0, m5), lpf0 = LP_INDEX_NODES, m < # lpt, n0 < # lpt, m ≤ n0 ⊦ replay-lpt(lpt, nx, n0)[n0, mklp(m3, LEB_SIZE, LP_INDEX_NODES, m5)][m] = replay-lpt(lpt, nx, n0)[m], lpf0 = LP_FREE, m3 = 0, n0 ∈ nx

• Proof step 31:

  replay-lpt(lpt, nx, n0)[m] = (lpf = LP_FREE ∨ m ∈ nx ⊃ mklp(m0, m1, lpf, m2) ;(lpf = LP_INDEX_NODES ∧ m0 ≠ 0 ⊃ mklp(m0, LEB_SIZE, LP_INDEX_NODES, m2);(m0 = 0 ⊃ mklp(0, 0, LP_FREE, m2);mklp(m0, m1, lpf, m2))) ), lpt[m] = mklp(m0, m1, lpf, m2), lpt[n0] = mklp(m3, m4, lpf0, m5), m < # lpt, n0 < # lpt, m ≤ n0, lpf0 ≠ LP_INDEX_NODES ∨ m3 = 0 ⊦ (m3 = 0 ⊃ replay-lpt(lpt, nx, n0)[n0, mklp(0, 0, LP_FREE, m5)];replay-lpt(lpt, nx, n0))[m] = replay-lpt(lpt, nx, n0)[m], lpf0 = LP_FREE, n0 ∈ nx

Rule argument

Additional information