| adr1 ≠ adr2, adr1 ≠ adr3, adr10 ≠ adr1, adr10 ≠ adr2, adr10 ≠ adr3, adr11 ≠ adr10, adr11 ≠ adr1, adr11 ≠ adr2, adr11 ≠ adr3, adr2 ≠ adr3, fo.inodes?, ro.inodes?, log-cons(log, fs), node-cons(nd4.key, nd4), node-cons(nd5.key, nd5), node-cons(nd1.key, nd1), node-cons(nd6.key, nd6), node-cons(nd7.key, nd7), ri-cons(ri, fs), ri-inj(fi), ri-inj(ri), ¬ adr11 ∈ fs, ¬ adr10 ∈ fs, ¬ adr1 ∈ fs, ¬ adr2 ∈ fs, ¬ adr3 ∈ fs ⊦ ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; adr4 := ?, adr5 := ?, adr9 := ?, adr10 := ?, adr11 := ?; boolvar := ?⟩ boolvar, ∃ adr13, adr12, adr3, adr2, adr1. ¬ adr13 ∈ fs ∧ ¬ adr12 ∈ fs ∧ ¬ adr3 ∈ fs ∧ ¬ adr2 ∈ fs ∧ ¬ adr1 ∈ fs ∧ adr13 ≠ adr12 ∧ adr13 ≠ adr3 ∧ adr13 ≠ adr2 ∧ adr13 ≠ adr1 ∧ adr12 ≠ adr3 ∧ adr12 ≠ adr2 ∧ adr12 ≠ adr1 ∧ adr3 ≠ adr2 ∧ adr3 ≠ adr1 ∧ adr2 ≠ adr1 ∧ ⟨adr4 := adr13, adr5 := adr12, adr9 := adr3, adr10 := adr2, adr11 := adr1; fs1 := fs[adr4, nd7][adr5, nd6][adr9, nd1][adr10, nd5][adr11, nd4], log1 := ((((log + adr4 ') + adr5 ') + adr9 ') + adr10 ') + adr11 ', err := ESUCCESS; boolvar := ?⟩ (boolvar ∧ fs = fs1 ∧ log = log1), ⟨boolvar := ?⟩ boolvar |