union Nat {
  zero
  suc(Nat)
}

add_assoc: (all m:Nat, n:Nat, o:Nat. (m + n) + o = m + (n + o))

add_both_monus: (all z:Nat, y:Nat, x:Nat. (z + y) ∸ (z + x) = y ∸ x)

add_both_sides_of_equal: (all x:Nat. (all y:Nat, z:Nat. ((x + y = x + z) ⇔ (y = z))))

add_both_sides_of_less: (all x:Nat, y:Nat, z:Nat. ((x + y < x + z) ⇔ (y < z)))

add_both_sides_of_less_equal: (all x:Nat. (all y:Nat, z:Nat. ((x + y ≤ x + z) ⇔ (y ≤ z))))

add_commute: (all n:Nat. (all m:Nat. n + m = m + n))

define add_div : (fn (Nat, Nat, Nat) -> Nat) = fun a:Nat, b:Nat, y:Nat {
      (a + b) / y
    }

add_mono_less: (all a:Nat, b:Nat, c:Nat, d:Nat. (if ((a < c) and (b < d)) then a + b < c + d))

add_mono_less_equal: (all a:Nat, b:Nat, c:Nat, d:Nat. (if ((a ≤ c) and (b ≤ d)) then a + b ≤ c + d))

add_monus_identity: (all m:Nat. (all n:Nat. (m + n) ∸ m = n))

add_suc: (all m:Nat. (all n:Nat. m + suc(n) = suc(m + n)))

assoc_add: (all m:Nat, n:Nat, o:Nat. m + (n + o) = (m + n) + o)

dichotomy: (all x:Nat, y:Nat. ((x ≤ y) or (y < x)))

recursive dist(Nat,Nat) -> Nat{
  dist(zero, n) = n
  dist(suc(m), n) = 
    switch n {
      case zero {
        suc(m)
      }
      case suc(n') {
        dist(m, n')
      }
    }
}

dist_mult_add: (all a:Nat, x:Nat, y:Nat. a * (x + y) = a * x + a * y)

dist_mult_add_right: (all x:Nat, y:Nat, a:Nat. (x + y) * a = x * a + y * a)

dist_mult_monus: (all x:Nat. (all y:Nat, z:Nat. x * (y ∸ z) = x * y ∸ x * z))

dist_mult_monus_one: (all x:Nat, y:Nat. x * (y ∸ suc(zero)) = x * y ∸ x)

recfun div_alt(a:Nat, b:Nat, y:Nat) -> Pair<Nat,Nat>
  measure (a + b) + b of Nat
{
  if b = zero then
    pair(zero, a)
  else
    if ((a = y) and (zero < a)) then
      define f = div_alt(zero, b, y);
	pair(suc(first(f)), second(f))
    else
      div_alt(suc(a), b ∸ suc(zero), y)
}
terminates {
  arbitrary a.s8_s40_4 : Nat,
  b.s8_s40_5 : Nat,
  y.s8_s40_6 : Nat
  have A: (if (b ≠ zero and (a = y) and (zero < a)) then (zero + b) + b < (a + b) + b) by {
    assume prem.s8_s40_7
    have X: b + b < (b + b) + a by {
      apply less_add_pos[b + b, a] to prem
    }
    replace add_commute[a, b + b]
X
  }
  have B: (if (b ≠ zero and not ((a = y) and (zero < a))) then (suc(a) + (b ∸ suc(zero))) + (b ∸ suc(zero)) < (a + b) + b) by {
    assume prem.s8_s40_10
    obtain b'.s8_s40_11 where bs.s8_s40_12 : b = suc(b') from apply not_zero_suc[b] to prem
    replace bs
    expand operator ∸
    replace monus_zero | add_suc | add_suc
    expand operator + | operator + | operator < | operator ≤ | operator ≤
less_equal_refl
  }
A, B
}

define divides : (fn (Nat, Nat) -> bool) = fun a:Nat, b:Nat {
      some k:Nat. a * k = b
    }

recursive equal(Nat,Nat) -> bool{
  equal(zero, n) = 
    switch n {
      case zero {
        true
      }
      case suc(n') {
        false
      }
    }
  equal(suc(m'), n) = 
    switch n {
      case zero {
        false
      }
      case suc(n') {
        equal(m', n')
      }
    }
}

equal_complete_sound: (all m:Nat. (all n:Nat. ((m = n) ⇔ equal(m, n))))

equal_implies_less_equal: (all x:Nat, y:Nat. (if x = y then x ≤ y))

equal_refl: (all n:Nat. equal(n, n))

exp_one_implies_zero_or_one: (all m:Nat, n:Nat. (if m ^ n = suc(zero) then ((n = zero) or (m = suc(zero)))))

recursive expt(Nat,Nat) -> Nat{
  expt(zero, n) = suc(zero)
  expt(suc(p), n) = n * expt(p, n)
}

recfun gcd(a:Nat, b:Nat) -> Nat
  measure b of Nat
{
  if b = zero then
    a
  else
    gcd(b, a % b)
}
terminates {
  arbitrary a.s15_3 : Nat,
  b.s15_4 : Nat
  assume bnz.s15_5: b ≠ zero
  have b_pos: zero < b by {
    apply or_not to zero_or_positive[b], bnz
  }
  conclude a % b < b by {
    apply mod_less_divisor[a, b] to b_pos
  }
}

gcd_divides: (all b:Nat, a:Nat. (divides(gcd(a, b), a) and divides(gcd(a, b), b)))

greater_implies_not_equal: (all x:Nat, y:Nat. (if x > y then x ≠ y))

recursive iterate<T>(Nat,T,(fn T -> T)) -> T{
  iterate(zero, init, f) = init
  iterate(suc(n), init, f) = f(@iterate<T>(n, init, f))
}

le_exists_monus: (all n:Nat, m:Nat. (if n ≤ m then some x:Nat. m = n + x))

le_less_trans: (all m:Nat, n:Nat, o:Nat. (if ((m ≤ n) and (n < o)) then m < o))

auto le_lit_suc

le_lit_suc: (all x:Nat, y:Nat. (lit(suc(x)) ≤ lit(suc(y))) = (lit(x) ≤ lit(y)))

left_cancel: (all x:Nat. (all y:Nat, z:Nat. (if x + y = x + z then y = z)))

less_equal_add: (all x:Nat. (all y:Nat. x ≤ x + y))

less_equal_add_left: (all x:Nat, y:Nat. y ≤ x + y)

less_equal_add_monus: (all m:Nat. (all n:Nat, o:Nat. (if ((n ≤ m) and (m ≤ n + o)) then m ∸ n ≤ o)))

less_equal_antisymmetric: (all x:Nat. (all y:Nat. (if ((x ≤ y) and (y ≤ x)) then x = y)))

less_equal_implies_less_or_equal: (all x:Nat. (all y:Nat. (if x ≤ y then ((x < y) or (x = y)))))

less_equal_not_equal_implies_less: (all x:Nat, y:Nat. (if ((x ≤ y) and x ≠ y) then x < y))

less_equal_pow_log: (all n:Nat. n ≤ pow2(log(n)))

less_equal_refl: (all n:Nat. n ≤ n)

less_equal_trans: (all m:Nat. (all n:Nat, o:Nat. (if ((m ≤ n) and (n ≤ o)) then m ≤ o)))

less_implies_less_equal: (all x:Nat. (all y:Nat. (if x < y then x ≤ y)))

less_implies_not_equal: (all x:Nat, y:Nat. (if x < y then x ≠ y))

less_implies_not_greater: (all x:Nat. (all y:Nat. (if x < y then not (y < x))))

less_irreflexive: (all x:Nat. not (x < x))

less_le_trans: (all m:Nat, n:Nat, o:Nat. (if ((m < n) and (n ≤ o)) then m < o))

auto less_lit_suc

less_lit_suc: (all x:Nat, y:Nat. (lit(suc(x)) < lit(suc(y))) = (lit(x) < lit(y)))

auto less_lit_zero_suc

less_lit_zero_suc: (all y:Nat. (ℕ0 < lit(suc(y))) = true)

less_suc_iff_suc_less: (all x:Nat, y:Nat. ((x < y) ⇔ (suc(x) < suc(y))))

less_trans: (all m:Nat, n:Nat, o:Nat. (if ((m < n) and (n < o)) then m < o))

auto less_zero_false

less_zero_false: (all x:Nat. (x < zero) = false)

define lit : (fn Nat -> Nat) = fun a:Nat {
      a
    }

auto lit_add_div

lit_add_div: (all b:Nat, y:Nat. add_div(suc(y), b, suc(y)) = ℕ1 + add_div(zero, b, suc(y)))

auto lit_add_div_suc

lit_add_div_suc: (all a:Nat, b:Nat, y:Nat. add_div(a, suc(b), y) = add_div(suc(a), b, y))

auto lit_add_div_zero

lit_add_div_zero: (all a:Nat, y:Nat. (if a < y then add_div(a, zero, y) = ℕ0))

auto lit_add_suc

lit_add_suc: (all n:Nat, m:Nat. lit(n) + suc(m) = lit(suc(n)) + m)

auto lit_dist_mult_add

lit_dist_mult_add: (all a:Nat, x:Nat, y:Nat. lit(a) * (x + y) = lit(a) * x + lit(a) * y)

auto lit_dist_mult_add_right

lit_dist_mult_add_right: (all x:Nat, y:Nat, a:Nat. (x + y) * lit(a) = x * lit(a) + y * lit(a))

auto lit_div

lit_div: (all x:Nat, y:Nat. lit(x) / lit(y) = add_div(zero, x, y))

auto lit_div_cancel

lit_div_cancel: (all y:Nat. lit(suc(y)) / lit(suc(y)) = ℕ1)

auto lit_expt_suc

lit_expt_suc: (all n:Nat, m:Nat. n ^ lit(suc(m)) = n * n ^ lit(m))

lit_expt_two: (all n:Nat. n ^ ℕ2 = n * n)

auto lit_expt_zero

lit_expt_zero: (all n:Nat. n ^ ℕ0 = ℕ1)

auto lit_idem

lit_idem: (all x:Nat. lit(lit(x)) = lit(x))

auto lit_less_zero_false

lit_less_zero_false: (all x:Nat. (x < ℕ0) = false)

lit_mult_left_cancel: (all m:Nat, a:Nat, b:Nat. (if lit(suc(m)) * a = lit(suc(m)) * b then a = b))

auto lit_mult_lit_suc

lit_mult_lit_suc: (all m:Nat, n:Nat. lit(m) * lit(suc(n)) = lit(m) + lit(m) * lit(n))

auto lit_mult_suc

lit_mult_suc: (all m:Nat, n:Nat. lit(m) * suc(n) = lit(m) + lit(m) * n)

auto lit_one_expt

lit_one_expt: (all n:Nat. ℕ1 ^ n = ℕ1)

auto lit_suc_add

lit_suc_add: (all x:Nat, y:Nat. lit(suc(x)) + lit(y) = lit(suc(lit(x) + lit(y))))

lit_suc_add2: (all x:Nat, y:Nat. suc(lit(x) + y) = lit(suc(x)) + y)

auto lit_suc_less_equal_zero_false

lit_suc_less_equal_zero_false: (all x:Nat. (lit(suc(x)) ≤ ℕ0) = false)

auto lit_suc_monus_suc

lit_suc_monus_suc: (all n:Nat, m:Nat. lit(suc(n)) ∸ lit(suc(m)) = lit(n) ∸ lit(m))

auto lit_suc_mult

lit_suc_mult: (all m:Nat, n:Nat. lit(suc(m)) * lit(n) = lit(n) + lit(m) * lit(n))

lit_two_mult: (all n:Nat. ℕ2 * n = n + n)

auto lit_zero_div

lit_zero_div: (all x:Nat. ℕ0 / lit(suc(x)) = ℕ0)

auto lit_zero_less_equal_true

lit_zero_less_equal_true: (all x:Nat. (ℕ0 ≤ x) = true)

define log : (fn Nat -> Nat) = fun n {
      find_log(n, zero, zero)
    }

define log2 : (fn Nat -> Nat) = fun n {
      find_log2(n, n, zero)
    }

recursive max(Nat,Nat) -> Nat{
  max(zero, n) = n
  max(suc(m'), n) = 
    switch n {
      case zero {
        suc(m')
      }
      case suc(n') {
        suc(max(m', n'))
      }
    }
}

max_assoc: (all x:Nat, y:Nat, z:Nat. max(max(x, y), z) = max(x, max(y, z)))

max_equal_greater_left: (all x:Nat, y:Nat. (if y ≤ x then max(x, y) = x))

max_equal_greater_right: (all x:Nat, y:Nat. (if x ≤ y then max(x, y) = y))

max_greater_left: (all x:Nat, y:Nat. x ≤ max(x, y))

max_greater_right: (all y:Nat, x:Nat. y ≤ max(x, y))

max_is_left_or_right: (all x:Nat, y:Nat. ((max(x, y) = x) or (max(x, y) = y)))

max_less_equal: (all x:Nat, y:Nat, z:Nat. (if ((x ≤ z) and (y ≤ z)) then max(x, y) ≤ z))

max_symmetric: (all x:Nat, y:Nat. max(x, y) = max(y, x))

recursive min(Nat,Nat) -> Nat{
  min(zero, n) = zero
  min(suc(m'), n) = 
    switch n {
      case zero {
        zero
      }
      case suc(n') {
        suc(min(m', n'))
      }
    }
}

monus_add_assoc: (all n:Nat. (all l:Nat, m:Nat. (if m ≤ n then l + (n ∸ m) = (l + n) ∸ m)))

monus_add_identity: (all n:Nat. (all m:Nat. (if m ≤ n then m + (n ∸ m) = n)))

monus_monus_eq_monus_add: (all x:Nat. (all y:Nat. (all z:Nat. (x ∸ y) ∸ z = x ∸ (y + z))))

monus_order: (all x:Nat, y:Nat, z:Nat. (x ∸ y) ∸ z = (x ∸ z) ∸ y)

monus_right_cancel: (all x:Nat, y:Nat, a:Nat. (if ((x ∸ a = y ∸ a) and (a ≤ x) and (a ≤ y)) then x = y))

mult_assoc: (all m:Nat. (all n:Nat, o:Nat. (m * n) * o = m * (n * o)))

mult_cancel_left_less: (all x:Nat, y:Nat, z:Nat. (if x * y < x * z then y < z))

mult_cancel_right_less: (all x:Nat, y:Nat, z:Nat. (if y * x < z * x then y < z))

mult_commute: (all m:Nat. (all n:Nat. m * n = n * m))

mult_mono_le: (all n:Nat. (all x:Nat, y:Nat. (if x ≤ y then n * x ≤ n * y)))

mult_mono_le2: (all n:Nat, x:Nat, m:Nat, y:Nat. (if ((n ≤ m) and (x ≤ y)) then n * x ≤ m * y))

mult_mono_le_r: (all n:Nat. (all x:Nat, y:Nat. (if x ≤ y then x * n ≤ y * n)))

mult_suc: (all m:Nat. (all n:Nat. m * suc(n) = m + m * n))

mult_to_zero: (all n:Nat, m:Nat. (if m * n = zero then ((m = zero) or (n = zero))))

mult_two: (all n:Nat. n + n = ℕ2 * n)

auto mult_zero

mult_zero: (all n:Nat. n * zero = zero)

n_le_nn: (all n:Nat. n ≤ n * n)

nat_add_to_zero: (all n:Nat, m:Nat. (if n + m = ℕ0 then ((n = ℕ0) and (m = ℕ0))))

auto nat_add_zero

nat_add_zero: (all x:Nat. x + ℕ0 = x)

nat_less_add_pos: (all x:Nat, y:Nat. (if ℕ0 < y then x < x + y))

nat_monus_cancel: (all n:Nat. n ∸ n = ℕ0)

nat_monus_one_pred: (all x:Nat. x ∸ ℕ1 = pred(x))

auto nat_monus_zero

nat_monus_zero: (all n:Nat. n ∸ ℕ0 = n)

nat_monus_zero_iff_less_eq: (all x:Nat, y:Nat. ((x ≤ y) ⇔ (x ∸ y = ℕ0)))

auto nat_mult_one

nat_mult_one: (all n:Nat. n * ℕ1 = n)

nat_not_one_add_zero: (all n:Nat. ℕ1 + n ≠ ℕ0)

auto nat_one_mult

nat_one_mult: (all n:Nat. ℕ1 * n = n)

nat_positive_suc: (all n:Nat. (if ℕ0 < n then some n':Nat. n = ℕ1 + n'))

nat_suc_one_add: (all n:Nat. suc(n) = ℕ1 + n)

auto nat_zero_add

nat_zero_add: (all y:Nat. ℕ0 + y = y)

nat_zero_le_zero: (all x:Nat. (if x ≤ ℕ0 then x = ℕ0))

nat_zero_less_one_add: (all n:Nat. ℕ0 < ℕ1 + n)

nat_zero_monus: (all m:Nat. ℕ0 ∸ lit(m) = ℕ0)

auto nat_zero_mult

nat_zero_mult: (all y:Nat. ℕ0 * lit(y) = ℕ0)

nat_zero_or_positive: (all x:Nat. ((x = ℕ0) or (ℕ0 < x)))

not_equal_not_eq: (all m:Nat, n:Nat. (if not equal(m, n) then m ≠ n))

not_less_equal_iff_greater: (all x:Nat, y:Nat. ((not (x ≤ y)) ⇔ (y < x)))

not_less_equal_less_equal: (all x:Nat, y:Nat. (if not (x ≤ y) then y ≤ x))

not_less_implies_less_equal: (all x:Nat. (all y:Nat. (if not (x < y) then y ≤ x)))

not_suc_less_equal_zero: (all x:Nat. not (suc(x) ≤ zero))

auto one_mult

one_mult: (all n:Nat. suc(zero) * n = n)

define operator % : (fn (Nat, Nat) -> Nat) = fun n:Nat, m:Nat {
      n ∸ (n / m) * m
    }

recursive operator *(Nat,Nat) -> Nat{
  operator *(zero, m) = zero
  operator *(suc(n), m) = m + n * m
}

recursive operator +(Nat,Nat) -> Nat{
  operator +(zero, m) = m
  operator +(suc(n), m) = suc(n + m)
}

recfun operator /(n:Nat, m:Nat) -> Nat
  measure n of Nat
{
  if n < m then
    zero
  else
    if m = zero then
      zero
    else
      suc(zero) + (n ∸ m) / m
}
terminates {
  arbitrary n.s8_s21_3 : Nat,
  m.s8_s21_4 : Nat
  assume cond.s8_s21_5: (not (n < m) and m ≠ zero)
  suffices m + (n ∸ m) < m + n  by {
add_both_sides_of_less[m, n ∸ m, n]
  }
  suffices n < m + n  by {
    have m_n: m ≤ n by {
      apply not_less_implies_less_equal to conjunct 0 of cond
    }
    replace apply monus_add_identity[n, m] to m_n
.
  }
  obtain m'.s8_s21_7 where m_sm.s8_s21_8 : m = suc(m') from apply not_zero_suc to conjunct 1 of cond
  suffices n < suc(m') + n  by {
    replace m_sm
.
  }
  suffices n ≤ m' + n  by {
    expand operator + | operator < | operator ≤
.
  }
  replace add_commute
  conclude n ≤ n + m' by {
less_equal_add
  }
}

define operator < : (fn (Nat, Nat) -> bool) = fun x:Nat, y:Nat {
      suc(x) ≤ y
    }

define operator > : (fn (Nat, Nat) -> bool) = fun x:Nat, y:Nat {
      y < x
    }

define operator ^ : (fn (Nat, Nat) -> Nat) = fun a:Nat, b:Nat {
      expt(b, a)
    }

recursive operator ∸(Nat,Nat) -> Nat{
  operator ∸(zero, m) = zero
  operator ∸(suc(n), m) = 
    switch m {
      case zero {
        suc(n)
      }
      case suc(m') {
        n ∸ m'
      }
    }
}

recursive operator ≤(Nat,Nat) -> bool{
  operator ≤(zero, m) = true
  operator ≤(suc(n'), m) = 
    switch m {
      case zero {
        false
      }
      case suc(m') {
        n' ≤ m'
      }
    }
}

define operator ≥ : (fn (Nat, Nat) -> bool) = fun x:Nat, y:Nat {
      y ≤ x
    }

pos_mult_both_sides_of_less: (all n:Nat, x:Nat, y:Nat. (if ((ℕ0 < n) and (x < y)) then n * x < n * y))

pos_mult_left_cancel: (all m:Nat, a:Nat, b:Nat. (if ((ℕ0 < m) and (m * a = m * b)) then a = b))

pos_mult_left_cancel_less_equal: (all n:Nat, x:Nat, y:Nat. (if ((ℕ0 < n) and (n * x ≤ n * y)) then x ≤ y))

pos_mult_right_cancel_less: (all c:Nat, a:Nat, b:Nat. (if ((ℕ0 < c) and (a * c < b * c)) then a < b))

recursive pow2(Nat) -> Nat{
  pow2(zero) = suc(zero)
  pow2(suc(n')) = suc(suc(zero)) * pow2(n')
}

pow_add_r: (all n:Nat, m:Nat, o:Nat. m ^ (n + o) = m ^ n * m ^ o)

pow_eq_zero: (all n:Nat, m:Nat. (if m ^ n = zero then m = zero))

pow_le_mono_l: (all c:Nat, a:Nat, b:Nat. (if a ≤ b then a ^ c ≤ b ^ c))

pow_log2_greater: (all n:Nat. n < ℕ2 * ℕ2 ^ log2(n))

pow_log2_less_equal: (all n:Nat. (if ℕ0 < n then ℕ2 ^ log2(n) ≤ n))

pow_lt_mono_l: (all c:Nat, a:Nat, b:Nat. (if zero < c then (if a < b then a ^ c < b ^ c)))

pow_lt_mono_r: (all c:Nat, a:Nat, b:Nat. (if suc(zero) < a then (if b < c then a ^ b < a ^ c)))

pow_mul_l: (all o:Nat, m:Nat, n:Nat. (m * n) ^ o = m ^ o * n ^ o)

pow_mul_r: (all o:Nat, m:Nat, n:Nat. (m ^ n) ^ o = m ^ (n * o))

pow_pos_nonneg: (all b:Nat, a:Nat. (if zero < a then zero < a ^ b))

pow_zero_l: (all a:Nat. (if zero < a then zero ^ a = zero))

define pred : (fn Nat -> Nat) = fun n:Nat {
      switch n {
        case zero {
          zero
        }
        case suc(n') {
          n'
        }
      }
    }

strong_induction: (all P:(fn Nat -> bool), n:Nat. (if (all j:Nat. (if (all i:Nat. (if i < j then P(i))) then P(j))) then P(n)))

auto suc_lit

suc_lit: (all n:Nat. suc(lit(n)) = lit(suc(n)))

sum_n': (all n:Nat. ℕ2 * summation(suc(n), ℕ0, fun x { x }) = n * (n + ℕ1))

sum_n: (all n:Nat. ℕ2 * summation(n, ℕ0, fun x { x }) = n * (n ∸ ℕ1))

recursive summation(Nat,Nat,(fn Nat -> Nat)) -> Nat{
  summation(zero, begin, f) = zero
  summation(suc(k), begin, f) = f(begin) + summation(k, suc(begin), f)
}

summation_add: (all a:Nat. (all b:Nat, s:Nat, t:Nat, f:(fn Nat -> Nat), g:(fn Nat -> Nat), h:(fn Nat -> Nat). (if ((all i:Nat. (if i < a then g(s + i) = f(s + i))) and (all i:Nat. (if i < b then h(t + i) = f((s + a) + i)))) then summation(a + b, s, f) = summation(a, s, g) + summation(b, t, h))))

summation_cong: (all k:Nat. (all f:(fn Nat -> Nat), g:(fn Nat -> Nat), s:Nat, t:Nat. (if (all i:Nat. (if i < k then f(s + i) = g(t + i))) then summation(k, s, f) = summation(k, t, g))))

summation_const_one: (all n:Nat. (all s:Nat. summation(n, s, fun i:Nat { suc(zero) }) = n))

summation_next: (all n:Nat, s:Nat, f:(fn Nat -> Nat). summation(ℕ1 + n, s, f) = summation(n, s, f) + f(s + n))

summation_pow2_succ: (all n:Nat. ℕ1 + summation(n, ℕ0, fun i:Nat { ℕ2 ^ i }) = ℕ2 ^ n)

summation_pow_succ: (all a:Nat. (if ℕ1 ≤ a then (all n:Nat. ℕ1 + (a ∸ ℕ1) * summation(n, ℕ0, fun i:Nat { a ^ i }) = a ^ n)))

trichotomy: (all x:Nat. (all y:Nat. ((x < y) or (x = y) or (y < x))))

trichotomy2: (all y:Nat, x:Nat. (if (x ≠ y and not (x < y)) then y < x))

auto zero_less_equal_true

zero_less_equal_true: (all x:Nat. (zero ≤ x) = true)