---

Comment: int_2_summary
Defines mod, floor, max and min functions over the 
integers.
Lemmas concern basic properties of arithmetic functions over integers,
and induction principles. 

Comment: int_2_intro
Contains definitions for integer functions such
as mod, floor, max and min. 

Gives many standard lemmas for standard arithmetic
functions over the integers, involving both
equalities and inequalities. 

At end, are some induction lemmas for 
various subsets of the integers.  ⋅

Lemma: int_trichot
∀i,j:ℤ.  (i < j ∨ (i = j ∈ ℤ) ∨ (i > j))

Lemma: injection_le
∀[k,m:ℕ].  k ≤ m supposing ∃f:ℕk ⟶ ℕm. Inj(ℕk;ℕm;f)

Lemma: disjoint_increasing_onto
∀[m,n,k:ℕ]. ∀[f:ℕn ⟶ ℕm]. ∀[g:ℕk ⟶ ℕm].
  (m = (n + k) ∈ ℕ) supposing 
     ((∀j1:ℕn. ∀j2:ℕk.  (¬((f j1) = (g j2) ∈ ℤ))) and 
     (∀i:ℕm. ((∃j:ℕn. (i = (f j) ∈ ℤ)) ∨ (∃j:ℕk. (i = (g j) ∈ ℤ)))) and 
     increasing(g;k) and 
     increasing(f;n))

Lemma: modulus_base_neg
∀[m:ℕ+]. ∀[a:{-m..0-}].  (a mod m ~ m + a)

Lemma: eq_to_le
∀[i,j:ℤ].  i ≤ j supposing i = j ∈ ℤ

Lemma: lt_to_le
∀[i,j:ℤ].  uiff(i < j;(i + 1) ≤ j)

Lemma: le_to_lt_weaken
∀[i,j:ℤ].  i ≤ j supposing i < j

Lemma: lt_to_le_rw
∀[i,j:ℤ].  {uiff(i < j;(i + 1) ≤ j)}

Lemma: le_to_lt
∀[i,j:ℤ].  uiff(i ≤ j;i < j + 1)

Lemma: le_to_lt_rw
∀[i,j:ℤ].  {uiff(i ≤ j;i < j + 1)}

Definition: rounding-div
[b ÷ m] ==
  eval n = m in
  eval a = b in
    let q,r = divrem(a; n) 
    in eval r2 = 2 * r in
       if (r2) < (n)  then if (-n) < (r2)  then q  else (q - 1)  else (q + 1)

Lemma: rounding-div_wf
∀[a:ℤ]. ∀[n:ℕ+].  ([a ÷ n] ∈ ℤ)

Lemma: rounding-div-property
∀[a:ℤ]. ∀[n:ℕ+].  ((2 * |(n * [a ÷ n]) - a|) ≤ n)

Lemma: minus_minus_cancel
∀[a:ℤ]. ((--a) = a ∈ ℤ)

Lemma: mul_ident
∀[i:ℤ]. (i = (i * 1) ∈ ℤ)

Lemma: mul_com
∀[a,b:ℤ].  ((a * b) = (b * a) ∈ ℤ)

Lemma: minus_thru_mul
∀[a,b:ℤ].  ((-(a * b)) = ((-a) * b) ∈ ℤ)

Lemma: equal-iff-diff-zero
∀x,y:ℤ.  uiff(x = y ∈ ℤ;(x - y) = 0 ∈ ℤ)

Lemma: equal-iff-diff-zero2
∀x,y:ℤ.  uiff(x = y ∈ ℤ;(y - x) = 0 ∈ ℤ)

Lemma: right_mul_preserves_le
∀[a,b:ℤ]. ∀[n:ℕ].  (a * n) ≤ (b * n) supposing a ≤ b

Comment: mul_fun_comment
This is only for first quadrant. Should we have variants for
each quadrant, or insist that all multiplications be
normalized to first quadrant before using this lemma?
⋅

Lemma: multiply_functionality_wrt_le
∀[i1,i2:ℕ]. ∀[j1,j2:ℤ].  ((i1 * i2) ≤ (j1 * j2)) supposing ((i2 ≤ j2) and (i1 ≤ j1))

Lemma: mul_functionality_wrt_eq
∀[i1,i2,j1,j2:ℤ].  ((i1 * i2) = (j1 * j2) ∈ ℤ) supposing ((i2 = j2 ∈ ℤ) and (i1 = j1 ∈ ℤ))

Lemma: mul_nat_plus
∀[a,b:ℕ+].  (a * b ∈ ℕ+)

Lemma: absval_nat_plus
∀[x:ℤ]. |x| ∈ ℕ+ supposing ¬(x = 0 ∈ ℤ)

Lemma: pos_mul_arg_bounds
∀a,b:ℤ.  ((a * b) > 0 ⇐⇒ ((a > 0) ∧ (b > 0)) ∨ (a < 0 ∧ b < 0))

Lemma: neg_mul_arg_bounds
∀a,b:ℤ.  (a * b < 0 ⇐⇒ (a < 0 ∧ (b > 0)) ∨ ((a > 0) ∧ b < 0))

Lemma: mul-non-neg1
∀[x,y:ℤ].  (0 ≤ (x * y)) supposing ((0 ≤ y) and (0 ≤ x))

Lemma: multiply_nat_plus
∀[i,j:ℕ+].  (i * j ∈ ℕ+)

Comment: quasi_lin_com
======================
QUASI-LINEAR FUNCTIONS
======================

Lemma: fun_exp-mul
∀[T:Type]. ∀[f:T ⟶ T]. ∀[n,m:ℕ]. ∀[x:T].  ((f^n * m x) = (λx.(f^m x)^n x) ∈ T)

Lemma: int-triangle-inequality
∀[a,b:ℤ].  (|a + b| ≤ (|a| + |b|))

Lemma: int-triangle-inequality2
∀[a,b:ℤ].  (|a - b| ≤ (|a| + |b|))

Definition: pm_equal
i = ± j ==  (i = j ∈ ℤ) ∨ (i = (-j) ∈ ℤ)

Lemma: pm_equal_wf
∀[a,b:ℤ].  (a = ± b ∈ ℙ)

Lemma: absval_eq
∀x,y:ℤ.  (|x| = |y| ∈ ℤ ⇐⇒ x = ± y)

Lemma: absval-sqequal-imax
∀[a:Top]. (imax(a;-a) ~ |a|)

Lemma: absval-as-imax
∀[a:ℤ]. (imax(a;-a) = |a| ∈ ℤ)

Lemma: mul-imax
∀[n:ℕ]. ∀[a,b:ℤ].  ((n * imax(a;b)) = imax(n * a;n * b) ∈ ℤ)

Lemma: absval-imax-difference
∀[a,b,c,d:ℤ].  (|imax(a;b) - imax(c;d)| ≤ imax(|a - c|;|b - d|))

Lemma: le-iff-imax
∀[a,b:ℤ].  uiff(a ≤ b;imax(a;b) = b ∈ ℤ)

Lemma: comb_for_imax_wf
λa,b,z. imax(a;b) ∈ a:ℤ ⟶ b:ℤ ⟶ (↓True) ⟶ ℤ

Lemma: imax_nat_plus
∀[a:ℤ]. ∀[b:ℕ+].  (imax(a;b) ∈ ℕ+)

Lemma: imax-wf-partial-nat
∀[x,y:partial(ℕ)].  (imax(x;y) ∈ partial(ℕ))

Definition: imin
imin(a;b) ==  eval a = a in eval b = b in   if a ≤z b then a else b fi 

Lemma: imin_wf
∀[a,b:ℤ].  (imin(a;b) ∈ ℤ)

Lemma: imin_unfold
∀[a,b:ℤ].  (imin(a;b) = if a ≤z b then a else b fi  ∈ ℤ)

Lemma: mul-imin
∀[n:ℕ]. ∀[a,b:ℤ].  ((n * imin(a;b)) = imin(n * a;n * b) ∈ ℤ)

Lemma: absval-imin-difference
∀[a,b,c,d:ℤ].  (|imin(a;b) - imin(c;d)| ≤ imax(|a - c|;|b - d|))

Lemma: absval-diff-symmetry
∀[x,y:ℤ].  (|x - y| ~ |y - x|)

Lemma: absval-diff-product-bound
∀u,v,x,y:ℕ.  ((|u - v| * |x - y|) ≤ |(imax(u;v) * imax(x;y)) - imin(u;v) * imin(x;y)|)

Lemma: absval-diff-product-bound2
∀u,v,x,y:ℤ.  (|(u * v) - x * y| ≤ ((|u| * |v - y|) + (|y| * |u - x|)))

Lemma: le-iff-imin
∀[a,b:ℤ].  uiff(a ≤ b;imin(a;b) = a ∈ ℤ)

Lemma: imin_nat
∀[a,b:ℕ].  (imin(a;b) ∈ ℕ)

Lemma: imin_nat_plus
∀[a,b:ℕ+].  (imin(a;b) ∈ ℕ+)

Lemma: comb_for_imin_wf
λa,b,z. imin(a;b) ∈ a:ℤ ⟶ b:ℤ ⟶ (↓True) ⟶ ℤ

Lemma: minus_imax
∀[a,b:ℤ].  ((-imax(a;b)) = imin(-a;-b) ∈ ℤ)

Lemma: minus_imin
∀[a,b:ℤ].  ((-imin(a;b)) = imax(-a;-b) ∈ ℤ)

Lemma: imax_lb
∀[a,b,c:ℤ].  uiff(imax(a;b) ≤ c;{(a ≤ c) ∧ (b ≤ c)})

Lemma: imax_ub
∀a,b,c:ℤ.  (a ≤ imax(b;c) ⇐⇒ (a ≤ b) ∨ (a ≤ c))

Lemma: imax-idempotent
∀[x:ℤ]. (imax(x;x) ~ x)

Lemma: imax-left
∀[a,b:ℤ].  uiff(imax(a;b) = a ∈ ℤ;b ≤ a)

Lemma: imax-right
∀[a,b:ℤ].  uiff(imax(a;b) = b ∈ ℤ;a ≤ b)

Lemma: imax_strict_ub
∀a,b,c:ℤ.  (a < imax(b;c) ⇐⇒ a < b ∨ a < c)

Lemma: imax_strict_lb
∀[a,b,c:ℤ].  uiff(imax(a;b) < c;a < c ∧ b < c)

Lemma: imax_add_r
∀[a,b,c:ℤ].  ((imax(a;b) + c) = imax(a + c;b + c) ∈ ℤ)

Lemma: imax_assoc
∀[a,b,c:ℤ].  (imax(a;imax(b;c)) = imax(imax(a;b);c) ∈ ℤ)

Lemma: imax_com
∀[a,b:ℤ].  (imax(a;b) = imax(b;a) ∈ ℤ)

Lemma: imin_assoc
∀[a,b,c:ℤ].  (imin(a;imin(b;c)) = imin(imin(a;b);c) ∈ ℤ)

Lemma: imin_com
∀[a,b:ℤ].  (imin(a;b) = imin(b;a) ∈ ℤ)

Lemma: imin-imax-absorption
∀[x,y:ℤ].  (imin(x;imax(x;y)) = x ∈ ℤ)

Lemma: imax-imin-absorption
∀[x,y:ℤ].  (imax(x;imin(x;y)) = x ∈ ℤ)

Lemma: imin-imax-distributive
∀[x,y,z:ℤ].  (imin(imax(x;y);imax(x;z)) = imax(x;imin(y;z)) ∈ ℤ)

Lemma: imax-imin-distributive
∀[x,y,z:ℤ].  (imax(imin(x;y);imin(x;z)) = imin(x;imax(y;z)) ∈ ℤ)

Lemma: imin_add_r
∀[a,b,c:ℤ].  ((imin(a;b) + c) = imin(a + c;b + c) ∈ ℤ)

Lemma: imin_lb
∀a,b,c:ℤ.  (imin(a;b) ≤ c ⇐⇒ (a ≤ c) ∨ (b ≤ c))

Lemma: imin_ub
∀[a,b,c:ℤ].  uiff(a ≤ imin(b;c);{(a ≤ b) ∧ (a ≤ c)})

Definition: ndiff
a -- b ==  imax(a - b;0)

Lemma: ndiff_wf
∀[a,b:ℤ].  (a -- b ∈ ℤ)

Lemma: comb_for_ndiff_wf
λa,b,z. (a -- b) ∈ a:ℤ ⟶ b:ℤ ⟶ (↓True) ⟶ ℤ

Lemma: ndiff_id_r
∀[a:ℕ]. ((a -- 0) = a ∈ ℤ)

Lemma: ndiff_ann_l
∀[a:ℕ]. ((0 -- a) = 0 ∈ ℤ)

Lemma: ndiff_inv
∀[a:ℕ]. ∀[b:ℤ].  (((a + b) -- b) = a ∈ ℤ)

Lemma: ndiff_ndiff
∀[a,b:ℤ]. ∀[c:ℕ].  (((a -- b) -- c) = (a -- (b + c)) ∈ ℤ)

Lemma: ndiff_ndiff_eq_imin
∀[a,b:ℕ].  ((a -- (a -- b)) = imin(a;b) ∈ ℤ)

Lemma: ndiff_add_eq_imax
∀[a,b:ℤ].  (((a -- b) + b) = imax(a;b) ∈ ℤ)

Lemma: ndiff_zero
∀[a,b:ℤ].  uiff((a -- b) = 0 ∈ ℤ;a ≤ b)

Comment: div_rem_com
================================
DIVISION AND REMAINDER FUNCTIONS
================================

Lemma: div_rem_sum2
∀[a:ℤ]. ∀[n:ℤ-o].  (n * (a ÷ n) ~ a - a rem n)

Lemma: remainder_wf
∀[a:ℕ]. ∀[n:ℕ+].  (a rem n ∈ ℕ)

Lemma: comb_for_remainder_wf
λa,n,z. (a rem n) ∈ a:ℕ ⟶ n:ℕ+ ⟶ (↓True) ⟶ ℕ

Lemma: rem_sym_1
∀[a:ℤ]. ∀[n:ℤ-o].  ((-(a rem n)) = (-a rem n) ∈ ℤ)

Lemma: rem_sym_1a
∀[a:ℤ]. ∀[n:ℤ-o].  ((a rem n) = (-(-a rem n)) ∈ ℤ)

Lemma: rem_sym_2
∀[a:ℤ]. ∀[n:ℤ-o].  ((a rem n) = (a rem -n) ∈ ℤ)

Lemma: omega-dark-shadow
∀a,b:ℕ+. ∀c,d:ℤ.  ((((a - 1) * (b - 1)) ≤ ((a * d) - b * c)) ⇒ (∃x:ℤ. ((c ≤ (a * x)) ∧ ((b * x) ≤ d))))

Lemma: omega-shadow-exact1
∀b:ℕ+. ∀c,d:ℤ.  (∃x:ℤ. ((c ≤ x) ∧ ((b * x) ≤ d)) ⇐⇒ (b * c) ≤ d)

Lemma: omega-shadow-exact2
∀a:ℕ+. ∀c,d:ℤ.  (∃x:ℤ. ((c ≤ (a * x)) ∧ (x ≤ d)) ⇐⇒ c ≤ (a * d))

Lemma: rem_mag_bound
∀[a:ℤ]. ∀[n:ℤ-o].  |a rem n| < |n|

Lemma: square_non_neg
∀x:ℤ. (0 ≤ (x * x))

Lemma: absval_square
∀[x:ℤ]. (|x * x| = (x * x) ∈ ℤ)

Lemma: absval_squared
∀[x:ℤ]. ((|x| * |x|) = (x * x) ∈ ℤ)

Lemma: zero-rem
∀[m:ℤ-o]. (0 rem m ~ 0)

Lemma: one-rem
∀[m:ℤ]. 1 rem m ~ 1 supposing 1 < m

Lemma: divide_wf
∀[a:ℕ]. ∀[n:ℕ+].  (a ÷ n ∈ ℕ)

Definition: div_nrel
Div(a;n;q) ==  n * q ≤ a < n * (q + 1)

Lemma: div_nrel_wf
∀[a:ℕ]. ∀[n:ℕ+]. ∀[q:ℕ].  (Div(a;n;q) ∈ ℙ)

Lemma: div_fun_sat_div_nrel
∀[a:ℕ]. ∀[n:ℕ+].  Div(a;n;a ÷ n)

Lemma: div_elim
∀a:ℕ. ∀n:ℕ+.  ∃q:ℕ. (Div(a;n;q) ∧ ((a ÷ n) = q ∈ ℤ))

Lemma: div_unique
∀[a:ℕ]. ∀[n:ℕ+]. ∀[p,q:ℕ].  (p = q ∈ ℤ) supposing (Div(a;n;q) and Div(a;n;p))

Lemma: div_unique2
∀[a:ℕ]. ∀[n:ℕ+]. ∀[p:ℕ].  uiff((a ÷ n) = p ∈ ℤ;Div(a;n;p))

Lemma: div-cancel
∀[x:ℤ]. ∀[y:ℤ-o].  ((x * y) ÷ y ~ x)

Lemma: div-self
∀[y:ℤ-o]. (y ÷ y ~ 1)

Lemma: div-cancel2
∀[x:ℤ]. ∀[y:ℤ-o].  ((y * x) ÷ y ~ x)

Lemma: div-cancel3
∀[x:ℕ]. ∀[y:ℕ+]. ∀[z:ℕy].  (((y * x) + z) ÷ y ~ x)

Lemma: div_mul_cancel
∀[a:ℕ]. ∀[b:ℕ+].  (((a * b) ÷ b) = a ∈ ℤ)

Lemma: div_mul_add_cancel
∀[a:ℕ]. ∀[b:ℕ+]. ∀[r:ℕb].  ((((a * b) + r) ÷ b) = a ∈ ℤ)

Lemma: div_lbound_1
∀[a:ℕ]. ∀[n:ℕ+]. ∀[k:ℕ].  uiff(k ≤ (a ÷ n);(k * n) ≤ a)

Lemma: div_preserves_le
∀[a,b:ℤ]. ∀[n:ℕ+].  ((a ≤ b) ⇒ ((a ÷ n) ≤ (b ÷ n)))

Lemma: div_div_nat
∀[a:ℕ]. ∀[n,m:ℕ+].  (a ÷ n ÷ m ~ a ÷ n * m)

Lemma: div_div
∀[a:ℤ]. ∀[n,m:ℤ-o].  (a ÷ n ÷ m ~ a ÷ n * m)

Lemma: div_div_commutes
∀[a:ℤ]. ∀[n,m:ℤ-o].  (a ÷ n ÷ m ~ a ÷ m ÷ n)

Lemma: div-mul-cancel
∀[a:ℤ]. ∀[n,m:ℤ-o].  ((a * n) ÷ m * n ~ a ÷ m)

Lemma: div-mul-cancel2
∀[a:ℤ]. ∀[n,m:ℤ-o].  ((n * a) ÷ n * m ~ a ÷ m)

Lemma: mul-div-bounds
∀[a,b:ℤ]. ∀[m:ℤ-o].  (|(a * (b ÷ m)) - b * (a ÷ m)| ≤ (|a| + |b|))

Lemma: rem-mul
∀[a:ℤ]. ∀[n,m:ℤ-o].  ((a * n rem m * n) = ((a rem m) * n) ∈ ℤ)

Lemma: implies-equal-div
∀[a,c:ℤ]. ∀[b,d:ℤ-o].  (a ÷ b) = (c ÷ d) ∈ ℤ supposing (d * a) = (b * c) ∈ ℤ

Lemma: div_one
∀[x:ℤ]. (x ÷ 1 ~ x)

Lemma: div_minus_one
∀[x:ℤ]. (x ÷ -1 ~ -x)

Lemma: implies-equal-div2
∀[a,c:ℤ]. ∀[b:ℤ-o].  (a ÷ b) = c ∈ ℤ supposing a = (b * c) ∈ ℤ

Definition: rem_nrel
Rem(a;n;r) ==  ∃q:ℕ. (Div(a;n;q) ∧ (((q * n) + r) = a ∈ ℤ))

Lemma: rem_nrel_wf
∀[a:ℕ]. ∀[n:ℕ+]. ∀[r:ℕ].  (Rem(a;n;r) ∈ ℙ)

Lemma: rem_fun_sat_rem_nrel
∀a:ℕ. ∀n:ℕ+.  Rem(a;n;a rem n)

Lemma: div_base_case
∀[a:ℕ]. ∀[n:ℕ+].  (a ÷ n) = 0 ∈ ℤ supposing a < n

Lemma: div_rec_case
∀[a:ℕ]. ∀[n:ℕ+].  (a ÷ n) = (((a - n) ÷ n) + 1) ∈ ℤ supposing a ≥ n 

Lemma: rem_base_case
∀[a:ℕ]. ∀[n:ℕ+].  (a rem n) = a ∈ ℤ supposing a < n

Lemma: rem_gen_base_case
∀[a:ℤ]. ∀[n:ℤ-o].  (a rem n) = a ∈ ℤ supposing |a| < |n|

Lemma: rem_rec_case
∀[a:ℕ]. ∀[n:ℕ+].  (a rem n) = (a - n rem n) ∈ ℤ supposing a ≥ n 

Lemma: rem_invariant
∀[a,b:ℕ]. ∀[n:ℕ+].  ((a + (b * n) rem n) = (a rem n) ∈ ℤ)

Lemma: rem_addition
∀[i,j:ℕ]. ∀[n:ℕ+].  (((i rem n) + (j rem n) rem n) = (i + j rem n) ∈ ℤ)

Lemma: rem_add1
∀[i:ℕ]. ∀[n:ℕ+].  ((i + 1 rem n) = if (i rem n =z n - 1) then 0 else (i rem n) + 1 fi  ∈ ℤ)

Lemma: rem_rem_to_rem
∀[a:ℕ]. ∀[n:ℕ+].  ((a rem n rem n) = (a rem n) ∈ ℤ)

Lemma: rem_base_case_z
∀[a:ℤ]. ∀[b:ℤ-o].  (a rem b) = a ∈ ℤ supposing |a| < |b|

Lemma: rem_eq_args
∀[a:ℕ+]. ((a rem a) = 0 ∈ ℤ)

Lemma: rem_eq_args_z
∀[a:ℤ]. ∀[b:ℤ-o].  (a rem b) = 0 ∈ ℤ supposing |a| = |b| ∈ ℤ

Lemma: fun_exp-rem
∀[T:Type]. ∀[f:T ⟶ T]. ∀[x:T]. ∀[n:ℕ+].  ∀[k:ℕ]. ((f^k x) = (f^k rem n x) ∈ T) supposing (f^n x) = x ∈ T

Lemma: int_mag_well_founded
WellFnd{i}(ℤ;x,y.|x| < |y|)

Lemma: int_upper_well_founded
∀n:ℤ. WellFnd{i}({n...};x,y.x < y)

Lemma: int_upper_uwell_founded
∀n:ℤ. uWellFnd({n...};x,y.x < y)

Lemma: int_upper_ind
∀i:ℤ. ∀[E:{i...} ⟶ ℙ{u}]. (E[i] ⇒ (∀k:{i + 1...}. (E[k - 1] ⇒ E[k])) ⇒ {∀k:{i...}. E[k]})

Lemma: int_upper_ind_uniform
∀i:ℤ. ∀[E:{i...} ⟶ ℙ{u}]. ((∀[k:{i...}]. ((∀[j:{i..k-}]. E[j]) ⇒ E[k])) ⇒ {∀[k:{i...}]. E[k]})

Lemma: int_seg_well_founded_up
∀i:ℤ. ∀j:{i...}.  WellFnd{i}({i..j-};x,y.x < y)

Lemma: int_seg_ind
∀i:ℤ. ∀j:{i + 1...}.  ∀[E:{i..j-} ⟶ ℙ{u}]. (E[i] ⇒ (∀k:{i + 1..j-}. (E[k - 1] ⇒ E[k])) ⇒ {∀k:{i..j-}. E[k]})

Lemma: int_seg_well_founded_down
∀i:ℤ. ∀j:{i...}.  WellFnd{i}({i..j-};x,y.x > y)

Definition: int_seg_decide_all
int_seg_decide_all(d;i;j) ==
  fix((λG,x. if j ≤z x then inl ⋅ else case d x of inl(z) => G (x + 1) | inr(z) => inr ⋅  fi )) i

Lemma: fan_theorem
∀[X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ]
  (∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s])) ⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f]) supposing ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. X[n;f])

Lemma: fan_theorem-ext
∀[X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ]
  (∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s])) ⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f]) supposing ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. X[n;f])

Lemma: injection-is-surjection
∀n:ℕ. ∀f:ℕn ⟶ ℕn.  Surj(ℕn;ℕn;f) supposing Inj(ℕn;ℕn;f)

Lemma: not-inject
∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ (∀n:ℕ. ∀f:ℕn ⟶ T.  ∃i:ℕn. ∃j:ℕi. ((f i) = (f j) ∈ T) supposing ¬Inj(ℕn;T;f)))

Lemma: divide-and-conquer
∀[Q:a:ℤ ⟶ {a...} ⟶ ℙ]
  ∀s:{2...}
    ((∀a:ℤ. ∀b:{a..a + s-}.  Q[a;b])
    ⇒ (∀a,b,c:ℤ.  (Q[a;c] ⇒ Q[a;b]) ∨ (Q[c;b] ⇒ Q[a;b]) supposing a < c ∧ c < b)
    ⇒ (∀a:ℤ. ∀b:{a...}.  Q[a;b]))

Lemma: divide-and-conquer-ext
∀[Q:a:ℤ ⟶ {a...} ⟶ ℙ]
  ∀s:{2...}
    ((∀a:ℤ. ∀b:{a..a + s-}.  Q[a;b])
    ⇒ (∀a,b,c:ℤ.  (Q[a;c] ⇒ Q[a;b]) ∨ (Q[c;b] ⇒ Q[a;b]) supposing a < c ∧ c < b)
    ⇒ (∀a:ℤ. ∀b:{a...}.  Q[a;b]))

Lemma: div-search-lemma
∀a:ℤ. ∀b:{a + 1...}. ∀f:ℤ ⟶ 𝔹.
  ∃x:{a..b-} [((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))] 
  supposing ∃x:{a..b-} [((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))]

Lemma: div-search-lemma-ext
∀a:ℤ. ∀b:{a + 1...}. ∀f:ℤ ⟶ 𝔹.
  ∃x:{a..b-} [((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))] 
  supposing ∃x:{a..b-} [((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))]

Definition: binary-search
binary-search(f;a;b)
==r if b=a + 1 then a else eval c = a + ((b - a) ÷ 2) in if f c then binary-search(f;a;c) else binary-search(f;c;b) fi 

Lemma: binary-search_wf
∀a:ℤ. ∀b:{a + 1...}. ∀f:{a..b + 1-} ⟶ 𝔹.
  binary-search(f;a;b) ∈ {x:{a..b-}| (¬↑(f x)) ∧ (↑(f (x + 1)))}  
  supposing ↓∃x:{a..b-}. ((∀y:{a..x + 1-}. (¬↑(f y))) ∧ (∀z:{x + 1..b + 1-}. (↑(f z))))

Definition: find-xover
find-xover(f;m;n;step)
==r if f n then <n, m> else eval step' = 2 * step in eval k = n + step in   find-xover(f;n;k;step') fi 

Lemma: find-xover_wf
∀[x:ℤ]. ∀[n:{x...}]. ∀[step:ℕ+]. ∀[f:{x...} ⟶ 𝔹].
  find-xover(f;x;n;step) ∈ n':{n':ℤ| (n ≤ n') ∧ f n' = tt}  × {x':ℤ| 
                                  ((n' = n ∈ ℤ) ∧ (x' = x ∈ ℤ))
                                  ∨ (((n ≤ x') ∧ f x' = ff) ∧ ((n' = (n + step) ∈ ℤ) ∨ ((n + step) ≤ x')))}  
  supposing ∃m:{n...}. ∀k:{m...}. f k = tt

Definition: find-xover-val
find-xover-val(test;f;m;n;step) ==
  eval v = f n in
  if test v then <v, n, m> else eval step' = 2 * step in eval k = n + step in   find-xover-val(test;f;n;k;step') fi 

Lemma: find-xover-val_wf
∀[T:Type]
  ∀[test:T ⟶ 𝔹]. ∀[x:ℤ]. ∀[n:{x...}]. ∀[step:ℕ+]. ∀[f:{x...} ⟶ T].
    find-xover-val(test;f;x;n;step) ∈ v:T
    × n':{n':ℤ| (n ≤ n') ∧ (v = (f n') ∈ T) ∧ test v = tt} 
    × {x':ℤ| 
       ((n' = n ∈ ℤ) ∧ (x' = x ∈ ℤ)) ∨ (((n ≤ x') ∧ test (f x') = ff) ∧ ((n' = (n + step) ∈ ℤ) ∨ ((n + step) ≤ x')))}  
    supposing ∃m:{n...}. ∀k:{m...}. test (f k) = tt 
  supposing value-type(T)

Definition: exact-xover
exact-xover(f;n)==r let a,b = find-xover(f;n;n;1) in if b=a + 1 then a else exact-xover(f;a)

Lemma: exact-xover_wf
∀[n:ℤ]. ∀[f:{n...} ⟶ 𝔹].
  exact-xover(f;n) ∈ {x:ℤ| (n ≤ x) ∧ f x = ff ∧ f (x + 1) = tt}  
  supposing (∃m:{n...}. ((∀k:{n..m-}. f k = ff) ∧ (∀k:{m...}. f k = tt))) ∧ f n = ff

Definition: find-ge
find-ge(f;n) ==  fst(find-xover(f;n;n;1))

Lemma: find-ge_wf
∀[n:ℤ]. ∀[f:{n...} ⟶ 𝔹].  find-ge(f;n) ∈ {n':ℤ| (n ≤ n') ∧ f n' = tt}  supposing ∃m:{n...}. ∀k:{m...}. f k = tt

Definition: find-ge-val
find-ge-val(test;f;n) ==  let v,n,m = find-xover-val(test;f;n;n;1) in <v, n>

Lemma: find-ge-val_wf
∀[T:Type]
  ∀[test:T ⟶ 𝔹]. ∀[n:ℤ]. ∀[f:{n...} ⟶ T].
    find-ge-val(test;f;n) ∈ v:T × {n':ℤ| (n ≤ n') ∧ (v = (f n') ∈ T) ∧ test v = tt}  
    supposing ∃m:{n...}. ∀k:{m...}. test (f k) = tt 
  supposing value-type(T)

Definition: mu-ge
mu-ge(f;n)==r if f n then n else eval m = n + 1 in mu-ge(f;m) fi 

Lemma: mu-ge_wf2
∀[n:ℤ]. ∀[f:{n...} ⟶ (Top + Top)].  mu-ge(f;n) ∈ {n...} supposing ∃m:{n...}. (↑isl(f m))

Lemma: mu-ge_wf
∀[n:ℤ]. ∀[f:{n...} ⟶ 𝔹].  mu-ge(f;n) ∈ {n...} supposing ∃m:{n...}. (↑(f m))

Lemma: mu-ge-property
∀[n:ℤ]. ∀[f:{n...} ⟶ 𝔹].  {(↑(f mu-ge(f;n))) ∧ (∀[i:{n..mu-ge(f;n)-}]. (¬↑(f i)))} supposing ∃m:{n...}. (↑(f m))

Lemma: sq_stable__ex_int_upper_ap
∀n:ℤ. ∀f:{n...} ⟶ 𝔹.  SqStable(∃m:{n...}. (↑(f m)))

Lemma: mu-ge-property2
∀n:ℤ
  ∀[P:{n...} ⟶ ℙ]
    ∀d:∀n:{n...}. Dec(P[n]). {P[mu-ge(d;n)] ∧ (∀[i:{n..mu-ge(d;n)-}]. (¬P[i]))} supposing ∃m:{n...}. P[m]

Lemma: mu-ge-bound
∀[n,m:ℤ]. ∀[f:{n..m-} ⟶ 𝔹].  mu-ge(f;n) ∈ {n..m-} supposing ∃k:{n..m-}. (↑(f k))

Lemma: mu-ge-bound-property
∀n,m:ℤ. ∀f:{n..m-} ⟶ 𝔹.  ((∃m:{n..m-}. (↑(f m))) ⇒ {(↑(f mu-ge(f;n))) ∧ (∀[i:{n..mu-ge(f;n)-}]. (¬↑(f i)))})

Lemma: sq_stable__ex_int_seg_ap
∀n,m:ℤ. ∀f:{n..m-} ⟶ 𝔹.  SqStable(∃k:{n..m-}. (↑(f k)))

Lemma: sq_stable__ex_int_upper
∀n:ℤ. ∀[P:{n...} ⟶ ℙ]. ((∀m:{n...}. Dec(P[m])) ⇒ SqStable(∃m:{n...}. P[m]))

Lemma: sq_stable__ex_nat
∀[P:ℕ ⟶ ℙ]. ((∀m:ℕ. Dec(P[m])) ⇒ SqStable(∃m:ℕ. P[m]))

Lemma: sq_stable__ex_nat_plus
∀[P:ℕ+ ⟶ ℙ]. ((∀m:ℕ+. Dec(P[m])) ⇒ SqStable(∃m:ℕ+. P[m]))

Definition: mu
mu(f) ==  mu-ge(f;0)

Lemma: mu_wf
∀[f:ℕ ⟶ 𝔹]. mu(f) ∈ ℕ supposing ∃n:ℕ. (↑(f n))

Lemma: mu-wf2
∀[P:ℕ ⟶ ℙ]. ∀[d:∀n:ℕ. Dec(P[n])].  mu(d) ∈ ℕ supposing ∃n:ℕ. P[n]

Lemma: mu-unroll
∀[f:Top]. (mu(f) ~ if f 0 then 0 else mu(λi.(f (i + 1))) + 1 fi )

Lemma: mu-property
∀[f:ℕ ⟶ 𝔹]. {(↑(f mu(f))) ∧ (∀[i:ℕ]. ¬↑(f i) supposing i < mu(f))} supposing ∃n:ℕ. (↑(f n))

Lemma: mu-property2
∀[P:ℕ ⟶ ℙ]. ∀d:∀n:ℕ. Dec(P[n]). {P[mu(d)] ∧ (∀i:ℕ. ¬P[i] supposing i < mu(d))} supposing ∃n:ℕ. P[n]

Lemma: mu-bound
∀[b:ℕ]. ∀[f:ℕb ⟶ 𝔹].  mu(f) ∈ ℕb supposing ∃n:ℕb. (↑(f n))

Lemma: mu-bound-property
∀[b:ℕ]. ∀[f:ℕb ⟶ 𝔹].  {(↑(f mu(f))) ∧ (∀[i:ℕb]. ¬↑(f i) supposing i < mu(f))} supposing ∃n:ℕb. (↑(f n))

Lemma: mu-bound-property+
∀[b:ℕ]. ∀[f:ℕb ⟶ 𝔹].  {(mu(f) ∈ ℕb) ∧ (↑(f mu(f))) ∧ (∀[i:ℕb]. ¬↑(f i) supposing i < mu(f))} supposing ∃n:ℕb. (↑(f n))

Lemma: mu-bound-unique
∀[b:ℕ]. ∀[f:ℕb ⟶ 𝔹]. ∀[x:ℕb].  mu(f) = x ∈ ℤ supposing (↑(f x)) ∧ (∀y:ℕb. ((↑(f y)) ⇒ (y = x ∈ ℤ)))

Lemma: mu-unique
∀[f:ℕ ⟶ 𝔹]. ∀[x:ℕ].  mu(f) = x ∈ ℤ supposing (↑(f x)) ∧ (∀y:ℕx. (¬↑(f y)))

Definition: mu-dec
mu-dec(d;a) ==  mu(λk.isl(d a k))

Lemma: mu-dec_wf
∀[A:Type]. ∀[P:A ⟶ ℕ ⟶ ℙ]. ∀[d:a:A ⟶ k:ℕ ⟶ Dec(P[a;k])]. ∀[a:A].  mu-dec(d;a) ∈ ℕ supposing ↓∃k:ℕ. P[a;k]

Lemma: mu-dec-in-bar-nat
∀[A:Type]. ∀[P:A ⟶ ℕ ⟶ ℙ]. ∀[d:a:A ⟶ k:ℕ ⟶ Dec(P[a;k])]. ∀[a:A].  (mu-dec(d;a) ∈ partial(ℕ))

Lemma: mu-dec-property
∀[A:Type]. ∀[P:A ⟶ ℕ ⟶ ℙ].
  ∀d:a:A ⟶ k:ℕ ⟶ Dec(P[a;k]). ∀a:A.  ((↓∃k:ℕ. P[a;k]) ⇒ {P[a;mu-dec(d;a)] ∧ (∀i:ℕmu-dec(d;a). (¬P[a;i]))})

Lemma: qsquash_ex
∀P:ℕ ⟶ ℙ. ((∀n:ℕ. Dec(P[n])) ⇒ ⇃∃n:ℕ. P[n] ⇒ (∃n:ℕ. P[n]))

Definition: funinv
inv(f) ==  λx.mu(λn.(f n =z x))

Lemma: funinv_wf
∀[n,m:ℕ]. ∀[f:{f:ℕn ⟶ ℕm| Surj(ℕn;ℕm;f)} ].  (inv(f) ∈ {g:ℕm ⟶ ℕn| Inj(ℕm;ℕn;g) ∧ (∀x:ℕm. ((f (g x)) = x ∈ ℤ))} )

Lemma: funinv_wf2
∀[n:ℕ]. ∀[f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ].  (inv(f) ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} )

Lemma: funinv-property
∀[n:ℕ]. ∀[f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ]. ∀[x:ℕn].  (((f (inv(f) x)) = x ∈ ℤ) ∧ ((inv(f) (f x)) = x ∈ ℕn))

Lemma: funinv-compose
∀[n:ℕ]. ∀[f,g:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ].  (inv(f o g) = (inv(g) o inv(f)) ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} )

Lemma: funinv-funinv
∀[n:ℕ]. ∀[f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ].  (inv(inv(f)) = f ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} )

Lemma: funinv-unique
∀[n:ℕ]. ∀[f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ]. ∀[g:ℕn ⟶ ℕn].
  inv(f) = g ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  supposing (f o g) = (λx.x) ∈ (ℕn ⟶ ℕn)

Definition: sum_aux
sum_aux(k;v;i;x.f[x])==r if (i) < (k)  then eval v' = f[i] + v in eval i' = i + 1 in   sum_aux(k;v';i';x.f[x])  else v

Lemma: sum_aux_wf
∀[v,i,k:ℤ]. ∀[f:{i..k-} ⟶ ℤ].  sum_aux(k;v;i;x.f[x]) ∈ ℤ supposing i ≤ k

Lemma: sum_aux-as-primrec
∀[v,i,k:ℤ]. ∀[f:{i..k-} ⟶ ℤ].  sum_aux(k;v;i;x.f[x]) ~ primrec(k - i;v;λj,x. (x + f[i + j])) supposing i ≤ k

Definition: sum
Σ(f[x] | x < k) ==  sum_aux(k;0;0;x.f[x])

Lemma: sum_wf
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  (Σ(f[x] | x < n) ∈ ℤ)

Lemma: sum-as-primrec
∀[k:ℕ]. ∀[f:ℕk ⟶ ℤ].  (Σ(f[x] | x < k) ~ primrec(k;0;λj,x. (x + f[j])))

Lemma: sum1
∀[f:ℕ1 ⟶ ℤ]. (Σ(f[x] | x < 1) ~ f[0])

Lemma: sum-unroll-1
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  (Σ(f[x] | x < n) ~ if (n =z 0) then 0 else Σ(f[x] | x < n - 1) + f[n - 1] fi )

Lemma: sum-has-value
∀[n,f:Base].  {(n ∈ ℤ) ∧ (f ∈ ℕn ⟶ ℤ)} supposing (Σ(f[x] | x < n))↓

Lemma: sum-unroll
∀[n,f:Top].  (Σ(f[x] | x < n) ~ if (0) < (n)  then Σ(f[x] | x < n - 1) + f[n - 1]  else 0)

Lemma: non_neg_sum
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  0 ≤ Σ(f[x] | x < n) supposing ∀x:ℕn. (0 ≤ f[x])

Lemma: sum-nat
∀[n:ℕ]. ∀[f:ℕn ⟶ ℕ].  (Σ(f[x] | x < n) ∈ ℕ)

Lemma: sum_linear
∀[n:ℕ]. ∀[f,g:ℕn ⟶ ℤ].  ((Σ(f[x] | x < n) + Σ(g[x] | x < n)) = Σ(f[x] + g[x] | x < n) ∈ ℤ)

Lemma: sum_scalar_mult
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ]. ∀[a:ℤ].  ((a * Σ(f[x] | x < n)) = Σ(a * f[x] | x < n) ∈ ℤ)

Lemma: sum_constant
∀[n:ℕ]. ∀[a:ℤ].  (Σ(a | x < n) = (a * n) ∈ ℤ)

Lemma: sum_functionality
∀[n:ℕ]. ∀[f,g:ℕn ⟶ ℤ].  Σ(f[x] | x < n) = Σ(g[x] | x < n) ∈ ℤ supposing ∀i:ℕn. (f[i] = g[i] ∈ ℤ)

Lemma: sum-is-zero
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  Σ(f[x] | x < n) = 0 ∈ ℤ supposing ∀i:ℕn. (f[i] = 0 ∈ ℤ)

Lemma: sum_difference
∀[n:ℕ]. ∀[f,g:ℕn ⟶ ℤ]. ∀[d:ℤ].  Σ(f[x] | x < n) = (Σ(g[x] | x < n) + d) ∈ ℤ supposing Σ(f[x] - g[x] | x < n) = d ∈ ℤ

Lemma: sum_le
∀[k:ℕ]. ∀[f,g:ℕk ⟶ ℤ].  Σ(f[x] | x < k) ≤ Σ(g[x] | x < k) supposing ∀x:ℕk. (f[x] ≤ g[x])

Lemma: sum_bound
∀[k,b:ℕ]. ∀[f:ℕk ⟶ ℤ].  Σ(f[x] | x < k) ≤ (b * k) supposing ∀x:ℕk. (f[x] ≤ b)

Lemma: sum_lower_bound
∀[k,b:ℕ]. ∀[f:ℕk ⟶ ℤ].  (b * k) ≤ Σ(f[x] | x < k) supposing ∀x:ℕk. (b ≤ f[x])

Lemma: sum-ite
∀[k:ℕ]. ∀[f,g:ℕk ⟶ ℤ]. ∀[p:ℕk ⟶ 𝔹].
  (Σ(if p[i] then f[i] + g[i] else f[i] fi  | i < k) = (Σ(f[i] | i < k) + Σ(if p[i] then g[i] else 0 fi  | i < k)) ∈ ℤ)

Lemma: sum_arith1
∀[n:ℕ]. ∀[a,b:ℤ].  ((Σ(a + (b * i) | i < n) * 2) = (n * (a + a + (b * (n - 1)))) ∈ ℤ)

Lemma: sum_arith
∀[n:ℕ]. ∀[a,b:ℤ].  (Σ(a + (b * i) | i < n) = ((n * (a + a + (b * (n - 1)))) ÷ 2) ∈ ℤ)

Lemma: sum-partial-nat
∀[n:ℕ]. ∀[f:ℕn ⟶ partial(ℕ)].  (Σ(f[x] | x < n) ∈ partial(ℕ))

Lemma: sum-partial-has-value
∀[n:ℕ]. ∀[f:ℕn ⟶ partial(ℕ)].  ∀i:ℕn. (f[i])↓ supposing (Σ(f[x] | x < n))↓

Lemma: isolate_summand
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ]. ∀[m:ℕn].  (Σ(f[x] | x < n) = (f[m] + Σ(if (x =z m) then 0 else f[x] fi  | x < n)) ∈ ℤ)

Lemma: isolate_summand2
∀m:ℕ. ∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  Σ(f[x] | x < n) = (f[m] + Σ(if (x =z m) then 0 else f[x] fi  | x < n)) ∈ ℤ supposing m < n

Lemma: sum-nat-less
∀[n:ℕ]. ∀[f:ℕn ⟶ ℕ]. ∀[b:ℤ].  {∀x:ℕn. (f[x] ≤ (b - 1))} supposing Σ(f[x] | x < n) < b

Lemma: sum-nat-le
∀[n:ℕ]. ∀[f:ℕn ⟶ ℕ]. ∀[b:ℤ].  {∀x:ℕn. (f[x] ≤ b)} supposing Σ(f[x] | x < n) ≤ b

Lemma: sum-nat-le-simple
∀[n:ℕ]. ∀[f:ℕn ⟶ ℕ].  ∀x:ℕn. (f[x] ≤ Σ(f[x] | x < n))

Lemma: empty_support
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  Σ(f[x] | x < n) = 0 ∈ ℤ supposing ∀x:ℕn. (f[x] = 0 ∈ ℤ)

Lemma: singleton_support_sum
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ]. ∀[m:ℕn].  Σ(f[x] | x < n) = f[m] ∈ ℤ supposing ∀x:ℕn. ((¬(x = m ∈ ℤ)) ⇒ (f[x] = 0 ∈ ℤ))

Lemma: sum_split
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ]. ∀[m:ℕn + 1].  (Σ(f[x] | x < n) = (Σ(f[x] | x < m) + Σ(f[x + m] | x < n - m)) ∈ ℤ)

Lemma: sum_split+
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ]. ∀[m:ℕn + 1].
  ((Σ(f[x] | x < n) = (Σ(f[x] | x < m) + Σ(f[x + m] | x < n - m)) ∈ ℤ)
  ∧ (Σ(f[x] | x < m) ∈ ℤ)
  ∧ (Σ(f[x + m] | x < n - m) ∈ ℤ))

Lemma: sum_split_first
∀[n:ℕ+]. ∀[f:ℕn ⟶ ℤ].  (Σ(f[x] | x < n) = (f[0] + Σ(f[x + 1] | x < n - 1)) ∈ ℤ)

Lemma: sum_split1
∀[n:ℕ+]. ∀[f:ℕn ⟶ ℤ].  (Σ(f[x] | x < n) = (Σ(f[x] | x < n - 1) + f[n - 1]) ∈ ℤ)

Lemma: summand-le-sum
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  ∀[i:ℕn]. (f[i] ≤ Σ(f[x] | x < n)) supposing ∀x:ℕn. (0 ≤ f[x])

Lemma: sum_functionality_wrt_sqequal
∀[n:ℕ]. ∀[f,g:Base].  Σ(f[x] | x < n) ~ Σ(g[x] | x < n) supposing ∀i:ℕn. (f[i] ~ g[i])

Lemma: sum-of-consecutive-squares
∀[n:ℕ]. ((6 * Σ(i * i | i < n)) = ((n - 1) * n * ((2 * n) - 1)) ∈ ℤ)

Lemma: sum-consecutive-squares
∀[n:ℕ]. (Σ(i * i | i < n) = (((n - 1) * n * ((2 * n) - 1)) ÷ 6) ∈ ℤ)

Lemma: sum-of-consecutive-cubes
∀[n:ℕ]. ((4 * Σ((i * i) * i | i < n)) = (((n - 1) * (n - 1)) * n * n) ∈ ℤ)

Lemma: sum-consecutive-cubes
∀[n:ℕ]. (Σ((i * i) * i | i < n) = ((((n - 1) * (n - 1)) * n * n) ÷ 4) ∈ ℤ)

Lemma: absval_sum
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  (|Σ(f[x] | x < n)| ≤ Σ(|f[x]| | x < n))

Definition: int-prod
Π(f[x] | x < k) ==  primrec(k;1;λx,n. (n * f[x]))

Lemma: int-prod_wf
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].  (Π(f[x] | x < n) ∈ ℤ)

Lemma: int-prod_wf_nat
∀[n:ℕ]. ∀[f:ℕn ⟶ ℕ].  (Π(f[x] | x < n) ∈ ℕ)

Lemma: int-prod_wf_nat_plus
∀[n:ℕ]. ∀[f:ℕn ⟶ ℕ+].  (Π(f[x] | x < n) ∈ ℕ+)

Lemma: int-prod_wf_absval_1
∀[n:ℕ]. ∀[f:ℕn ⟶ {s:ℤ| |s| = 1 ∈ ℤ} ].  (Π(f[x] | x < n) ∈ {s:ℤ| |s| = 1 ∈ ℤ} )

Lemma: int_prod0_lemma
∀f:Top. (Π(f[x] | x < 0) ~ 1)

Lemma: int-prod-unroll-hi
∀[n:ℕ]. ∀[f:Top].  (Π(f[x] | x < n) ~ if (n =z 0) then 1 else Π(f[x] | x < n - 1) * f[n - 1] fi )

Lemma: int-prod-single
∀[f:Top]. (Π(f[x] | x < 1) ~ 1 * f[0])

Lemma: int-prod-split
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ]. ∀[m:ℕn + 1].  (Π(f[x] | x < n) = (Π(f[x] | x < m) * Π(f[x + m] | x < n - m)) ∈ ℤ)

Lemma: int-prod-split2
∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[f:ℕn ⟶ ℤ].  (Π(f[x] | x < n) = (Π(f[x] | x < m) * Π(f[x + m] | x < n - m)) ∈ ℤ)

Lemma: int-prod-isolate
∀[n:ℕ]. ∀[m:ℕn]. ∀[f:ℕn ⟶ ℤ].  (Π(f[x] | x < n) = (Π(if (x =z m) then 1 else f[x] fi  | x < n) * f[m]) ∈ ℤ)

Lemma: int-prod-1
∀[n:ℕ]. (Π(1 | x < n) = 1 ∈ ℤ)

Lemma: int-prod-factor
∀[n:ℕ]. ∀[f,g:ℕn ⟶ ℤ].  (Π(f[x] * g[x] | x < n) = (Π(f[x] | x < n) * Π(g[x] | x < n)) ∈ ℤ)

Lemma: mul-nat
∀[x,y:ℕ].  (x * y ∈ ℕ)

Definition: exp
i^n ==  primrec(n;1;λx,y. (i * y))

Lemma: exp_wf
∀[n:ℕ]. ∀[i:ℕ+].  (i^n ∈ ℕ+)

Lemma: exp_wf2
∀[n:ℕ]. ∀[i:ℤ].  (i^n ∈ ℤ)

Lemma: exp_wf3
∀[v:ℤ-o]. ∀[n:ℕ].  (v^n ∈ ℤ-o)

Lemma: exp_wf4
∀[n,v:ℕ].  (v^n ∈ ℕ)

Lemma: exp_wf_nat_plus
∀[n:ℕ]. ∀[v:ℕ+].  (v^n ∈ ℕ+)

Lemma: exp0_lemma
∀i:Top. (i^0 ~ 1)

Lemma: exp_add
∀[n,m:ℕ]. ∀[i:ℤ].  (i^(n + m) = (i^n * i^m) ∈ ℤ)

Lemma: exp1
∀[i:ℤ]. (i^1 = i ∈ ℤ)

Lemma: exp_step
∀[n:ℕ+]. ∀[i:ℤ].  (i^n ~ i * i^(n - 1))

Lemma: exp2
∀[i:ℤ]. (i^2 = (i * i) ∈ ℤ)

Lemma: exp-ge-1
∀[b:{2...}]. ∀[j:ℕ+].  1 < b^j

Lemma: exp-increasing
∀[b:{2...}]. ∀[i:ℕ].  ∀j:ℕ. b^i < b^j supposing i < j

Lemma: exp-nondecreasing
∀[b:{2...}]. ∀[i:ℕ].  ∀j:ℕ. b^i ≤ b^j supposing i ≤ j

Lemma: absval_div_nat
∀[n:ℕ+]. ∀[i:ℤ].  (|i| ÷ n ~ |i ÷ n|)

Lemma: absval_div_decreases
∀[n:{2...}]. ∀[i:ℤ-o].  |i ÷ n| < |i|

Lemma: div_is_zero
∀[n:{2...}]. ∀[i:ℤ].  i ÷ n ~ 0 supposing |i| < n

Lemma: div_absval_bound
∀[M:ℕ+]. ∀[z:ℤ]. ∀[n:ℕ].  |z ÷ M| ≤ n supposing |z| ≤ (n * M)

Lemma: absval-squeeze
∀[a,b,c,d:ℤ].  |b - c| ≤ (d - a) supposing ((a ≤ b) ∧ (b ≤ d)) ∧ (a ≤ c) ∧ (c ≤ d)

Lemma: biject-int-nat
∃f:ℤ ⟶ ℕ. Bij(ℤ;ℕ;f)

Definition: mccarthy91
mccarthy91(x) ==  if (100) < (x)  then x - 10  else eval y = x + 11 in eval z = mccarthy91(y) in   mccarthy91(z)

Lemma: mccarthy91_wf1
∀x:ℤ. (mccarthy91(x) ∈ {m:ℤ| m = if x ≤z 101 then 91 else x - 10 fi  ∈ ℤ} )

Lemma: mccarthy91_wf
∀x:ℤ. (mccarthy91(x) ∈ {91...})

Lemma: mccarthy91-sqeq
∀x:Top. (mccarthy91(x) ~ if (x) < (102)  then 91  else (x - 10))

Lemma: mccarthy91-eq-91
∀x:ℤ. (mccarthy91(x) = if (x) < (102)  then 91  else (x - 10) ∈ ℤ)

Definition: test-mutual-corec
test-mutual-corec() ==
  mutual-corec(X.λi.if (i =z 0) then Unit + (X 0 × ((X 1) List)) else Unit + (X 1 × ((X 0) List)) fi )

Lemma: test-mutual-corec_wf
test-mutual-corec() ∈ ℕ2 ⟶ Type

Lemma: test-mutual-corec-ext
test-mutual-corec() ≡ λi.if (i =z 0)
                         then Unit + (test-mutual-corec() 0 × ((test-mutual-corec() 1) List))
                         else Unit + (test-mutual-corec() 1 × ((test-mutual-corec() 0) List))
                         fi 

Definition: test-mutual-corec-size
test-mutual-corec-size(i;x) ==
  fix((λf,i,x. if (i =z 0)
              then case x of inl(_) => 0 | inr(p) => let a,L = p in 1 + (f 0 a) + Σ(f 1 L[i] | i < ||L||)
              else case x of inl(_) => 0 | inr(p) => let a,L = p in 1 + (f 1 a) + Σ(f 0 L[i] | i < ||L||)
              fi )) 
  i 
  x

Lemma: test-mutual-corec-size_wf
∀[i:ℕ2]. ∀[x:test-mutual-corec() i].  (test-mutual-corec-size(i;x) ∈ partial(ℕ))



Home Index