def jperm

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqc.bend:75

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

75# (b + (K + D)) twice, then p, then s, regrouped
76def jperm(+b: Nat, +K: Nat, +D: Nat, +p: Nat, +s: Nat) -> {Nat.add(Nat.add(Nat.add(Nat.add(b, Nat.add(K, D)), Nat.add(b, Nat.add(K, D))), p), s) == Nat.add(Nat.add(b, b), Nat.add(Nat.add(Nat.add(K, K), p), Nat.add(Nat.add(D, D), s))) : Nat}:
77  +KD = Nat.add(K, D)
78  +e1 = NA.add_assoc(b, KD, Nat.add(b, KD))
79  +e2 = Equal.cong(Nat, Nat, z => Nat.add(b, z), Nat.add(KD, Nat.add(b, KD)), Nat.add(b, Nat.add(KD, KD)), NA.add_swap(KD, b, KD))
80  +e3 = Equal.sym(Nat, Nat.add(Nat.add(b, b), Nat.add(KD, KD)), Nat.add(b, Nat.add(b, Nat.add(KD, KD))), NA.add_assoc(b, b, Nat.add(KD, KD)))
81  +eA = Equal.trans(Nat, Nat.add(Nat.add(b, KD), Nat.add(b, KD)), Nat.add(b, Nat.add(KD, Nat.add(b, KD))), Nat.add(Nat.add(b, b), Nat.add(KD, KD)), e1, Equal.trans(Nat, Nat.add(b, Nat.add(KD, Nat.add(b, KD))), Nat.add(b, Nat.add(b, Nat.add(KD, KD))), Nat.add(Nat.add(b, b), Nat.add(KD, KD)), e2, e3))
82  +f1 = NA.add_assoc(K, D, Nat.add(K, D))
83  +f2 = Equal.cong(Nat, Nat, z => Nat.add(K, z), Nat.add(D, Nat.add(K, D)), Nat.add(K, Nat.add(D, D)), NA.add_swap(D, K, D))
84  +f3 = Equal.sym(Nat, Nat.add(Nat.add(K, K), Nat.add(D, D)), Nat.add(K, Nat.add(K, Nat.add(D, D))), NA.add_assoc(K, K, Nat.add(D, D)))
85  +eKD = Equal.trans(Nat, Nat.add(KD, KD), Nat.add(K, Nat.add(D, Nat.add(K, D))), Nat.add(Nat.add(K, K), Nat.add(D, D)), f1, Equal.trans(Nat, Nat.add(K, Nat.add(D, Nat.add(K, D))), Nat.add(K, Nat.add(K, Nat.add(D, D))), Nat.add(Nat.add(K, K), Nat.add(D, D)), f2, f3))
86  +B2 = Nat.add(b, b)
87  +K2 = Nat.add(K, K)
88  +D2 = Nat.add(D, D)
89  +g0 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(z, p), s), Nat.add(Nat.add(b, KD), Nat.add(b, KD)), Nat.add(B2, Nat.add(K2, D2)), Equal.trans(Nat, Nat.add(Nat.add(b, KD), Nat.add(b, KD)), Nat.add(B2, Nat.add(KD, KD)), Nat.add(B2, Nat.add(K2, D2)), eA, Equal.cong(Nat, Nat, z => Nat.add(B2, z), Nat.add(KD, KD), Nat.add(K2, D2), eKD)))
90  +g1 = Equal.cong(Nat, Nat, z => Nat.add(z, s), Nat.add(Nat.add(B2, Nat.add(K2, D2)), p), Nat.add(B2, Nat.add(Nat.add(K2, D2), p)), NA.add_assoc(B2, Nat.add(K2, D2), p))
91  +g2 = NA.add_assoc(B2, Nat.add(Nat.add(K2, D2), p), s)
92  +h1 = Equal.cong(Nat, Nat, z => Nat.add(z, s), Nat.add(Nat.add(K2, D2), p), Nat.add(K2, Nat.add(D2, p)), NA.add_assoc(K2, D2, p))
93  +h2 = Equal.cong(Nat, Nat, z => Nat.add(z, s), Nat.add(K2, Nat.add(D2, p)), Nat.add(K2, Nat.add(p, D2)), Equal.cong(Nat, Nat, z => Nat.add(K2, z), Nat.add(D2, p), Nat.add(p, D2), NA.add_comm(D2, p)))
94  +h3 = Equal.trans(Nat, Nat.add(Nat.add(K2, Nat.add(p, D2)), s), Nat.add(Nat.add(Nat.add(K2, p), D2), s), Nat.add(Nat.add(K2, p), Nat.add(D2, s)), Equal.cong(Nat, Nat, z => Nat.add(z, s), Nat.add(K2, Nat.add(p, D2)), Nat.add(Nat.add(K2, p), D2), Equal.sym(Nat, Nat.add(Nat.add(K2, p), D2), Nat.add(K2, Nat.add(p, D2)), NA.add_assoc(K2, p, D2))), NA.add_assoc(Nat.add(K2, p), D2, s))
95  +hh = Equal.trans(Nat, Nat.add(Nat.add(Nat.add(K2, D2), p), s), Nat.add(Nat.add(K2, Nat.add(D2, p)), s), Nat.add(Nat.add(K2, p), Nat.add(D2, s)), h1, Equal.trans(Nat, Nat.add(Nat.add(K2, Nat.add(D2, p)), s), Nat.add(Nat.add(K2, Nat.add(p, D2)), s), Nat.add(Nat.add(K2, p), Nat.add(D2, s)), h2, h3))
96  Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(b, KD), Nat.add(b, KD)), p), s), Nat.add(Nat.add(Nat.add(B2, Nat.add(K2, D2)), p), s), Nat.add(B2, Nat.add(Nat.add(K2, p), Nat.add(D2, s))), g0, Equal.trans(Nat, Nat.add(Nat.add(Nat.add(B2, Nat.add(K2, D2)), p), s), Nat.add(B2, Nat.add(Nat.add(Nat.add(K2, D2), p), s)), Nat.add(B2, Nat.add(Nat.add(K2, p), Nat.add(D2, s))), Equal.trans(Nat, Nat.add(Nat.add(Nat.add(B2, Nat.add(K2, D2)), p), s), Nat.add(Nat.add(B2, Nat.add(Nat.add(K2, D2), p)), s), Nat.add(B2, Nat.add(Nat.add(Nat.add(K2, D2), p), s)), g1, g2), Equal.cong(Nat, Nat, z => Nat.add(B2, z), Nat.add(Nat.add(Nat.add(K2, D2), p), s), Nat.add(Nat.add(K2, p), Nat.add(D2, s)), hh)))