def o48_lo_lt

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64bgcd.bend:185

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/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L

185# two 16-bit digits make a value below 2^32
186def o48_lo_lt(+one: Nat, +h1: {one == 1n : Nat}, +r1: Nat, +r2: Nat, +hr1: {Nat.is_lt(r1, 65536n) == True{} : Bool}, +hr2: {Nat.is_lt(r2, 65536n) == True{} : Bool}) -> {Nat.is_lt(Nat.add(C.shift(16n, r2), r1), C.shift(32n, one)) == True{} : Bool}:
187  +S = C.shift(16n, one)
188  +k = k16s(one, h1)
189  +a1 = L.subst(Nat, z => {Nat.is_lt(r1, z) == True{} : Bool}, 65536n, S, k, hr1)
190  +a2 = L.subst(Nat, z => {Nat.is_lt(r2, z) == True{} : Bool}, 65536n, S, k, hr2)
191  +b1 = N.lt_add_left(r1, S, C.shift(16n, r2), a1)
192  +l1 = N.lt_succ_le_succ(r2, S, a2)
193  +l2 = L.subst(Nat, z => {Nat.is_le(z, S) == True{} : Bool}, 1n+r2, Nat.add(r2, one), Equal.trans(Nat, 1n+r2, Nat.add(r2, 1n), Nat.add(r2, one), Equal.sym(Nat, Nat.add(r2, 1n), 1n+r2, WA.plus1(r2)), Equal.cong(Nat, Nat, z => Nat.add(r2, z), 1n, one, Equal.sym(Nat, one, 1n, h1))), l1)
194  +c1 = WW.shift_mono(16n, Nat.add(r2, one), S, l2)
195  +c2 = L.subst(Nat, z => {Nat.is_le(z, C.shift(16n, S)) == True{} : Bool}, C.shift(16n, Nat.add(r2, one)), Nat.add(C.shift(16n, r2), S), WW.shift_add(16n, r2, one), c1)
196  +c3 = L.subst(Nat, z => {Nat.is_le(Nat.add(C.shift(16n, r2), S), z) == True{} : Bool}, C.shift(16n, S), C.shift(32n, one), Equal.sym(Nat, C.shift(32n, one), C.shift(16n, S), WW.shift_comp(16n, 16n, one)), c2)
197  N.lt_le_trans(Nat.add(C.shift(16n, r2), r1), Nat.add(C.shift(16n, r2), S), C.shift(32n, one), b1, c3)