def F_add

bend-kit-collections@0.1.4.1 · nat_order.bend:83

import Base
import bend-mathlib@0.7.4.0/nat.bend as MNat

83def F_add(p: Lin, q: Lin, v: Vs) -> {Nat.add(F(p, v), F(q, v)) == F(ladd(p, q), v) : Nat}:
84  match p q v:
85    case L{+a0, +a1, +a2, +a3, +a4} L{+b0, +b1, +b2, +b3, +b4} VS{+v1, +v2, +v3, +v4}:
86      +x1 = Nat.mul(a1, v1)
87      +x2 = Nat.mul(a2, v2)
88      +x3 = Nat.mul(a3, v3)
89      +x4 = Nat.mul(a4, v4)
90      +y1 = Nat.mul(b1, v1)
91      +y2 = Nat.mul(b2, v2)
92      +y3 = Nat.mul(b3, v3)
93      +y4 = Nat.mul(b4, v4)
94      +z1 = Nat.mul(Nat.add(a1, b1), v1)
95      +z2 = Nat.mul(Nat.add(a2, b2), v2)
96      +z3 = Nat.mul(Nat.add(a3, b3), v3)
97      +z4 = Nat.mul(Nat.add(a4, b4), v4)
98      step(a0, Nat.add(x1, Nat.add(x2, Nat.add(x3, x4))), b0, Nat.add(y1, Nat.add(y2, Nat.add(y3, y4))),
99        Nat.add(a0, b0), Nat.add(z1, Nat.add(z2, Nat.add(z3, z4))), {==},
100        step(x1, Nat.add(x2, Nat.add(x3, x4)), y1, Nat.add(y2, Nat.add(y3, y4)), z1,
101          Nat.add(z2, Nat.add(z3, z4)), MNat.add_mul_sym(a1, b1, v1),
102          step(x2, Nat.add(x3, x4), y2, Nat.add(y3, y4), z2, Nat.add(z3, z4), MNat.add_mul_sym(a2, b2, v2),
103            step(x3, x4, y3, y4, z3, z4, MNat.add_mul_sym(a3, b3, v3), MNat.add_mul_sym(a4, b4, v4)))))