def permsim
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:840
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int.bend as U32int
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/u32laws.bend as LW
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
840def permsim(+f: Nat, +k: U32, +m: U32, +a: U32, +nn: Nat, +j: Nat, +r: Nat, +k0: Nat, +K: Nat, +ok: Bool, +more: Bool, +cn: Bool, +hK: {K == 32n : 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(32n, 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(32n, S.desc(nn, k0)) == cn : Bool}) -> {G.perm_go(~U32, ~I.u32_op, ~I.u32_is, f, k, m, (a, ok), more) == G.fits(U32, Bool.not(cn), of(S.desc(nn, k0))) : Maybe<&2, U32>}:
841 match f r ok more cn:
842 case 0n _ True{} _ _:
843 +hjk = L.subst(Nat, z => {Nat.is_le(j, z) == True{} : Bool}, Nat.add(j, r), k0, hj, N.le_add_right(j, r))
844 +big = NF.dbig(K, nn, j, hf, N.le_trans(j, k0, nn, hjk, hle))
845 Empty.absurd({G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 0n, k, m, (a, True{}), more) == G.fits(U32, Bool.not(cn), of(S.desc(nn, k0))) : Maybe<&2, U32>}, 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))))
846 case 0n _ False{} _ True{}:
847 Empty.absurd({G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 0n, k, m, (a, False{}), more) == G.fits(U32, Bool.not(True{}), of(S.desc(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.desc(nn, k0)), False{}, Equal.sym(Bool, C.fits(32n, S.desc(nn, k0)), True{}, hcn), unfit_mono(32n, S.desc(nn, j), S.desc(nn, k0), pmon(nn, j, r, k0, hj, hle), hok))))
848 case 0n _ False{} _ False{}:
849 {==}
850 case 1n+g _ False{} _ True{}:
851 Empty.absurd({G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, k, m, (a, False{}), more) == G.fits(U32, Bool.not(True{}), of(S.desc(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.desc(nn, k0)), False{}, Equal.sym(Bool, C.fits(32n, S.desc(nn, k0)), True{}, hcn), unfit_mono(32n, S.desc(nn, j), S.desc(nn, k0), pmon(nn, j, r, k0, hj, hle), hok))))
852 case 1n+g _ False{} _ False{}:
853 {==}
854 case 1n+g 0n True{} False{} True{}:
855 +ejk = Equal.trans(Nat, j, Nat.add(j, 0n), k0, Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)), hj)
856 Equal.cong(U32, Maybe<&2, U32>, 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))))
857 case 1n+g 0n True{} False{} False{}:
858 +ejk = Equal.trans(Nat, j, Nat.add(j, 0n), k0, Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)), hj)
859 Empty.absurd({G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, k, m, (a, True{}), False{}) == G.fits(U32, Bool.not(False{}), of(S.desc(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.trans(Bool, True{}, C.fits(32n, S.desc(nn, j)), False{}, Equal.sym(Bool, C.fits(32n, S.desc(nn, j)), True{}, hok), Equal.trans(Bool, C.fits(32n, S.desc(nn, j)), C.fits(32n, S.desc(nn, k0)), False{}, Equal.cong(Nat, Bool, t => C.fits(32n, S.desc(nn, t)), j, k0, ejk), hcn))))
860 case 1n+g 1n+rp True{} False{} _:
861 Empty.absurd({G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, k, m, (a, True{}), False{}) == G.fits(U32, Bool.not(cn), of(S.desc(nn, k0))) : Maybe<&2, U32>}, true_ne_false(Equal.sym(Bool, False{}, True{}, hmore)))
862 case 1n+g 0n True{} True{} _:
863 Empty.absurd({G.perm_go(~U32, ~I.u32_op, ~I.u32_is, 1n+g, k, m, (a, True{}), True{}) == G.fits(U32, Bool.not(cn), of(S.desc(nn, k0))) : Maybe<&2, U32>}, true_ne_false(hmore))
864 case 1n+ +g 1n+ +rp True{} True{} _:
865 +one = I.u32_op(NM.One{})
866 +es = NA.add_succ(j, rp)
867 +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)))
868 +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)
869 +hjn = N.lt_le_trans(j, k0, nn, hj2, hle)
870 +X = Nat.sub(nn, 1n+j)
871 +esx = FA.sub_lt_succ(nn, j, hjn)
872 +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)))
873 +dk = G.dec(~U32, ~I.u32_op, k)
874 +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)))
875 +emx = Equal.trans(Nat, v(m), Nat.sub(nn, j), 1n+X, hm, esx)
876 +dm2 = G.dec(~U32, ~I.u32_op, m)
877 +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)))
878 +hmore2 = Equal.cong(Bool, Bool, t => Bool.not(t), I.u32_is(NM.IsZero{dk}), Nat.is_eq(rp, 0n), iz(dk, rp, edk))
879 +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)
880 +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)
881 +pn = S.desc(nn, 1n+j)
882 permsim(g, dk, dm2, I.u32_op(NM.Mul{a, m}), nn, 1n+j, rp, k0, K, Bool.not(I.u32_is(NM.MulOver{a, m})), Bool.not(I.u32_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(32n, pn), {==}), hmore2, hcn)