def two_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:716

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/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

716def two_v() -> {v(I.u32_op(NM.Add{I.u32_op(NM.One{}), I.u32_op(NM.One{})})) == 2n : Nat}:
717  +one = I.u32_op(NM.One{})
718  +e11 = nadd(v(one), v(one), 1n, 1n, one_v(), one_v())
719  +hao = Equal.trans(Bool, I.u32_is(NM.AddOver{one, one}), Bool.not(C.fits(32n, Nat.add(v(one), v(one)))), False{}, LW.tests_add_over(one, one), Equal.cong(Nat, Bool, t => Bool.not(C.fits(32n, t)), Nat.add(v(one), v(one)), 2n, e11))
720  Equal.trans(Nat, v(I.u32_op(NM.Add{one, one})), Nat.add(v(one), v(one)), 2n, LW.ops_add(one, one, hao), e11)