def run_go_le

bend-osdev-acpi@0.1.1.0 · PROOF.bend:2522

import Base
import bend-osdev-acpi@0.1.1.0/aml_host.bend as Hs
import bend-osdev-acpi@0.1.1.0/aml_interp.bend as I
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

2522def run_go_le(+n: Nat, +h: Bool, +m: I.AmlMachine<Hs.AmlMemHost>, +u: Nat) -> {Nat.is_le(I.AmlRun.steps(Hs.AmlMemHost, I.AmlM.run.go(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, n, h, m, u)), Nat.add(n, u)) == True{} : Bool}:
2523  match n:
2524    case 0n:
2525      UL.nat_le_refl(u)
2526    case 1n+p:
2527      match h:
2528        case True{}:
2529          le_step(u, Nat.add(p, u), UL.nat_le_add(u, p))
2530        case False{}:
2531          %Equal.sym(Nat, 1n+Nat.add(p, u), Nat.add(p, 1n+u), add_succ(p, u)) : {Nat.is_le(I.AmlRun.steps(Hs.AmlMemHost, I.AmlM.run.go(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, p, I.AmlMachine.halted(Hs.AmlMemHost, I.AmlM.step(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, m)), I.AmlM.step(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, m), 1n+u)), _) == True{} : Bool}
2532          run_go_le(p, I.AmlMachine.halted(Hs.AmlMemHost, I.AmlM.step(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, m)), I.AmlM.step(~Hs.AmlMemHost, ~Hs.AmlMemHost.io, m), 1n+u)