def F_mono

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

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

128def F_mono(p: Lin, q: Lin, v: Vs, +h: {lle(p, q) == True{} : Bool}) -> LE(F(p, v), F(q, v)):
129  match p q v:
130    case L{+a0, +a1, +a2, +a3, +a4} L{+b0, +b1, +b2, +b3, +b4} VS{+v1, +v2, +v3, +v4}:
131      +l0 = Nat.is_le(a0, b0)
132      +l1 = Nat.is_le(a1, b1)
133      +l2 = Nat.is_le(a2, b2)
134      +l3 = Nat.is_le(a3, b3)
135      +l4 = Nat.is_le(a4, b4)
136      +r1 = and5_r(l0, l1, l2, l3, l4, h)
137      +r2 = MBool.eq_true_of_and_right(l1, Bool.and(l2, Bool.and(l3, l4)), r1)
138      +r3 = MBool.eq_true_of_and_right(l2, Bool.and(l3, l4), r2)
139      +x1 = Nat.mul(a1, v1)
140      +x2 = Nat.mul(a2, v2)
141      +x3 = Nat.mul(a3, v3)
142      +x4 = Nat.mul(a4, v4)
143      +y1 = Nat.mul(b1, v1)
144      +y2 = Nat.mul(b2, v2)
145      +y3 = Nat.mul(b3, v3)
146      +y4 = Nat.mul(b4, v4)
147      MNat.add_le_add(a0, Nat.add(x1, Nat.add(x2, Nat.add(x3, x4))), b0, Nat.add(y1, Nat.add(y2, Nat.add(y3, y4))), and5_1(l0, l1, l2, l3, l4, h), MNat.add_le_add(x1, Nat.add(x2, Nat.add(x3, x4)), y1, Nat.add(y2, Nat.add(y3, y4)), MNat.mul_le_mul_right(a1, b1, v1, MBool.eq_true_of_and_left(l1, Bool.and(l2, Bool.and(l3, l4)), r1)), MNat.add_le_add(x2, Nat.add(x3, x4), y2, Nat.add(y3, y4), MNat.mul_le_mul_right(a2, b2, v2, MBool.eq_true_of_and_left(l2, Bool.and(l3, l4), r2)), MNat.add_le_add(x3, x4, y3, y4, MNat.mul_le_mul_right(a3, b3, v3, MBool.eq_true_of_and_left(l3, l4, r3)), MNat.mul_le_mul_right(a4, b4, v4, MBool.eq_true_of_and_right(l3, l4, r3))))))