def plus_one

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixgen.bend:124

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

124# ((x + t) + 1) + y == x + S when y + t == M and 1 + M == S
125def plus_one(+x: Nat, +t: Nat, +y: Nat, +M: Nat, +S: Nat, +h: {Nat.add(y, t) == M : Nat}, +hS: {1n+M == S : Nat}) -> {Nat.add(Nat.add(Nat.add(x, t), 1n), y) == Nat.add(x, S) : Nat}:
126  +A = Nat.add(x, t)
127  +e1 = Equal.trans(Nat, Nat.add(Nat.add(A, 1n), y), Nat.add(A, Nat.add(1n, y)), Nat.add(A, Nat.add(y, 1n)), N.add_assoc(A, 1n, y), Equal.cong(Nat, Nat, z => Nat.add(A, z), Nat.add(1n, y), Nat.add(y, 1n), N.add_comm(1n, y)))
128  +e2 = Equal.sym(Nat, Nat.add(Nat.add(A, y), 1n), Nat.add(A, Nat.add(y, 1n)), N.add_assoc(A, y, 1n))
129  +e3 = Equal.trans(Nat, Nat.add(A, y), Nat.add(x, Nat.add(t, y)), Nat.add(x, M), N.add_assoc(x, t, y), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(t, y), M, Equal.trans(Nat, Nat.add(t, y), Nat.add(y, t), M, N.add_comm(t, y), h)))
130  +e4 = Equal.cong(Nat, Nat, z => Nat.add(z, 1n), Nat.add(A, y), Nat.add(x, M), e3)
131  +e5 = Equal.cong(Nat, Nat, z => Nat.add(x, z), 1n+M, S, hS)
132  Equal.trans(Nat, Nat.add(Nat.add(A, 1n), y), Nat.add(A, Nat.add(y, 1n)), Nat.add(x, S), e1, Equal.trans(Nat, Nat.add(A, Nat.add(y, 1n)), Nat.add(Nat.add(A, y), 1n), Nat.add(x, S), e2, Equal.trans(Nat, Nat.add(Nat.add(A, y), 1n), Nat.add(Nat.add(x, M), 1n), Nat.add(x, S), e4, Equal.trans(Nat, Nat.add(Nat.add(x, M), 1n), Nat.add(x, 1n+M), Nat.add(x, S), Equal.trans(Nat, Nat.add(Nat.add(x, M), 1n), Nat.add(x, Nat.add(M, 1n)), Nat.add(x, 1n+M), N.add_assoc(x, M, 1n), Equal.cong(Nat, Nat, z => Nat.add(x, z), Nat.add(M, 1n), 1n+M, N.add_comm(M, 1n))), e5))))