---

Lemma: sqequalIffSqle
∀a,b:Base.  ((a ~ b) ⇒ ((a ≤ b) ∧ (b ≤ a)))

Lemma: not-id-sqle-bottom
¬(λx.x ≤ ⊥)

Lemma: not-btrue-sqle-bottom
¬(tt ≤ ⊥)

Lemma: not_id_sqeq_bottom
¬(λx.x ~ ⊥)

Lemma: not_id_sqle_bottom
¬(λx.x ≤ ⊥)

Lemma: not_has-value_decidable_on_base
¬(∀t:Base. ((t)↓ ∨ (¬(t)↓)))

Lemma: no-excluded-middle
¬(∀P:ℙ. (P ∨ (¬P)))

Lemma: not-not-excluded-middle
∀P:ℙ. (¬¬(P ∨ (¬P)))

Lemma: minimal-not-not-excluded-middle
∀[A,P:ℙ].  (((P ∨ (P ⇒ A)) ⇒ A) ⇒ A)

Lemma: minimal-not-not-excluded-middle-ext
∀[A,P:ℙ].  (((P ∨ (P ⇒ A)) ⇒ A) ⇒ A)

Lemma: double-negation-hyp-elim
∀[P,Q:ℙ].  ((P ⇒ (¬Q)) ⇒ (¬¬P) ⇒ (¬Q))

Lemma: minimal-double-negation-hyp-elim
∀[A,P,Q:ℙ].  ((P ⇒ Q ⇒ A) ⇒ ((P ⇒ A) ⇒ A) ⇒ Q ⇒ A)

Lemma: stable-implies-sq_stable
∀[A:ℙ]. (Stable{A} ⇒ SqStable(A))

Lemma: proof-by-cont-implies-LEM
(∀p:ℙ. ((¬¬p) ⇒ p)) ⇒ (∀p:ℙ. (p ∨ (¬p)))

Definition: id-fun
id-fun(T) ==  x:T ⟶ {y:T| x = y ∈ T} 

Lemma: id-fun_wf
∀[T:Type]. (id-fun(T) ∈ Type)

Definition: sq-id-fun
sq-id-fun(T) ==  x:T ⟶ {y:T| x ~ y} 

Lemma: sq-id-fun_wf
∀[T:Type]. sq-id-fun(T) ∈ Type supposing T ⊆r Base

Definition: norm-pair
norm-pair(Na;Nb) ==  λp.let a,b = p in eval a' = Na a in eval b' = Nb b in   <a', b'>

Lemma: norm-pair_wf
∀[A:Type]. ∀[B:A ⟶ Type].
  (∀[Na:id-fun(A)]. ∀[Nb:⋂a:A. id-fun(B[a])].  (norm-pair(Na;Nb) ∈ id-fun(a:A × B[a]))) supposing 
     ((∀a:A. value-type(B[a])) and 
     value-type(A))

Lemma: norm-pair_wf_sq
∀[A,B:Type].
  (∀[Na:sq-id-fun(A)]. ∀[Nb:sq-id-fun(B)].  (norm-pair(Na;Nb) ∈ sq-id-fun(A × B))) supposing 
     ((B ⊆r Base) and 
     (A ⊆r Base) and 
     value-type(B) and 
     value-type(A))

Definition: norm-fst
norm-fst(N) ==  λp.let a,b = p in eval a' = N a in <a', b>

Lemma: norm-fst_wf
∀[A:Type]. ∀[B:A ⟶ Type].  ∀[N:id-fun(A)]. (norm-fst(N) ∈ id-fun(a:A × B[a])) supposing value-type(A)

Definition: norm-snd
norm-snd(N) ==  λp.let a,b = p in eval b' = N b in <a, b'>

Lemma: norm-snd_wf
∀[A:Type]. ∀[B:A ⟶ Type].  ∀[N:⋂a:A. id-fun(B[a])]. (norm-snd(N) ∈ id-fun(a:A × B[a])) supposing ∀a:A. value-type(B[a])

Definition: norm-union
norm-union(Na;Nb) ==  λu.case u of inl(a) => eval a' = Na a in inl a' | inr(b) => eval b' = Nb b in inr b' 

Lemma: norm-union_wf
∀[A,B:Type].
  (∀[Na:id-fun(A)]. ∀[Nb:id-fun(B)].  (norm-union(Na;Nb) ∈ id-fun(A + B))) supposing (value-type(B) and value-type(A))

Lemma: int_eq-sqle-lemma1
∀[x:Top]. ∀[y:ℤ].  (if x=y then x else ⊥ ≤ x)

Lemma: int_eq-sqle-lemma2
∀[x:Top]. (if x=0 then x else ⊥ ≤ x)

Lemma: atom_eq_sq_normalize
∀[b1,b2,i,j:Top].  (if i=j then b1[i] else b2 fi  ~ if i=j then b1[j] else b2 fi )

Lemma: has-value-monotonic
∀[a,b:Base].  ((b)↓) supposing ((a ≤ b) and (a)↓)

Lemma: not-btrue-sqle-bfalse
¬(tt ≤ ff)

Lemma: not-bfalse-sqle-btrue
¬(ff ≤ tt)

Lemma: spread-ispair-spread
∀[t,B:Top].  (let x,y = t in B[x;y] ~ if t is a pair then let x,y = t in B[x;y] otherwise ⊥)

Lemma: pi12-sqle-spread
∀[t:Top]. ∀[P:Base].  P[fst(t);snd(t)] ≤ let x,y = t in P[x;y] supposing strict4(λx,y,z,w. P[x;y])

Lemma: spread-sqle-pi12
∀[P:Base]
  ∀[t:Top]. (let x,y = t in P[x;y] ≤ P[fst(t);snd(t)]) 
  supposing ∀u,v:Base.  (P[exception(u; v);exception(u; v)] ~ exception(u; v))

Lemma: spread-sq-pi12
∀[t:Top]. ∀[P:Base].  P[fst(t);snd(t)] ~ let x,y = t in P[x;y] supposing strict4(λx,y,z,w. P[x;y])

Definition: primtailrec
primtailrec(n;i;b;f) ==  if (n) < (1)  then b  else eval m = n - 1 in eval j = i + 1 in   primtailrec(m;j;f i b;f)

Lemma: primtailrec-unroll
∀[n:ℤ]. ∀[b,c:Top].  (primtailrec(n;0;b;c) ~ if n <z 1 then b else c (n - 1) primtailrec(n - 1;0;b;c) fi )

Definition: primrec
primrec(n;b;c) ==  primtailrec(n;0;b;c)

Lemma: primrec-unroll
∀[n:ℤ]. ∀[b,c:Top].  (primrec(n;b;c) ~ if n <z 1 then b else c (n - 1) primrec(n - 1;b;c) fi )

Lemma: primrec-wf-upper
∀[k:ℤ]. ∀[P:{k...} ⟶ ℙ]. ∀[b:P[k]]. ∀[s:∀n:{k...}. (P[n] ⇒ P[n + 1])]. ∀[n:{k...}].
  (primrec(n - k;b;λi,x. (s (i + k) x)) ∈ P[n])

Lemma: primrec-wf-nat-plus
∀[P:ℕ+ ⟶ ℙ]. ∀[b:P[1]]. ∀[s:∀n:ℕ+. (P[n] ⇒ P[n + 1])]. ∀[n:ℕ+].  (primrec(n - 1;b;λi,x. (s (i + 1) x)) ∈ P[n])

Lemma: primrec-wf
∀[P:ℕ ⟶ ℙ]. ∀[b:P[0]]. ∀[s:∀n:ℕ. (P[n] ⇒ P[n + 1])]. ∀[n:ℕ].  (primrec(n;b;s) ∈ P[n])

Lemma: primrec-wf-int_seg
∀[a,b:ℤ].
  ∀[P:{a..b-} ⟶ ℙ]. ∀[init:P[a]]. ∀[s:∀n:ℕb - 1 - a. (P[a + n] ⇒ P[a + n + 1])]. ∀[n:{a..b-}].
    (primrec(n - a;init;s) ∈ P[n]) 
  supposing a < b

Lemma: primrec-wf-nsub
∀[b:ℕ+]. ∀[P:ℕb ⟶ ℙ]. ∀[init:P[0]]. ∀[s:∀n:ℕb - 1. (P[n] ⇒ P[n + 1])]. ∀[n:ℕb].  (primrec(n;init;s) ∈ P[n])

Lemma: primrec-wf2
∀[P:ℕ ⟶ ℙ]. ∀[b:P[0]]. ∀[s:∀n:{n:ℤ| 0 < n} . (P[n - 1] ⇒ P[n])]. ∀[n:ℕ].  (primrec(n;b;λi,x. (s (i + 1) x)) ∈ P[n])

Lemma: primrec_wf
∀[T:Type]. ∀[n:ℕ]. ∀[b:T]. ∀[c:ℕn ⟶ T ⟶ T].  (primrec(n;b;c) ∈ T)

Lemma: primrec0_lemma
∀c,b:Top.  (primrec(0;b;c) ~ b)

Lemma: primrec1_lemma
∀c,b:Top.  (primrec(1;b;c) ~ c 0 b)

Lemma: primrec-unroll-1
∀[n:{n:ℤ| 0 < n} ]. ∀[b,c:Top].  (primrec(n;b;c) ~ c (n - 1) primrec(n - 1;b;c))

Lemma: primrec-unroll+1
∀[n:{n:ℤ| 0 < n} ]. ∀[b,c:Top].  (primrec(n + 1;b;c) ~ c n primrec(n;b;c))

Lemma: primrec_add
∀[T:Type]. ∀[n,m:ℕ]. ∀[b:T]. ∀[c:ℕn + m ⟶ T ⟶ T].  (primrec(n + m;b;c) ~ primrec(n;primrec(m;b;c);λi,t. (c (i + m) t))\000C)

Lemma: simple-primrec-add
∀[b,F:Top]. ∀[n,m:ℕ].  (primrec(n + m;b;λi.F) ~ primrec(n;primrec(m;b;λi.F);λi.F))

Lemma: primrec-as-fix
∀[n,b,c:Top].  (primrec(n;b;c) ~ fix((λp,n. if (n) < (1)  then b  else (c (n - 1) (p (n - 1))))) n)

Lemma: nat_ind_a
∀[P:ℕ ⟶ ℙ{k}]. (P[0] ⇒ (∀i:ℕ+. (P[i - 1] ⇒ P[i])) ⇒ {∀i:ℕ. P[i]})

Lemma: comp_nat_ind_tp
∀[P:ℕ ⟶ ℙ{k}]. ((∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) ⇒ P[i])) ⇒ {∀i:ℕ. P[i]})

Lemma: comp_nat_ind_a
∀[P:ℕ ⟶ ℙ{k}]. ((∀i:ℕ. ((∀j:ℕ. P[j] supposing j < i) ⇒ P[i])) ⇒ {∀i:ℕ. P[i]})

Lemma: nat_well_founded
WellFnd{i}(ℕ;x,y.x < y)

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

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

Lemma: integer-induction
∀[P:ℤ ⟶ ℙ]. (P[0] ⇒ (∀y:{x:ℤ| 0 < x} . (P[y - 1] ⇒ P[y])) ⇒ (∀y:{x:ℤ| x < 0} . (P[y + 1] ⇒ P[y])) ⇒ (∀x:ℤ. P[x]))

Definition: int-seg-case
int-seg-case(i;j;d) ==
  if (j) < (i)
     then inr (λk.Ax) 
     else primrec(j - i;inr (λk.Ax) ;λn,x. case x
                                           of inl(p) =>
                                           inl p
                                           | inr(f) =>
                                           case d (i + n)
                                            of inl(z) =>
                                            inl <i + n, z>
                                            | inr(u) =>
                                            inr (λk.if (k) < (i + n)  then f k  else u) )

Lemma: int-seg-case_wf
∀[i,j:ℤ]. ∀[F,G:{i..j-} ⟶ ℙ]. ∀[d:∀k:{i..j-}. (F[k] ∨ G[k])].
  (int-seg-case(i;j;d) ∈ (∃k:{i..j-}. F[k]) ∨ (∀k:{i..j-}. G[k]))

Lemma: int-seg-case-monotone
∀[i,j:ℤ]. ∀[F,G:{i..j-} ⟶ ℙ]. ∀[d:∀k:{i..j-}. (F[k] ∨ G[k])].
  ∀k:{i..j + 1-}. ((↑isl(int-seg-case(i;k;d))) ⇒ (∀k':{k..j + 1-}. (↑isl(int-seg-case(i;k';d)))))

Lemma: int_seg-case
∀i,j:ℤ.  ∀[F,G:{i..j-} ⟶ ℙ].  ((∀k:{i..j-}. (F[k] ∨ G[k])) ⇒ ((∃k:{i..j-}. F[k]) ∨ (∀k:{i..j-}. G[k])))

Lemma: decidable-exists-int_seg-subtype
∀[i:ℤ]. ∀[j:{i + 1...}]. ∀[P:{i..j-} ⟶ ℙ].  Dec(∃k:{i + 1..j-}. P[k]) ⊆r Dec(∃k:{i..j-}. P[k]) supposing ¬P[i]

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

Lemma: int_seg_decide_wf
∀[i,j:ℤ]. ∀[F:{i..j-} ⟶ ℙ{u}]. ∀[d:∀k:{i..j-}. Dec(F[k])].  (int_seg_decide(d;i;j) ∈ Dec(∃k:{i..j-}. F[k]))

Lemma: decidable__exists_int_seg
∀i,j:ℤ.  ∀[F:{i..j-} ⟶ ℙ{u}]. ((∀k:{i..j-}. Dec(F[k])) ⇒ Dec(∃k:{i..j-}. F[k]))

Lemma: decidable__all_int_seg
∀i,j:ℤ.  ∀[F:{i..j-} ⟶ ℙ{u}]. ((∀k:{i..j-}. Dec(F[k])) ⇒ Dec(∀k:{i..j-}. F[k]))

Definition: canonical-function
canonical-function(f) ==  λx.if (x) < (0)  then ⊥  else (f x)

Lemma: canonical-function_wf
∀X:{X:Type| X ⊆r Base} . ∀f:ℕ ⟶ X.  (canonical-function(f) ∈ {g:Base| g = f ∈ (ℕ ⟶ X)} )

Definition: canonicalizable
canonicalizable(T) ==  ∃f:T ⟶ Base. ∀x:T. ((f x) = x ∈ T)

Lemma: canonicalizable_wf
∀[T:Type]. (canonicalizable(T) ∈ ℙ)

Lemma: canonicalizable-iff
∀[T:Type]. (canonicalizable(T) ⇐⇒ ∀t:T. ∃x:Base. (t = x ∈ T))

Lemma: canonicalizable-base
∀[T:Type]. ((T ⊆r Base) ⇒ canonicalizable(T))

Lemma: canonicalizable-product
∀[T:Type]. ∀[B:T ⟶ Type].  (canonicalizable(T) ⇒ (∀x:T. canonicalizable(B[x])) ⇒ canonicalizable(x:T × B[x]))

Lemma: canonicalizable-set
∀[T:Type]. ∀[B:T ⟶ Type].  (canonicalizable(T) ⇒ canonicalizable({x:T| B[x]} ))

Lemma: canonicalizable-top
canonicalizable(Top)

Definition: retractible
retractible(T) ==  ∃f:Base. ((∀x:T. ((f x) = x ∈ T)) ∧ (∀x:Base. ((f x)↓ ⇒ (x ∈ T))))

Lemma: retractible_wf
∀[T:Type]. retractible(T) ∈ ℙ supposing T ⊆r Base

Lemma: nat-retractible
retractible(ℕ)

Lemma: canonicalizable-function
∀[T:Type]
  ∀[B:T ⟶ Type]. retractible(T) ⇒ canonicalizable(x:T ⟶ B[x]) supposing ∀x:T. (B[x] ⊆r Base) 
  supposing (T ⊆r Base) ∧ value-type(T)

Lemma: canonicalizable-nat-to-nat
canonicalizable(ℕ ⟶ ℕ)

Lemma: canonicalizable-baire-direct
canonicalizable(ℕ ⟶ ℕ)



Home Index