Lemma: nat-id-fun-example
∀n:ℕ. (∃m:ℕ [(m = n ∈ ℕ)])
Lemma: nat-id-fun-ext
∀n:ℕ. (∃m:ℕ [(m = n ∈ ℕ)])
Definition: sbcode
sbcode(m;n)==r if (m) < (n) then [0 / sbcode(m;n - m)] else if (n) < (m) then [1 / sbcode(m - n;n)] else []
Lemma: sbcode_wf
∀[m,n:ℕ+]. (sbcode(m;n) ∈ ℕ2 List)
Definition: sbcode_aux
sbcode_aux(L;m;n)
==r if (m) < (n)
then eval n' = n - m in
sbcode_aux([0 / L];m;n')
else if (n) < (m) then eval m' = m - n in sbcode_aux([1 / L];m';n) else L
Lemma: sbcode-mul
∀[m,n,k:ℕ+]. (sbcode(k * m;k * n) ~ sbcode(m;n))
Definition: sbdecode
sbdecode(L) == reduce(λx,p. let m,n = p in if x=0 then <m, m + n> else <m + n, n>;<1, 1>;L)
Lemma: sbdecode_wf
∀[L:ℕ2 List]. (sbdecode(L) ∈ ℕ+ × ℕ+)
Lemma: sbdecode-code
∀[m,n:ℕ+]. (sbdecode(sbcode(m;n)) ~ <m ÷ gcd(m;n), n ÷ gcd(m;n)>)
Lemma: sbcode-decode
∀[L:ℕ2 List]. (let m,n = sbdecode(L) in sbcode(m;n) ~ L)
Lemma: sbdecode_wf_gcd
∀[L:ℕ2 List]. (sbdecode(L) ∈ {p:ℕ+ × ℕ+| let m,n = p in gcd(m;n) = 1 ∈ ℤ} )
Lemma: sb-equipollent
ℕ2 List ~ {p:ℕ+ × ℕ+| let m,n = p in gcd(m;n) = 1 ∈ ℤ}
Definition: mtge1
mtge1(a;b;c;d) == (c ≤z a ∧b d <z b) ∨b(c <z a ∧b d ≤z b)
Lemma: mtge1_wf
∀[a,b,c,d:ℤ]. (mtge1(a;b;c;d) ∈ 𝔹)
Definition: sbhomout
sbhomout(a;b;c;d;L)
==r if L = Ax then sbcode(a + b;c + d) otherwise let h,t = L
in if mtge1(a;b;c;d)
then eval a' = a - c in
eval b' = b - d in
[1 / sbhomout(a';b';c;d;L)]
if mtge1(c;d;a;b)
then eval c' = c - a in
eval d' = d - b in
[0 / sbhomout(a;b;c';d';L)]
else let h,t = L
in if h=0
then eval a' = a + b in
eval c' = c + d in
sbhomout(a';b;c';d;t)
else eval b' = a + b in
eval d' = c + d in
sbhomout(a;b';c;d';t)
fi
Lemma: sbhomout_wf
∀[a,b,c,d:ℕ]. (0 < a + b ⇒ 0 < c + d ⇒ (∀[L:ℕ2 List]. (sbhomout(a;b;c;d;L) ∈ ℕ2 List)))
Lemma: sbhomout-correct
∀[a,b,c,d:ℕ].
(0 < a + b
⇒ 0 < c + d
⇒ (∀[L:ℕ2 List]
(sbhomout(a;b;c;d;L) = let m,n = sbdecode(L) in sbcode((a * m) + (b * n);(c * m) + (d * n)) ∈ (ℕ2 List))))
Lemma: test-sq-lift3
∀[x:Top]. (if (x) < (0) then 1 else (1 + 1) + 1 ~ if (x) < (0) then 2 else 3)
Lemma: coprime-equiv-unique
∀[p,q,a,b:ℤ].
({(p = a ∈ ℤ) ∧ (q = b ∈ ℤ)}) supposing
((q < 0 ⇐⇒ b < 0) and
(p < 0 ⇐⇒ a < 0) and
((p * b) = (a * q) ∈ ℤ) and
CoPrime(a,b) and
CoPrime(p,q))
Lemma: coprime-equiv-unique-pair
∀[p:ℤ]. ∀[q:ℤ-o]. ∀[a,b:ℤ].
(<p, q> = <a, b> ∈ (ℤ × ℤ-o)) supposing
((q < 0 ⇐⇒ b < 0) and
(p < 0 ⇐⇒ a < 0) and
((p * b) = (a * q) ∈ ℤ) and
CoPrime(a,b) and
CoPrime(p,q))
Definition: qeq
qeq(r;s) ==
let r' ⟵ r
in let s' ⟵ s
in if isint(r')
then if isint(s') then (r' =z s') else let i,j = s' in (r' * j =z i) fi
else let p,q = r'
in if isint(s') then (p =z s' * q) else let i,j = s' in (p * j =z i * q) fi
fi
Lemma: qeq_wf
∀[r,s:ℤ ⋃ (ℤ × ℤ-o)]. (qeq(r;s) ∈ 𝔹)
Lemma: qeq_refl
∀[r:ℤ ⋃ (ℤ × ℤ-o)]. qeq(r;r) = tt
Lemma: qeq-refl
Refl(ℤ ⋃ (ℤ × ℤ-o);r,s.qeq(r;s) = tt)
Lemma: qeq-sym
Sym(ℤ ⋃ (ℤ × ℤ-o);r,s.qeq(r;s) = tt)
Lemma: qeq-functionality
∀[r,s,x:ℤ ⋃ (ℤ × ℤ-o)]. qeq(r;x) = qeq(s;x) supposing qeq(r;s) = tt
Lemma: qeq-trans
Trans(ℤ ⋃ (ℤ × ℤ-o);r,s.qeq(r;s) = tt)
Lemma: qeq-equiv
EquivRel(ℤ ⋃ (ℤ × ℤ-o);r,s.qeq(r;s) = tt)
Definition: rationals
ℚ == r,s:ℤ ⋃ (ℤ × ℤ-o)//qeq(r;s) = tt
Lemma: rationals_wf
ℚ ∈ Type
Lemma: int-rational
∀[n:ℤ]. (n ∈ ℚ)
Lemma: int-subtype-rationals
ℤ ⊆r ℚ
Lemma: int_inc_rationals
ℤ ⊆r ℚ
Lemma: int_inc
ℤ ⊆r ℚ
Lemma: int_seg_inc
∀[i,j:ℤ]. ({i..j-} ⊆r ℚ)
Lemma: qeq-wf
∀[r,s:ℚ]. (qeq(r;s) ∈ 𝔹)
Lemma: int-equal-in-rationals
∀[x,y:ℤ]. uiff(x = y ∈ ℚ;x = y ∈ ℤ)
Lemma: rational-form-has-value
∀[r:ℤ ⋃ (ℤ × ℤ-o)]. has-valueall(r)
Lemma: rationals-valueall-type
valueall-type(ℚ)
Lemma: rationals-value-type
value-type(ℚ)
Lemma: rational-has-value
∀[r:ℚ]. has-valueall(r)
Lemma: rational-has-value2
∀[r:ℚ]. (r)↓
Definition: proportional-round
proportional-round(r;k;l) == let r' ⟵ r in if isint(r') then (r' * k) ÷ l else let p,q = r' in (p * k) ÷ q * l fi
Lemma: proportional-round_wf
∀[r:ℚ]. ∀[k:ℤ]. ∀[l:ℤ-o]. (proportional-round(r;k;l) ∈ ℤ)
Definition: rounded-numerator
rounded-numerator(r;k) == let r' ⟵ r in if isint(r') then r' * k else let p,q = r' in (p * k) ÷ q fi
Lemma: rounded-numerator_wf
∀[r:ℚ]. ∀[k:ℕ+]. (rounded-numerator(r;k) ∈ ℤ)
Definition: qadd
r + s ==
let r' ⟵ r
in let s' ⟵ s
in if isint(r')
then if isint(s') then r' + s' else let i,j = s' in <(r' * j) + i, j> fi
else let p,q = r'
in if isint(s') then <p + (s' * q), q> else let i,j = s' in <(p * j) + (i * q), q * j> fi
fi
Lemma: qadd_wf
∀[r,s:ℚ]. (r + s ∈ ℚ)
Lemma: qadd-add
∀[x,y:ℤ]. (x + y ~ x + y)
Definition: qmul
r * s ==
let r' ⟵ r
in let s' ⟵ s
in if isint(r')
then if isint(s') then r' * s' else let i,j = s' in <r' * i, j> fi
else let p,q = r'
in if isint(s') then <p * s', q> else let i,j = s' in <p * i, q * j> fi
fi
Lemma: qmul_wf
∀[r,s:ℚ]. (r * s ∈ ℚ)
Lemma: qmul-mul
∀[x,y:ℤ]. (x * y ~ x * y)
Lemma: qminus-minus
∀[x:ℤ]. (-(x) ~ -x)
Definition: mk-rational
mk-rational(a;b) == <a, b>
Lemma: mk-rational_wf
∀[a:ℤ]. ∀[b:ℤ-o]. (mk-rational(a;b) ∈ ℚ)
Definition: qround
qround(r;k) == mk-rational(rounded-numerator(r;2 * k);2 * k)
Lemma: qround_wf
∀[r:ℚ]. ∀[k:ℕ+]. (qround(r;k) ∈ ℚ)
Definition: qinv
1/r == let r' ⟵ r in if isint(r') then <1, r'> else let p,q = r' in <q, p> fi
Lemma: qinv-wf
∀[r:ℤ ⋃ (ℤ × ℤ-o)]. 1/r ∈ ℤ ⋃ (ℤ × ℤ-o) supposing ¬↑qeq(r;0)
Lemma: qinv_wf
∀[r:ℚ]. 1/r ∈ ℚ supposing ¬↑qeq(r;0)
Definition: qpositive
qpositive(r) ==
let r' ⟵ r
in if isint(r') then 0 <z r' else let p,q = r' in (0 <z p ∧b 0 <z q) ∨b(p <z 0 ∧b q <z 0) fi
Lemma: qpositive_wf
∀[r:ℚ]. (qpositive(r) ∈ 𝔹)
Definition: qrep
qrep(r) ==
let r' ⟵ r
in if isint(r')
then <r', 1>
else let p,q = r'
in let g,a,b = gcd_reduce(p;q) in
if 0 ≤z b then <a, b> else <-a, -b> fi
fi
Lemma: qrep_wf
∀[r:ℚ]. (qrep(r) ∈ ℤ × ℕ+)
Lemma: qrep-denom
∀[r:ℚ]. (qrep(r) ∈ ℤ × ℕ+)
Lemma: qeq_wf2
∀[r,s:ℚ]. (qeq(r;s) ∈ 𝔹)
Lemma: assert-qeq
∀[r,s:ℚ]. uiff(↑qeq(r;s);r = s ∈ ℚ)
Definition: qdeq
qdeq() == λa,b. qeq(a;b)
Lemma: qdeq_wf
qdeq() ∈ EqDecider(ℚ)
Lemma: int-eq-in-rationals
∀[x,y:ℤ]. uiff(x = y ∈ ℚ;x = y ∈ ℤ)
Definition: qdiv
(r/s) == r * 1/s
Lemma: qdiv_wf
∀[r,s:ℚ]. (r/s) ∈ ℚ supposing ¬(s = 0 ∈ ℚ)
Lemma: mk-rational-qdiv
∀[a,b:ℤ]. (mk-rational(a;b) ~ (a/b))
Lemma: qround-eq
∀[r:ℚ]. ∀[k:ℕ+]. (qround(r;k) = (rounded-numerator(r;2 * k)/2 * k) ∈ ℚ)
Definition: qsub
r - s == r + -(s)
Lemma: qsub_wf
∀[r,s:ℚ]. (r - s ∈ ℚ)
Lemma: qeq-qrep
∀[r:ℚ]. qeq(r;qrep(r)) = tt
Lemma: equals-qrep
∀[r:ℚ]. (qrep(r) = r ∈ ℚ)
Lemma: qpositive-elim
∀[r:ℚ]. (qpositive(r) ~ if isint(r) then 0 <z r else let p,q = r in (0 <z p ∧b 0 <z q) ∨b(p <z 0 ∧b q <z 0) fi )
Lemma: qinv-elim
∀[r:ℚ]. (1/r ~ if isint(r) then <1, r> else let p,q = r in <q, p> fi )
Lemma: qadd-elim
∀[r,s:ℚ].
(r + s ~ if isint(r)
then if isint(s) then r + s else let i,j = s in <(r * j) + i, j> fi
else let p,q = r
in if isint(s) then <p + (s * q), q> else let i,j = s in <(p * j) + (i * q), q * j> fi
fi )
Lemma: qmul-elim
∀[r,s:ℚ].
(r * s ~ if isint(r)
then if isint(s) then r * s else let i,j = s in <r * i, j> fi
else let p,q = r
in if isint(s) then <p * s, q> else let i,j = s in <p * i, q * j> fi
fi )
Lemma: qdiv-int-elim
∀[p:ℤ]. ∀[q:ℤ-o]. ((p/q) ~ <p, q>)
Lemma: qeq-elim
∀[r,s:ℚ].
(qeq(r;s) ~ if isint(r)
then if isint(s) then (r =z s) else let i,j = s in (r * j =z i) fi
else let p,q = r
in if isint(s) then (p =z s * q) else let i,j = s in (p * j =z i * q) fi
fi )
Lemma: q-elim
∀r:ℚ. ∃p:ℤ. ∃q:ℕ+. ((¬(q = 0 ∈ ℚ)) c∧ (r = (p/q) ∈ ℚ))
Lemma: better-q-elim
∀r:ℚ. ∃p:ℤ. ∃q:ℕ+. ((¬(q = 0 ∈ ℚ)) c∧ (r = (p/q) ∈ ℚ))
Lemma: qrep-coprime
∀[r:ℚ]. (|gcd(fst(qrep(r));snd(qrep(r)))| = 1 ∈ ℤ)
Definition: is-qrep
is-qrep(p) == let a,b = p in eval g = better-gcd(a;b) in (g =z 1) ∨b(g =z -1)
Lemma: is-qrep_wf
∀p:ℤ × ℕ+. (is-qrep(p) ∈ 𝔹)
Lemma: assert-is-qrep
∀p:ℤ × ℕ+. (↑is-qrep(p) ⇐⇒ ∃q:ℚ. (qrep(q) = p ∈ (ℤ × ℕ+)))
Lemma: equipollent-rationals
ℚ ~ {p:ℤ × ℕ+| ↑is-qrep(p)}
Lemma: equipollent-rationals-ext
ℚ ~ {p:ℤ × ℕ+| ↑is-qrep(p)}
Lemma: equipollent-nat-rationals
(our proof is constructive so we can compute the listing of rationals
see first-25-rationals)⋅
ℕ ~ ℚ
Lemma: equipollent-nat-rationals-ext
ℕ ~ ℚ
Definition: nth-rational
nth-rational(n) == (fst(TERMOF{equipollent-nat-rationals-ext:o, 1:l})) n
Lemma: nth-rational_wf
∀[n:ℕ]. (nth-rational(n) ∈ ℚ)
Lemma: first-25-rationals
map(λn.nth-rational(n);upto(25))
= [0;
-1;
1;
(-1/2);
-2;
(1/2);
(-1/3);
2;
(1/3);
(-1/4);
-3;
(-2/3);
(1/4);
(-1/5);
3;
(-3/2);
(2/3);
(1/5);
(-1/6);
-4;
(3/2);
(-2/5);
(1/6);
(-1/7);
4]
∈ (ℚ List)
Definition: q_le
q_le(r;s) == let r' ⟵ r in let s' ⟵ s in qpositive(s' - r') ∨bqeq(r';s')
Lemma: q_le_wf
∀[r,s:ℚ]. (q_le(r;s) ∈ 𝔹)
Lemma: q_le-elim
∀[r,s:ℚ]. (q_le(r;s) ~ qpositive(s + -(r)) ∨bqeq(r;s))
Lemma: qmul_ident
∀[r:ℚ]. ((1 * r) = r ∈ ℚ)
Lemma: qmul_com
∀[r,s:ℚ]. ((r * s) = (s * r) ∈ ℚ)
Lemma: qmul_assoc
∀[r,s,t:ℚ]. (((r * s) * t) = (r * s * t) ∈ ℚ)
Lemma: qmul_inv
∀[r:ℚ]. (r * 1/r) = 1 ∈ ℚ supposing ¬(r = 0 ∈ ℚ)
Lemma: qmul_inv_l
∀[r:ℚ]. (1/r * r) = 1 ∈ ℚ supposing ¬(r = 0 ∈ ℚ)
Lemma: qadd_ident
∀[r:ℚ]. ((0 + r) = r ∈ ℚ)
Lemma: qadd_com
∀[r,s:ℚ]. ((r + s) = (s + r) ∈ ℚ)
Lemma: qadd_assoc
∀[r,s,t:ℚ]. (((r + s) + t) = (r + s + t) ∈ ℚ)
Lemma: qadd_minus
∀[r:ℚ]. ((r + -(r)) = 0 ∈ ℚ)
Lemma: qmul_positive
∀[r,s:ℚ]. (↑qpositive(r * s)) supposing ((↑qpositive(s)) and (↑qpositive(r)))
Lemma: qadd_positive
∀[r,s:ℚ]. (↑qpositive(r + s)) supposing ((↑qpositive(s)) and (↑qpositive(r)))
Lemma: qminus_positive
∀[r:ℚ]. ¬↑qpositive(-(r)) supposing ↑qpositive(r)
Lemma: q_trichotomy
∀r:ℚ. ((↑qpositive(r)) ∨ (r = 0 ∈ ℚ) ∨ (↑qpositive(-(r))))
Lemma: q_distrib
∀[r,s,t:ℚ]. (((r + s) * t) = ((r * t) + (s * t)) ∈ ℚ)
Definition: qadd_grp
<ℚ+> == <ℚ, λx,y. qeq(x;y), λx,y. q_le(x;y), λx,y. (x + y), 0, λx.-(x)>
Lemma: qadd_grp_wf
<ℚ+> ∈ AbGrp
Lemma: mon_assoc_q
∀[a,b,c:ℚ]. ((a + b + c) = ((a + b) + c) ∈ ℚ)
Lemma: mon_ident_q
∀[a:ℚ]. (((a + 0) = a ∈ ℚ) ∧ ((0 + a) = a ∈ ℚ))
Lemma: qinverse_q
∀[a:ℚ]. (((a + -(a)) = 0 ∈ ℚ) ∧ ((-(a) + a) = 0 ∈ ℚ))
Lemma: qinv_thru_op_q
∀[a,b:ℚ]. (-(a + b) = (-(b) + -(a)) ∈ ℚ)
Lemma: qinv_inv_q
∀[a:ℚ]. (-(-(a)) = a ∈ ℚ)
Lemma: qinv_id_q
-(0) = 0 ∈ ℚ
Lemma: qinv_assoc_q
∀[a,b:ℚ]. (((a + -(a) + b) = b ∈ ℚ) ∧ ((-(a) + a + b) = b ∈ ℚ))
Lemma: qadd_inv_assoc_q
∀[a,b:ℚ]. (((a + -(a) + b) = b ∈ ℚ) ∧ ((-(a) + a + b) = b ∈ ℚ))
Lemma: qadd_comm_q
∀[a,b:ℚ]. ((a + b) = (b + a) ∈ ℚ)
Lemma: qadd_ac_1_q
∀[a,b,c:ℚ]. ((a + b + c) = (b + a + c) ∈ ℚ)
Lemma: qadd_grp_wf2
<ℚ+> ∈ OGrp
Definition: qless
r < s == r < s
Definition: qle
r ≤ s == r ≤ s
Lemma: qle_iff_lt_or_eq_qorder
∀a,b:ℚ. (a ≤ b ⇐⇒ a < b ∨ (a = b ∈ ℚ))
Lemma: qless_is_sp_of_leq_a_qorder
∀[a,b:ℚ]. uiff(a < b;(a ≤ b) ∧ (¬(b ≤ a)))
Lemma: qless_trans_qorder
∀[a,b,c:ℚ]. (a < c) supposing (b < c and a < b)
Lemma: qless_irreflexivity_qorder
∀[a:ℚ]. False supposing a < a
Lemma: qless_transitivity_2_qorder
∀[a,b,c:ℚ]. (a < c) supposing ((b ≤ c) and a < b)
Lemma: qless_transitivity_1_qorder
∀[a,b,c:ℚ]. (a < c) supposing (b < c and (a ≤ b))
Lemma: qle_weakening_eq_qorder
∀[a,b:ℚ]. a ≤ b supposing a = b ∈ ℚ
Lemma: qle_weakening_lt_qorder
∀[a,b:ℚ]. a ≤ b supposing a < b
Lemma: qle_transitivity_qorder
∀[a,b,c:ℚ]. (a ≤ c) supposing ((b ≤ c) and (a ≤ b))
Lemma: qle_antisymmetry_qorder
∀[a,b:ℚ]. (a = b ∈ ℚ) supposing ((b ≤ a) and (a ≤ b))
Lemma: qless_complement_qorder
∀[a,b:ℚ]. uiff(¬b < a;a ≤ b)
Lemma: qle_complement_qorder
∀[a,b:ℚ]. uiff(¬(a ≤ b);b < a)
Lemma: qless_trichot_qorder
∀a,b:ℚ. (a < b ∨ (a = b ∈ ℚ) ∨ b < a)
Lemma: grp_op_preserves_le_qorder
∀[x,y,z:ℚ]. (x + y) ≤ (x + z) supposing y ≤ z
Lemma: grp_op_preserves_lt_qorder
∀[u,v,w:ℚ]. u + v < u + w supposing v < w
Lemma: qless_irreflexivity
∀[a:ℚ]. False supposing a < a
Lemma: qle_antisymmetry
∀[a,b:ℚ]. (a = b ∈ ℚ) supposing ((b ≤ a) and (a ≤ b))
Definition: qmax
qmax(x;y) == if q_le(x;y) then y else x fi
Lemma: qmax_wf
∀[x,y:ℚ]. (qmax(x;y) ∈ ℚ)
Definition: qmax-list
qmax-list(L) == combine-list(x,y.qmax(x;y);L)
Lemma: qmax-list_wf
∀[L:ℚ List]. qmax-list(L) ∈ ℚ supposing 0 < ||L||
Lemma: qmax-list-member
∀L:ℚ List. (qmax-list(L) ∈ L) supposing 0 < ||L||
Definition: qmin
qmin(x;y) == if q_le(x;y) then x else y fi
Lemma: qmin_wf
∀[x,y:ℚ]. (qmin(x;y) ∈ ℚ)
Definition: qmin-list
qmin-list(L) == combine-list(x,y.qmin(x;y);L)
Lemma: qmin-list_wf
∀[L:ℚ List]. qmin-list(L) ∈ ℚ supposing 0 < ||L||
Lemma: qmin-list-member
∀L:ℚ List. (qmin-list(L) ∈ L) supposing 0 < ||L||
Definition: qrng
<ℚ+*> ==
<ℚ, λx,y. qeq(x;y), λx,y. q_le(x;y), λx,y. (x + y), 0, λx.-(x), λx,y. (x * y), 1, λx,y. if qeq(y;0) then inr ⋅ else i\000Cnl (x/y) fi >
Lemma: qrng_wf
<ℚ+*> ∈ CRng
Lemma: qmul_over_plus_qrng
∀[a,b,c:ℚ]. (((a * (b + c)) = ((a * b) + (a * c)) ∈ ℚ) ∧ (((b + c) * a) = ((b * a) + (c * a)) ∈ ℚ))
Lemma: qmul_over_minus_qrng
∀[a,b:ℚ]. (((-(a) * b) = -(a * b) ∈ ℚ) ∧ ((a * -(b)) = -(a * b) ∈ ℚ))
Lemma: qmul_zero_qrng
∀[a:ℚ]. (((0 * a) = 0 ∈ ℚ) ∧ ((a * 0) = 0 ∈ ℚ))
Lemma: qmul_assoc_qrng
∀[a,b,c:ℚ]. ((a * b * c) = ((a * b) * c) ∈ ℚ)
Lemma: qmul_one_qrng
∀[a:ℚ]. (((a * 1) = a ∈ ℚ) ∧ ((1 * a) = a ∈ ℚ))
Lemma: qmul_comm_qrng
∀[a,b:ℚ]. ((a * b) = (b * a) ∈ ℚ)
Lemma: qmul_ac_1_qrng
∀[a,b,c:ℚ]. ((a * b * c) = (b * a * c) ∈ ℚ)
Lemma: qdiv-self
∀[r:ℚ]. (r/r) = 1 ∈ ℚ supposing ¬(r = 0 ∈ ℚ)
Lemma: qmul-ident-div
∀[r,s:ℚ]. ((r/r) * s) = s ∈ ℚ supposing ¬(r = 0 ∈ ℚ)
Lemma: qmul-zero-div
∀[a:ℚ]. ∀[b:ℤ-o]. (((0/b) * a) = 0 ∈ ℚ)
Lemma: qmul-qdiv-cancel
∀[a,b:ℚ]. (a * (b/a)) = b ∈ ℚ supposing ¬(a = 0 ∈ ℚ)
Lemma: qmul-qdiv-cancel2
∀[a,b:ℚ]. ((b/a) * a) = b ∈ ℚ supposing ¬(a = 0 ∈ ℚ)
Lemma: qmul-qdiv-cancel3
∀[a,b,c:ℚ]. (a * (b/a) * c) = (b * c) ∈ ℚ supposing ¬(a = 0 ∈ ℚ)
Lemma: qmul-qdiv-cancel4
∀[a,b,c:ℚ]. ((b/a) * a * c) = (b * c) ∈ ℚ supposing ¬(a = 0 ∈ ℚ)
Lemma: qmul-preserves-eq
∀[a,b,c:ℚ]. uiff(a = b ∈ ℚ;(c * a) = (c * b) ∈ ℚ) supposing ¬(c = 0 ∈ ℚ)
Lemma: qmul-qdiv-cancel5
∀[a,b,c:ℚ]. ((a * (b/a * c)) = (b/c) ∈ ℚ) supposing ((¬(c = 0 ∈ ℚ)) and (¬(a = 0 ∈ ℚ)))
Lemma: qmul-qdiv-cancel6
∀[a,b,c:ℚ]. (((b/c * a) * a) = (b/c) ∈ ℚ) supposing ((¬(c = 0 ∈ ℚ)) and (¬(a = 0 ∈ ℚ)))
Lemma: qdiv-one
∀[q:ℚ]. ((q/1) = q ∈ ℚ)
Lemma: test-q-norm-conv
∀[a,b,c:ℚ]. (((a + b) * (c + b)) = (((a * c) + (b * c)) + (b * b) + (a * b)) ∈ ℚ)
Lemma: qmul-not-zero
∀[a,b:ℚ]. uiff(¬((a * b) = 0 ∈ ℚ);(¬(a = 0 ∈ ℚ)) ∧ (¬(b = 0 ∈ ℚ)))
Definition: qabs
|r| == let r' ⟵ r in if qpositive(r') then r' else -(r') fi
Lemma: qabs_wf
∀[r:ℚ]. (|r| ∈ ℚ)
Lemma: qabs-abs
∀[x:ℤ]. (|x| ~ |x|)
Lemma: qpositive-qabs
∀[r:ℚ]. ↑qpositive(|r|) supposing ¬(r = 0 ∈ ℚ)
Lemma: qabs-zero
∀[r:ℚ]. uiff(r = 0 ∈ ℚ;|r| = 0 ∈ ℚ)
Lemma: qabs-squared
∀[r:ℚ]. ((|r| * |r|) = (r * r) ∈ ℚ)
Lemma: qminus-qsub
∀[r,s:ℚ]. (-(s - r) = (r - s) ∈ ℚ)
Lemma: qsub-zero
∀[r:ℚ]. ((r - 0) = r ∈ ℚ)
Lemma: qsub-sub
∀[a,b:ℤ]. (a - b ~ a - b)
Lemma: qless_wf
∀[r,s:ℚ]. (r < s ∈ ℙ)
Lemma: qless_witness
∀[r,s:ℚ]. (r < s ⇒ (Ax ∈ r < s))
Lemma: qless_transitivity
∀[a,b,c:ℚ]. (a < c) supposing (b < c and a < b)
Lemma: qless-int
∀[x,y:ℤ]. uiff(x < y;x < y)
Lemma: qle_wf
∀[r,s:ℚ]. (r ≤ s ∈ ℙ)
Lemma: qle_witness
∀[r,s:ℚ]. ((r ≤ s) ⇒ (Ax ∈ r ≤ s))
Lemma: sq_stable_qle
∀[r,s:ℚ]. SqStable(r ≤ s)
Lemma: qle-int
∀[x,y:ℤ]. uiff(x ≤ y;x ≤ y)
Definition: qge
a ≥ b == b ≤ a
Lemma: qge_wf
∀[a,b:ℚ]. (a ≥ b ∈ ℙ)
Definition: qgt
a > b == b < a
Lemma: qgt_wf
∀[a,b:ℚ]. (a > b ∈ ℙ)
Lemma: qle-iff
∀a,b:ℚ. uiff(a ≤ b;a < b ∨ (a = b ∈ ℚ))
Lemma: decidable__equal_rationals
∀r,s:ℚ. Dec(r = s ∈ ℚ)
Lemma: assert-qpositive
∀[r:ℚ]. uiff(↑qpositive(r);0 < r)
Lemma: qadd_preserves_qless
∀[a,b,c:ℚ]. {uiff(a < b;c + a < c + b)}
Lemma: qmul-positive
∀a,b:ℚ. ((0 < a ∧ 0 < b) ∨ (0 < -(a) ∧ 0 < -(b)) ⇐⇒ 0 < a * b)
Lemma: qminus-positive
∀[r:ℚ]. uiff(0 < -(r);r < 0)
Lemma: qmax-imax
∀[x,y:ℤ]. (qmax(x;y) ~ imax(x;y))
Lemma: zero-qle-qabs
∀[r:ℚ]. (0 ≤ |r|)
Lemma: qabs-qle-zero
∀[r:ℚ]. uiff(|r| ≤ 0;r = 0 ∈ ℚ)
Lemma: qabs-of-nonneg
∀[q:ℚ]. |q| = q ∈ ℚ supposing 0 ≤ q
Lemma: qabs-of-positive
∀[q:ℚ]. |q| ~ q supposing 0 < q
Lemma: qabs-of-non-positive
∀[q:ℚ]. |q| ~ -(q) supposing q ≤ 0
Lemma: qabs-difference-zero
∀[r,s:ℚ]. uiff(|r - s| ≤ 0;r = s ∈ ℚ)
Lemma: qabs-positive
∀[r:ℚ]. 0 < |r| supposing ¬(r = 0 ∈ ℚ)
Lemma: qabs-positive-iff
∀[r:ℚ]. uiff(¬(r = 0 ∈ ℚ);0 < |r|)
Lemma: qabs-qmul
∀[r,s:ℚ]. (|r * s| = (|r| * |s|) ∈ ℚ)
Lemma: qabs-qminus
∀[r:ℚ]. (|r| = |-(r)| ∈ ℚ)
Lemma: qabs-qmul-case1
∀[r,s,a:ℚ]. (|(r * a) - s * a| = (|r - s| * |a|) ∈ ℚ)
Lemma: qabs-qmul-case2
∀[r,s,a:ℚ]. (|(a * r) - a * s| = (|r - s| * |a|) ∈ ℚ)
Lemma: decidable__qle
∀a,b:ℚ. Dec(a ≤ b)
Lemma: decidable__qless
∀a,b:ℚ. Dec(a < b)
Lemma: qless-witness
∀[a,b:ℚ]. ⋅ ∈ a < b supposing a < b
Lemma: qabs-neg
∀[r:ℚ]. (|-(r)| = |r| ∈ ℚ)
Lemma: rational_set_blt
∀[r,s:ℚ].
(r <b s ~ if isint(r)
then if isint(s) then r <z s else let i,j = s in if 0 <z j then j * r <z i else i <z j * r fi fi
else let p,q = r
in if isint(s)
then if 0 <z q then p <z q * s else q * s <z p fi
else let i,j = s
in if 0 <z q * j then j * p <z q * i else q * i <z j * p fi
fi
fi )
Definition: q_less
q_less(r;s) ==
if isint(r)
then if isint(s) then r <z s else let i,j = s in if 0 <z j then j * r <z i else i <z j * r fi fi
else let p,q = r
in if isint(s)
then if 0 <z q then p <z q * s else q * s <z p fi
else let i,j = s
in if 0 <z q * j then j * p <z q * i else q * i <z j * p fi
fi
fi
Lemma: q_less_wf
∀[a,b:ℚ]. (q_less(a;b) ∈ 𝔹)
Lemma: assert-q_less
∀[a,b:ℚ]. (↑q_less(a;b) ~ a < b)
Lemma: assert-q_less-eq
∀[a,b:ℚ]. ((↑q_less(a;b)) = a < b ∈ ℙ)
Lemma: assert-q_le
∀[a,b:ℚ]. (↑q_le(a;b) ~ a ≤ b)
Lemma: assert-q_le-eq
∀[a,b:ℚ]. ((↑q_le(a;b)) = (a ≤ b) ∈ ℙ)
Lemma: qmax_ub
∀a,b,c:ℚ. (a ≤ qmax(b;c) ⇐⇒ (a ≤ b) ∨ (a ≤ c))
Lemma: qmin_ub
∀[a,b,c:ℚ]. uiff(a ≤ qmin(b;c);(a ≤ b) ∧ (a ≤ c))
Lemma: qmax_strict_ub
∀a,b,c:ℚ. (a < qmax(b;c) ⇐⇒ a < b ∨ a < c)
Lemma: qmin_strict_ub
∀[a,b,c:ℚ]. uiff(a < qmin(b;c);a < b ∧ a < c)
Lemma: qmax_lb
∀[a,b,c:ℚ]. uiff(qmax(b;c) ≤ a;(b ≤ a) ∧ (c ≤ a))
Lemma: qmin_lb
∀a,b,c:ℚ. (qmin(b;c) ≤ a ⇐⇒ (b ≤ a) ∨ (c ≤ a))
Lemma: qmin-assoc
Assoc(ℚ;λx,y. qmin(x;y))
Lemma: qmax-assoc
∀[x,y,z:ℚ]. (qmax(qmax(x;y);z) = qmax(x;qmax(y;z)) ∈ ℚ)
Lemma: qmax_strict_lb
∀[a,b,c:ℚ]. uiff(qmax(b;c) < a;b < a ∧ c < a)
Lemma: qmin_strict_lb
∀a,b,c:ℚ. (qmin(b;c) < a ⇐⇒ b < a ∨ c < a)
Lemma: qmin-list-bounds
∀L:ℚ List
(0 < ||L||
⇒ (∀x:ℚ
((x ≤ qmin-list(L) ⇐⇒ (∀y∈L.x ≤ y))
∧ (qmin-list(L) ≤ x ⇐⇒ (∃y∈L. y ≤ x))
∧ (x < qmin-list(L) ⇐⇒ (∀y∈L.x < y))
∧ (qmin-list(L) < x ⇐⇒ (∃y∈L. y < x)))))
Lemma: qmax-list-bounds
∀L:ℚ List
(0 < ||L||
⇒ (∀x:ℚ
((qmax-list(L) ≤ x ⇐⇒ (∀y∈L.y ≤ x))
∧ (x ≤ qmax-list(L) ⇐⇒ (∃y∈L. x ≤ y))
∧ (qmax-list(L) < x ⇐⇒ (∀y∈L.y < x))
∧ (x < qmax-list(L) ⇐⇒ (∃y∈L. x < y)))))
Lemma: qmax-list-unique
∀[L:ℚ List]. ∀[a:ℚ]. uiff(qmax-list(L) = a ∈ ℚ;(∀b∈L.b ≤ a)) supposing (a ∈ L)
Lemma: qmin-list-unique
∀[L:ℚ List]. ∀[a:ℚ]. uiff(qmin-list(L) = a ∈ ℚ;(∀b∈L.a ≤ b)) supposing (a ∈ L)
Lemma: qmul-zero
∀a,b:ℚ. ((a * b) = 0 ∈ ℚ ⇐⇒ (a = 0 ∈ ℚ) ∨ (b = 0 ∈ ℚ))
Lemma: qmul-non-neg
∀a,b:ℚ. ((a = 0 ∈ ℚ) ∨ (b = 0 ∈ ℚ) ∨ (0 < a ∧ 0 < b) ∨ (0 < -(a) ∧ 0 < -(b)) ⇐⇒ 0 ≤ (a * b))
Lemma: non-neg-qmul
∀[a,b:ℚ]. (0 ≤ (a * b)) supposing ((0 ≤ b) and (0 ≤ a))
Lemma: q-square-non-neg
∀[q:ℚ]. (0 ≤ (q * q))
Lemma: q-square-positive
∀[q:ℚ]. 0 < q * q supposing ¬(q = 0 ∈ ℚ)
Lemma: qadd_preserves_qle
∀[a,b,c:ℚ]. {uiff(a ≤ b;(c + a) ≤ (c + b))}
Lemma: qadd_preserves_eq
∀[a,b,c:ℚ]. uiff(a = b ∈ ℚ;(c + a) = (c + b) ∈ ℚ)
Lemma: qmul_preserves_qless
∀[a,b,c:ℚ]. uiff(a < b;c * a < c * b) supposing 0 < c
Lemma: qmul_preserves_qle
∀[a,b,c:ℚ]. uiff(a ≤ b;(c * a) ≤ (c * b)) supposing 0 < c
Lemma: qmul_preserves_qle2
∀[a,b,c:ℚ]. ((c * a) ≤ (c * b)) supposing ((a ≤ b) and (0 ≤ c))
Lemma: qmul_reverses_qle
∀[a,b,c:ℚ]. uiff(a ≤ b;(c * b) ≤ (c * a)) supposing c < 0
Lemma: qmul_reverses_qless
∀[a,b,c:ℚ]. uiff(a < b;c * b < c * a) supposing c < 0
Lemma: qmul_reverses_qle2
∀[a,b,c:ℚ]. uiff(a ≤ b;(b * c) ≤ (a * c)) supposing c < 0
Lemma: test33
∀[a,b,c:ℚ]. (b * c < a * c) supposing (c < 0 and a < b)
Lemma: qadd_functionality_wrt_qle
∀[a,b,c,d:ℚ]. ((a + c) ≤ (b + d)) supposing ((c ≤ d) and (a ≤ b))
Lemma: qadd_functionality_wrt_qless
∀[a,b,c,d:ℚ]. (a + c < b + d) supposing ((c ≤ d) and a < b)
Lemma: qadd_functionality_wrt_qless_2
∀[a,b,c,d:ℚ]. (a + c < b + d) supposing (c < d and (a ≤ b))
Lemma: qadd_functionality_wrt_qless_3
∀[a,b,c,d:ℚ]. (a + c < b + d) supposing (c < d and a < b)
Lemma: qle_functionality_wrt_implies
∀[a,b,c,d:ℚ]. ({a ≤ d supposing b ≤ c}) supposing ((c ≤ d) and (b ≥ a))
Lemma: qless_functionality_wrt_implies_1
∀[a,b,c,d:ℚ]. ({a < d supposing b < c}) supposing ((c ≤ d) and (b ≥ a))
Lemma: qadd-qmax
∀[a,b,c:ℚ]. ((a + qmax(b;c)) = qmax(a + b;a + c) ∈ ℚ)
Lemma: qadd-qmin
∀[a,b,c:ℚ]. ((a + qmin(b;c)) = qmin(a + b;a + c) ∈ ℚ)
Lemma: qmul_functionality_wrt_qle
∀[a,b,c,d:ℚ]. ((a * c) ≤ (b * d)) supposing ((c ≤ d) and (a ≤ b) and (0 ≤ c) and (0 ≤ a))
Lemma: qmul_functionality_wrt_qless1
∀[a,b,c,d:ℚ]. (a * c < b * d) supposing (c < d and (a ≤ b) and (0 ≤ d) and 0 < a)
Lemma: qmul_functionality_wrt_qless2
∀[a,b,c,d:ℚ]. (a * c < b * d) supposing ((c ≤ d) and a < b and (0 ≤ b) and 0 < c)
Lemma: qmul-positive2
∀a,b:ℚ. ((0 < a ∧ 0 < b) ∨ (a < 0 ∧ b < 0) ⇐⇒ 0 < a * b)
Lemma: qmul-negative
∀a,b:ℚ. ((a < 0 ∧ 0 < b) ∨ (0 < a ∧ b < 0) ⇐⇒ a * b < 0)
Lemma: qmul-qdiv
∀[a,b,c,d:ℚ]. (((a/c) * (b/d)) = (a * b/c * d) ∈ ℚ) supposing ((¬(d = 0 ∈ ℚ)) and (¬(c = 0 ∈ ℚ)))
Lemma: qdiv-qminus
∀[x,y:ℚ]. (x/-(y)) = (-(x)/y) ∈ ℚ supposing ¬(y = 0 ∈ ℚ)
Lemma: qabs-qinv
∀[s:{s:ℚ| ¬(s = 0 ∈ ℚ)} ]. (|1/s| = 1/|s| ∈ ℚ)
Lemma: qabs-qdiv
∀[r:ℚ]. ∀[s:{s:ℚ| ¬(s = 0 ∈ ℚ)} ]. (|(r/s)| = (|r|/|s|) ∈ ℚ)
Lemma: qabs-nonneg
∀[r:ℚ]. (0 ≤ |r|)
Lemma: qless-minus
∀[a,b:ℚ]. uiff(a < b;-(b) < -(a))
Lemma: qle-minus
∀[a,b:ℚ]. uiff(a ≤ b;-(b) ≤ -(a))
Lemma: qle_connex
∀a,b:ℚ. ((a ≤ b) ∨ (b ≤ a))
Lemma: qmax-symmetry
∀[x,y:ℚ]. (qmax(x;y) = qmax(y;x) ∈ ℚ)
Lemma: qmin-symmetry
∀[x,y:ℚ]. (qmin(x;y) = qmin(y;x) ∈ ℚ)
Lemma: qmax-idempotent
∀[q:ℚ]. (qmax(q;q) = q ∈ ℚ)
Lemma: qmin-idempotent
∀[q:ℚ]. (qmin(q;q) = q ∈ ℚ)
Lemma: not-qle
∀[q,r:ℚ]. ((¬(q ≤ r)) ⇒ r < q)
Lemma: qmax-eq-iff
∀[q,r,s:ℚ]. uiff(qmax(q;r) = s ∈ ℚ;((r ≤ q) ⇒ (s = q ∈ ℚ)) ∧ ((q ≤ r) ⇒ (s = r ∈ ℚ)))
Lemma: qmax-eq-iff-cases
∀q,r,s:ℚ. uiff(qmax(q;r) = s ∈ ℚ;((r ≤ q) ∧ (s = q ∈ ℚ)) ∨ ((q ≤ r) ∧ (s = r ∈ ℚ)))
Lemma: qmax-eq-iff-1
∀[q,r:ℚ]. uiff(qmax(q;r) = q ∈ ℚ;r ≤ q)
Lemma: qmax-eq-iff-2
∀[q,r:ℚ]. uiff(qmax(q;r) = r ∈ ℚ;q ≤ r)
Lemma: qmin-eq-iff
∀[q,r,s:ℚ]. uiff(qmin(q;r) = s ∈ ℚ;((r ≤ q) ⇒ (s = r ∈ ℚ)) ∧ ((q ≤ r) ⇒ (s = q ∈ ℚ)))
Lemma: qmin-eq-iff-cases
∀q,r,s:ℚ. uiff(qmin(q;r) = s ∈ ℚ;((q ≤ r) ∧ (s = q ∈ ℚ)) ∨ ((r ≤ q) ∧ (s = r ∈ ℚ)))
Lemma: qmin-eq-iff-1
∀[q,r:ℚ]. uiff(qmin(q;r) = q ∈ ℚ;q ≤ r)
Lemma: qmin-eq-iff-2
∀[q,r:ℚ]. uiff(qmin(q;r) = r ∈ ℚ;r ≤ q)
Lemma: qabs-difference-symmetry
∀[x,y:ℚ]. (|x - y| = |y - x| ∈ ℚ)
Lemma: qabs-difference-qmax
∀[a,b,c,d:ℚ]. (|qmax(a;b) - qmax(c;d)| ≤ qmax(|a - c|;|b - d|))
Lemma: qabs-as-qmax
∀[q:ℚ]. (|q| = qmax(q;-(q)) ∈ ℚ)
Lemma: qle-qabs
∀[q:ℚ]. (q ≤ |q|)
Lemma: qabs-non-zero
∀[q:ℚ]. uiff(0 < |q|;¬(q = 0 ∈ ℚ))
Lemma: rounded-numerator-property
∀[k:ℕ+]. ∀[r:ℚ]. |(k * r) - rounded-numerator(r;k)| < 1
Lemma: proportional-round-property
∀[k,l:ℕ+]. ∀[r:ℚ]. |(k * r) - l * proportional-round(r;k;l)| < l
Lemma: qround-property
∀[k:ℕ+]. ∀[r:ℚ]. |r - qround(r;k)| < (1/2 * k)
Lemma: qmin-as-qmax
∀[x,y:ℚ]. (qmin(x;y) = -(qmax(-(x);-(y))) ∈ ℚ)
Lemma: qinv-positive
∀[v:ℚ]. 0 < (1/v) supposing 0 < v
Lemma: qinv-nonneg
∀[v:ℚ]. 0 ≤ (1/v) supposing 0 < v
Lemma: qinv-negative
∀[v:ℚ]. (1/v) < 0 supposing v < 0
Lemma: qneginv-positive
∀[v:ℚ]. 0 < (-1/v) supposing v < 0
Lemma: qinv-zero
∀[c:ℚ]. ¬(1/c = 0 ∈ ℚ) supposing ¬(c = 0 ∈ ℚ)
Lemma: qdiv-qdiv
∀[a,b,c:ℚ]. ((a/(b/c)) = (a * c/b) ∈ ℚ) supposing ((¬(c = 0 ∈ ℚ)) and (¬(b = 0 ∈ ℚ)))
Lemma: qdiv_functionality_wrt_qle
∀[a,b,c,d:ℚ]. ((a/c) ≤ (b/d)) supposing ((c ≥ d) and (a ≤ b) and 0 < d and (0 ≤ a))
Lemma: qdiv_functionality_wrt_qless
∀[a,b,c,d:ℚ]. ((a/c) < (b/d)) supposing ((c ≥ d) and a < b and 0 < d and (0 ≤ a))
Lemma: qdiv_functionality_wrt_qless2
∀[a,b,c,d:ℚ]. ((a/c) < (b/d)) supposing (d < c and (a ≤ b) and 0 < d and 0 < a)
Lemma: q-ineq-test
∀[a,b,c:ℚ]. (False) supposing (0 < c and ((b + ((1/3) * c)) ≤ a) and ((a + c + c) ≤ b))
Lemma: qadd-non-neg
∀[a,b:ℚ]. (0 ≤ (a + b)) supposing ((0 ≤ b) and (0 ≤ a))
Lemma: qdiv-non-neg
∀a,b:ℚ. (0 < b ∧ (0 ≤ a)) ∨ (b < 0 ∧ (a ≤ 0)) ⇐⇒ 0 ≤ (a/b) supposing ¬(b = 0 ∈ ℚ)
Lemma: qdiv-non-neg1
∀[a,b:ℚ]. 0 ≤ (a/b) supposing 0 < b ∧ (0 ≤ a)
Definition: qdist
qdist(r;s) == |r - s|
Lemma: qdist_wf
∀[r,s:ℚ]. (qdist(r;s) ∈ ℚ)
Definition: qbetween
a ≤ b ≤ c == (a ≤ b) ∧ (b ≤ c)
Lemma: qbetween_wf
∀[a,b,c:ℚ]. (a ≤ b ≤ c ∈ ℙ)
Definition: q-between
a < b < c == a < b ∧ b < c
Lemma: q-between_wf
∀[a,b,c:ℚ]. (a < b < c ∈ ℙ)
Lemma: q-between-overlap
∀a,b,c,d,q:ℚ.
(∃x,y:ℚ. (x < q < y ∧ (∀q':ℚ. a < q' < b ∧ c < q' < d supposing x < q' < y))) supposing (c < q < d and a < q < b)
Lemma: qle-normalize
∀[a,b:ℚ]. uiff(a ≤ b;0 ≤ (b - a))
Lemma: qle_reflexivity
∀[a:ℚ]. (a ≤ a)
Lemma: qbetween-qdist
∀[a,b,r,s:ℚ]. (qdist(a;b) ≤ (s - r)) supposing (r ≤ b ≤ s and r ≤ a ≤ s)
Definition: qavg
qavg(a;b) == (a + b/2)
Lemma: qavg_wf
∀[a,b:ℚ]. (qavg(a;b) ∈ ℚ)
Lemma: qavg-same
∀[a:ℚ]. (qavg(a;a) = a ∈ ℚ)
Lemma: qavg-eq-iff-1
∀[a,b:ℚ]. uiff(a = qavg(a;b) ∈ ℚ;a = b ∈ ℚ)
Lemma: qavg-eq-iff-2
∀[a,b:ℚ]. uiff(qavg(a;b) = a ∈ ℚ;a = b ∈ ℚ)
Lemma: qavg-eq-iff-3
∀[a,b:ℚ]. uiff(qavg(b;a) = a ∈ ℚ;a = b ∈ ℚ)
Lemma: qavg-eq-iff-4
∀[a,b:ℚ]. uiff(a = qavg(b;a) ∈ ℚ;a = b ∈ ℚ)
Lemma: qavg-eq-iff-5
∀[a,b,c:ℚ]. uiff(qavg(b;a) = qavg(a;c) ∈ ℚ;b = c ∈ ℚ)
Lemma: qavg-eq-iff-6
∀[a,b,c:ℚ]. uiff(qavg(a;b) = qavg(c;a) ∈ ℚ;b = c ∈ ℚ)
Lemma: qavg-eq-iff-7
∀[a,b,c:ℚ]. uiff(qavg(a;b) = qavg(a;c) ∈ ℚ;b = c ∈ ℚ)
Lemma: qavg-eq-iff-8
∀[a,b,c:ℚ]. uiff(qavg(b;a) = qavg(c;a) ∈ ℚ;b = c ∈ ℚ)
Lemma: qle-qavg-iff-1
∀[a,b:ℚ]. uiff(a ≤ qavg(a;b);a ≤ b)
Lemma: qless-qavg-iff-1
∀[a,b:ℚ]. uiff(a < qavg(a;b);a < b)
Lemma: qle-qavg-iff-4
∀[a,b:ℚ]. uiff(a ≤ qavg(b;a);a ≤ b)
Lemma: qle-qavg-iff-2
∀[a,b,c:ℚ]. uiff(qavg(a;b) ≤ qavg(a;c);b ≤ c)
Lemma: qle-qavg-iff-3
∀[a,b,c:ℚ]. uiff(qavg(b;a) ≤ qavg(c;a);b ≤ c)
Lemma: qle-qavg-iff-5
∀[a,b,c:ℚ]. uiff(qavg(b;a) ≤ qavg(a;c);b ≤ c)
Lemma: qle-qavg-iff-6
∀[a,b,c:ℚ]. uiff(qavg(a;b) ≤ qavg(c;a);b ≤ c)
Lemma: qavg-qle-iff-1
∀[a,b:ℚ]. uiff(qavg(a;b) ≤ b;a ≤ b)
Lemma: qavg-qless-iff-1
∀[a,b:ℚ]. uiff(qavg(a;b) < b;a < b)
Lemma: qavg-qle-iff-2
∀[a,b:ℚ]. uiff(qavg(b;a) ≤ b;a ≤ b)
Lemma: qavg-between
∀[a,b:ℚ]. a < qavg(a;b) < b supposing a < b
Lemma: qle-mk-rational
∀[a,c:ℤ]. ∀[b,d:ℕ+]. uiff(mk-rational(a;b) ≤ mk-rational(c;d);(a * d) ≤ (b * c))
Lemma: qless-mk-rational
∀[a,c:ℤ]. ∀[b,d:ℕ+]. uiff(mk-rational(a;b) < mk-rational(c;d);a * d < b * c)
Definition: rational-interval
ℚInterval == ℚ × ℚ
Lemma: rational-interval_wf
ℚInterval ∈ Type
Definition: rat-sub-interval
rat-sub-interval(I;J) == let a,b = I in let c,d = J in ((c ≤ a) ∧ (b ≤ d)) ∧ (c < d ⇒ a < b)
Lemma: rat-sub-interval_wf
∀[I,J:ℚInterval]. (rat-sub-interval(I;J) ∈ ℙ)
Definition: ri-deq
ri-deq() == product-deq(ℚ;ℚ;qdeq();qdeq())
Lemma: ri-deq_wf
ri-deq() ∈ EqDecider(ℚInterval)
Lemma: decidable__equal_rational-interval
∀I,J:ℚInterval. Dec(I = J ∈ ℚInterval)
Definition: rat-point-interval
[a] == <a, a>
Lemma: rat-point-interval_wf
∀[a:ℚ]. ([a] ∈ ℚInterval)
Definition: rat-interval-face
I ≤ J == let c,d = J in (I = [c] ∈ ℚInterval) ∨ (I = [d] ∈ ℚInterval) ∨ (I = J ∈ ℚInterval)
Lemma: rat-interval-face_wf
∀[I,J:ℚInterval]. (I ≤ J ∈ ℙ)
Lemma: decidable__rat-interval-face
∀I,J:ℚInterval. Dec(I ≤ J)
Lemma: rat-interval-face-self
∀I:ℚInterval. I ≤ I
Definition: inhabited-rat-interval
Inhabited(I) == let a,b = I in q_le(a;b)
Lemma: inhabited-rat-interval_wf
∀[I:ℚInterval]. (Inhabited(I) ∈ 𝔹)
Lemma: assert-inhabited-rat-interval
∀[I:ℚInterval]. uiff(↑Inhabited(I);(fst(I)) ≤ (snd(I)))
Lemma: inhabited-rat-point-interval
∀[a:ℚ]. (Inhabited([a]) ~ tt)
Definition: rat-interval-dimension
dim(I) == let a,b = I in if q_less(a;b) then 1 else 0 fi
Lemma: rat-interval-dimension_wf
∀[I:ℚInterval]. (dim(I) ∈ ℕ2)
Lemma: rat-interval-dimension-single
∀[a:ℚ]. (dim([a]) ~ 0)
Lemma: rat-interval-face-dimension
∀J:ℚInterval. ((↑Inhabited(J)) ⇒ (∀I:ℚInterval. (I ≤ J ⇒ ((I = J ∈ ℚInterval) ∨ (dim(I) = (dim(J) - 1) ∈ ℤ)))))
Definition: rat-interval-intersection
I ⋂ J == let a,b = I in let c,d = J in <qmax(a;c), qmin(b;d)>
Lemma: rat-interval-intersection_wf
∀[I,J:ℚInterval]. (I ⋂ J ∈ ℚInterval)
Lemma: rat-interval-intersection-symm
∀[I,J:ℚInterval]. (I ⋂ J = J ⋂ I ∈ ℚInterval)
Lemma: rat-interval-intersection-idemp
∀[I:ℚInterval]. (I ⋂ I = I ∈ ℚInterval)
Definition: rational-cube
ℚCube(k) == ℕk ⟶ ℚInterval
Lemma: rational-cube_wf
∀[k:ℕ]. (ℚCube(k) ∈ Type)
Definition: rat-sub-cube
rat-sub-cube(k;a;b) == ∀i:ℕk. rat-sub-interval(a i;b i)
Lemma: rat-sub-cube_wf
∀[k:ℕ]. ∀[a,b:ℚCube(k)]. (rat-sub-cube(k;a;b) ∈ ℙ)
Lemma: rat-sub-cube_transitivity
∀[k:ℕ]. ∀a,b,c:ℚCube(k). (rat-sub-cube(k;a;b) ⇒ rat-sub-cube(k;b;c) ⇒ rat-sub-cube(k;a;c))
Definition: rc-deq
rc-deq(k) == finite-fun-deq(k;ri-deq())
Lemma: rc-deq_wf
∀[k:ℕ]. (rc-deq(k) ∈ EqDecider(ℚCube(k)))
Lemma: decidable__equal_rc
∀k:ℕ. ∀x,y:ℚCube(k). Dec(x = y ∈ ℚCube(k))
Definition: rceq
rceq(k;a;b) == rc-deq(k) a b
Lemma: rceq_wf
∀[k:ℕ]. ∀[a,b:ℚCube(k)]. (rceq(k;a;b) ∈ 𝔹)
Lemma: assert-rceq
∀[k:ℕ]. ∀[a,b:ℚCube(k)]. uiff(↑rceq(k;a;b);a = b ∈ ℚCube(k))
Definition: rat-cube-face
c ≤ d == ∀i:ℕk. c i ≤ d i
Lemma: rat-cube-face_wf
∀[k:ℕ]. ∀[c,d:ℚCube(k)]. (c ≤ d ∈ ℙ)
Lemma: rat-cube-face-self
∀[k:ℕ]. ∀c:ℚCube(k). c ≤ c
Lemma: decidable__rat-cube-face
∀k:ℕ. ∀c,d:ℚCube(k). Dec(c ≤ d)
Definition: rat-cube-face-decider
rat-cube-face-decider(k;c;d) ==
eval x = k in
case int_seg_decide(λk.let a,J1 = d k
in let x,x1 = c k
in if qeq(a;x)
then if qeq(x1;J1)
then ifunion(qeq(J1;x); ifunion(qeq(x1;a); inr (λ%.Ax) ))
else ifunion(qeq(J1;x); if qeq(x1;a) then inr (λ%.Ax) else inl (λ%.Ax) fi )
fi
if qeq(J1;x) then if qeq(x1;J1) then inr (λ%.Ax) else inl (λ%.Ax) fi
else inl (λ%.Ax)
fi ;0;x)
of inl(%6) =>
inr let k,%7 = %6
in λ%8.Ax
| inr(%7) =>
inl (λk.let a,J1 = d k
in let x,x1 = c k
in if qeq(a;x)
then if qeq(x1;J1)
then if qeq(J1;x) then if qeq(x1;a) then inl Ax else inr (inl Ax) fi
if qeq(x1;a) then inl Ax
else inr inr Ax
fi
else ifunion(qeq(J1;x); if qeq(x1;a) then inl Ax else Ax fi )
fi
if qeq(J1;x) then if qeq(x1;J1) then inr (inl Ax) else Ax fi
else Ax
fi )
Lemma: decidable__rat-cube-face-ext
∀k:ℕ. ∀c,d:ℚCube(k). Dec(c ≤ d)
Lemma: rat-cube-face-decider_wf
∀k:ℕ. ∀c,d:ℚCube(k). (rat-cube-face-decider(k;c;d) ∈ Dec(c ≤ d))
Definition: is-rat-cube-face
is-rat-cube-face(k;c;d) == isl(rat-cube-face-decider(k;c;d))
Lemma: is-rat-cube-face_wf
∀k:ℕ. ∀c,d:ℚCube(k). (is-rat-cube-face(k;c;d) ∈ 𝔹)
Lemma: assert-is-rat-cube-face
∀k:ℕ. ∀c,d:ℚCube(k). uiff(↑is-rat-cube-face(k;c;d);c ≤ d)
Definition: is-half-interval
is-half-interval(I;J) == let a,b = I in let c,d = J in (qeq(a;c) ∧b qeq(b;qavg(c;d))) ∨b(qeq(a;qavg(c;d)) ∧b qeq(b;d))
Lemma: is-half-interval_wf
∀[I,J:ℚInterval]. (is-half-interval(I;J) ∈ 𝔹)
Lemma: is-half-interval-sub-interval
∀I,J:ℚInterval. (rat-sub-interval(I;J)) supposing ((↑is-half-interval(I;J)) and (↑Inhabited(J)))
Lemma: half-point-interval
∀[I:ℚInterval]. ∀[a:ℚ]. I = [a] ∈ ℚInterval supposing ↑is-half-interval(I;[a])
Definition: is-half-cube
is-half-cube(k;h;c) == bdd-all(k;i.is-half-interval(h i;c i))
Lemma: is-half-cube_wf
∀[k:ℕ]. ∀[h,c:ℚCube(k)]. (is-half-cube(k;h;c) ∈ 𝔹)
Lemma: assert-is-half-cube
∀[k:ℕ]. ∀[h,c:ℚCube(k)]. uiff(↑is-half-cube(k;h;c);∀i:ℕk. (↑is-half-interval(h i;c i)))
Definition: rat-cube-intersection
c ⋂ d == λi.c i ⋂ d i
Lemma: rat-cube-intersection_wf
∀[k:ℕ]. ∀[c,d:ℚCube(k)]. (c ⋂ d ∈ ℚCube(k))
Lemma: rat-cube-intersection-symm
∀[k:ℕ]. ∀[c,d:ℚCube(k)]. (c ⋂ d = d ⋂ c ∈ ℚCube(k))
Lemma: rat-cube-intersection-idemp
∀[k:ℕ]. ∀[c:ℚCube(k)]. (c ⋂ c = c ∈ ℚCube(k))
Definition: rat-point-in-cube
rat-point-in-cube(k;x;c) == ∀i:ℕk. (((fst((c i))) ≤ (x i)) ∧ ((x i) ≤ (snd((c i)))))
Lemma: rat-point-in-cube_wf
∀[k:ℕ]. ∀[x:ℕk ⟶ ℚ]. ∀[c:ℚCube(k)]. (rat-point-in-cube(k;x;c) ∈ ℙ)
Lemma: rat-point-in-intersection
∀[k:ℕ]. ∀[x:ℕk ⟶ ℚ]. ∀[c,d:ℚCube(k)].
uiff(rat-point-in-cube(k;x;c ⋂ d);rat-point-in-cube(k;x;c) ∧ rat-point-in-cube(k;x;d))
Lemma: rat-point-in-half-cube
∀[k:ℕ]. ∀[x:ℕk ⟶ ℚ]. ∀[c,d:ℚCube(k)].
(rat-point-in-cube(k;x;c)) supposing (rat-point-in-cube(k;x;d) and (↑is-half-cube(k;d;c)))
Definition: inhabited-rat-cube
Inhabited(c) == bdd-all(k;i.Inhabited(c i))
Lemma: inhabited-rat-cube_wf
∀[k:ℕ]. ∀[c:ℚCube(k)]. (Inhabited(c) ∈ 𝔹)
Lemma: assert-inhabited-rat-cube
∀[k:ℕ]. ∀[c:ℚCube(k)]. uiff(↑Inhabited(c);∀i:ℕk. (↑Inhabited(c i)))
Lemma: inhabited-rat-cube-iff-point
∀[k:ℕ]. ∀c:ℚCube(k). uiff(↑Inhabited(c);∃x:ℕk ⟶ ℚ. rat-point-in-cube(k;x;c))
Lemma: is-half-cube-sub-cube
∀[k:ℕ]. ∀h,c:ℚCube(k). (rat-sub-cube(k;h;c)) supposing ((↑is-half-cube(k;h;c)) and (↑Inhabited(c)))
Lemma: rat-point-in-face
∀[k:ℕ]. ∀[x:ℕk ⟶ ℚ]. ∀[c,d:ℚCube(k)].
(rat-point-in-cube(k;x;c)) supposing (rat-point-in-cube(k;x;d) and d ≤ c and (↑Inhabited(c)))
Lemma: inhabited-rat-cube-face
∀[k:ℕ]. ∀[c:ℚCube(k)]. ((↑Inhabited(c)) ⇒ (∀f:ℚCube(k). (f ≤ c ⇒ (↑Inhabited(f)))))
Definition: rat-point-in-cube-interior
rat-point-in-cube-interior(k;x;a) ==
∀i:ℕk
((((fst((a i))) ≤ (x i)) ∧ ((x i) ≤ (snd((a i)))))
∧ (fst((a i)) < snd((a i)) ⇒ (fst((a i)) < x i ∧ x i < snd((a i)))))
Lemma: rat-point-in-cube-interior_wf
∀[k:ℕ]. ∀[x:ℕk ⟶ ℚ]. ∀[a:ℚCube(k)]. (rat-point-in-cube-interior(k;x;a) ∈ ℙ)
Lemma: center-point-in-cube-interior
∀[k:ℕ]. ∀[a:ℚCube(k)]. rat-point-in-cube-interior(k;λj.qavg(fst((a j));snd((a j)));a) supposing ↑Inhabited(a)
Lemma: rat-point-in-cube-interior-not-in-face
∀[k:ℕ]. ∀[x:ℕk ⟶ ℚ]. ∀[a:ℚCube(k)].
∀f:ℚCube(k). (f ≤ a ⇒ rat-point-in-cube(k;x;f) ⇒ (f = a ∈ ℚCube(k))) supposing rat-point-in-cube-interior(k;x;a)
Definition: has-interior-point
has-interior-point(k;c;a) == ∃x:ℕk ⟶ ℚ. (rat-point-in-cube(k;x;c) ∧ rat-point-in-cube-interior(k;x;a))
Lemma: has-interior-point_wf
∀[k:ℕ]. ∀[c,a:ℚCube(k)]. (has-interior-point(k;c;a) ∈ ℙ)
Definition: rat-cube-dimension
dim(c) == if Inhabited(c) then Σ(dim(c i) | i < k) else -1 fi
Lemma: rat-cube-dimension_wf
∀[k:ℕ]. ∀[c:ℚCube(k)]. (dim(c) ∈ {-1..k + 1-})
Lemma: rat-cube-dimension-0
∀[k:ℕ]. ∀[c:ℚCube(k)]. uiff(dim(c) = 0 ∈ ℤ;(↑Inhabited(c)) ∧ (∀i:ℕk. (dim(c i) = 0 ∈ ℤ)))
Lemma: rat-cube-dimension-1
∀k:ℕ. ∀c:ℚCube(k).
uiff(dim(c) = 1 ∈ ℤ;(↑Inhabited(c)) ∧ (∃i:ℕk. ((dim(c i) = 1 ∈ ℤ) ∧ (∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ (dim(c j) = 0 ∈ ℤ))))))
Lemma: rat-cube-dimension-zero
∀[k:ℕ]. ∀[c:ℚCube(k)]. uiff(dim(c) = 0 ∈ ℤ;∀i:ℕk. ((fst((c i))) = (snd((c i))) ∈ ℚ))
Lemma: rat-cube-dimension-one
∀k:ℕ. ∀c:ℚCube(k).
(dim(c) = 1 ∈ ℤ ⇐⇒ ∃i:ℕk. (fst((c i)) < snd((c i)) ∧ (∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ ((fst((c j))) = (snd((c j))) ∈ ℚ)))))
Lemma: positive-rat-cube-dimension
∀k:ℕ. ∀c:ℚCube(k). (0 < dim(c) ⇒ (∃i:ℕk. (dim(c i) = 1 ∈ ℤ)))
Lemma: rat-cube-face-dimension-equal
∀[k:ℕ]. ∀[c:ℚCube(k)]. ∀f:ℚCube(k). (f = c ∈ ℚCube(k)) supposing ((dim(f) = dim(c) ∈ ℤ) and f ≤ c) supposing ↑Inhabited\000C(c)
Lemma: half-cubes-listable
∀k:ℕ. ∀c:{c:ℚCube(k)| ↑Inhabited(c)} .
(∃L:ℚCube(k) List [(no_repeats(ℚCube(k);L) ∧ (∀h:ℚCube(k). ((h ∈ L) ⇐⇒ ↑is-half-cube(k;h;c))))])
Definition: half-cubes
half-cubes(k) ==
primrec(k;λc.<λx.x, Ax>;λi,x,c. if dim(c ((i + 1) - 1))=1
then let v1,v2 = c ((i + 1) - 1)
in if q_less(v1;v2)
then map(λh,i@0. if i@0 <z (i + 1) - 1 then h i@0 else <v1, qavg(v1;v2)> fi ;x\000C c)
@ map(λh,i@0. if i@0 <z (i + 1) - 1 then h i@0 else <qavg(v1;v2), v2> fi \000C;x c)
else Ax
fi
else map(λh,i@0. if i@0 <z (i + 1) - 1 then h i@0 else c i@0 fi ;x c))
Lemma: half-cubes-listable-ext
∀k:ℕ. ∀c:{c:ℚCube(k)| ↑Inhabited(c)} .
(∃L:ℚCube(k) List [(no_repeats(ℚCube(k);L) ∧ (∀h:ℚCube(k). ((h ∈ L) ⇐⇒ ↑is-half-cube(k;h;c))))])
Lemma: half-cubes_wf
∀[k:ℕ]
(half-cubes(k) ∈ c:{c:ℚCube(k)| ↑Inhabited(c)} ⟶ {L:ℚCube(k) List|
no_repeats(ℚCube(k);L) ∧ (∀h:ℚCube(k). ((h ∈ L) ⇐⇒ ↑is-half-cube(k;h;c)))} )
Definition: half-cubes-of
half-cubes-of(k;c) == half-cubes(k) c
Lemma: half-cubes-of_wf
∀[k:ℕ]. ∀[c:{c:ℚCube(k)| ↑Inhabited(c)} ].
(half-cubes-of(k;c) ∈ {L:ℚCube(k) List| no_repeats(ℚCube(k);L) ∧ (∀h:ℚCube(k). ((h ∈ L) ⇐⇒ ↑is-half-cube(k;h;c)))} )
Lemma: half-cube-dimension
∀[k:ℕ]. ∀[c:{c:ℚCube(k)| ↑Inhabited(c)} ]. ∀[h:ℚCube(k)]. ((↑is-half-cube(k;h;c)) ⇒ (dim(h) = dim(c) ∈ ℤ))
Lemma: has-interior-point-implies
∀[k:ℕ]. ∀[c,a:ℚCube(k)].
(has-interior-point(k;c;a) ⇒ dim(c) < dim(a) ⇒ (∀d:ℚCube(k). ((↑is-half-cube(k;c;d)) ⇒ (¬d ≤ a))))
Definition: immediate-rc-face
immediate-rc-face(k;f;c) == f ≤ c ∧ (dim(f) = (dim(c) - 1) ∈ ℤ)
Lemma: immediate-rc-face_wf
∀[k:ℕ]. ∀[f,c:ℚCube(k)]. (immediate-rc-face(k;f;c) ∈ ℙ)
Lemma: immediate-rc-face-implies
∀k:ℕ. ∀f,c:ℚCube(k).
(0 < dim(c)
⇒ immediate-rc-face(k;f;c)
⇒ (∃i:ℕk
((dim(c i) = 1 ∈ ℤ)
∧ (∀j:ℕk. ((¬(j = i ∈ ℤ)) ⇒ ((f j) = (c j) ∈ ℚInterval)))
∧ (((f i) = [fst((c i))] ∈ ℚInterval) ∨ ((f i) = [snd((c i))] ∈ ℚInterval)))))
Lemma: compatible-rat-intervals-iff
∀I,J:ℚInterval.
((↑Inhabited(I))
⇒ (↑Inhabited(J))
⇒ (↑Inhabited(I ⋂ J))
⇒ (I ⋂ J ≤ I ∧ I ⋂ J ≤ J ⇐⇒ (I = J ∈ ℚInterval) ∨ ((snd(I)) = (fst(J)) ∈ ℚ) ∨ ((snd(J)) = (fst(I)) ∈ ℚ)))
Definition: compatible-rat-cubes
Compatible(c;d) == (↑Inhabited(c ⋂ d)) ⇒ (c ⋂ d ≤ c ∧ c ⋂ d ≤ d)
Lemma: compatible-rat-cubes_wf
∀[k:ℕ]. ∀[c,d:ℚCube(k)]. (Compatible(c;d) ∈ ℙ)
Lemma: compatible-rat-cubes-symm
∀[k:ℕ]. ∀[c,d:ℚCube(k)]. (Compatible(c;d) ⇒ Compatible(d;c))
Lemma: compatible-rat-cubes-refl
∀[k:ℕ]. ∀[c:ℚCube(k)]. ∀d:ℚCube(k). ((c = d ∈ ℚCube(k)) ⇒ Compatible(d;c))
Lemma: faces-of-compatible-rat-cubes
∀k:ℕ. ∀f,g,c,d:ℚCube(k). ((↑Inhabited(c)) ⇒ (↑Inhabited(d)) ⇒ f ≤ c ⇒ g ≤ d ⇒ Compatible(c;d) ⇒ Compatible(f;g))
Lemma: decidable__compatible-rat-cubes
∀k:ℕ. ∀c,d:ℚCube(k). Dec(Compatible(c;d))
Lemma: sq_stable__compatible-rat-cubes
∀k:ℕ. ∀c,d:ℚCube(k). SqStable(Compatible(c;d))
Lemma: inhabited-half-cube
∀k:ℕ. ∀a,b:ℚCube(k). ((↑is-half-cube(k;a;b)) ⇒ (↑Inhabited(a) ⇐⇒ ↑Inhabited(b)))
Lemma: inhabited-intersection-half-cubes
∀k:ℕ. ∀a,b,c,d:ℚCube(k).
((↑is-half-cube(k;c;a)) ⇒ (↑is-half-cube(k;d;b)) ⇒ (↑Inhabited(c ⋂ d)) ⇒ (↑Inhabited(a ⋂ b)))
Lemma: common-face-inhabited-intersection
∀k:ℕ. ∀a,b,b':ℚCube(k). ((↑Inhabited(b')) ⇒ (↑Inhabited(b)) ⇒ (a ≤ b ∧ a ≤ b') ⇒ (↑Inhabited(b ⋂ b')))
Lemma: face-of-intersection
∀k:ℕ. ∀a,b,b':ℚCube(k). ((↑Inhabited(b')) ⇒ (↑Inhabited(b)) ⇒ (a ≤ b ∧ a ≤ b') ⇒ a ≤ b ⋂ b')
Lemma: compatible-half-cubes
∀k:ℕ. ∀a,b,c,d:ℚCube(k). ((↑is-half-cube(k;c;a)) ⇒ (↑is-half-cube(k;d;b)) ⇒ Compatible(a;b) ⇒ Compatible(c;d))
Lemma: same-half-cube-of-compatible
∀k:ℕ. ∀a,b,c:ℚCube(k).
((↑Inhabited(c)) ⇒ (↑is-half-cube(k;c;a)) ⇒ (↑is-half-cube(k;c;b)) ⇒ Compatible(a;b) ⇒ (a = b ∈ ℚCube(k)))
Lemma: compatible-cubes-with-interior-point
∀k:ℕ. ∀a,b:ℚCube(k).
(a ≤ b) supposing ((∃x:ℕk ⟶ ℚ. (rat-point-in-cube-interior(k;x;a) ∧ rat-point-in-cube(k;x;b))) and Compatible(a;b))
Lemma: compatible-same-dim-cubes-with-interior-point
∀[k:ℕ]. ∀[a,b:ℚCube(k)].
(a = b ∈ ℚCube(k)) supposing
((∃x:ℕk ⟶ ℚ. (rat-point-in-cube-interior(k;x;a) ∧ rat-point-in-cube(k;x;b))) and
Compatible(a;b) and
(dim(a) = dim(b) ∈ ℤ))
Lemma: half-cube-of-face
∀k:ℕ. ∀a,b,c,d,e:ℚCube(k).
(Compatible(a;e)
⇒ b ≤ e
⇒ d ≤ c
⇒ (b ≤ a) supposing ((↑Inhabited(e)) and (↑Inhabited(a)) and (↑is-half-cube(k;c;a)) and (↑is-half-cube(k;d;b))))
Lemma: face-of-half-cube
∀k:ℕ. ∀a,b,c:ℚCube(k). (b ≤ c ⇒ (↑is-half-cube(k;a;b)) ⇒ (∃!d:ℚCube(k). ((↑is-half-cube(k;d;c)) ∧ a ≤ d)))
Lemma: extend-half-cube-face
∀k:ℕ. ∀a,b,c:ℚCube(k).
(0 < dim(c)
⇒ a ≤ b
⇒ (↑is-half-cube(k;b;c))
⇒ (dim(a) = (dim(b) - 1) ∈ ℤ)
⇒ (((∃!d:ℚCube(k). ((↑is-half-cube(k;a;d)) ∧ d ≤ c))
∧ (∀b':ℚCube(k). ((↑is-half-cube(k;b';c)) ⇒ a ≤ b' ⇒ (b' = b ∈ ℚCube(k)))))
∨ ((∃!b':ℚCube(k). (a ≤ b' ∧ (↑is-half-cube(k;b';c)) ∧ (¬(b' = b ∈ ℚCube(k))))) ∧ has-interior-point(k;a;c))))
Definition: rational-cube-complex
n-dim-complex == {L:ℚCube(k) List| no_repeats(ℚCube(k);L) ∧ (∀c,d∈L. Compatible(c;d)) ∧ (∀c∈L.dim(c) = n ∈ ℤ)}
Lemma: rational-cube-complex_wf
∀[k,n:ℕ]. (n-dim-complex ∈ Type)
Lemma: member-rat-cube-complex-inhabited
∀[k:ℕ]. ∀[c:ℚCube(k)]. ↑Inhabited(c) supposing ∃n:ℕ. ∃K:n-dim-complex. (c ∈ K)
Definition: rat-cube-sub-complex
rat-cube-sub-complex(P;L) == filter(P;L)
Lemma: rat-cube-sub-complex_wf
∀[k,n:ℕ]. ∀[K:n-dim-complex]. ∀[P:{x:ℚCube(k)| (x ∈ K)} ⟶ 𝔹]. (rat-cube-sub-complex(P;K) ∈ n-dim-complex)
Definition: lower-rc-face
lower-rc-face(c;j) == λi.if (i =z j) then [fst((c i))] else c i fi
Lemma: lower-rc-face_wf
∀[k:ℕ]. ∀[c:ℚCube(k)]. ∀[j:ℕk]. (lower-rc-face(c;j) ∈ ℚCube(k))
Lemma: lower-rc-face-is-face
∀k:ℕ. ∀c:ℚCube(k). ∀j:ℕk. lower-rc-face(c;j) ≤ c
Lemma: inhabited-lower-rc-face
∀k:ℕ. ∀c:ℚCube(k). ∀j:ℕk. ((↑Inhabited(c j)) ⇒ Inhabited(lower-rc-face(c;j)) = Inhabited(c))
Lemma: lower-rc-face-dimension
∀k:ℕ. ∀c:ℚCube(k). ∀j:ℕk.
((↑Inhabited(c)) ⇒ (dim(lower-rc-face(c;j)) = if (dim(c j) =z 0) then dim(c) else dim(c) - 1 fi ∈ ℤ))
Definition: upper-rc-face
upper-rc-face(c;j) == λi.if (i =z j) then [snd((c i))] else c i fi
Lemma: upper-rc-face_wf
∀[k:ℕ]. ∀[c:ℚCube(k)]. ∀[j:ℕk]. (upper-rc-face(c;j) ∈ ℚCube(k))
Lemma: upper-rc-face-is-face
∀k:ℕ. ∀c:ℚCube(k). ∀j:ℕk. upper-rc-face(c;j) ≤ c
Lemma: inhabited-upper-rc-face
∀k:ℕ. ∀c:ℚCube(k). ∀j:ℕk. ((↑Inhabited(c j)) ⇒ Inhabited(upper-rc-face(c;j)) = Inhabited(c))
Lemma: upper-rc-face-dimension
∀k:ℕ. ∀c:ℚCube(k). ∀j:ℕk.
((↑Inhabited(c)) ⇒ (dim(upper-rc-face(c;j)) = if (dim(c j) =z 0) then dim(c) else dim(c) - 1 fi ∈ ℤ))
Lemma: positive-rat-cube-immediate-face
∀k:ℕ. ∀c:ℚCube(k). (0 < dim(c) ⇒ (∃f:ℚCube(k). immediate-rc-face(k;f;c)))
Definition: rat-cube-faces
rat-cube-faces(k;c) == concat(mapfilter(λj.[lower-rc-face(c;j); upper-rc-face(c;j)];λj.(dim(c j) =z 1);upto(k)))
Lemma: rat-cube-faces_wf
∀[k:ℕ]. ∀[c:ℚCube(k)]. rat-cube-faces(k;c) ∈ {f:ℚCube(k)| f ≤ c ∧ (dim(f) = (dim(c) - 1) ∈ ℤ)} List supposing ↑Inhabit\000Ced(c)
Lemma: implies-member-rat-cube-faces
∀k:ℕ. ∀c:ℚCube(k).
∀f:{f:ℚCube(k)| f ≤ c ∧ (dim(f) = (dim(c) - 1) ∈ ℤ)} . (f ∈ rat-cube-faces(k;c)) supposing ↑Inhabited(c)
Lemma: member-rat-cube-faces
∀k:ℕ. ∀c:ℚCube(k).
∀f:ℚCube(k). ((f ∈ rat-cube-faces(k;c)) ⇐⇒ f ≤ c ∧ (dim(f) = (dim(c) - 1) ∈ ℤ)) supposing ↑Inhabited(c)
Lemma: length-rat-cube-faces
∀k:ℕ. ∀c:ℚCube(k). ((↑Inhabited(c)) ⇒ (||rat-cube-faces(k;c)|| = (2 * dim(c)) ∈ ℤ))
Lemma: no_repeats-rat-cube-faces
∀k:ℕ. ∀c:ℚCube(k). no_repeats(ℚCube(k);rat-cube-faces(k;c))
Definition: face-complex
face-complex(k;L) == remove-repeats(rc-deq(k);concat(map(λc.if Inhabited(c) then rat-cube-faces(k;c) else [] fi ;L)))
Lemma: member-face-complex
∀k:ℕ. ∀K:ℚCube(k) List. ∀f:ℚCube(k).
((f ∈ face-complex(k;K)) ⇐⇒ ∃c:ℚCube(k). ((c ∈ K) ∧ (↑Inhabited(c)) ∧ (f ∈ rat-cube-faces(k;c))))
Lemma: face-complex_wf
∀[k:ℕ]. ∀[n:ℕ+]. ∀[K:n-dim-complex]. (face-complex(k;K) ∈ n - 1-dim-complex)
Definition: in-complex-boundary
in-complex-boundary(k;f;K) == isOdd(||filter(λc.is-rat-cube-face(k;f;c);K)||)
Lemma: in-complex-boundary_wf
∀[k:ℕ]. ∀[f:ℚCube(k)]. ∀[K:ℚCube(k) List]. (in-complex-boundary(k;f;K) ∈ 𝔹)
Definition: rat-complex-boundary
∂(K) == rat-cube-sub-complex(λf.in-complex-boundary(k;f;K);face-complex(k;K))
Lemma: boundary-of-0-dim-is-nil
∀[k:ℕ]. ∀[K:ℚCube(k) List]. ∂(K) ~ [] supposing (∀c∈K.dim(c) = 0 ∈ ℤ)
Lemma: rat-complex-boundary_wf
∀[k,n:ℕ]. ∀[K:n-dim-complex]. (∂(K) ∈ n - 1-dim-complex)
Lemma: rat-complex-boundary-0-dim
∀[k:ℕ]. ∀[K:0-dim-complex]. (∂(K) ~ [])
Definition: singleton-complex
singleton-complex(c) == [c]
Lemma: singleton-complex_wf
∀[k,n:ℕ]. ∀[c:{c:ℚCube(k)| dim(c) = n ∈ ℤ} ]. (singleton-complex(c) ∈ n-dim-complex)
Lemma: boundary-singleton-complex
∀[k,n:ℕ]. ∀[c:{c:ℚCube(k)| dim(c) = n ∈ ℤ} ]. (∂(singleton-complex(c)) ~ remove-repeats(rc-deq(k);rat-cube-faces(k;c)))
Lemma: member-rat-complex-boundary
∀k:ℕ. ∀K:ℚCube(k) List. ∀f:ℚCube(k).
((f ∈ ∂(K))
⇐⇒ (∃c:ℚCube(k). ((c ∈ K) ∧ (↑Inhabited(c)) ∧ f ≤ c ∧ (dim(f) = (dim(c) - 1) ∈ ℤ))) ∧ (↑in-complex-boundary(k;f;K)))
Lemma: member-rat-complex-boundary-n
∀n,k:ℕ. ∀K:n-dim-complex. ∀f:ℚCube(k). ((f ∈ ∂(K)) ⇐⇒ (↑in-complex-boundary(k;f;K)) ∧ (dim(f) = (n - 1) ∈ ℤ))
Lemma: rat-complex-boundary-remove1
∀k,n:ℕ. ∀K:n-dim-complex. ∀c:ℚCube(k).
((c ∈ K)
⇒ (∀f:ℚCube(k)
((f ∈ ∂(rat-cube-sub-complex(λa.(¬brceq(k;a;c));K)))
⇐⇒ ((f ∈ ∂(K)) ∧ (¬f ≤ c)) ∨ ((¬(f ∈ ∂(K))) ∧ f ≤ c ∧ (dim(f) = (dim(c) - 1) ∈ ℤ)))))
Lemma: length-rat-complex-boundary-even
∀k,n:ℕ. ∀K:n-dim-complex. (↑isEven(||∂(K)||))
Lemma: face-of-face-pairity
∀k:ℕ. ∀a,b,c:ℚCube(k).
(1 < dim(c)
⇒ immediate-rc-face(k;a;b)
⇒ immediate-rc-face(k;b;c)
⇒ (∃!b':ℚCube(k). (immediate-rc-face(k;a;b') ∧ immediate-rc-face(k;b';c) ∧ (¬(b' = b ∈ ℚCube(k))))))
Lemma: rat-complex-boundary-boundary
∀[k,n:ℕ]. ∀[K:n-dim-complex]. (∂(∂(K)) ~ [])
Definition: rat-complex-subdiv
(K)' == concat(map(λc.half-cubes-of(k;c);K))
Lemma: member-rat-complex-subdiv
∀k:ℕ. ∀K:{c:ℚCube(k)| ↑Inhabited(c)} List. ∀c:ℚCube(k).
((c ∈ (K)') ⇐⇒ ∃a:ℚCube(k). ((a ∈ K) ∧ (↑is-half-cube(k;c;a))))
Lemma: rat-complex-subdiv_wf
∀[k,n:ℕ]. ∀[K:n-dim-complex]. ((K)' ∈ n-dim-complex)
Lemma: member-rat-complex-subdiv2
∀k,n:ℕ. ∀K:n-dim-complex. ∀c:ℚCube(k). ((c ∈ (K)') ⇐⇒ ∃a:ℚCube(k). ((a ∈ K) ∧ (↑is-half-cube(k;c;a))))
Lemma: member-rat-complex-subdiv-sub-cube
∀k,n:ℕ. ∀K:n-dim-complex. ∀c:ℚCube(k). ((c ∈ (K)') ⇒ (∃a:ℚCube(k). ((a ∈ K) ∧ rat-sub-cube(k;c;a))))
Lemma: rat-complex-subdiv-non-nil
∀[k,n:ℕ]. ∀[K:n-dim-complex]. 0 < ||(K)'|| supposing 0 < ||K||
Lemma: equal-rat-cube-complexes
∀k:ℕ
∀[n:ℕ]
∀K,L:n-dim-complex.
uiff(permutation(ℚCube(k);K;L);∀c:{c:ℚCube(k)| (↑Inhabited(c)) ∧ (dim(c) = n ∈ ℤ)} . ((c ∈ K) ⇐⇒ (c ∈ L)))
Lemma: rat-complex-boundary-subdiv
∀k,n:ℕ. ∀K:n-dim-complex. permutation(ℚCube(k);∂((K)');(∂(K))')
Definition: rat-complex-iter-subdiv
K'^(n) == primrec(n;K;λi,c. (c)')
Lemma: rat-complex-iter-subdiv_wf
∀[k,n:ℕ]. ∀[K:n-dim-complex]. ∀[j:ℕ]. (K'^(j) ∈ n-dim-complex)
Lemma: rat-complex-boundary-iter-subdiv
∀k,n,j:ℕ. ∀K:n-dim-complex. permutation(ℚCube(k);∂(K'^(j));∂(K)'^(j))
Lemma: member-iter-subdiv-sub-cube
∀k,n,j:ℕ. ∀K:n-dim-complex. ∀c:ℚCube(k). ((c ∈ K'^(j)) ⇒ (∃a:ℚCube(k). ((a ∈ K) ∧ rat-sub-cube(k;c;a))))
Definition: qsum
Σa ≤ j < b. E[j] == Σ(<ℚ+*>) a ≤ j < b. E[j]
Lemma: qsum_wf
∀[a,b:ℤ]. ∀[E:{a..b-} ⟶ ℚ]. (Σa ≤ j < b. E[j] ∈ ℚ)
Lemma: qsum_unroll
∀[a,b:ℤ]. ∀[E:{a..b-} ⟶ ℚ]. (Σa ≤ j < b. E[j] ~ if a <z b then Σa ≤ j < b - 1. E[j] + E[b - 1] else 0 fi )
Definition: q-rng-nexp
q-rng-nexp(r;n) == r ↑<ℚ+*> n
Lemma: q-rng-nexp_wf
∀[r:ℚ]. ∀[n:ℕ]. (q-rng-nexp(r;n) ∈ ℚ)
Definition: qexp
r ↑ n == eval n = n in let a,b = qrep(r) in mk-rational(a^n;b^n)
Lemma: qexp_wf
∀[r:ℚ]. ∀[n:ℕ]. (r ↑ n ∈ ℚ)
Lemma: qexp-eq-q-rng-nexp
∀[n:ℕ]. ∀[r:ℚ]. (r ↑ n = q-rng-nexp(r;n) ∈ ℚ)
Lemma: exp_zero_q
∀[e:ℚ]. (e ↑ 0 = 1 ∈ ℚ)
Lemma: exp_unroll_q
∀[n:ℕ+]. ∀[e:ℚ]. (e ↑ n = (e ↑ n - 1 * e) ∈ ℚ)
Lemma: qexp_step
∀[n:ℕ]. ∀[e:ℚ]. (e ↑ n + 1 = (e ↑ n * e) ∈ ℚ)
Lemma: sum_unroll_base_q
∀[i,j:ℤ]. ∀[E:{i..j-} ⟶ ℚ]. (Σi ≤ k < j. E[k] = 0 ∈ ℚ) supposing i = j ∈ ℤ
Lemma: sum_unroll_hi_q
∀[i,j:ℤ]. ∀[E:{i..j-} ⟶ ℚ]. (Σi ≤ k < j. E[k] = (Σi ≤ k < j - 1. E[k] + E[j - 1]) ∈ ℚ) supposing i < j
Lemma: sum_unroll_unit_q
∀[i,j:ℤ]. ∀[E:{i..j-} ⟶ ℚ]. (Σi ≤ k < j. E[k] = E[i] ∈ ℚ) supposing (i + 1) = j ∈ ℤ
Lemma: sum_unroll_lo_q
∀[i,j:ℤ]. ∀[E:{i..j-} ⟶ ℚ]. (Σi ≤ k < j. E[k] = (E[i] + Σi + 1 ≤ k < j. E[k]) ∈ ℚ) supposing i < j
Lemma: sum_shift_q
∀[a,b:ℤ]. ∀[E:{a..b-} ⟶ ℚ]. ∀[k:ℤ]. (Σa ≤ j < b. E[j] = Σa + k ≤ j < b + k. E[j - k] ∈ ℚ) supposing a ≤ b
Lemma: sum_split_q
∀[a,b,c:ℤ].
(∀[E:{a..c-} ⟶ ℚ]. (Σa ≤ j < c. E[j] = (Σa ≤ j < b. E[j] + Σb ≤ j < c. E[j]) ∈ ℚ)) supposing ((b ≤ c) and (a ≤ b))
Lemma: sum_plus_q
∀[a,b:ℤ]. ∀[E,F:{a..b-} ⟶ ℚ]. (Σa ≤ i < b. E[i] + F[i] = (Σa ≤ i < b. E[i] + Σa ≤ i < b. F[i]) ∈ ℚ) supposing a ≤ b
Lemma: prod_sum_l_q
∀[a,b:ℤ]. ∀[E:{a..b-} ⟶ ℚ]. ∀[u:ℚ]. ((u * Σa ≤ j < b. E[j]) = Σa ≤ j < b. u * E[j] ∈ ℚ) supposing a ≤ b
Lemma: prod_sum_r_q
∀[a,b:ℤ]. ∀[E:{a..b-} ⟶ ℚ]. ∀[u:ℚ]. ((Σa ≤ j < b. E[j] * u) = Σa ≤ j < b. E[j] * u ∈ ℚ) supposing a ≤ b
Lemma: binomial_q
∀[a,b:ℚ]. ∀[n:ℕ]. (a + b ↑ n = Σ0 ≤ i < n + 1. choose(n;i) ⋅<ℚ+*> (a ↑ i * b ↑ n - i) ∈ ℚ)
Lemma: sum_of_geometric_prog_q
∀[a:ℚ]. ∀[n:ℕ]. (((1 + -(a)) * Σ0 ≤ i < n. a ↑ i) = (1 + -(a ↑ n)) ∈ ℚ)
Lemma: qsum-int
∀[i,j:ℤ]. ∀[X:{i..j-} ⟶ ℤ]. (Σi ≤ x < j. X[x] ∈ ℤ)
Lemma: qsum-qle
∀[a,b:ℤ]. ∀[E,F:{a..b-} ⟶ ℚ]. Σa ≤ j < b. E[j] ≤ Σa ≤ j < b. F[j] supposing ∀j:ℤ. ((a ≤ j) ⇒ j < b ⇒ (E[j] ≤ F[j]))
Definition: delta
delta(i;j) == if (i =z j) then 1 else 0 fi
Lemma: delta_wf
∀[i,j:ℤ]. (delta(i;j) ∈ ℕ2)
Lemma: qsum-delta
∀[a,b:ℤ]. ∀[E:{a..b-} ⟶ ℚ]. ∀[i:ℤ]. (Σa ≤ j < b. E[j] * delta(i;j) = if a ≤z i ∧b i <z b then E[i] else 0 fi ∈ ℚ)
Lemma: summand-qle-sum
∀[a,b:ℤ]. ∀[E:{a..b-} ⟶ ℚ]. ∀[i:{a..b-}]. (E[i] ≤ Σa ≤ j < b. E[j]) supposing ∀j:{a..b-}. (0 ≤ E[j])
Lemma: qexp-zero
∀[r:ℚ]. (r ↑ 0 = 1 ∈ ℚ)
Lemma: qexp-exp
∀[n:ℕ]. ∀[x:ℤ]. (x ↑ n = x^n ∈ ℚ)
Lemma: qexp-sign
∀n:ℕ. ∀r:ℚ.
((0 < r ↑ n ⇐⇒ (n = 0 ∈ ℤ) ∨ 0 < r ∨ (r < 0 ∧ (↑isEven(n))))
∧ (r ↑ n < 0 ⇐⇒ r < 0 ∧ (↑isOdd(n)))
∧ (r ↑ n = 0 ∈ ℚ ⇐⇒ (r = 0 ∈ ℚ) ∧ (¬(n = 0 ∈ ℤ))))
Lemma: qexp-positive
∀[n:ℕ]. ∀[r:ℚ]. 0 < r ↑ n supposing 0 < r
Lemma: qexp-positive-iff
∀n:ℕ. ∀r:ℚ. (0 < r ↑ n ⇐⇒ (n = 0 ∈ ℤ) ∨ 0 < r ∨ (r < 0 ∧ (↑isEven(n))))
Lemma: qexp-non-zero
∀[n:ℕ]. ∀[r:ℚ]. ¬(r ↑ n = 0 ∈ ℚ) supposing ¬(r = 0 ∈ ℚ)
Lemma: qexp-nonneg
∀[n:ℕ]. ∀[r:ℚ]. 0 ≤ r ↑ n supposing 0 ≤ r
Lemma: qexp-one
∀[n:ℕ]. (1 ↑ n = 1 ∈ ℚ)
Lemma: qexp-minus-one
∀[n:ℕ]. (-1 ↑ n = if (n rem 2 =z 0) then 1 else -1 fi ∈ ℚ)
Lemma: qexp1
∀[q:ℚ]. (q ↑ 1 = q ∈ ℚ)
Lemma: qexp2
∀[q:ℚ]. (q ↑ 2 = (q * q) ∈ ℚ)
Lemma: qexp_preserves_qle
∀[a,b:ℚ]. (∀[n:ℕ]. (a ↑ n ≤ b ↑ n)) supposing ((a ≤ b) and (0 ≤ a))
Lemma: qexp_preserves_qless
∀[a,b:ℚ]. (∀[n:ℕ]. a ↑ n < b ↑ n supposing 0 < n) supposing (a < b and (0 ≤ a))
Lemma: qexp-qmul
∀[a,b:ℚ]. ∀[n:ℕ]. (a * b ↑ n = (a ↑ n * b ↑ n) ∈ ℚ)
Lemma: qexp-add
∀[m,n:ℕ]. ∀[b:ℚ]. (b ↑ n + m = (b ↑ n * b ↑ m) ∈ ℚ)
Lemma: qexp-mul
∀[m,n:ℕ]. ∀[b:ℚ]. (b ↑ n * m = b ↑ n ↑ m ∈ ℚ)
Lemma: qexp-qdiv
∀[a,b:ℚ]. ∀[n:ℕ]. ((a/b) ↑ n = (a ↑ n/b ↑ n) ∈ ℚ) supposing ¬(b = 0 ∈ ℚ)
Lemma: qexp-qabs
∀[a:ℚ]. ∀[n:ℕ]. (|a| ↑ n = |a ↑ n| ∈ ℚ)
Lemma: qexp-le-one
∀[a:ℚ]. ∀[n:ℕ]. (a ↑ n ≤ 1) supposing (0 ≤ a) ∧ (a ≤ 1)
Lemma: qexp-convex
∀a,b:ℚ. ((0 ≤ b) ⇒ (b ≤ a) ⇒ (∀n:ℕ+. (a - b ↑ n ≤ (a ↑ n - b ↑ n))))
Lemma: qexp-qminus
∀n:ℕ. ∀a:ℚ. (-(a) ↑ n = if isEven(n) then a ↑ n else -(a ↑ n) fi ∈ ℚ)
Lemma: qexp-convex2
∀a,b:ℚ. (((0 ≤ a) ∧ (0 ≤ b)) ⇒ (∀n:ℕ+. (|a - b| ↑ n ≤ |a ↑ n - b ↑ n|)))
Lemma: qexp-convex3
∀a,b:ℚ. ((((0 ≤ a) ∧ (0 ≤ b)) ∨ ((a ≤ 0) ∧ (b ≤ 0))) ⇒ (∀n:ℕ+. (|a - b| ↑ n ≤ |a ↑ n - b ↑ n|)))
Lemma: qexp-greater-one
∀e:{e:ℚ| 0 < e} . ∀r:{r:ℚ| 1 + e < r} . ∀n:ℕ. 1 + (n * e) < r ↑ n supposing 1 ≤ n
Lemma: qsum-const
∀[n:ℕ]. ∀[q:ℚ]. (Σ0 ≤ i < n. q = (n * q) ∈ ℚ)
Lemma: qsum-const2
∀[a,b:ℤ]. ∀[q:ℚ]. (Σa ≤ i < b. q = (if a ≤z b then b - a else 0 fi * q) ∈ ℚ)
Lemma: qsum-linearity1
∀[a,b:ℤ]. ∀[q:ℚ]. ∀[X:{a..b-} ⟶ ℚ]. (Σa ≤ i < b. q * X[i] = (q * Σa ≤ i < b. X[i]) ∈ ℚ)
Lemma: qsum-linearity2
∀[a,b:ℤ]. ∀[X,Y:{a..b-} ⟶ ℚ]. (Σa ≤ i < b. X[i] + Y[i] = (Σa ≤ i < b. X[i] + Σa ≤ i < b. Y[i]) ∈ ℚ)
Lemma: qsum_product
∀[a,b,c,d:ℤ]. ∀[x:{a..b + 1-} ⟶ ℚ]. ∀[y:{c..d + 1-} ⟶ ℚ].
((Σa ≤ i < b. x[i] * Σc ≤ j < d. y[j]) = Σa ≤ i < b. Σc ≤ j < d. x[i] * y[j] ∈ ℚ)
Lemma: qsum_functionality_wrt_qle
∀[n,m:ℤ]. ∀[x,y:{n..m + 1-} ⟶ ℚ].
Σn ≤ k < m. x[k] ≤ Σn ≤ k < m. y[k] supposing ∀k:ℤ. ((n ≤ k) ⇒ (k ≤ m) ⇒ (x[k] ≤ y[k]))
Lemma: q-geometric-series
∀[a:ℚ]. ∀[n:ℕ]. (Σ0 ≤ i < n. a ↑ i = if qeq(a;1) then n else (1 - a ↑ n/1 - a) fi ∈ ℚ)
Lemma: qsum-reciprocal-squares
∀[J:ℕ+]. (Σ1 ≤ n < J + 1. (1/n * n) ≤ (2 - (1/J)))
Lemma: qsum-reciprocal-squares-bound
∀[J:ℕ]. Σ1 ≤ n < J. (1/n * n) < 2
Lemma: q-Cauchy-Schwarz
∀[n:ℕ]. ∀[x,y:ℕn + 1 ⟶ ℚ].
((Σ0 ≤ i < n. x[i] * y[i] * Σ0 ≤ i < n. x[i] * y[i]) ≤ (Σ0 ≤ i < n. x[i] * x[i] * Σ0 ≤ i < n. y[i] * y[i]))
Lemma: qexp-difference-factor
∀[a,b:ℚ]. ∀n:ℕ. ((a ↑ n - b ↑ n) = ((a - b) * Σ0 ≤ i < n. a ↑ i * b ↑ n - i + 1) ∈ ℚ)
Lemma: q-archimedean
∀a:ℚ. ∃n:ℕ. ((-(n) ≤ a) ∧ (a ≤ n))
Lemma: q-archimedean-ext
∀a:ℚ. ∃n:ℕ. ((-(n) ≤ a) ∧ (a ≤ n))
Lemma: small-reciprocal-proof
∀e:ℚ. ∃m:ℕ+. (1/m) < e supposing 0 < e
Lemma: reciprocal-qle-proof
∀e:ℚ. ∃m:ℕ+. ((1/m) ≤ e) supposing 0 < e
Lemma: small-reciprocal
∀e:ℚ. ∃m:ℕ+. (1/m) < e supposing 0 < e
Lemma: reciprocal-qle
∀e:ℚ. ∃m:ℕ+. ((1/m) ≤ e) supposing 0 < e
Definition: reciprocal_qle
reciprocal_qle(e) == fst((TERMOF{reciprocal-qle:o, 1:l} e))
Lemma: reciprocal_qle_wf
∀e:{q:ℚ| 0 < q} . (reciprocal_qle(e) ∈ {n:ℕ+| (1/n) ≤ e} )
Definition: small_reciprocal
small_reciprocal(e) == fst((TERMOF{small-reciprocal:o, 1:l} e))
Lemma: small_reciprocal_wf
∀e:{q:ℚ| 0 < q} . (small_reciprocal(e) ∈ {n:ℕ+| (1/n) < e} )
Definition: qexpfact
qexpfact(n;x;p;b) ==
fix((λqexpfact,n,p,b. if q_less(p;b)
then n
else eval n' = n + 1 in
eval p' = x * p in
eval b' = n' * b in
qexpfact n' p' b'
fi ))
n
p
b
Lemma: qexpfact_wf
∀[n:ℕ]. ∀[x:{q:ℚ| 0 ≤ q} ]. ∀[p:ℚ]. ∀[b:{b:ℤ| b = (n)! ∈ ℤ} ]. (qexpfact(n;x;p;b) ∈ {n...})
Lemma: qexpfact-property
∀[n:ℕ]. ∀[x:{q:ℚ| 0 ≤ q} ]. ∀[p:ℚ]. ∀[b:{b:ℤ| b = (n)! ∈ ℤ} ]. p * x ↑ qexpfact(n;x;p;b) - n < (qexpfact(n;x;p;b))!
Lemma: factorial-greater-qexp
∀x:{q:ℚ| 0 ≤ q} . ∀p:ℚ. ∃n:ℕ. p * x ↑ n < (n)!
Lemma: qlog-bound
∀e:{e:ℚ| 0 < e} . ∀q:{q:ℚ| (e ≤ q) ∧ q < 1} . ∃N:ℕ+. q ↑ N < e
Lemma: qlog-lemma
∀e:{e:ℚ| 0 < e} . ∀q:{q:ℚ| (e ≤ q) ∧ q < 1} . {nr:ℕ × ℚ| let n,r = nr in (r = q ↑ n ∈ ℚ) ∧ (e ≤ r) ∧ r * r < e}
Lemma: qlog-lemma-ext
∀e:{e:ℚ| 0 < e} . ∀q:{q:ℚ| (e ≤ q) ∧ q < 1} . {nr:ℕ × ℚ| let n,r = nr in (r = q ↑ n ∈ ℚ) ∧ (e ≤ r) ∧ r * r < e}
Lemma: qlog-exists
∀e:{e:ℚ| 0 < e} . ∀q:{q:ℚ| (0 ≤ q) ∧ q < 1} . {n:ℕ+| ((e ≤ 1) ⇒ (e ≤ q ↑ n - 1)) ∧ q ↑ n < e}
Lemma: qlog-ext
∀e:{e:ℚ| 0 < e} . ∀q:{q:ℚ| (0 ≤ q) ∧ q < 1} . {n:ℕ+| ((e ≤ 1) ⇒ (e ≤ q ↑ n - 1)) ∧ q ↑ n < e}
Definition: qlog
qlog(q;e) == TERMOF{qlog-ext:o, 1:l} e q
Definition: qlog-type
qlog-type(q;e) == {n:ℕ+| ((e ≤ 1) ⇒ (e ≤ q ↑ n - 1)) ∧ q ↑ n < e}
Lemma: qlog-type_wf
∀[q,e:ℚ]. (qlog-type(q;e) ∈ Type)
Lemma: qlog_wf
∀e:{e:ℚ| 0 < e} . ∀q:{q:ℚ| (0 ≤ q) ∧ q < 1} . (qlog(q;e) ∈ qlog-type(q;e))
Lemma: qsum-non-neg
∀[j:ℕ]. ∀[f:ℕj ⟶ ℚ]. 0 ≤ Σ0 ≤ n < j. f[n] supposing ∀n:ℕj. (0 ≤ f[n])
Lemma: qsum-non-neg2
∀[i,j:ℤ]. ∀[f:{i..j-} ⟶ ℚ]. 0 ≤ Σi ≤ n < j. f[n] supposing ∀n:{i..j-}. (0 ≤ f[n])
Lemma: qsum-subsequence-qle
∀[f:ℕ ⟶ ℚ]
∀[k:ℕ]. ∀[g:ℕk + 1 ⟶ ℕ]. Σ0 ≤ i < k. f[g i] ≤ Σ0 ≤ i < g k. f[i] supposing ∀n:ℕk + 1. ∀i:ℕn. g i < g n
supposing ∀n:ℕ. (0 ≤ f[n])
Lemma: q-not-limit-zero-diverges
∀f:ℕ ⟶ ℚ
(∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. ((n ≤ m) ∧ (q ≤ f[m]))))) ⇒ (∀B:ℚ. ∃n:ℕ. (B ≤ Σ0 ≤ i < n. f[i]))
supposing ∀n:ℕ. (0 ≤ f[n])
Lemma: q-not-limit-zero-diverges-2
∀f:ℕ+ ⟶ ℚ
(∃q:ℚ. (0 < q ∧ (∀n:ℕ. ∃m:ℕ. (n < m ∧ (q ≤ f[m]))))) ⇒ (∀B:ℚ. ∃n:ℕ. (B ≤ Σ1 ≤ i < n. f[i]))
supposing ∀n:ℕ+. (0 ≤ f[n])
Lemma: q-geometric-series-converges
∀a:{a:ℚ| |a| < 1} . ∀e:{e:ℚ| 0 < e ∧ (e ≤ 1)} . ∃n:ℕ. ∀m:ℕ. ((n ≤ m) ⇒ |Σ0 ≤ i < m. a ↑ i - (1/1 - a)| < e)
Lemma: q-min-exists
∀as:ℚ List. ∃a:ℚ. ((a ∈ as) supposing ¬↑null(as) ∧ (∀a'∈as.a ≤ a'))
Lemma: q-max-exists
∀as:ℚ List. ∃a:ℚ. ((a ∈ as) supposing ¬↑null(as) ∧ (∀a'∈as.a' ≤ a))
Definition: q-linear
q-linear(k;i.X[i];y) == X[0] + Σ0 ≤ j < k. X[j + 1] * y[j]
Lemma: q-linear_wf
∀[k:ℕ]. ∀[X:ℕ ⟶ ℚ]. ∀[y:ℚ List]. q-linear(k;j.X[j];y) ∈ ℚ supposing k ≤ ||y||
Lemma: q-linear-base
∀[X:ℕ ⟶ ℚ]. ∀[y:ℚ List]. (q-linear(0;j.X[j];y) = X[0] ∈ ℚ)
Lemma: q-linear-unroll
∀[k:ℕ+]. ∀[X:ℕ ⟶ ℚ]. ∀[y:ℚ List].
q-linear(k;j.X[j];y) = (q-linear(k - 1;j.X[j];y) + (X[k] * y[k - 1])) ∈ ℚ supposing k ≤ ||y||
Lemma: q-linear-sum
∀[X,Y:ℕ ⟶ ℚ]. ∀[k:ℕ]. ∀[y:ℚ List].
q-linear(k;j.X[j] + Y[j];y) = (q-linear(k;j.X[j];y) + q-linear(k;j.Y[j];y)) ∈ ℚ supposing k ≤ ||y||
Lemma: q-linear-times
∀[X:ℕ ⟶ ℚ]. ∀[a:ℚ]. ∀[k:ℕ]. ∀[y:ℚ List]. q-linear(k;j.a * X[j];y) = (a * q-linear(k;j.X[j];y)) ∈ ℚ supposing k ≤ ||y||
Lemma: q-linear-equal
∀[k:ℕ]. ∀[X:ℕ ⟶ ℚ]. ∀[y,z:ℚ List].
(q-linear(k;j.X[j];y) = q-linear(k;j.X[j];z) ∈ ℚ) supposing
((∀i:ℕk. (y[i] = z[i] ∈ ℚ)) and
(k ≤ ||z||) and
(k ≤ ||y||))
Definition: q-rel
q-rel(r;x) == if (r =z 0) then 0 = x ∈ ℚ if (r =z 1) then 0 ≤ x else 0 < x fi
Lemma: q-rel_wf
∀[r:ℤ]. ∀[x:ℚ]. (q-rel(r;x) ∈ ℙ)
Definition: q-rel-decider
q-rel-decider(r;x) ==
if ((r =z 0) ∧b qeq(0;x)) ∨b((r =z 1) ∧b (qeq(0;x) ∨bqpositive(x))) ∨b(((¬b(r =z 0)) ∧b (¬b(r =z 1))) ∧b qpositive(x))
then inl ⋅
else inr (λx.⋅)
fi
Lemma: q-rel-decider_wf
∀r:ℤ. ∀x:ℚ. (q-rel-decider(r;x) ∈ Dec(q-rel(r;x)))
Lemma: decidable__q-rel
∀r:ℤ. ∀x:ℚ. Dec(q-rel(r;x))
Definition: q-rel-lub
q-rel-lub(r1;r2) == if (r1 =z 0) then r2 if (r2 =z 0) then r1 if (r1 =z 1) ∧b (r2 =z 1) then 1 else 2 fi
Lemma: q-rel-lub_wf
∀[r1,r2:ℤ]. (q-rel-lub(r1;r2) ∈ ℤ)
Lemma: q-constraint-times
∀[x:ℕ ⟶ ℚ]. ∀[r:ℤ]. ∀[a:ℚ]. ∀[k:ℕ]. ∀[y:ℚ List].
(q-rel(r;q-linear(k;j.a * (x j);y))) supposing
(q-rel(r;q-linear(k;j.x j;y)) and
((r = 0 ∈ ℤ) ∨ 0 < a ∨ ((0 ≤ a) ∧ (r = 1 ∈ ℤ))) and
(k ≤ ||y||))
Lemma: q-constraint-sum
∀[x,x':ℕ ⟶ ℚ]. ∀[r1,r2:ℤ]. ∀[k:ℕ]. ∀[y:ℚ List].
(q-rel(q-rel-lub(r1;r2);q-linear(k;j.(x j) + (x' j);y))) supposing
(q-rel(r2;q-linear(k;j.x' j;y)) and
q-rel(r1;q-linear(k;j.x j;y)) and
(k ≤ ||y||))
Lemma: q-constraint-zero
∀[x:ℕ ⟶ ℚ]. ∀[r:ℤ]. ∀[k:ℕ+]. ∀[y:ℚ List].
(uiff(q-rel(r;q-linear(k;j.x j;y));q-rel(r;q-linear(k - 1;j.x j;y)))) supposing (((x k) = 0 ∈ ℚ) and (k ≤ ||y||))
Lemma: q-constraint-positive
∀[x:ℕ ⟶ ℚ]. ∀[r:ℤ]. ∀[k:ℕ+]. ∀[y:ℚ List].
(uiff(q-rel(r;q-linear(k;j.x j;y));q-rel(r;y[k - 1] + ((1/x k) * q-linear(k - 1;j.x j;y))))) supposing
(0 < x k and
(k ≤ ||y||))
Lemma: q-constraint-negative
∀[x:ℕ ⟶ ℚ]. ∀[r:ℤ]. ∀[k:ℕ+]. ∀[y:ℚ List].
(uiff(q-rel(r;q-linear(k;j.x j;y));q-rel(r;-(y[k - 1]) + ((-1/x k) * q-linear(k - 1;j.x j;y))))) supposing
(x k < 0 and
(k ≤ ||y||))
Definition: q-constraints
q-constraints(k;A;y) == (||y|| = k ∈ ℤ) c∧ (∀xr∈A.q-rel(snd(xr);q-linear(k;j.(fst(xr)) j;y)))
Lemma: q-constraints_wf
∀[A:(ℕ ⟶ ℚ × ℤ) List]. ∀[k:ℕ]. ∀[y:ℚ List]. (q-constraints(k;A;y) ∈ ℙ)
Lemma: product-map
∀[A,B,C:Type].
∀as:A List. ∀bs:B List. ∀F:A ⟶ B ⟶ C. ∃cs:C List. ∀c:C. ((c ∈ cs) ⇐⇒ (∃a∈as. (∃b∈bs. c = (F a b) ∈ C)))
Lemma: average-qbetween
∀[a,b:ℚ]. a ≤ (a + b/2) ≤ b supposing a ≤ b
Lemma: average-q-between
∀[a,b:ℚ]. a < (a + b/2) < b supposing a < b
Definition: qdot
qdot(as;bs) == Σ0 ≤ i < dimension(as). as[i] * bs[i]
Definition: qv-dim
dimension(as) == ||as||
Lemma: qv-dim_wf
∀[as:Top List]. (dimension(as) ∈ ℕ)
Lemma: qdot_wf
∀[as,bs:ℚ List]. qdot(as;bs) ∈ ℚ supposing dimension(as) = dimension(bs) ∈ ℤ
Definition: qv-add
qv-add(as;bs) == fix((λqv-add,as,bs. if null(as) then as else [hd(as) + hd(bs) / (qv-add tl(as) tl(bs))] fi )) as bs
Lemma: qv-add_wf
∀[as,bs:ℚ List]. qv-add(as;bs) ∈ ℚ List supposing dimension(as) = dimension(bs) ∈ ℤ
Lemma: select-qv-add
∀[as,bs:Top List]. ∀[i:ℕdimension(as)]. (qv-add(as;bs)[i] ~ as[i] + bs[i]) supposing dimension(as) = dimension(bs) ∈ ℤ
Lemma: dim-qv-add
∀[as,bs:Top List]. dimension(qv-add(as;bs)) ~ dimension(as) supposing dimension(as) = dimension(bs) ∈ ℤ
Definition: qv-mul
qv-mul(r;bs) == map(λb.(r * b);bs)
Lemma: qv-mul_wf
∀[r:ℚ]. ∀[bs:ℚ List]. (qv-mul(r;bs) ∈ ℚ List)
Lemma: select-qv-mul
∀[as:Top List]. ∀[r:Top]. ∀[i:ℕdimension(as)]. (qv-mul(r;as)[i] ~ r * as[i])
Lemma: dim-qv-mul
∀[as:Top List]. ∀[r:Top]. (dimension(qv-mul(r;as)) ~ dimension(as))
Lemma: qdot-linear
∀[as,bs,cs:ℚ List].
qdot(as;qv-add(bs;cs)) = (qdot(as;bs) + qdot(as;cs)) ∈ ℚ
supposing (dimension(as) = dimension(bs) ∈ ℤ) ∧ (dimension(as) = dimension(cs) ∈ ℤ)
Lemma: qdot-linear2
∀[as,bs:ℚ List]. ∀[r:ℚ]. qdot(as;qv-mul(r;bs)) = (r * qdot(as;bs)) ∈ ℚ supposing dimension(as) = dimension(bs) ∈ ℤ
Definition: qv-convex
qv-convex(p.S[p]) ==
∀p,q:ℚ List.
((dimension(p) = dimension(q) ∈ ℤ)
⇒ S[p]
⇒ S[q]
⇒ (∀t:ℚ. ((0 ≤ t) ⇒ (t ≤ 1) ⇒ S[qv-add(qv-mul(t;p);qv-mul(1 - t;q))])))
Lemma: qv-convex_wf
∀[S:(ℚ List) ⟶ ℙ]. (qv-convex(p.S[p]) ∈ ℙ)
Lemma: qv-convex-and
∀[S1,S2:(ℚ List) ⟶ ℙ]. (qv-convex(p.S1[p]) ⇒ qv-convex(p.S2[p]) ⇒ qv-convex(p.S1[p] ∧ S2[p]))
Lemma: qv-convex-all
∀[T:Type]. ∀[S:T ⟶ (ℚ List) ⟶ ℙ]. ((∀x:T. qv-convex(p.S[x;p])) ⇒ qv-convex(p.∀x:T. S[x;p]))
Lemma: qv-convex-upper-half
∀[r:ℚ]. ∀[v:ℚ List]. qv-convex(p.(dimension(p) = dimension(v) ∈ ℤ) ∧ (r ≤ qdot(v;p)))
Lemma: qv-convex-lower-half
∀[r:ℚ]. ∀[v:ℚ List]. qv-convex(p.(dimension(p) = dimension(v) ∈ ℤ) ∧ (qdot(v;p) ≤ r))
Definition: qvn
ℚ^n == {v:ℚ List| dimension(v) = n ∈ ℤ}
Lemma: qvn_wf
∀[n:ℕ]. (ℚ^n ∈ Type)
Definition: q-linear-form
q-linear-form(n) == ℚ^n × ℚ
Lemma: q-linear-form_wf
∀[n:ℕ]. (q-linear-form(n) ∈ Type)
Definition: qv-lower
qv-lower(lf;p) == let v,r = lf in qdot(v;p) ≤ r
Lemma: qv-lower_wf
∀[n:ℕ]. ∀[lf:q-linear-form(n)]. ∀[p:ℚ^n]. (qv-lower(lf;p) ∈ ℙ)
Definition: qv-constrained
qv-constrained(S;p) == (∀lf∈S.qv-lower(lf;p))
Lemma: qv-constrained_wf
∀[n:ℕ]. ∀[S:q-linear-form(n) List]. ∀[p:ℚ^n]. (qv-constrained(S;p) ∈ ℙ)
Definition: qlf-val
qlf-val(lf;p) == let v,r = lf in qdot(v;p) + r
Lemma: qlf-val_wf
∀[n:ℕ]. ∀[lf:q-linear-form(n)]. ∀[p:ℚ^n]. (qlf-val(lf;p) ∈ ℚ)
Definition: qlfs-min-val
qlfs-min-val(lfs;p) == qmin-list(map(λlf.qlf-val(lf;p);lfs))
Lemma: qlfs-min-val_wf
∀[n:ℕ]. ∀[lfs:q-linear-form(n) List]. ∀[p:ℚ^n]. qlfs-min-val(lfs;p) ∈ ℚ supposing 0 < ||lfs||
Definition: qlfs-max-val
qlfs-max-val(lfs;p) == qmax-list(map(λlf.qlf-val(lf;p);lfs))
Lemma: qlfs-max-val_wf
∀[n:ℕ]. ∀[lfs:q-linear-form(n) List]. ∀[p:ℚ^n]. qlfs-max-val(lfs;p) ∈ ℚ supposing 0 < ||lfs||
Definition: qv-constrained-no-sup
qv-constrained-no-sup(n;S;lfs) ==
(∃p:ℚ^n. qv-constrained(S;p))
∧ (∀p:ℚ^n. (qv-constrained(S;p) ⇒ (∃q:ℚ^n. (qv-constrained(S;q) ∧ qlfs-min-val(lfs;p) < qlfs-min-val(lfs;q)))))
Lemma: qv-constrained-no-sup_wf
∀[n:ℕ]. ∀[S,lfs:q-linear-form(n) List]. qv-constrained-no-sup(n;S;lfs) ∈ ℙ supposing 0 < ||lfs||
Definition: qv-constrained-no-inf
qv-constrained-no-inf(n;S;lfs) ==
(∃p:ℚ^n. qv-constrained(S;p))
∧ (∀p:ℚ^n. (qv-constrained(S;p) ⇒ (∃q:ℚ^n. (qv-constrained(S;q) ∧ qlfs-max-val(lfs;q) < qlfs-max-val(lfs;p)))))
Lemma: qv-constrained-no-inf_wf
∀[n:ℕ]. ∀[S,lfs:q-linear-form(n) List]. qv-constrained-no-inf(n;S;lfs) ∈ ℙ supposing 0 < ||lfs||
Definition: qv-constrained-sup
qv-constrained-sup(n;S;lfs;p;r) ==
qv-constrained(S;p)
∧ (qlfs-min-val(lfs;p) = r ∈ ℚ)
∧ (∀q:ℚ^n. (qv-constrained(S;q) ⇒ (qlfs-min-val(lfs;q) ≤ qlfs-min-val(lfs;p))))
Lemma: qv-constrained-sup_wf
∀[n:ℕ]. ∀[S,lfs:q-linear-form(n) List]. ∀[p:ℚ^n]. ∀[r:ℚ]. qv-constrained-sup(n;S;lfs;p;r) ∈ ℙ supposing 0 < ||lfs||
Definition: qv-constrained-inf
qv-constrained-inf(n;S;lfs;p;r) ==
qv-constrained(S;p)
∧ (qlfs-max-val(lfs;p) = r ∈ ℚ)
∧ (∀q:ℚ^n. (qv-constrained(S;q) ⇒ (qlfs-max-val(lfs;p) ≤ qlfs-max-val(lfs;q))))
Lemma: qv-constrained-inf_wf
∀[n:ℕ]. ∀[S,lfs:q-linear-form(n) List]. ∀[p:ℚ^n]. ∀[r:ℚ]. qv-constrained-inf(n;S;lfs;p;r) ∈ ℙ supposing 0 < ||lfs||
Definition: select?
as[i]?a == if i <z ||as|| then as[i] else a fi
Lemma: select?_wf
∀[A:Type]. ∀[as:A List]. ∀[a:A]. ∀[i:ℕ]. (as[i]?a ∈ A)
Definition: normalize-constraint
normalize-constraint(k;p) == let f,r = p in eval r = r in let as ⟵ map(f;upto(k)) in <λn.as[n]?f n, r>
Lemma: normalize-constraint_wf
∀[k:ℕ]. ∀[A:ℕ ⟶ ℚ × ℤ]. (normalize-constraint(k;A) ∈ ℕ ⟶ ℚ × ℤ)
Lemma: normalize-constraint-eq
∀[k:ℕ]. ∀[A:ℕ ⟶ ℚ × ℤ]. (normalize-constraint(k;A) = A ∈ (ℕ ⟶ ℚ × ℤ))
Definition: normalize-constraints
normalize-constraints(k;A) == let A' ⟵ map(λp.normalize-constraint(k;p);A) in A'
Lemma: normalize-constraints_wf
∀[k:ℕ]. ∀[A:(ℕ ⟶ ℚ × ℤ) List]. (normalize-constraints(k;A) ∈ (ℕ ⟶ ℚ × ℤ) List)
Lemma: normalize-constraints-eq
∀[k:ℕ]. ∀[A:(ℕ ⟶ ℚ × ℤ) List]. (normalize-constraints(k;A) = A ∈ ((ℕ ⟶ ℚ × ℤ) List))
Lemma: test-recursion-extract
∀k:ℕ. ∀f:ℕ ⟶ ℚ. ((∃n:ℕk. ((f n) = 0 ∈ ℚ)) ∨ True)
Lemma: decidable__q-constraints
∀k:ℕ. ∀A:(ℕ ⟶ ℚ × ℤ) List. Dec(∃y:ℚ List [q-constraints(k;A;y)])
Definition: q-constraints-decider
q-constraints-decider ==
λk.letrec rec(k)=λA.eval z = evalall(A) in
if if k=0 then inl Ax else (inr (λx.Ax) )
then λA.if l-all-decider() A (λxr.q-rel-decider(let x,y = xr in y;let x,y = xr in x 0))
then inl []
else inr (λ%6.Ax)
fi
else λA.case l-exists-decider() evalall(A)
(λxr.case if let x,y = xr in y=0 then inl Ax else (inr (λx.Ax) )
of inl(%2) =>
case if if qeq(let x,y = xr in x k;0) then inl Ax else inr (λx.Ax) fi
then inr (λ%.Ax)
else inl (λ%.Ax)
fi
of inl(%3) =>
inl <%2, %3>
| inr(%4) =>
inr (λ%.let %5,%6 = %
in Ax)
| inr(%3) =>
inr (λ%.let %4,%5 = %
in Ax) )
of inl(%@0) =>
let xr,%10 = let i,%1 = %@0
in <evalall(A)[i], <i, Ax, Ax>, %1>
in let x1,x2 = xr
in let %11,%13,%14 = %10 in
case rec (k - 1)
map(λxr.let x,r = xr
in <λj.((x j) + -((x k/x1 k) * (x1 j))), r>;evalall(A))
of inl(%15) =>
inl (%15 @ [q-linear(k - 1;j.(-1/x1 k) * (x1 j);%15)])
| inr(%16) =>
inr (λ%.Ax)
| inr(%8) =>
case rec (k - 1)
eval A' = evalall(map(λp.let f,r = p
in eval r = r in
eval as = evalall(map(f;[0, k))) in
<λn.if if (n) < (||as||) then inl Ax else (inr Ax )
then as[n]
else f n
fi
, r
>;filter(λa.qeq(let x,y = a in x k;0);evalall(A))
@ concat(map(λa.map(λb.<λj.(((let x,y = a in x k)
* (let x,y = b in x j))
+ -((let x,y = b in x k)
* (let x,y = a in x j)))
, q-rel-lub(let x,y = a
in y;let x,y = b
in y)
>;filter(λc.q_less(let x,y = c
in x
k;0);evalall(A)));
filter(λb.q_less(0;let x,y = b in x k);
evalall(A)))))) in
A'
of inl(%) =>
inl case l-exists-decider() evalall(A)
(λa.if qpositive((let x,y = a in x k) + -(0))
then inl Ax
else inr (λx.Ax)
fi )
of inl(%@0) =>
case l-exists-decider() evalall(A)
(λa.if qpositive(0 + -(let x,y = a in x k)) then inl Ax else inr (λx.Ax) fi )
of inl(%17) =>
let b,%28,%30,%31 = let a,%25,%26 = if if if map(λc.(-((1/let x,y = c in x k))
* q-linear(k - 1;j.let x,y = c
in x
j;%));
filter(λc.q_less(let x,y = c
in x
k;0);
evalall(A))) = Ax then inl Ax
otherwise inr Ax
then inl Ax
else inr Ax
fi
then <0, Ax, λi.Ax>
else let u,v = map(λc.(-((1/let x,y = c in x k))
* q-linear(k - 1;j.let x,y = c in x j;%));
filter(λc.q_less(let x,y = c in x k;0);evalall(A)))
in <accumulate (with value x and list item y):
if eval r' = evalall(x) in
eval s' = evalall(y) in
qpositive(s' + -(r')) ∨bqeq(r';s')
then x
else y
fi
over list:
tl([u / v])
with starting value:
hd([u / v]))
, if if if [u / v] = Ax then inl Ax otherwise inr Ax
then inl Ax
else inr Ax
fi
then Ax
else let u,v = [u / v]
in rec-case(v) of
[] => λ-any.<0, Ax, Ax>
a::L =>
r.λu@0.if if eval r' = evalall(u@0) in
eval s' = evalall(a) in
qpositive(s' + -(r')) ∨bqeq(r';s')
then inl Ax
if if eval r' = evalall(u@0) in
eval s' = evalall(a) in
qpositive(s' + -(r')) ∨bqeq(r';s')
then inl Ax
else inr Ax
fi
then Ax
else inr Ax
fi
then case case case let i,%2,%3 = r u@0 in
if case if i=0 then inl Ax else (inr Ax )
of inl(x) =>
inl x
| inr(x) =>
inr (λx.Ax)
then λ%,%4. (inl Ax)
else λ%,%6. (inr <i - 1, Ax, Ax> )
fi
Ax
Ax
of inl(%9) =>
inl Ax
| inr(%10) =>
inr inr %10
of inl(-any) =>
inl Ax
| inr(-any) =>
inr case -any
of inl(%1) =>
<0, Ax, Ax>
| inr(%2) =>
let i,%4,%5 = %2 in
<i + 1, Ax, Ax>
of inl(%1) =>
<0, Ax, Ax>
| inr(%2) =>
let i,%4,%5 = %2 in
<i + 1, Ax, Ax>
else let i,%4,%5 = r a in
<i + 1, Ax, Ax>
fi
u
fi
, let %7,%8 =
primrec(||[u / v]|| + 1;λn.Ax;
λi,x,n. if if n=(i + 1) - 1 then inl Ax else (inr (λx.Ax) )
then λL,%7,a. if if if L = Ax then inl Ax otherwise inr Ax
then inl Ax
else inr Ax
fi
then Ax
else let u,v = L
in if null(v)
then <λ-any,i. -any, λ-any.(-any 0)>
else let %18,%19 =
let %23,%24 =
let %22,%23 =
x ||v|| v
case case if if (||v||) < (...)
then inl Ax
else (inr ... )
then inr (λ%.Ax)
else inl (λ%.Ax)
fi
of inl(%2) =>
inl <%2, Ax, Ax>
| inr(%3) =>
inr (λ%.let %4,%5 = %
in Ax)
of inl(%13) =>
%13
| inr(%14) =>
Ax
a
in <λ%26.<let %27,%28 = %26
in %27
, let %27,%28 = %26
in %28
>
, λ%26.<let %27,%28 = %26
in %27
, let %27,%28 = %26
in %28
>
>
in <λ%24...., ...>
in ...
fi
fi
else ...
fi )
...
...
...
...
in ...>
fi in
...
in ...
| inr(%18) =>
...
| inr(%17) =>
...
| inr(%16) =>
...
fi
... in
rec(...)
Lemma: decidable__q-constraints-squash
∀k:ℕ. ∀A:(ℕ ⟶ ℚ × ℤ) List. Dec(∃y:ℚ List [q-constraints(k;A;y)])
Lemma: decidable__q-constraints-opt
∀k:ℕ. ∀A:(ℕ ⟶ ℚ × ℤ) List. Dec(∃y:ℚ List [q-constraints(k;A;y)])
Definition: q-sat-constraints
q-sat-constraints(k;A;y) ==
(||y|| = k ∈ ℤ)
c∧ (∀a∈A.let F,r,G = a in
if (r =z 0) then q-linear(k;j.F[j]?0;y) = q-linear(k;j.G[j]?0;y) ∈ ℚ
if (r =z 1) then q-linear(k;j.F[j]?0;y) ≤ q-linear(k;j.G[j]?0;y)
else q-linear(k;j.F[j]?0;y) < q-linear(k;j.G[j]?0;y)
fi )
Lemma: q-sat-constraints_wf
∀[k:ℕ]. ∀[A:(ℚ List × ℤ × (ℚ List)) List]. ∀[y:ℚ List]. (q-sat-constraints(k;A;y) ∈ ℙ)
Lemma: decidable__q-constraints2
∀k:ℕ. ∀A:(ℚ List × ℤ × (ℚ List)) List. Dec(∃y:ℚ List [q-sat-constraints(k;A;y)])
Lemma: q-triangle-inequality
∀[r,s:ℚ]. (|r + s| ≤ (|r| + |s|))
Lemma: q-triangle-inequality2
∀[x,y,z:ℚ]. (|x - z| ≤ (|x - y| + |y - z|))
Lemma: q-triangle-inequality3
∀[x,y,a,b:ℚ]. (|x + y| ≤ (a + b)) supposing ((|y| ≤ b) and (|x| ≤ a))
Lemma: implies-qle
∀[a,b:ℚ]. a ≤ b supposing ∀n:ℕ+. (a ≤ (b + (1/n)))
Lemma: implies-qle2
∀[a,b:ℚ]. a ≤ b supposing ∀e:ℚ. (0 < e ⇒ (a ≤ (b + e)))
Lemma: qabs-qsum-qle
∀[a,b:ℤ]. ∀[E:{a..b-} ⟶ ℚ]. ∀[x:ℚ].
|Σa ≤ j < b. E[j]| ≤ ((b - a) * x) supposing (a ≤ b) ∧ (∀j:ℤ. ((a ≤ j) ⇒ j < b ⇒ (|E[j]| ≤ x)))
Lemma: qexp-difference-bound
∀[a,b:ℚ]. ∀n:ℕ+. (|a ↑ n - b ↑ n| ≤ (|a - b| * n * qmax(|a|;|b|) ↑ n - 1))
Lemma: test23
∀[a,b,c:ℚ]. (False) supposing (0 < c and ((b + c) ≤ a) and ((a + c) ≤ b))
Definition: test_case1
test_case1() == case TERMOF{decidable__q-constraints:o, 1:l} 1 [<λj.if j <z 2 then [1; 2][j] else 0 fi , 0>] of inl(y) \000C=> inl y | inr(x) => inr "not"
Lemma: test_case1_wf
test_case1() ∈ ℚ List + Atom
Lemma: int_nzero-rational
∀[z:ℤ-o]. (¬(z = 0 ∈ ℚ))
Definition: rat-int-part
rat-int-part(q) ==
if q is an integer then <q, 0>
else let n,m = q
in eval a = n ÷ m in
eval b = n rem m in
if (b =z 0) then <a, 0>
if 0 <z m then if 0 ≤z n then <a, (b/m)> else <a - 1, (b + m/m)> fi
if 0 ≤z n then <a - 1, (b + m/m)>
else <a, (b/m)>
fi
Lemma: rat-int-part_wf
∀q:ℤ ⋃ (ℤ × ℤ-o). (rat-int-part(q) ∈ {p:ℤ × {r:ℚ| (0 ≤ r) ∧ r < 1} | let x,r = p in q = (x + r) ∈ ℚ} )
Lemma: rat-int-part_wf2
∀q:ℚ. (rat-int-part(q) ∈ {p:ℤ × {r:ℚ| (0 ≤ r) ∧ r < 1} | let x,r = p in q = (x + r) ∈ ℚ} )
Definition: rat-int-bound
rat-int-bound(q) == let n,r = rat-int-part(q) in if qeq(r;0) then n else n + 1 fi
Lemma: rat-int-bound_wf
∀[q:ℚ]. (rat-int-bound(q) ∈ {n:ℤ| n - 1 < q ∧ (q ≤ n)} )
Definition: q-floor
[r] == fst(rat-int-part(r))
Lemma: q-floor_wf
∀[r:ℚ]. ([r] ∈ ℤ)
Lemma: q-floor-property
∀[r:ℚ]. (([r] ≤ r) ∧ r < [r] + 1)
Definition: q-ceil
q-ceil(r) == rat-int-bound(r)
Lemma: q-ceil_wf
∀[r:ℚ]. (q-ceil(r) ∈ ℤ)
Lemma: q-ceil-property
∀[r:ℚ]. (q-ceil(r) - 1 < r ∧ (r ≤ q-ceil(r)))
Lemma: q-ceil_functionality
∀[a,b:ℚ]. q-ceil(a) ≤ q-ceil(b) supposing a ≤ b
Definition: qtruncate
qtruncate(q;N) == (q-ceil(q * N)/N)
Lemma: qtruncate_wf
∀[q:ℚ]. ∀[N:ℕ+]. (qtruncate(q;N) ∈ ℚ)
Lemma: qtruncate-property
∀[q:ℚ]. ∀[N:ℕ+]. (qtruncate(q;N) - (1/N) < q ∧ (q ≤ qtruncate(q;N)))
Lemma: qtruncate_functionality
∀[a,b:ℚ]. ∀[N:ℕ+]. qtruncate(a;N) ≤ qtruncate(b;N) supposing a ≤ b
Lemma: qroot
∀k:{2...}. ∀a:{a:ℚ| (0 ≤ a) ∨ (↑isOdd(k))} . ∀n:ℕ+. (∃q:ℚ [((0 ≤ a ⇐⇒ 0 ≤ q) ∧ |q ↑ k - a| < (1/n))])
Lemma: qroot-ext
∀k:{2...}. ∀a:{a:ℚ| (0 ≤ a) ∨ (↑isOdd(k))} . ∀n:ℕ+. (∃q:ℚ [((0 ≤ a ⇐⇒ 0 ≤ q) ∧ |q ↑ k - a| < (1/n))])
Definition: approx-root
k-th root(q) within 1/err == TERMOF{qroot-ext:o, 1:l} k q err
Lemma: approx-root_wf
∀k:{2...}. ∀a:{a:ℚ| (0 ≤ a) ∨ (↑isOdd(k))} . ∀n:ℕ+. (k-th root(a) within 1/n ∈ ℚ)
Lemma: approx-root-property
∀k:{2...}. ∀a:{a:ℚ| (0 ≤ a) ∨ (↑isOdd(k))} . ∀n:ℕ+.
((0 ≤ a ⇐⇒ 0 ≤ k-th root(a) within 1/n) ∧ |k-th root(a) within 1/n ↑ k - a| < (1/n))
Definition: nqsqrt
nqsqrt(err;q;r) == Y (λnqsqrt,r. eval s = (r + (q/r)/2) in if q_less((s * s) - q;err) then s else nqsqrt s fi ) r
Lemma: square-between-lemma1
∀n:ℕ+. ∀k:ℕn - 1. (∃q:ℚ [(((k/n) ≤ (q * q)) ∧ q * q < (k + 1/n) ∧ (0 ≤ q))])
Lemma: square-between-lemma2
∀n:ℕ+. ∀k:ℕ. (∃q:ℚ [(((k/n) ≤ (q * q)) ∧ q * q < (k + 1/n) ∧ (0 ≤ q))])
Lemma: square-between-lemma3
∀a:ℕ. ∀b,n:ℕ+. (∃q:ℚ [((a/b) - (1/n) < q * q ∧ q * q < (a/b) + (1/n) ∧ (0 ≤ q))])
Lemma: approximate-qsqrt
∀a:{a:ℚ| 0 ≤ a} . ∀n:ℕ+. (∃q:ℚ [((0 ≤ q) ∧ |(q * q) - a| < (1/n))])
Lemma: approximate-qsqrt-ext
∀a:{a:ℚ| 0 ≤ a} . ∀n:ℕ+. (∃q:ℚ [((0 ≤ q) ∧ |(q * q) - a| < (1/n))])
Lemma: square-between
∀a:{a:ℚ| 0 ≤ a} . ∀b:{b:ℚ| a < b} . (∃r:ℚ [(a < r * r < b ∧ 0 < r)])
Definition: qsqrt
qsqrt(r;n) == TERMOF{approximate-qsqrt-ext:o, 1:l} r n
Lemma: qsqrt_wf
∀[r:{r:ℚ| 0 ≤ r} ]. ∀[n:ℕ+]. (qsqrt(r;n) ∈ ℚ)
Lemma: qsqrt-nonneg
∀[r:{r:ℚ| 0 ≤ r} ]. ∀[n:ℕ+]. (0 ≤ qsqrt(r;n))
Lemma: qsqrt-property
∀[r:{r:ℚ| 0 ≤ r} ]. ∀[n:ℕ+]. |(qsqrt(r;n) * qsqrt(r;n)) - r| < (1/n)
Definition: qsqrt2
qsqrt2(r;n) == let e ⟵ (1/n) in nqsqrt(e;r;1)
Definition: nqsqrt3
nqsqrt3(n;q;r) ==
eval n' = 10 * n in
Y
(λnqsqrt3,r. eval s = (r + (q/r)/2) in
let a,b = qrep(s)
in eval a' = (a * n') ÷ b in
let x ⟵ (a'/n')
in if q_less((x * x) - q;(1/n)) then x else nqsqrt3 <a', n'> fi )
r
Definition: qsqrt-normal
qsqrt-normal(r;n) == let e,d = TERMOF{approximate-qsqrt-ext:o, 1:l} r n in <(e * 10 * n) ÷ d, 10 * n>
Definition: isqrt2
isqrt2(x) ==
letrec sqrt(i)=if i=0 then 0 else eval r = (sqrt (i ÷ 4)) * 2 in if (r * (r + 2)) < (i) then r + 1 else r in sqrt x
Definition: qsqrt-normal2
qsqrt-normal2(a;n) ==
let v1,v2 = qrep(a)
in eval n' = 10^(log(10;v1 ÷ v2) + 1) * n in
<isqrt2((v1 * n' * n') ÷ v2), n'>
Lemma: integer-part-decomp
∀q:ℚ. (∃p:ℤ × {r:ℚ| (0 ≤ r) ∧ r < 1} [let x,r = p in q = (x + r) ∈ ℚ])
Definition: int_part_decomp
int_part_decomp(q) == rat-int-part(q)
Lemma: int_part_decomp_wf
∀[q:ℚ]. (int_part_decomp(q) ∈ {p:ℤ × ℚ| (0 ≤ (snd(p))) ∧ snd(p) < 1 ∧ (q = ((fst(p)) + (snd(p))) ∈ ℚ)} )
Definition: integer-part
integer-part(q) == fst(int_part_decomp(q))
Lemma: integer-part_wf
∀q:ℚ. (integer-part(q) ∈ ℤ)
Definition: fractional-part
fractional-part(q) == snd(int_part_decomp(q))
Lemma: fractional-part_wf
∀q:ℚ. (fractional-part(q) ∈ {r:ℚ| (0 ≤ r) ∧ r < 1} )
Lemma: integer-fractional-parts
∀q:ℚ. (q = (integer-part(q) + fractional-part(q)) ∈ ℚ)
Lemma: rational-truncate1
∀q:ℚ. ∀e:{e:ℚ| 0 < e ∧ e < 1} . (∃p:ℤ × ℕ+ [((|q - (fst(p)/snd(p))| ≤ e) ∧ (((snd(p)) * e) ≤ 2))])
Lemma: rational-truncate
∀q:ℚ. ∀e:{e:ℚ| 0 < e} . (∃q':ℚ [(|q - q'| ≤ e)])
Definition: truncate-rational
truncate-rational(q;e) == case q_less(e;1) of inl() => eval b = rat-int-bound((1/e)) in <integer-part(q * b), b> | inr(\000C) => integer-part(q)
Lemma: truncate-rational_wf
∀q:ℚ. ∀e:{e:ℚ| 0 < e} . (truncate-rational(q;e) ∈ ∃q':ℚ [(|q - q'| ≤ e)])
Lemma: truncate-rational-property
∀q:ℚ. ∀e:{e:ℚ| 0 < e} . ((|q - truncate-rational(q;e)| ≤ e) ∧ (|truncate-rational(q;e) - q| ≤ e))
Lemma: fractional-part-rep
∀r:{r:ℚ| (0 ≤ r) ∧ r < 1} . ∃a,b:ℕ. ((0 ≤ a) ∧ a < b ∧ (r = (a/b) ∈ ℚ))
Lemma: egyptian-fraction
∀r:{r:ℚ| (0 ≤ r) ∧ r < 1} . (∃L:ℕ+ List [(r = Σ0 ≤ i < ||L||. (1/L[i]) ∈ ℚ)])
Lemma: egyptian-number
∀q:ℚ. (∃p:ℤ × (ℕ+ List) [let x,L = p in q = (x + Σ0 ≤ i < ||L||. (1/L[i])) ∈ ℚ])
Definition: egyptian
egyptian(q) == norm-pair(λx.x;norm-list(λx.x)) (TERMOF{egyptian-number:o, 1:l} q)
Lemma: egyptian_wf
∀q:ℚ. (egyptian(q) ∈ {p:ℤ × (ℕ+ List)| let x,L = p in q = (x + Σ0 ≤ i < ||L||. (1/L[i])) ∈ ℚ} )
Lemma: int-with-rational-square-root
∀n:ℤ. ∀q:ℚ. (((q * q) = n ∈ ℚ) ⇒ (∃m:ℤ. ((m * m) = n ∈ ℤ)))
Lemma: int-has-rational-square-root
∀n:ℤ. (∃q:ℚ. ((q * q) = n ∈ ℚ) ⇐⇒ ∃m:ℤ. ((m * m) = n ∈ ℤ))
Home
Index