def fuel_ok2

bend-collections-laws-math@1.0.0.0 · proofs/math/number/fixprime.bend:169

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA

169# 2^32 stays C.shift(32, one) for a symbolic one: with one == 1n the checker
170# would expand the closed 2^32 in unary
171def fuel_ok2(+one: Nat, +h1: {one == 1n : Nat}, +n: U32) -> {Nat.is_le(C.shift(32n, one), Nat.add(1n+v(n), Nat.add(v(U32.not(n)), 1n))) == True{} : Bool}:
172  L.subst(Nat, z => {Nat.is_le(C.shift(32n, one), Nat.add(1n+v(n), z)) == True{} : Bool}, 1n+v(U32.not(n)), Nat.add(v(U32.not(n)), 1n), Equal.sym(Nat, Nat.add(v(U32.not(n)), 1n), 1n+v(U32.not(n)), WA.plus1(v(U32.not(n)))), fuel_ok(one, h1, n))