Documentation

Acmoi.Exercise3_1_2

def sat_eq (a : × ) (n : ) (x : × ) :
Equations
def unique_sol (a : × ) (n : ) :
Equations
theorem paireq (a : ) (b : ) (c : ) (d : ) (ha : a = c) (hb : b = d) :
(a, b) = (c, d)
theorem proj1eq {a : } {b : } {c : } {d : } (h : (a, b) = (c, d)) :
a = c
theorem proj2eq {a : } {b : } {c : } {d : } (h : (a, b) = (c, d)) :
b = d
theorem reduce (a : × ) (n : ) (x₀ : ) (u : ) (v : ) (original : unique_sol a (n + a.2 * v) sat_eq a (n + a.2 * v) (x₀, u + v)) :
theorem amplify (a : × ) (n : ) (x₀ : ) (u : ) (v : ) (u_pos : 0 < u) (original : unique_sol a n sat_eq a n (x₀, u * v)) :
unique_sol (a.1, a.2 * u) n