def permsim
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64int.bend:841
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int.bend as U64int
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/generic.bend as G
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/lib/nat.bend as N
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/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64laws.bend as LW
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/fact.bend as FA
import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as S
841def permsim(+f: Nat, +k: WU.U64, +m: WU.U64, +a: WU.U64, +nn: Nat, +j: Nat, +r: Nat, +k0: Nat, +K: Nat, +ok: Bool, +more: Bool, +cn: Bool, +hK: {K == 64n : Nat}, +hkr: {v(k) == r : Nat}, +hm: {v(m) == Nat.sub(nn, j) : Nat}, +hj: {Nat.add(j, r) == k0 : Nat}, +hle: {Nat.is_le(k0, nn) == True{} : Bool}, +hf: {Nat.is_le(1n+K, Nat.add(f, j)) == True{} : Bool}, +hok: {C.fits(64n, S.desc(nn, j)) == ok : Bool}, ha: FR(ok, a, S.desc(nn, j)), +hmore: {more == Bool.not(Nat.is_eq(r, 0n)) : Bool}, +hcn: {C.fits(64n, S.desc(nn, k0)) == cn : Bool}) -> {G.perm_go(~WU.U64, ~I.u64_op, ~I.u64_is, f, k, m, (a, ok), more) == G.fits(WU.U64, Bool.not(cn), of(S.desc(nn, k0))) : Maybe<&2, WU.U64>}:
842 match f r ok more cn:
843 case 0n _ True{} _ _:
844 +hjk = L.subst(Nat, z => {Nat.is_le(j, z) == True{} : Bool}, Nat.add(j, r), k0, hj, N.le_add_right(j, r))
845 +big = NF.dbig(K, nn, j, hf, N.le_trans(j, k0, nn, hjk, hle))
846 Empty.absurd({G.perm_go(~WU.U64, ~I.u64_op, ~I.u64_is, 0n, k, m, (a, True{}), more) == G.fits(WU.U64, Bool.not(cn), of(S.desc(nn, k0))) : Maybe<&2, WU.U64>}, true_ne_false(Equal.trans(Bool, True{}, Nat.is_lt(S.desc(nn, j), C.pow2(K)), False{}, Equal.sym(Bool, Nat.is_lt(S.desc(nn, j), C.pow2(K)), True{}, fk(K, hK, S.desc(nn, j), hok)), N.le_not_lt(S.desc(nn, j), C.pow2(K), big))))
847 case 0n _ False{} _ True{}:
848 Empty.absurd({G.perm_go(~WU.U64, ~I.u64_op, ~I.u64_is, 0n, k, m, (a, False{}), more) == G.fits(WU.U64, Bool.not(True{}), of(S.desc(nn, k0))) : Maybe<&2, WU.U64>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(64n, S.desc(nn, k0)), False{}, Equal.sym(Bool, C.fits(64n, S.desc(nn, k0)), True{}, hcn), unfit_mono(64n, S.desc(nn, j), S.desc(nn, k0), pmon(nn, j, r, k0, hj, hle), hok))))
849 case 0n _ False{} _ False{}:
850 {==}
851 case 1n+g _ False{} _ True{}:
852 Empty.absurd({G.perm_go(~WU.U64, ~I.u64_op, ~I.u64_is, 1n+g, k, m, (a, False{}), more) == G.fits(WU.U64, Bool.not(True{}), of(S.desc(nn, k0))) : Maybe<&2, WU.U64>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(64n, S.desc(nn, k0)), False{}, Equal.sym(Bool, C.fits(64n, S.desc(nn, k0)), True{}, hcn), unfit_mono(64n, S.desc(nn, j), S.desc(nn, k0), pmon(nn, j, r, k0, hj, hle), hok))))
853 case 1n+g _ False{} _ False{}:
854 {==}
855 case 1n+g 0n True{} False{} True{}:
856 +ejk = Equal.trans(Nat, j, Nat.add(j, 0n), k0, Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)), hj)
857 Equal.cong(WU.U64, Maybe<&2, WU.U64>, t => Some{t}, a, of(S.desc(nn, k0)), as_of(a, S.desc(nn, k0), Equal.trans(Nat, v(a), S.desc(nn, j), S.desc(nn, k0), ha, Equal.cong(Nat, Nat, t => S.desc(nn, t), j, k0, ejk))))
858 case 1n+g 0n True{} False{} False{}:
859 +ejk = Equal.trans(Nat, j, Nat.add(j, 0n), k0, Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)), hj)
860 Empty.absurd({G.perm_go(~WU.U64, ~I.u64_op, ~I.u64_is, 1n+g, k, m, (a, True{}), False{}) == G.fits(WU.U64, Bool.not(False{}), of(S.desc(nn, k0))) : Maybe<&2, WU.U64>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(64n, S.desc(nn, j)), False{}, Equal.sym(Bool, C.fits(64n, S.desc(nn, j)), True{}, hok), Equal.trans(Bool, C.fits(64n, S.desc(nn, j)), C.fits(64n, S.desc(nn, k0)), False{}, Equal.cong(Nat, Bool, t => C.fits(64n, S.desc(nn, t)), j, k0, ejk), hcn))))
861 case 1n+g 1n+rp True{} False{} _:
862 Empty.absurd({G.perm_go(~WU.U64, ~I.u64_op, ~I.u64_is, 1n+g, k, m, (a, True{}), False{}) == G.fits(WU.U64, Bool.not(cn), of(S.desc(nn, k0))) : Maybe<&2, WU.U64>}, true_ne_false(Equal.sym(Bool, False{}, True{}, hmore)))
863 case 1n+g 0n True{} True{} _:
864 Empty.absurd({G.perm_go(~WU.U64, ~I.u64_op, ~I.u64_is, 1n+g, k, m, (a, True{}), True{}) == G.fits(WU.U64, Bool.not(cn), of(S.desc(nn, k0))) : Maybe<&2, WU.U64>}, true_ne_false(hmore))
865 case 1n+ +g 1n+ +rp True{} True{} _:
866 +one = I.u64_op(NM.One{})
867 +es = NA.add_succ(j, rp)
868 +hj1 = N.le_lt_trans(j, Nat.add(j, rp), 1n+Nat.add(j, rp), N.le_add_right(j, rp), N.lt_succ(Nat.add(j, rp)))
869 +hj2 = L.subst(Nat, z => {Nat.is_lt(j, z) == True{} : Bool}, 1n+Nat.add(j, rp), k0, Equal.trans(Nat, 1n+Nat.add(j, rp), Nat.add(j, 1n+rp), k0, Equal.sym(Nat, Nat.add(j, 1n+rp), 1n+Nat.add(j, rp), es), hj), hj1)
870 +hjn = N.lt_le_trans(j, k0, nn, hj2, hle)
871 +X = Nat.sub(nn, 1n+j)
872 +esx = FA.sub_lt_succ(nn, j, hjn)
873 +hpn = Equal.trans(Nat, Nat.mul(v(a), v(m)), Nat.mul(S.desc(nn, j), Nat.sub(nn, j)), S.desc(nn, 1n+j), nmul(v(a), v(m), S.desc(nn, j), Nat.sub(nn, j), ha, hm), NA.mul_comm(S.desc(nn, j), Nat.sub(nn, j)))
874 +dk = G.dec(~WU.U64, ~I.u64_op, k)
875 +edk = Equal.trans(Nat, v(dk), Nat.sub(v(k), v(one)), rp, LW.ops_sub(k, one, le_v(one, k, 1n, 1n+rp, one_v(), hkr, N.zero_le(rp))), Equal.trans(Nat, Nat.sub(v(k), v(one)), Nat.sub(1n+rp, 1n), rp, nsub(v(k), v(one), 1n+rp, 1n, hkr, one_v()), N.sub_zero(rp)))
876 +emx = Equal.trans(Nat, v(m), Nat.sub(nn, j), 1n+X, hm, esx)
877 +dm2 = G.dec(~WU.U64, ~I.u64_op, m)
878 +edm = Equal.trans(Nat, v(dm2), Nat.sub(v(m), v(one)), X, LW.ops_sub(m, one, le_v(one, m, 1n, 1n+X, one_v(), emx, N.zero_le(X))), Equal.trans(Nat, Nat.sub(v(m), v(one)), Nat.sub(1n+X, 1n), X, nsub(v(m), v(one), 1n+X, 1n, emx, one_v()), N.sub_zero(X)))
879 +hmore2 = Equal.cong(Bool, Bool, t => Bool.not(t), I.u64_is(NM.IsZero{dk}), Nat.is_eq(rp, 0n), iz(dk, rp, edk))
880 +hjj = Equal.trans(Nat, 1n+Nat.add(j, rp), Nat.add(j, 1n+rp), k0, Equal.sym(Nat, Nat.add(j, 1n+rp), 1n+Nat.add(j, rp), es), hj)
881 +hf2 = L.subst(Nat, z => {Nat.is_le(1n+K, z) == True{} : Bool}, 1n+Nat.add(g, j), Nat.add(g, 1n+j), Equal.sym(Nat, Nat.add(g, 1n+j), 1n+Nat.add(g, j), NA.add_succ(g, j)), hf)
882 +pn = S.desc(nn, 1n+j)
883 permsim(g, dk, dm2, I.u64_op(NM.Mul{a, m}), nn, 1n+j, rp, k0, K, Bool.not(I.u64_is(NM.MulOver{a, m})), Bool.not(I.u64_is(NM.IsZero{dk})), cn, hK, edk, edm, hjj, hle, hf2, ok_mul(a, m, pn, hpn), fr_mul(a, m, pn, hpn, C.fits(64n, pn), {==}), hmore2, hcn)