def perm7

bend-collections-laws-math@1.0.0.0 · proofs/math/random/pcg/step.bend:83

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

83# (((a + c) + d) + (e + g)) + (b + f) == (a + b) + (((c + (e + d)) + f) + g)
84def perm7(+a: Nat, +b: Nat, +c: Nat, +d: Nat, +e: Nat, +f: Nat, +g: Nat) -> {Nat.add(Nat.add(Nat.add(Nat.add(a, c), d), Nat.add(e, g)), Nat.add(b, f)) == Nat.add(Nat.add(a, b), Nat.add(Nat.add(Nat.add(c, Nat.add(e, d)), f), g)) : Nat}:
85  +R2 = Nat.add(e, Nat.add(f, g))
86  +T = Nat.add(Nat.add(e, g), Nat.add(b, f))
87  +CAN = Nat.add(a, Nat.add(b, Nat.add(c, Nat.add(d, R2))))
88  +eT1 = Equal.trans(Nat, T, Nat.add(e, Nat.add(g, Nat.add(b, f))), Nat.add(e, Nat.add(b, Nat.add(g, f))),
89    NA.add_assoc(e, g, Nat.add(b, f)),
90    Equal.cong(Nat, Nat, z => Nat.add(e, z), Nat.add(g, Nat.add(b, f)), Nat.add(b, Nat.add(g, f)), NA.add_swap(g, b, f)))
91  +eT2 = Equal.trans(Nat, Nat.add(e, Nat.add(b, Nat.add(g, f))), Nat.add(e, Nat.add(b, Nat.add(f, g))), Nat.add(b, R2),
92    Equal.cong(Nat, Nat, z => Nat.add(e, Nat.add(b, z)), Nat.add(g, f), Nat.add(f, g), NA.add_comm(g, f)),
93    NA.add_swap(e, b, Nat.add(f, g)))
94  +eT = Equal.trans(Nat, T, Nat.add(e, Nat.add(b, Nat.add(g, f))), Nat.add(b, R2), eT1, eT2)
95  +eU = Equal.trans(Nat, Nat.add(Nat.add(c, d), Nat.add(b, R2)), Nat.add(c, Nat.add(d, Nat.add(b, R2))), Nat.add(b, Nat.add(c, Nat.add(d, R2))),
96    NA.add_assoc(c, d, Nat.add(b, R2)),
97    Equal.trans(Nat, Nat.add(c, Nat.add(d, Nat.add(b, R2))), Nat.add(c, Nat.add(b, Nat.add(d, R2))), Nat.add(b, Nat.add(c, Nat.add(d, R2))),
98      Equal.cong(Nat, Nat, z => Nat.add(c, z), Nat.add(d, Nat.add(b, R2)), Nat.add(b, Nat.add(d, R2)), NA.add_swap(d, b, R2)),
99      NA.add_swap(c, b, Nat.add(d, R2))))
100  +eL1 = Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(a, c), d), Nat.add(e, g)), Nat.add(b, f)), Nat.add(Nat.add(Nat.add(a, c), d), T), Nat.add(Nat.add(a, Nat.add(c, d)), T),
101    NA.add_assoc(Nat.add(Nat.add(a, c), d), Nat.add(e, g), Nat.add(b, f)),
102    Equal.cong(Nat, Nat, z => Nat.add(z, T), Nat.add(Nat.add(a, c), d), Nat.add(a, Nat.add(c, d)), NA.add_assoc(a, c, d)))
103  +eL2 = Equal.trans(Nat, Nat.add(Nat.add(a, Nat.add(c, d)), T), Nat.add(a, Nat.add(Nat.add(c, d), T)), CAN,
104    NA.add_assoc(a, Nat.add(c, d), T),
105    Equal.cong(Nat, Nat, z => Nat.add(a, z), Nat.add(Nat.add(c, d), T), Nat.add(b, Nat.add(c, Nat.add(d, R2))),
106      Equal.trans(Nat, Nat.add(Nat.add(c, d), T), Nat.add(Nat.add(c, d), Nat.add(b, R2)), Nat.add(b, Nat.add(c, Nat.add(d, R2))),
107        Equal.cong(Nat, Nat, z => Nat.add(Nat.add(c, d), z), T, Nat.add(b, R2), eT), eU)))
108  +eL = Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(a, c), d), Nat.add(e, g)), Nat.add(b, f)), Nat.add(Nat.add(a, Nat.add(c, d)), T), CAN, eL1, eL2)
109  +Rr = Nat.add(Nat.add(Nat.add(c, Nat.add(e, d)), f), g)
110  +eR1 = Equal.trans(Nat, Rr, Nat.add(Nat.add(c, Nat.add(e, d)), Nat.add(f, g)), Nat.add(c, Nat.add(Nat.add(e, d), Nat.add(f, g))),
111    NA.add_assoc(Nat.add(c, Nat.add(e, d)), f, g),
112    NA.add_assoc(c, Nat.add(e, d), Nat.add(f, g)))
113  +eR2 = Equal.trans(Nat, Nat.add(Nat.add(e, d), Nat.add(f, g)), Nat.add(e, Nat.add(d, Nat.add(f, g))), Nat.add(d, R2),
114    NA.add_assoc(e, d, Nat.add(f, g)),
115    NA.add_swap(e, d, Nat.add(f, g)))
116  +eR = Equal.trans(Nat, Nat.add(Nat.add(a, b), Rr), Nat.add(a, Nat.add(b, Rr)), CAN,
117    NA.add_assoc(a, b, Rr),
118    Equal.cong(Nat, Nat, z => Nat.add(a, Nat.add(b, z)), Rr, Nat.add(c, Nat.add(d, R2)),
119      Equal.trans(Nat, Rr, Nat.add(c, Nat.add(Nat.add(e, d), Nat.add(f, g))), Nat.add(c, Nat.add(d, R2)), eR1,
120        Equal.cong(Nat, Nat, z => Nat.add(c, z), Nat.add(Nat.add(e, d), Nat.add(f, g)), Nat.add(d, R2), eR2))))
121  Equal.trans(Nat, Nat.add(Nat.add(Nat.add(Nat.add(a, c), d), Nat.add(e, g)), Nat.add(b, f)), CAN, Nat.add(Nat.add(a, b), Rr), eL, Equal.sym(Nat, Nat.add(Nat.add(a, b), Rr), CAN, eR))