[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 56 from proof btree-clean-fwd (previous step)

# zbrar0 = BRANCH_SIZE, # asar = (n0 + n) + 1, # asar0 = # asar, # zbrar = BRANCH_SIZE, # asar1 = # asar, # asar2 = # asar, # asar = n2 + n, asar[n] = asar0[n], asar1[n] = asar2[n], zbrar[n] = mkzbranch(key, adr0, r3), zbrar0[n] = mkzbranch(key, adr0, r4), union(asar, 0, # asar) = alladrs0 -- adr, union(asar0, 0, # asar) = alladrs0 -- adr, union(asar1, 0, # asar) = alladrs1 -- adr, union(asar2, 0, # asar) = alladrs1 -- adr, (( ( ( btree(r, r3, adr0, height0, false, key-range(zbrar, n, # asar, ri1), iast, asar2[n], asar2[n], ok) * (λ n1. ⌜zbrar[n1].branch?⌝ ∧ btree(r, zbrar[n1].child, zbrar[n1].adr, height0, false, key-range(zbrar, n1, # asar, ri1), iast, asar1[n1], asar2[n1], ok) )⊗_ (0, n )) * (λ n1. ⌜zbrar[n1].branch?⌝ ∧ btree(r, zbrar[n1].child, zbrar[n1].adr, height0, false, key-range(zbrar, n1, # asar, ri1), iast, asar1[n1], asar2[n1], ok) )⊗_ (1 + n, n0 )) * P1) )(zh3), (( btree(r2, r4, adr0, height, false, key-range(zbrar0, n, # asar, ri0), iast, asar0[n], asar0[n], ok) * (λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree(r2, zbrar0[n1].child, zbrar0[n1].adr, height, false, key-range(zbrar0, n1, # asar, ri0), iast, asar[n1], asar0[n1], ok) )⊗_ (0, n ) * (λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree(r2, zbrar0[n1].child, zbrar0[n1].adr, height, false, key-range(zbrar0, n1, # asar, ri0), iast, asar[n1], asar0[n1], ok) )⊗_ (1 + n, n2 - 1 ) * P0) )(zh), n < BRANCH_SIZE, n0 + n < BRANCH_SIZE, n < # asar, ((r2 => mkznode(rp0, zbrar0, false, false, # asar)))(zh5), ((r => mkznode(rp1, zbrar, false, false, # asar)))(zh4), disj(asar, 0, # asar), disj(asar0, 0, # asar), disj(asar1, 0, # asar), disj(asar2, 0, # asar), nsize(# asar, nstat), sorted(zbrar, 0, n0 + n), sorted(zbrar0, 0, n0 + n), unmodified(adr, mkznode(rp1, zbrar, false, false, # asar), iast), unmodified(adr, mkznode(rp0, zbrar0, false, false, # asar), iast), adr ∈ iast, adr ∈ alladrs1, adr ∈ alladrs0, n ≤ # asar, alladrs1 ⊆ dom iast, alladrs0 ⊆ dom iast, asar2[n] ⊆ dom iast, asar0[n] ⊆ dom iast, zh5 ⊥ zh, zh4 ⊥ zh3, (r0 = null ⊃ P0(zh0);r2 = r0 ∧ zh5 ∪ zh = zh0), (r1 = null ⊃ P1(zh1);r = r1 ∧ zh4 ∪ zh3 = zh1), ∀ rp0, r0, adr, ri0, iast, as0, alladrs0, nstat, P0, zh0, rp1, r1, height1, ri1, as1, alladrs1, P1, zh1. ((btree(rp0, r0, adr, height, false, ri0, iast, as0, alladrs0, nstat) * P0))(zh0) ∧ ((btree(rp1, r1, adr, height1, false, ri1, iast, as1, alladrs1, nstat) * P1))(zh1) → height = height1 ∧ as0 = as1 ∧ ri0 = ri1 ∧ alladrs0 = alladrs1 ⊦ # alladrs1 = 0, # alladrs0 = 0, alladrs0 = ∅, alladrs1 = ∅, key-range(zbrar0, n, # asar, ri0) = key-range(zbrar0, n, # asar, ri1)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 57:
# zbrar0 = BRANCH_SIZE, # asar = # asar0, # asar2 = # asar0, # asar1 = # asar0, # zbrar = BRANCH_SIZE, # asar0 = (n0 + 1) + n, zbrar0[n] = mkzbranch(key, adr0, r4), zbrar[n] = mkzbranch(key, adr0, r3), asar1[n] = asar2[n], asar[n] = asar0[n], union(asar2, 0, # asar0) = alladrs1 -- adr, union(asar1, 0, # asar0) = alladrs1 -- adr, union(asar0, 0, # asar0) = alladrs0 -- adr, union(asar, 0, # asar0) = alladrs0 -- adr, (( btree(r2, r4, adr0, height, false, key-range(zbrar0, n, # asar0, ri0), iast, asar0[n], asar0[n], ok) * (λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree(r2, zbrar0[n1].child, zbrar0[n1].adr, height, false, key-range(zbrar0, n1, # asar0, ri0), iast, asar[n1], asar0[n1], ok) )⊗_ (0, n ) * (λ n1. ⌜zbrar0[n1].branch?⌝ ∧ btree(r2, zbrar0[n1].child, zbrar0[n1].adr, height, false, key-range(zbrar0, n1, # asar0, ri0), iast, asar[n1], asar0[n1], ok) )⊗_ (1 + n, n0 ) * P0) )(zh), (( ( ( btree(r, r3, adr0, height0, false, key-range(zbrar, n, # asar0, ri1), iast, asar2[n], asar2[n], ok) * (λ n1. ⌜zbrar[n1].branch?⌝ ∧ btree(r, zbrar[n1].child, zbrar[n1].adr, height0, false, key-range(zbrar, n1, # asar0, ri1), iast, asar1[n1], asar2[n1], ok) )⊗_ (0, n )) * (λ n1. ⌜zbrar[n1].branch?⌝ ∧ btree(r, zbrar[n1].child, zbrar[n1].adr, height0, false, key-range(zbrar, n1, # asar0, ri1), iast, asar1[n1], asar2[n1], ok) )⊗_ (1 + n, n0 )) * P1) )(zh3), n < BRANCH_SIZE, n0 + n < BRANCH_SIZE, ((r => mkznode(rp1, zbrar, false, false, # asar0)))(zh4), ((r2 => mkznode(rp0, zbrar0, false, false, # asar0)))(zh5), disj(asar2, 0, # asar0), disj(asar1, 0, # asar0), disj(asar0, 0, # asar0), disj(asar, 0, # asar0), nsize(# asar0, nstat), sorted(zbrar0, 0, n0 + n), sorted(zbrar, 0, n0 + n), unmodified(adr, mkznode(rp0, zbrar0, false, false, # asar0), iast), unmodified(adr, mkznode(rp1, zbrar, false, false, # asar0), iast), adr ∈ alladrs0, adr ∈ alladrs1, adr ∈ iast, asar0[n] ⊆ dom iast, asar2[n] ⊆ dom iast, alladrs0 ⊆ dom iast, alladrs1 ⊆ dom iast, zh4 ⊥ zh3, zh5 ⊥ zh, (r1 = null ⊃ P1(zh1);r = r1 ∧ zh4 ∪ zh3 = zh1), (r0 = null ⊃ P0(zh0);r2 = r0 ∧ zh5 ∪ zh = zh0), ∀ rp0, r0, adr, ri0, iast, as0, alladrs0, nstat, P0, zh0, rp1, r1, height1, ri1, as1, alladrs1, P1, zh1. ((btree(rp0, r0, adr, height, false, ri0, iast, as0, alladrs0, nstat) * P0))(zh0) ∧ ((btree(rp1, r1, adr, height1, false, ri1, iast, as1, alladrs1, nstat) * P1))(zh1) → height = height1 ∧ as0 = as1 ∧ ri0 = ri1 ∧ alladrs0 = alladrs1 ⊦ # alladrs0 = 0, # alladrs1 = 0, alladrs0 = ∅, alladrs1 = ∅, key-range(zbrar0, n, # asar0, ri0) = key-range(zbrar0, n, # asar0, ri1)

Rule argument

Additional information

Used simplifier rules: ⊦ m + 1 ≤ n ↔ m < n; (s)% ⊦ ¬ m + n < m; (s)% ⊦ m < n + 1 ↔ ¬ n < m; (s)% ⊦ n + 0 = n; (s)% ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s)% ⊦ m + 1 ≠ 0; (s)% ⊦ m < m + n ↔ n ≠ 0; (s)% ⊦ m < n → n ≠ 0; (s)% ⊦ m + n = m + n0 ↔ n = n0; (s)%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat% ⊦ m < n → m ≤ n; (s)