| fs0 = fs, log0 = log, ro.inodes?, fo.inodes?, log-cons(log, fs), node-cons(nd7.key, nd7), node-cons(nd6.key, nd6), node-cons(nd1.key, nd1), node-cons(nd5.key, nd5), node-cons(nd4.key, nd4), ri-cons(ri, fs), ri-inj(ri), ri-inj(fi) ⊦ ⟨choose adr1, adr2, adr3, adr4, adr5 with new(adr1 ' + adr2 ' + adr3 ' + (adr4 ' + adr5), fs) ∧ ¬ dups(adr1 ' + adr2 ' + adr3 ' + adr4 ' + adr5 ') in {adr8 := adr1, adr7 := adr2, adr6 := adr3, adr0 := adr4, adr := adr5; fs := fs[adr8, nd7][adr7, nd6][adr6, nd1][adr0, nd5][adr, nd4], log := ((((log + adr8) + adr7) + adr6) + adr0) + adr, err := ESUCCESS} ifnone err := ENOSPC; boolvar := ?⟩ (boolvar ∧ fs0 = fs ∧ log0 = log), ⟨fail#(; ; err); adr8 := ?, adr7 := ?, adr6 := ?, adr0 := ?, adr := ?; boolvar := ?⟩ boolvar |
fs0 = fs, log0 = log, 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) ⊦ (∀ adr1, adr2, adr3, adr4, adr5. ¬(new(adr1 ' + adr2 ' + adr3 ' + (adr4 ' + adr5), fs) ∧ ¬ dups(adr1 ' + adr2 ' + adr3 ' + adr4 ' + adr5 '))) ∧ ⟨err := ENOSPC; boolvar := ?⟩ (boolvar ∧ fs0 = fs ∧ log0 = log), ∃ adr1, adr2, adr3, adr4, adr5. (new(adr1 ' + adr2 ' + adr3 ' + (adr4 ' + adr5), fs) ∧ ¬ dups(adr1 ' + adr2 ' + adr3 ' + adr4 ' + adr5 ')) ∧ ⟨adr8 := adr1, adr7 := adr2, adr6 := adr3, adr0 := adr4, adr := adr5; fs := fs[adr8, nd7][adr7, nd6][adr6, nd1][adr0, nd5][adr, nd4], log := ((((log + adr8) + adr7) + adr6) + adr0) + adr, err := ESUCCESS; boolvar := ?⟩ (boolvar ∧ fs0 = fs ∧ log0 = log), ⟨fail#(; ; err); adr8 := ?, adr7 := ?, adr6 := ?, adr0 := ?, adr := ?; boolvar := ?⟩ boolvar