Lemma: add-is-int-iff
∀[a,b:Base]. uiff(a + b ∈ ℤ;(a ∈ ℤ) ∧ (b ∈ ℤ))
Lemma: multiply-is-int-iff
∀[a,b:Base]. uiff(a * b ∈ ℤ;(a ∈ ℤ) ∧ (b ∈ ℤ))
Lemma: minus-is-int-iff
∀[a:Base]. uiff(-a ∈ ℤ;a ∈ ℤ)
Lemma: subtract-is-int-iff
∀[a,b:Base]. uiff(a - b ∈ ℤ;(a ∈ ℤ) ∧ (b ∈ ℤ))
Lemma: exception-sqle-is-exception
∀[u,v,t:Base]. is-exception(t) supposing exception(u; v) ≤ t
Lemma: evalall-is-exception
∀[x,u,v:Base]. ((evalall(x) ~ exception(u; v)) ⇒ (↓(x ~ exception(u; v)) ∨ (x)↓))
Lemma: is-exception-evalall
∀[x:Base]. (is-exception(evalall(x)) ⇒ (↓is-exception(x) ∨ (x)↓))
Lemma: not-is-exception-bottom
¬is-exception(⊥)
Lemma: cbv-sqequal0
∀[a:Base]. eval x = a in 0 ~ 0 supposing (a)↓
Lemma: cbva-sqequal0
∀[a:Base]. let x ⟵ a in 0 ~ 0 supposing has-valueall(a)
Lemma: int-add-exception
∀[x:ℤ]. ∀[u,v:Top]. (x + (exception(u; v)) ~ exception(u; v))
Lemma: int-mul-exception
∀[x:ℤ]. ∀[u,v:Top]. (x * (exception(u; v)) ~ exception(u; v))
Lemma: int-div-exception
∀[x:ℤ]. ∀[u,v:Top]. (x ÷ exception(u; v) ~ exception(u; v))
Lemma: int-rem-exception
∀[x:ℤ]. ∀[u,v:Top]. (x rem exception(u; v) ~ exception(u; v))
Lemma: add-associates
∀[x,y,z:Top]. ((x + y) + z ~ x + y + z)
Lemma: add-commutes
∀[x:ℤ]. ∀[y:Top]. (x + y ~ y + x)
Lemma: add-inverse
∀[x:ℤ]. (x + (-x) ~ 0)
Lemma: add-inverse2
∀[x:ℤ]. ((-x) + x ~ 0)
Lemma: mul-commutes
∀[x:ℤ]. ∀[y:Top]. (x * y ~ y * x)
Lemma: zero-add
∀[x:ℤ]. (0 + x ~ x)
Lemma: zero-add-sqle
∀[x:Top]. (0 + x ≤ x)
Lemma: zero-add-sq
∀[x,y:Top]. (x + y ~ (x + 0) + y)
Lemma: one-mul
∀[x:ℤ]. (1 * x ~ x)
Lemma: add-zero
∀[x:ℤ]. (x + 0 ~ x)
Lemma: add-subtract-cancel
∀[x,y:ℤ]. ((x + y) - y ~ x)
Lemma: subtract-add-cancel
∀[x,y:ℤ]. ((x - y) + y ~ x)
Lemma: add-zero-base
∀[x:Base]. x + 0 ~ x supposing (x)↓ ⇒ (x ∈ ℤ)
Lemma: zero-add-base
∀[x:Base]. 0 + x ~ x supposing (x)↓ ⇒ (x ∈ ℤ)
Lemma: mul-one
∀[x:ℤ]. (x * 1 ~ x)
Lemma: mul-associates
∀[x,y,z:Top]. ((x * y) * z ~ x * y * z)
Lemma: mul-distributes
∀[x,y,z:Top]. (x * (y + z) ~ (x * y) + (x * z))
Lemma: mul-distributes-right
∀[x:ℤ]. ∀[y,z:Top]. ((y + z) * x ~ (y * x) + (z * x))
Lemma: mul-swap
∀[x:ℤ]. ∀[y,z:Top]. (x * y * z ~ y * x * z)
Lemma: add-swap
∀[x:ℤ]. ∀[y,z:Top]. (x + y + z ~ y + x + z)
Lemma: zero-mul
∀[x:ℤ]. (0 * x ~ 0)
Lemma: mul-zero
∀[x:ℤ]. (x * 0 ~ 0)
Lemma: add-inverse-unique
∀[x,y:ℤ]. (((x + y) = 0 ∈ ℤ) ⇒ (y = (-x) ∈ ℤ))
Lemma: minus-one-mul
∀[x:ℤ]. (-x ~ (-1) * x)
Lemma: minus-one-mul-top
∀[x:Top]. (-x ~ (-1) * x)
Lemma: minus-zero
-0 ~ 0
Lemma: mul-minus-1
∀x,y:Top. ((-x) * y ~ -(x * y))
Lemma: mul-minus-2
∀x,y:Top. (x * (-y) ~ -(x * y))
Lemma: minus-minus
∀[x:ℤ]. (--x ~ x)
Lemma: minus-minus-sq
∀x:Top. (--x ~ x + 0)
Lemma: mul-minus
∀x,y:Top. ((-x) * (-y) ~ x * y)
Lemma: two-mul
∀[x:Top]. (x + x ~ 2 * x)
Lemma: add-mul-special
∀[x:ℤ]. ∀[y:Top]. (x + (y * x) ~ (1 + y) * x)
Lemma: minus-add
∀[x,y:Top]. (-(x + y) ~ (-x) + (-y))
Lemma: le_wf
∀[i,j:ℤ]. (i ≤ j ∈ ℙ)
Lemma: istype-le
∀[i,j:ℤ]. istype(i ≤ j)
Lemma: istype-lt
∀[i,j:ℤ]. istype(i < j)
Lemma: le_witness_for_triv
∀[i,j:ℤ]. <λx.Ax, Ax, Ax> ∈ i ≤ j supposing i ≤ j
Lemma: le_witness
∀[i,j:ℤ]. ∀[x:i ≤ j]. (x = <λx.x, Ax, Ax> ∈ (i ≤ j))
Lemma: gt_wf
∀[i,j:ℤ]. (i > j ∈ ℙ)
Lemma: ge_wf
∀[i,j:ℤ]. (i ≥ j ∈ ℙ)
Lemma: not-lt
∀x,y:ℤ. uiff(¬x < y;y ≤ x)
Lemma: not-le
∀x,y:ℤ. uiff(¬(x ≤ y);y < x)
Lemma: not-ge
∀x,y:ℤ. uiff(¬(x ≥ y );y > x)
Lemma: not-gt
∀x,y:ℤ. uiff(¬(y > x);x ≥ y )
Lemma: less-iff-positive
∀[x,y:ℤ]. uiff(x < y;0 < y - x)
Lemma: le-iff-nonneg
∀[x,y:ℤ]. uiff(x ≤ y;0 ≤ (y - x))
Lemma: add-positive
∀[x,y:ℤ]. (0 < x + y) supposing (0 < x and 0 < y)
Lemma: add-positive-nonneg
∀[x,y:ℤ]. (0 < x + y) supposing (0 < x and (0 ≤ y))
Lemma: le_antisymmetry
∀[x,y:ℤ]. ((x ≤ y) ⇒ (y ≤ x) ⇒ (x = y ∈ ℤ))
Lemma: less_than_irreflexivity
∀[x:ℤ]. (x < x ⇒ False)
Lemma: less_than_anti-reflexive
∀[x:ℤ]. (¬x < x)
Lemma: less_than_transitivity
∀[x,y,z:ℤ]. (x < z) supposing (y < z and x < y)
Lemma: le-iff-less-or-equal
∀x,y:ℤ. uiff(x ≤ y;x < y ∨ (x = y ∈ ℤ))
Lemma: less_than_transitivity1
∀[x,y,z:ℤ]. (x < z) supposing ((y ≤ z) and x < y)
Lemma: less_than_transitivity2
∀[x,y,z:ℤ]. (x < z) supposing (y < z and (x ≤ y))
Lemma: add_functionality_wrt_le
∀[i1,i2,j1,j2:ℤ]. ((i1 + i2) ≤ (j1 + j2)) supposing ((i2 ≤ j2) and (i1 ≤ j1))
Lemma: add_functionality_wrt_lt
∀[i1,i2,j1,j2:ℤ]. (i1 + i2 < j1 + j2) supposing ((i2 ≤ j2) and i1 < j1)
Lemma: decidable__int_equal
∀i,j:ℤ. Dec(i = j ∈ ℤ)
Lemma: add-nonneg
∀x,y:ℤ. (0 ≤ (x + y)) supposing ((0 ≤ x) and (0 ≤ y))
Lemma: le_transitivity
∀[x,y,z:ℤ]. (x ≤ z) supposing ((y ≤ z) and (x ≤ y))
Lemma: le_weakening
∀a,b:ℤ. a ≤ b supposing a = b ∈ ℤ
Lemma: le_reflexive
∀a:ℤ. (a ≤ a)
Lemma: le_weakening2
∀a,b:ℤ. a ≤ b supposing a < b
Lemma: lt_transitivity_1
∀[i,j,k:ℤ]. (i < k) supposing ((j ≤ k) and i < j)
Lemma: lt_transitivity_2
∀[i,j,k:ℤ]. (i < k) supposing (j < k and (i ≤ j))
Lemma: le_antisymmetry_iff
∀[x,y:ℤ]. uiff(x = y ∈ ℤ;{(x ≤ y) ∧ (y ≤ x)})
Lemma: le_functionality
∀[a,b,c,d:ℤ]. ({a ≤ d supposing b ≤ c}) supposing ((c ≤ d) and (b ≥ a ))
Lemma: less_than_functionality
∀[a,b,c,d:ℤ]. ({a < d supposing b < c}) supposing ((c ≤ d) and (b ≥ a ))
Lemma: add_functionality_wrt_eq
∀[i1,i2,j1,j2:ℤ]. ((i1 + i2) = (j1 + j2) ∈ ℤ) supposing ((i2 = j2 ∈ ℤ) and (i1 = j1 ∈ ℤ))
Lemma: less-iff-le
∀x,y:ℤ. uiff(x < y;(1 + x) ≤ y)
Lemma: not-le-2
∀x,y:ℤ. uiff(¬(x ≤ y);(y + 1) ≤ x)
Lemma: not-lt-2
∀x,y:ℤ. uiff(¬x < y;y ≤ x)
Lemma: not-ge-2
∀x,y:ℤ. uiff(¬(x ≥ y );(x + 1) ≤ y)
Lemma: not-gt-2
∀x,y:ℤ. uiff(¬(y > x);y ≤ x)
Lemma: le-add-cancel
∀[c,t:ℤ]. uiff((c + t) ≤ t;c ≤ 0)
Lemma: le-add-cancel-alt
∀[c,t:ℤ]. uiff(t ≤ (c + t);0 ≤ c)
Lemma: le-add-cancel2
∀[c,d,t:ℤ]. uiff((c + t) ≤ (d + t);c ≤ d)
Lemma: le-add-cancel3
∀[c,d,t,t':ℤ]. uiff((c + t) ≤ (d + t');c ≤ d) supposing t = t' ∈ ℤ
Lemma: le-add-cancel4
∀[c,t,t':ℤ]. uiff((c + t) ≤ t';c ≤ 0) supposing t = t' ∈ ℤ
Lemma: le-add-shift
∀[x,y,z:ℤ]. uiff(x ≤ (y + z);((-y) + x) ≤ z)
Lemma: condition-implies-le
∀[a,b,c,d:ℤ]. (a ≤ b) supposing ((c ≤ d) and ((b - a) = (d - c) ∈ ℤ))
Lemma: not-equal-2
∀x,y:ℤ. uiff(¬(x = y ∈ ℤ);((1 + x) ≤ y) ∨ ((1 + y) ≤ x))
Lemma: minus-le
∀[n,x:ℤ]. uiff((-n) ≤ x;0 ≤ (x + n))
Lemma: subtract-is-less
∀[x,y:ℤ]. uiff(x - y < x;0 < y)
Lemma: nequal-le-implies
∀[x,y:ℤ]. ((x + 1) ≤ y) supposing ((x ≤ y) and y ≠ x)
Lemma: subtract-1-ge-0
∀z:ℤ. (0 < z ⇒ ((z - 1) ≥ 0 ))
Lemma: arith-example1
∀x,y,z:ℤ.
((((x - 1) ≤ y) ∧ (y ≤ (x + 1)))
⇒ (((x - 1) ≤ z) ∧ (z ≤ (x + 1)))
⇒ (((y - 1) ≤ z) ∧ (z ≤ (y + 1)))
⇒ (((x = y ∈ ℤ) ∨ (x = z ∈ ℤ)) ∨ (y = z ∈ ℤ)))
Lemma: arith-example2
∀f:ℤ ⟶ ℤ. ∀a,b:ℤ.
((a = b ∈ ℤ)
⇒ (∀x,y,z:ℤ.
(((f a) ≤ x)
⇒ (x ≤ (f b))
⇒ (((x - 1) ≤ y) ∧ (y ≤ ((f b) + 1)))
⇒ ((((f b) - 1) ≤ z) ∧ (z ≤ (x + 1)))
⇒ (((y - 1) ≤ z) ∧ (z ≤ (y + 1)))
⇒ (((x = y ∈ ℤ) ∨ (x = z ∈ ℤ)) ∨ (y = z ∈ ℤ)))))
Lemma: trivial-arith
(3 = 2 ∈ ℤ) ⇒ False
Lemma: test-arith
∀[x,y,z:ℤ]. (((y + 1) ≤ x) ⇒ ((z + 1) ≤ y) ⇒ ((x + (-1)) ≤ z) ⇒ False)
Lemma: test-nat-param
$n ~ $n
Lemma: test-int-cmp-normalize
∀[x,y,a,b:Top].
(if (a) < (b)
then <if (a) < (b) then 1 else 2, if (b) < (a) then 1 else 2, if b=a then 1 else 2>
else <if (a) < (b) then 1 else 2, if (b) < (a) then 1 else 2, if b=a then 1 else 2> ~ if (a) < (b)
then <1, 2, 2>
else <2
, if (b) < (a)
then 1
else 2
, if b=a
then 1
else 2>)
Definition: nat
ℕ == {i:ℤ| 0 ≤ i}
Lemma: nat_wf
ℕ ∈ Type
Lemma: istype-nat
istype(ℕ)
Lemma: nat_properties
∀[i:ℕ]. (i ≥ 0 )
Lemma: zero-le-nat
∀[i:ℕ]. (0 ≤ i)
Definition: nat_plus
ℕ+ == {i:ℤ| 0 < i}
Lemma: nat_plus_wf
ℕ+ ∈ Type
Lemma: nat_plus_properties
∀[i:ℕ+]. 0 < i
Lemma: nat_plus_subtype_nat
ℕ+ ⊆r ℕ
Lemma: mul_positive
∀a,b:ℤ. (0 < a ⇒ 0 < b ⇒ 0 < a * b)
Lemma: mul_preserves_le
∀[a,b:ℤ]. ∀[n:ℕ]. (n * a) ≤ (n * b) supposing a ≤ b
Lemma: mul_preserves_le2
∀[a,c:ℕ]. ∀[b,d:ℤ]. ((a * c) ≤ (b * d)) supposing ((a ≤ b) and (c ≤ d))
Lemma: mul_preserves_lt
∀[a,b:ℤ]. ∀[n:ℕ+]. n * a < n * b supposing a < b
Lemma: mul_positive_iff
∀a,b:ℤ. (0 < a * b ⇐⇒ (0 < a ∧ 0 < b) ∨ (a < 0 ∧ b < 0))
Lemma: omega-shadow
∀a,b:ℕ+. ∀c,d,x:ℤ. ((c ≤ (a * x)) ⇒ ((b * x) ≤ d) ⇒ ((b * c) ≤ (a * d)))
Lemma: not-equal-implies-less
∀[T:Type]. ∀x,y:T. ((¬(x = y ∈ T)) ⇒ (x < y ∨ y < x)) supposing T ⊆r ℤ
Lemma: not-less-implies-equal
∀x,y:ℤ. (x = y ∈ ℤ) supposing ((¬x < y) and (¬y < x))
Definition: int_nzero
ℤ-o == {i:ℤ| i ≠ 0}
Lemma: int_nzero_wf
ℤ-o ∈ Type
Lemma: int_nzero_properties
∀[i:ℤ-o]. i ≠ 0
Definition: int_lower
{...i} == {j:ℤ| j ≤ i}
Lemma: int_lower_wf
∀[i:ℤ]. ({...i} ∈ Type)
Lemma: int_lower_properties
∀[i:ℤ]. ∀[j:{...i}]. (j ≤ i)
Definition: lelt
i ≤ j < k == (i ≤ j) ∧ j < k
Lemma: divrem_wf
∀[a:ℤ]. ∀[n:ℤ-o]. (divrem(a; n) ∈ ℤ × ℤ)
Lemma: divrem-sq
∀[a:ℤ]. ∀[n:ℤ-o]. (divrem(a; n) ~ <a ÷ n, a rem n>)
Lemma: remainder_wfa
∀[a:ℤ]. ∀[n:ℤ-o]. (a rem n ∈ ℤ)
Lemma: divide_wfa
∀[a:ℤ]. ∀[n:ℤ-o]. (a ÷ n ∈ ℤ)
Definition: int_seg
{i..j-} == {k:ℤ| i ≤ k < j}
Lemma: int_seg_wf
∀[m,n:ℤ]. ({m..n-} ∈ Type)
Lemma: member-int_seg
∀[i,j,x:ℤ]. (x ∈ {i..j-}) supposing ((i ≤ x) and x < j)
Lemma: int_seg_equality
∀[m,n:ℤ]. ∀[x:{m..n-}]. ∀y:ℤ. x = y ∈ {m..n-} supposing x = y ∈ ℤ
Lemma: int_seg_subtype_special
∀[n,m:ℤ]. ({n + 1..m-} ⊆r {n..m-})
Lemma: int_seg_cases
∀[m,n:ℤ]. ∀[x:{m..n-}]. x ∈ {m + 1..n-} supposing ¬(x = m ∈ ℤ)
Lemma: decidable__equal-int_seg
∀[a,b:ℤ]. ∀x,y:{a..b-}. Dec(x = y ∈ {a..b-})
Definition: int_upper
{i...} == {j:ℤ| i ≤ j}
Lemma: int_upper_wf
∀[n:ℤ]. ({n...} ∈ Type)
Lemma: istype-int_upper
∀[n:ℤ]. istype({n...})
Lemma: int_upper_subtype_nat
∀[n:ℕ]. ({n...} ⊆r ℕ)
Lemma: int_upper_subtype_int_upper
∀[n,m:ℤ]. {n...} ⊆r {m...} supposing m ≤ n
Lemma: comb_for_int_upper_wf
λn,z. {n...} ∈ n:ℤ ⟶ (↓True) ⟶ 𝕌1
Lemma: int_upper_properties
∀[i:ℤ]. ∀[j:{i...}]. (i ≤ j)
Lemma: int_seg_subtype_nat_plus
∀[a,b:ℤ]. {a..b-} ⊆r ℕ+ supposing 1 ≤ a
Lemma: int_seg_subtype_nat
∀[a,b:ℤ]. {a..b-} ⊆r ℕ supposing 0 ≤ a
Lemma: retraction-nat-nsub
∀k:ℕ+. ∃r:ℕ ⟶ ℕk. ∀x:ℕk. ((r x) = x ∈ ℕk)
Lemma: div_rem_sum
∀[a:ℤ]. ∀[n:ℤ-o]. (a = (((a ÷ n) * n) + (a rem n)) ∈ ℤ)
Lemma: rem-zero
∀[n:ℤ-o]. ((0 rem n) = 0 ∈ ℤ)
Comment: quadrants_com
Quadrants for a rem b and a ÷ b are
numbered as follows:
# a b
1 + +
2 - +
3 - -
4 + -
Lemma: rem_bounds_1
∀[a:ℕ]. ∀[n:ℕ+]. ((0 ≤ (a rem n)) ∧ a rem n < n)
Lemma: rem_bounds_2
∀[a:{...0}]. ∀[n:ℕ+]. ((0 ≥ (a rem n) ) ∧ ((a rem n) > (-n)))
Lemma: rem_bounds_3
∀[a:{...0}]. ∀[n:{...-1}]. ((0 ≥ (a rem n) ) ∧ ((a rem n) > n))
Lemma: rem_bounds_4
∀[a:ℕ]. ∀[n:{...-1}]. ((0 ≤ (a rem n)) ∧ a rem n < -n)
Definition: absval
|i| == eval x = i in if (0) < (x) then x else (-x)
Lemma: absval_unfold
∀[x:ℤ]. (|x| ~ if (-1) < (x) then x else (-x))
Lemma: absval_unfold2
∀[x:ℤ]. (|x| ~ if (0) < (x) then x else (-x))
Lemma: absval_unfold3
∀[x:ℤ]. (|x| ~ if x <z 0 then -x else x fi )
Lemma: absval_wf
∀[x:ℤ]. (|x| ∈ ℕ)
Lemma: comb_for_absval_wf
λx,z. |x| ∈ x:ℤ ⟶ (↓True) ⟶ ℕ
Lemma: absval_pos
∀[i:ℕ]. (|i| = i ∈ ℤ)
Lemma: absval_neg
∀[i:{...0}]. (|i| = (-i) ∈ ℤ)
Lemma: absval-minus
∀[x:ℤ]. (|-x| = |x| ∈ ℤ)
Lemma: absval-positive
∀[x:ℤ]. uiff(0 < |x|;x ≠ 0)
Lemma: absval-non-neg
∀[x:ℤ]. (0 ≤ |x|)
Lemma: absval_zero
∀[i:ℤ]. uiff(|i| = 0 ∈ ℤ;i = 0 ∈ ℤ)
Lemma: absval_le_zero
∀[i:ℤ]. uiff(|i| ≤ 0;i = 0 ∈ ℤ)
Lemma: absval_ubound
∀[i:ℤ]. ∀[n:ℕ]. uiff(|i| ≤ n;((-n) ≤ i) ∧ (i ≤ n))
Lemma: absval_strict_ubound
∀[i:ℤ]. ∀[n:ℕ]. uiff(|i| < n;-n < i ∧ i < n)
Lemma: absval_lbound
∀i:ℤ. ∀n:ℕ. (|i| > n ⇐⇒ i < -n ∨ (i > n))
Lemma: absval_sym
∀[i:ℤ]. (|i| = |-i| ∈ ℤ)
Lemma: absval_elim
∀[P:ℤ ⟶ ℙ]. (∀x:ℤ. P[|x|] ⇐⇒ ∀x:ℕ. P[x])
Lemma: absval_cases
∀x:ℤ. ∀[y:ℕ]. uiff(|x| = y ∈ ℤ;(x = y ∈ ℤ) ∨ (x = (-y) ∈ ℤ))
Lemma: mul_preserves_eq
∀[a,b,n:ℤ]. (n * a) = (n * b) ∈ ℤ supposing a = b ∈ ℤ
Lemma: absval_mul
∀[x,y:ℤ]. (|x * y| = (|x| * |y|) ∈ ℤ)
Lemma: nat-mul-absval
∀[n:ℕ]. ∀[x:ℤ]. ((n * |x|) = |n * x| ∈ ℤ)
Lemma: rem-sign
∀[a:ℤ]. ∀[n:ℤ-o]. (((0 ≤ a) ⇒ (0 ≤ (a rem n))) ∧ (0 < a rem n ⇒ 0 < a) ∧ (a rem n < 0 ⇒ a < 0))
Lemma: rem_bounds_absval
∀b:ℤ-o. ∀a:ℤ. |a rem b| < |b|
Lemma: rem-1
∀a:ℤ. (a rem 1 ~ 0)
Lemma: rem-minus-1
∀a:ℤ. (a rem -1 ~ 0)
Lemma: rem_bounds_absval_le
∀b:ℤ-o. ∀a:ℤ. (|a rem b| ≤ |b|)
Lemma: div_bounds_1
∀[a:ℕ]. ∀[n:ℕ+]. (0 ≤ (a ÷ n))
Lemma: div_bounds_2
∀[a:{...-1}]. ∀[n:ℕ+]. ((a ÷ n) ≤ 0)
Lemma: div_bounds_3
∀[a:{...0}]. ∀[n:{...-1}]. (0 ≤ (a ÷ n))
Lemma: div_bounds_4
∀[a:{...0}]. ∀[n:{...-1}]. (0 ≤ (a ÷ n))
Lemma: rem_to_div
∀[a:ℤ]. ∀[n:ℤ-o]. ((a rem n) = (a - (a ÷ n) * n) ∈ ℤ)
Lemma: div_unique3
∀a:ℤ. ∀n:ℤ-o.
∀[p:ℤ]
uiff((a ÷ n) = p ∈ ℤ;∃r:ℤ
(|r| < |n|
∧ (a = ((p * n) + r) ∈ ℤ)
∧ ((0 ≤ a) ⇒ (0 ≤ r))
∧ (0 < r ⇒ 0 < a)
∧ (r < 0 ⇒ a < 0)))
Lemma: div-cancel-1
∀a:ℤ. ∀b:ℤ-o. (((a * b) ÷ b) = a ∈ ℤ)
Lemma: div-positive-1
∀n:ℕ+. ∀i:ℕ+n + 1. 0 < n ÷ i
Lemma: quotient-is-zero
∀[a,n:ℕ]. (a ÷ n) = 0 ∈ ℤ supposing a < n
Lemma: zero-div-rem
∀[x:ℤ-o]. ((0 ÷ x ~ 0) ∧ (0 rem x ~ 0))
Lemma: div_2_to_1
∀[a:{...0}]. ∀[b:ℕ+]. ((a ÷ b) = (-((-a) ÷ b)) ∈ ℤ)
Lemma: div_3_to_1
∀[a:{...0}]. ∀[b:{...-1}]. ((a ÷ b) = ((-a) ÷ -b) ∈ ℤ)
Lemma: div_4_to_1
∀[a:ℕ]. ∀[b:{...-1}]. ((a ÷ b) = (-(a ÷ -b)) ∈ ℤ)
Lemma: div_anti_sym
∀[a:ℤ]. ∀[b:ℤ-o]. ((a ÷ -b) = (-(a ÷ b)) ∈ ℤ)
Lemma: div_anti_sym2
∀[a:ℤ]. ∀[b:ℤ-o]. (((-a) ÷ b) = (-(a ÷ b)) ∈ ℤ)
Lemma: div_minus
∀[a:ℤ]. ∀[b:ℤ-o]. (((-a) ÷ -b) = (a ÷ b) ∈ ℤ)
Lemma: rem_2_to_1
∀[a:{...0}]. ∀[n:ℕ+]. ((a rem n) = (-(-a rem n)) ∈ ℤ)
Lemma: rem_3_to_1
∀[a:{...0}]. ∀[n:{...-1}]. ((a rem n) = (-(-a rem -n)) ∈ ℤ)
Lemma: rem_sym
∀[a:ℤ]. ∀[b:ℤ-o]. ((a rem -b) = (a rem b) ∈ ℤ)
Lemma: rem_antisym
∀[a:ℤ]. ∀[b:ℤ-o]. ((-a rem b) = (-(a rem b)) ∈ ℤ)
Lemma: rem_bounds_z
∀[a:ℤ]. ∀[b:ℤ-o]. |a rem b| < |b|
Definition: gcd
gcd(a;b) == fix((λgcd,a,b. if (b =z 0) then a else gcd b (a rem b) fi )) a b
Lemma: gcd_wf
∀a,b:ℤ. (gcd(a;b) ∈ ℤ)
Lemma: comb_for_gcd_wf
λa,b,z. gcd(a;b) ∈ a:ℤ ⟶ b:ℤ ⟶ (↓True) ⟶ ℤ
Definition: better-gcd
better-gcd(a;b) == fix((λbetter-gcd,a,b. if (b =z 0) then a else eval r = a rem b in better-gcd b r fi )) a b
Lemma: better-gcd-gcd
∀[y,x:ℤ]. (better-gcd(x;y) ~ gcd(x;y))
Lemma: better-gcd_wf
∀[x,y:ℤ]. (better-gcd(x;y) ∈ ℤ)
Definition: modulus
a mod n == eval r = a rem n in if (r) < (0) then |n| + r else r
Lemma: modulus_wf
∀[a:ℤ]. ∀[n:ℤ-o]. (a mod n ∈ ℕ)
Lemma: modulus-is-rem
∀[a:ℕ]. ∀[n:ℤ-o]. (a mod n ~ a rem n)
Lemma: modulus_base
∀[m:ℕ+]. ∀[a:ℕm]. (a mod m ~ a)
Lemma: mod_bounds_1
∀[a:ℤ]. ∀[n:ℤ-o]. ((0 ≤ (a mod n)) ∧ a mod n < |n|)
Lemma: mod_bounds
∀[a:ℤ]. ∀[n:ℕ+]. ((0 ≤ (a mod n)) ∧ a mod n < n)
Definition: div_floor
a ÷↓ n ==
eval r = a rem n in
if (n) < (0) then if (r) < (1) then a ÷ n else ((a ÷ n) - 1) else if (r) < (0) then (a ÷ n) - 1 else (a ÷ n)
Lemma: div_floor_wf
∀[a:ℤ]. ∀[n:ℤ-o]. (a ÷↓ n ∈ ℤ)
Lemma: div_floor_bounds
∀[a:ℤ]. ∀[n:ℤ-o].
((((a ÷↓ n) * n) ≤ a) ∧ a < ((a ÷↓ n) + 1) * n supposing 0 < n
∧ ((a ÷↓ n) + 1) * n < a ∧ (a ≤ ((a ÷↓ n) * n)) supposing n < 0)
Lemma: div_floor_mod_sum
∀[a:ℤ]. ∀[n:ℕ+]. (a = (((a ÷↓ n) * n) + (a mod n)) ∈ ℤ)
Lemma: div_reduce_inequality
∀[a:ℤ]
((∀n:ℕ+. ∀x:ℤ. uiff(0 ≤ (a + (n * x));0 ≤ ((a ÷↓ n) + x)))
∧ (∀n:{...-1}. ∀x:ℤ. uiff(0 ≤ (a + (n * x));0 ≤ ((a ÷↓ (-n)) + ((-1) * x)))))
Definition: adjust_div
adjust_div(b;a) == if (0) < (b rem a) then (b ÷ a) + 1 else (b ÷ a)
Lemma: adjust_div_wf
∀[b:ℤ]. ∀[a:ℤ-o]. (adjust_div(b;a) ∈ ℤ)
Lemma: divide-le
∀[a:ℕ+]. ∀[b,x:ℤ]. uiff(b ≤ (a * x);adjust_div(b;a) ≤ x)
Lemma: divide-exact
∀[g:ℤ-o]. ∀[v:ℤ]. (((g * v) ÷ g) = v ∈ ℤ)
Lemma: trivial-cancel
∀[g:ℤ-o]. ∀[v:ℤ]. uiff((g * v) = 0 ∈ ℤ;v = 0 ∈ ℤ)
Lemma: rem-exact
∀[g:ℤ-o]. ∀[v:ℤ]. ((g * v rem g) = 0 ∈ ℤ)
Lemma: mod2-cases
∀x:ℤ. (((x mod 2) = 0 ∈ ℤ) ∨ ((x mod 2) = 1 ∈ ℤ))
Lemma: mod2-add1
∀n:ℤ. (((n + 1) mod 2) = if (n mod 2 =z 0) then 1 else 0 fi ∈ ℤ)
Lemma: mod2-add2
∀n:ℤ. (((n + 2) mod 2) = (n mod 2) ∈ ℤ)
Lemma: mod2-add2n
∀k:ℤ. ∀n:ℕ. (((k + (2 * n)) mod 2) = (k mod 2) ∈ ℤ)
Lemma: mod2-2n
∀n:ℤ. (((2 * n) mod 2) = 0 ∈ ℤ)
Lemma: mod2-is-zero
∀x:ℤ. ((x mod 2) = 0 ∈ ℤ ⇐⇒ ∃n:ℤ. (x = (2 * n) ∈ ℤ))
Lemma: mod2-is-one
∀x:ℤ. ((x mod 2) = 1 ∈ ℤ ⇐⇒ ∃n:ℤ. (x = ((2 * n) + 1) ∈ ℤ))
Lemma: mod2-2n-plus-1
∀n:ℤ. ((((2 * n) + 1) mod 2) = 1 ∈ ℤ)
Lemma: singleton_int_seg
∀[a,b:ℤ]. ∀[x,y:{a..b-}]. x = y ∈ {a..b-} supposing b ≤ (a + 1)
Lemma: add-member-int_seg1
∀[k,m,n,x:ℤ]. uiff(k + x ∈ {m..n-};x ∈ {m - k..n - k-})
Lemma: add-member-int_seg2
∀[k,m,n,x:ℤ]. uiff(x + k ∈ {m..n-};x ∈ {m - k..n - k-})
Lemma: general_add_assoc
∀[a,b,c:Top]. (a + b + c ~ (a + b) + c)
Lemma: general_add_com
∀[a:ℤ]. ∀[b:Top]. (a + b ~ b + a)
Lemma: general_arith_equation1
∀[b:ℤ]. ∀[a,c:Top]. ((a - b) + c ~ (a + c) - b)
Lemma: general_arith_equation2
∀[b:ℤ]. ∀[a,c:Top]. ((a - b - c) + b ~ a - c)
Comment: add_nat_wf_com
It is a bad idea to make these usual wf
lemmas since often one mixes integer funs and
nat funs. (e.g. ∀n:ℕ. ∀i:{0...n}. ((-i) + n ∈ ℕ))
Sometime maybe should figure out systematic way of
dealing with ℕ,ℤ polymorphism
Lemma: add_nat_wf
∀[i,j:ℕ]. (i + j ∈ ℕ)
Lemma: subtract_nat_wf
∀[i,j:ℤ]. i - j ∈ ℕ supposing j ≤ i
Lemma: add_nat_plus
∀[i:ℕ]. ∀[j:ℕ+]. (i + j ∈ ℕ+)
Lemma: sq_stable__le
∀[i,j:ℤ]. SqStable(i ≤ j)
Lemma: stable__le
∀[i,j:ℤ]. Stable{i ≤ j}
Lemma: add_ident
∀[i:ℤ]. (i = (i + 0) ∈ ℤ)
Lemma: add_com
∀[a,b:ℤ]. ((a + b) = (b + a) ∈ ℤ)
Lemma: add_cancel_in_eq
∀[a,b,n:ℤ]. a = b ∈ ℤ supposing (a + n) = (b + n) ∈ ℤ
Lemma: add_cancel_in_lt
∀[a,b,n:ℤ]. a < b supposing a + n < b + n
Lemma: add_cancel_in_le
∀[a,b,n:ℤ]. a ≤ b supposing (a + n) ≤ (b + n)
Lemma: add_mono_wrt_eq
∀[a,b,n:ℤ]. uiff(a = b ∈ ℤ;(a + n) = (b + n) ∈ ℤ)
Lemma: add_mono_wrt_eq_rw
∀[a,b,n:ℤ]. {uiff(a = b ∈ ℤ;(a + n) = (b + n) ∈ ℤ)}
Lemma: add_mono_wrt_lt
∀[a,b,n:ℤ]. uiff(a < b;a + n < b + n)
Lemma: add_mono_wrt_lt_rw
∀[a,b,n:ℤ]. {uiff(a < b;a + n < b + n)}
Lemma: add_mono_wrt_le
∀[a,b,n:ℤ]. uiff(a ≤ b;(a + n) ≤ (b + n))
Lemma: add_mono_wrt_le_rw
∀[a,b,n:ℤ]. {uiff(a ≤ b;(a + n) ≤ (b + n))}
Lemma: minus_functionality_wrt_le
∀[i,j:ℤ]. (-i) ≤ (-j) supposing i ≥ j
Lemma: minus_mono_wrt_le
∀[i,j:ℤ]. uiff(i ≥ j ;(-i) ≤ (-j))
Lemma: minus_functionality_wrt_eq
∀[i,j:ℤ]. (-i) = (-j) ∈ ℤ supposing i = j ∈ ℤ
Lemma: minus_mono_wrt_eq
∀[i,j:ℤ]. uiff(i = j ∈ ℤ;(-i) = (-j) ∈ ℤ)
Lemma: minus_functionality_wrt_lt
∀[i,j:ℤ]. -i < -j supposing i > j
Lemma: minus_mono_wrt_lt
∀[i,j:ℤ]. uiff(i > j;-i < -j)
Lemma: sub_functionality_wrt_le
∀[i1,i2,j1,j2:ℤ]. ((i1 - i2) ≤ (j1 - j2)) supposing ((i2 ≥ j2 ) and (i1 ≤ j1))
Lemma: easy-member-int_seg
∀[i,j,a:ℤ]. (j - a ∈ {i..j-}) supposing (((i + a) ≤ j) and 0 < a)
Lemma: mul_cancel_in_eq
∀[a,b:ℤ]. ∀[n:ℤ-o]. a = b ∈ ℤ supposing (n * a) = (n * b) ∈ ℤ
Lemma: mul_cancel_in_lt
∀[a,b:ℤ]. ∀[n:ℕ+]. a < b supposing n * a < n * b
Lemma: mul_cancel_in_le
∀[a,b:ℤ]. ∀[n:ℕ+]. a ≤ b supposing (n * a) ≤ (n * b)
Lemma: int_entire
∀a,b:ℤ. (a = 0 ∈ ℤ) ∨ (b = 0 ∈ ℤ) supposing (a * b) = 0 ∈ ℤ
Lemma: int_entire_a
∀[a,b:ℤ]. (a * b ≠ 0) supposing (b ≠ 0 and a ≠ 0)
Lemma: mul_bounds_1a
∀[a,b:ℕ]. (0 ≤ (a * b))
Lemma: mul_bounds_1b
∀[a,b:ℕ+]. 0 < a * b
Lemma: multiply_nat_wf
∀[i,j:ℕ]. (i * j ∈ ℕ)
Lemma: multiply_nat_plus_iff
∀[i:ℕ+]. ∀[x:ℤ]. (i * x ∈ ℕ ⇐⇒ x ∈ ℕ)
Lemma: zero_ann
∀[i:ℤ]. (0 = (i * 0) ∈ ℤ)
Lemma: zero_ann_a
∀[a,b:ℤ]. (a * b) = 0 ∈ ℤ supposing (a = 0 ∈ ℤ) ∨ (b = 0 ∈ ℤ)
Lemma: zero_ann_b
∀[a,b:ℤ]. (¬(a = 0 ∈ ℤ)) ∧ (¬(b = 0 ∈ ℤ)) supposing ¬((a * b) = 0 ∈ ℤ)
Lemma: add-nat
∀[x,y:ℕ]. (x + y ∈ ℕ)
Lemma: assert_of_le_int
∀[x,y:ℤ]. uiff(↑x ≤z y;x ≤ y)
Definition: sequence
sequence(T) == k:ℕ × (ℕk ⟶ T)
Lemma: sequence_wf
∀[T:Type]. (sequence(T) ∈ Type)
Definition: seq-len
||s|| == fst(s)
Lemma: seq-len_wf
∀[T:Type]. ∀[s:sequence(T)]. (||s|| ∈ ℕ)
Definition: seq-item
s[i] == (snd(s)) i
Lemma: seq-item_wf
∀[T:Type]. ∀[s:sequence(T)]. ∀[i:ℕ||s||]. (s[i] ∈ T)
Definition: seq-comp
f o s == let k,g = s in <k, λi.(f (g i))>
Lemma: seq-comp_wf
∀[T:Type]. ∀[s:sequence(T)]. ∀[B:Type]. ∀[f:T ⟶ B]. (f o s ∈ sequence(B))
Lemma: seq-comp-item
∀[T:Type]. ∀[s:sequence(T)]. ∀[f,i:Top]. (f o s[i] ~ f s[i])
Lemma: seq-comp-len
∀[T:Type]. ∀[s:sequence(T)]. ∀[f:Top]. (||f o s|| ~ ||s||)
Definition: seq-truncate
seq-truncate(s;n) == let k,f = s in <n, f>
Lemma: seq-truncate_wf
∀[T:Type]. ∀[s:sequence(T)]. ∀[n:ℕ]. seq-truncate(s;n) ∈ sequence(T) supposing n ≤ ||s||
Lemma: seq-truncate-item
∀[T:Type]. ∀[s:sequence(T)]. ∀[n,i:Top]. (seq-truncate(s;n)[i] ~ s[i])
Lemma: seq-len-truncate
∀[T:Type]. ∀[s:sequence(T)]. ∀[n:Top]. (||seq-truncate(s;n)|| ~ n)
Lemma: seq-truncate-truncate
∀[T:Type]. ∀[s:sequence(T)]. ∀[n,m:Top]. (seq-truncate(seq-truncate(s;n);m) ~ seq-truncate(s;m))
Lemma: seq-comp-truncate
∀[T:Type]. ∀[s:sequence(T)]. ∀[f,n:Top]. (f o seq-truncate(s;n) ~ seq-truncate(f o s;n))
Definition: seq-cons
seq-cons(a;s) == let n,f = s in <n + 1, λi.if (i =z 0) then a else f (i - 1) fi >
Lemma: seq-cons_wf
∀[T:Type]. ∀[a:T]. ∀[s:sequence(T)]. (seq-cons(a;s) ∈ sequence(T))
Lemma: seq-cons-item
∀[T:Type]. ∀[a:Top]. ∀[s:sequence(T)]. ∀[i:Top]. (seq-cons(a;s)[i] ~ if (i =z 0) then a else s[i - 1] fi )
Lemma: seq-cons-len
∀[T:Type]. ∀[a:Top]. ∀[s:sequence(T)]. (||seq-cons(a;s)|| ~ ||s|| + 1)
Definition: seq-tl
seq-tl(s) == let n,f = s in <n - 1, λi.(f (i + 1))>
Lemma: seq-tl_wf
∀[T:Type]. ∀[s:sequence(T)]. seq-tl(s) ∈ sequence(T) supposing 0 < ||s||
Lemma: seq-tl-len
∀[T:Type]. ∀[s:sequence(T)]. ||seq-tl(s)|| ~ ||s|| - 1 supposing 0 < ||s||
Lemma: seq-tl-item
∀[T:Type]. ∀[s:sequence(T)]. ∀[i:Top]. (seq-tl(s)[i] ~ s[i + 1])
Definition: seq-nil
seq-nil() == <0, ⋅>
Lemma: seq-nil_wf
∀[T:Type]. (seq-nil() ∈ sequence(T))
Lemma: seq-nil-len
||seq-nil()|| ~ 0
Lemma: seq-settype
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[s:sequence(T)]. s ∈ sequence({x:T| P[x]} ) supposing ∀i:ℕ||s||. (↓P[s[i]])
Lemma: sequence_subtype
∀[A,B:Type]. sequence(A) ⊆r sequence(B) supposing A ⊆r B
Definition: seq-add
seq-add(s;x) == let n,f = s in <n + 1, λi.if i <z n then f i else x fi >
Lemma: seq-add_wf
∀[T:Type]. ∀[s:sequence(T)]. ∀[x:T]. (seq-add(s;x) ∈ sequence(T))
Lemma: seq-add-len
∀[T:Type]. ∀[s:sequence(T)]. ∀[x:Top]. (||seq-add(s;x)|| ~ ||s|| + 1)
Lemma: seq-add-item
∀[T:Type]. ∀[s:sequence(T)]. ∀[x,i:Top]. (seq-add(s;x)[i] ~ if i <z ||s|| then s[i] else x fi )
Definition: sorted-seq
sorted-seq(x,y.R[x; y];s) == ∀i,j:ℕ||s||. (i < j ⇒ R[s[i]; s[j]])
Lemma: sorted-seq_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[s:sequence(T)]. (sorted-seq(x,y.R[x;y];s) ∈ ℙ)
Home
Index