Proof step 1 from proof prepost-recover-main-same (conclusion)

Heuristic nonrecursive calls applied rule call right

And obtained the following new goals

• Proof step 2:

  avol0 = avol, logoff = n0, m0 = n2, m1 = n1, m2 = m ⊦ [ebm_avol_recover#(; avol; err); if err ≠ ESUCCESS then debug#("persistence-io: ubi recover failed") else let m = ? in {ebm_avol_get_leb_size#(avol; ; m0); ebm_avol_get_page_size#(avol; ; m1); ebm_avol_get_volume_size#(avol; ; m); persistence_io_read_superblock#(m1, m0, avol; sb; err); if err ≠ ESUCCESS then debug#("persistence-io: reading superblock failed"); if err = ESUCCESS then {persistence_io_read_log#(sb, m1, m0, avol; logoff; log, err); if err ≠ ESUCCESS then debug#("persistence-io: reading log failed")}; if err = ESUCCESS then {persistence_io_read_orphans#(sb, avol; orphans; err); if err ≠ ESUCCESS then debug#("persistence-io: reading orphans failed")}; if err = ESUCCESS then {m := m - sb.main; let buf = ? in {persistence_io_read_lebs#(sb.lpt, lptlebs(m, m0), m0, avol; ; buf, err); if err = ESUCCESS then {lpt := mklparray(m); lpt := fill(lpt, mklp(0, 0, LP_FREE, 0)); persistence_io_decode_lpt#(buf; lpt, err)}; if err ≠ ESUCCESS then debug#("persistence-io: reading LPT failed")}}; if err = ESUCCESS then {logoff := m0; adr := sb.indexaddr; m2 := sb.maxino}}] (err = ESUCCESS → avol0 = avol)

Rule argument

Additional information

Used simplifier rules: recover: ⊦ ;