def sat_eq' (a : ℤ × ℤ) (n : ℤ) (x : ℤ × ℤ) : Prop

Equations

• sat_eq' a n x = (a.1 * x.1 + a.2 * x.2 = n)

def sat_eq3 (a : ℤ) (b : ℤ) (c : ℤ) (n : ℤ) (x : ℤ) (y : ℤ) (z : ℤ) : Prop

Equations

• sat_eq3 a b c n x y z = (a * x + b * y + c * z = n)

theorem depth1 {a : ℤ} {b : ℤ} {x : ℤ} {y : ℤ} {k : ℤ} {n : ℤ} (hsat : sat_eq' (a, b) n (x, y)) : sat_eq' (a, b) n (x - k * b, y + k * a)

theorem depth2 {a : ℤ} {b : ℤ} {n : ℤ} (h : gcd a b = 1) : ∃ (x : ℤ) (y : ℤ), sat_eq' (a, b) n (x, y)

theorem depth3 (a : ℤ) (b : ℤ) (n : ℤ) (h : gcd a b = 1) : ∃ (x : ℤ) (y : ℤ), ∀ (k : ℤ), sat_eq' (a, b) n (x - k * b, y + k * a)

theorem solve3 (a : ℤ) (b : ℤ) (c : ℤ) (n : ℤ) (h : gcd (gcd a b) c = 1) : ∃ (x : ℤ) (y : ℤ) (z : ℤ), sat_eq3 a b c n x y z