def hovm

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addf.bend:84

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L

84def hovm(+e: Nat, +h: {Nat.is_lt(e, 2047n) == True{} : Bool}) -> {Nat.is_lt(Nat.add(Nat.sub(e, 1n), 1n), 2047n) == True{} : Bool}:
85  match e:
86    case 0n:
87      {==}
88    case 1n+ +p:
89      +e1 = Equal.trans(Nat, Nat.add(Nat.sub(p, 0n), 1n), Nat.add(p, 1n), 1n+p, Equal.cong(Nat, Nat, z => Nat.add(z, 1n), Nat.sub(p, 0n), p, N.sub_zero(p)), Equal.trans(Nat, Nat.add(p, 1n), 1n+Nat.add(p, 0n), 1n+p, N.add_succ(p, 0n), N.succ_cong(Nat.add(p, 0n), p, N.add_zero(p))))
90      L.subst(Nat, z => {Nat.is_lt(z, 2047n) == True{} : Bool}, 1n+p, Nat.add(Nat.sub(p, 0n), 1n), Equal.sym(Nat, Nat.add(Nat.sub(p, 0n), 1n), 1n+p, e1), h)