Lemma: eval_list-append-nil-is-eval_list
[t:Top]. (eval_list(t []) eval_list(t))

Definition: islist
islist(t) ==  (eval_list(t))↓

Lemma: islist_wf
[t:Base]. (islist(t) ∈ ℙ)

Lemma: islist-list
[T:Type]. ∀[t:T List].  islist(t)

Lemma: islist-append-nil-sqequal-islist
[t:Top]. (islist(t []) islist(t))

Lemma: islist-implies-is-list
[t:Base]. t ∈ Base List supposing islist(t)

Lemma: eval_list-sqle-append-nil
[t:Base]. eval_list(t) ≤ [] supposing ¬is-exception(eval_list(t))

Lemma: islist-append-nil-is-list
[l:Base]. l ∈ Base List supposing islist(l [])

Definition: is-list
is-list(t) ==
  fix((λis-list,t. eval in if is pair then is-list (snd(u)) otherwise if Ax then tt otherwise ⊥)) t

Lemma: is-list_wf
[T:Type]. ∀[t:colist(T)].  (is-list(t) ∈ partial(𝔹))

Lemma: is_list_pair_lemma
b,a:Top.  (is-list(<a, b>is-list(snd(<a, b>)))

Lemma: is_list_axiom_lemma
is-list(Ax) tt

Lemma: is-list-map
[t,f:Top].  (is-list(map(f;t)) is-list(t))

Lemma: is-list-prop1
[t:Base]. t ∈ Base List supposing (is-list(t))↓

Lemma: is-list-prop2
[T:Type]. ∀[t:T List].  (is-list(t))↓

Lemma: is-list-wf-list
[t:Top List]. (is-list(t) ∈ 𝔹)

Lemma: is-list-btrue-if-list
[t:Top List]. (is-list(t) tt)

Definition: list-strict
list-strict(F) ==
     ((F x)↓
      ((∀a,b:Base.  (if is pair then otherwise a)) ∨ (∀a,b:Base.  (if Ax then otherwise a)))))
  ∧ (∃G:Base. ((∀x,y:Base.  (F <x, y> (F y) y)) ∧ strict(G)))

Lemma: list-strict_wf
[F:Base]. (list-strict(F) ∈ ℙ)

Lemma: unit-product-disjoint
[T,S:Type].  Unit ⋂ T × S)

Lemma: product-unit-disjoint
[T,S:Type].  T × S ⋂ Unit)

Lemma: union-product-disjoint
[T,S,A,B:Type].  B ⋂ T × S)

Lemma: atom-product-disjoint
[T,S:Type].  Atom ⋂ T × S)

Lemma: int-product-disjoint
[T,S:Type].  (¬ℤ ⋂ T × S)

Lemma: int-union-disjoint
[T,S:Type].  (¬ℤ ⋂ S)

Lemma: int-atom-disjoint
¬ℤ ⋂ Atom

Lemma: union-atom-disjoint
[T,S:Type].  S ⋂ Atom)

Lemma: product-union-atom-disjoint
[T,S,A,B:Type].  T × S ⋂ (A B) ⋃ Atom)

Lemma: int-product-union-atom-disjoint
[T,S,A,B:Type].  (¬ℤ ⋂ (T × S) ⋃ (A B) ⋃ Atom)

Lemma: has-value-if-has-value-map
[t,f:Base].  (t)↓ supposing (map(f;t))↓

Lemma: decomp-map-if-has-value
[t,f:Base].  if ispair(t) then ~ <fst(t), snd(t)> else Ax fi  supposing (map(f;t))↓

Definition: is-list-if-has-value
ListLike ==  corec(L.partial(Unit ⋃ (Top × L)))

Lemma: is-list-if-has-value_wf
ListLike ∈ Type

Lemma: is-list-if-has-value-hv-prp
[t:ListLike]. ((t)↓ ∈ ℙ)

Lemma: is-list-if-has-value-ext
ListLike ≡ partial(Unit ⋃ (Top × ListLike))

Lemma: is-list-if-has-value-decomp
   (((↑isaxiom(t)) ∧ (t Ax ∈ Unit)) ∨ ((↑ispair(t)) ∧ (∃a:Top. ∃b:ListLike. (t = <a, b> ∈ (Top × ListLike))))))

Definition: is-list-if-has-value-fun
is-list-if-has-value-fun(t;n) ==
  primrec(n;λt.Unit;λm,T,t. if is pair then (snd(t)) otherwise ↑isaxiom(t) supposing (t)↓t

Lemma: is-list-if-has-value-fun_wf
[t:Base]. ∀[n:ℕ].  (is-list-if-has-value-fun(t;n) ∈ ℙ)

Lemma: is-list-if-has-value-fun-ax-mem
[t:Base]. ∀[n:ℕ].  Ax ∈ is-list-if-has-value-fun(t;n) supposing is-list-if-has-value-fun(t;n)

Lemma: sq_stable__is-list-if-has-value-fun
[t:Base]. ∀[n:ℕ].  SqStable(is-list-if-has-value-fun(t;n))

Definition: is-list-if-has-value-rec
is-list-if-has-value-rec(t) ==  ⋂n:ℕis-list-if-has-value-fun(t;n)

Lemma: is-list-if-has-value-rec_wf
[t:Base]. (is-list-if-has-value-rec(t) ∈ ℙ)

Lemma: is-list-if-has-value-rec-subtype-unit
[t:Base]. (is-list-if-has-value-rec(t) ⊆Unit)

Lemma: is-list-if-has-value-rec-map
[t,f:Base].  is-list-if-has-value-rec(map(f;t))

Lemma: is-list-if-has-value-rec-decomp
[t:Base]. (if ispair(t) then ~ <fst(t), snd(t)> else Ax fi supposing ((t)↓ and is-list-if-has-value-rec(t))

Lemma: is-list-if-has-value-rec-snd
[t:Base]. (is-list-if-has-value-rec(snd(t))) supposing (is-list-if-has-value-rec(t) and (t ~ <fst(t), snd(t)>))

Lemma: is-list-if-has-value-rec-pair-bot
[t:Base]. is-list-if-has-value-rec(<t, ⊥>)

Lemma: sqle-append-nil-if-has-value
[t:Base]. t ≤ [] supposing (t)↓  (is-list(t))↓

Lemma: sqle-append-nil-if-has-value4
[t:ListLike]. (t ≤ [])

Lemma: map-append-empty2
[f,b:Top].  (map(f;b) [] map(f;b))

Definition: ev-list
ev-list(t;f) ==
  fix((λev-list,t,f. eval in
                     if is pair then let a,b 
                                         in ev-list c.(f <a, c>)) otherwise if Ax then Ax otherwise ⊥)) 

Lemma: co-list-ext
[T:Type]. colist(T) ≡ Unit ⋃ (T × colist(T))

Lemma: co-list-subtype
[T:Type]. (colist(T) ⊆(Unit ⋃ (T × colist(T))))

Lemma: co-list-subtype2
[T:Type]. ((Unit ⋃ (T × colist(T))) ⊆colist(T))

Lemma: unit-subtype-co-list
[T:Type]. (Unit ⊆colist(T))

Lemma: product-subtype-co-list
[T:Type]. ((T × colist(T)) ⊆colist(T))

Lemma: co-list-cases2
[T:Type]. ∀x:colist(T). ((x Ax ∈ colist(T)) ∨ (∃t:T. ∃y:colist(T). (x = <t, y> ∈ colist(T))))

Lemma: co-list-cases
    (((↑isaxiom(x)) ∧ (x Ax ∈ Unit)) ∨ ((↑ispair(x)) ∧ (∃t:T. ∃y:colist(T). (x = <t, y> ∈ (T × colist(T))))))

Lemma: co-list-has-value
[T:Type]. ∀[t:colist(T)].  (t)↓

Lemma: co-list-value-type
[T:Type]. value-type(colist(T))

Definition: co-list-cons
co-list-cons(h;t) ==  <h, t>

Lemma: co-list-cons_wf
[T:Type]. ∀[h:T]. ∀[t:colist(T)].  (co-list-cons(h;t) ∈ colist(T))

Definition: co-list-nil
co-list-nil() ==  Ax

Lemma: co-list-nil_wf
[T:Type]. (co-list-nil() ∈ colist(T))

Lemma: ispair_wf_listunion
[A,B:Type]. ∀[L:Unit ⋃ (A × B)].  (ispair(L) ∈ 𝔹)

Lemma: pair-listunion
[A,B:Type]. ∀[L:Unit ⋃ (A × B)].  L ∈ A × supposing ispair(L) tt

Lemma: non-pair-listunion
[A,B:Type]. ∀[L:Unit ⋃ (A × B)].  L ∈ Unit supposing ispair(L) ff

Lemma: ispair-bool-if-bunion-unit-prod
[t:Unit ⋃ (Top × Top)]. (ispair(t) ∈ 𝔹)

Lemma: isaxiom-bool-if-bunion-unit-prod
[t:Unit ⋃ (Top × Top)]. (isaxiom(t) ∈ 𝔹)

Lemma: ispair-bool-if-co-list
[T:Type]. ∀[t:colist(T)].  (ispair(t) ∈ 𝔹)

Definition: is-list-fun
is-list-fun() ==  λis-list,t. eval in if is pair then is-list (snd(u)) otherwise if Ax then tt otherwise ⊥

Lemma: is-list-fun_wf
[T:Type]. (is-list-fun() ∈ (colist(T) ⟶ partial(𝔹)) ⟶ colist(T) ⟶ partial(𝔹))

Lemma: is_list_fun_pair_lemma
b,a,f:Top.  (is-list-fun() f <a, b> (snd(<a, b>)))

Lemma: is_list_fun_axiom_lemma
f:Top. (is-list-fun() Ax tt)

Definition: is-list-approx
is-list-approx(j) ==  is-list-fun()^j ⊥

Lemma: is-list-approx_wf
T:Type. ∀j:ℕ.  (is-list-approx(j) ∈ colist(T) ⟶ partial(𝔹))

Lemma: is-list-approx0
[x:Top]. (is-list-approx(0) ~ ⊥)

Lemma: is-list-approx-step
j:ℕ+. ∀[x:Top]. (is-list-approx(j) is-list-fun() is-list-approx(j 1) x)

Lemma: is-list-wf-co-list
[T:Type]. ∀[t:colist(T)].  (is-list(t) ∈ partial(𝔹))

Lemma: has-value-is-list-map-if-has-value-is-list
[T:Type]. ∀[t:colist(T)]. ∀[f:Base].  ((is-list(t))↓  (is-list(map(f;t)))↓)

Lemma: has-value-is-list-map-iff-has-value-is-list
[T:Type]. ∀[t:colist(T)]. ∀[f:Base].  ((is-list(t))↓ ⇐⇒ (is-list(map(f;t)))↓)

Lemma: has-value-is-list-of-co-list
[T:Type]. ∀[t:colist(T)].  ((is-list(t))↓ ∈ ℙ)

Lemma: length-in-bar-int-if-co-list
[T:Type]. ∀[t:colist(T)].  (||t|| ∈ partial(ℤ))

Lemma: length-in-prop-if-co-list
[T:Type]. ∀[t:colist(T)].  (∃n:ℕ(||t|| n ∈ partial(ℤ)) ∈ ℙ)

Lemma: length-if-co-list-sq
[T:Type]. ∀[t:colist(T)]. ∀[n:ℕ].  ||t|| supposing ||t|| n ∈ partial(ℤ)

Lemma: has-value-is-list-approx-is-type
[T:Type]. ∀[t:colist(T)]. ∀[n:ℕ].
  ((λis-list,t. eval in if is pair then is-list (snd(u)) otherwise if Ax then tt otherwise ⊥^n ⊥ t)↓ ∈ Typ\000Ce)

Definition: co-list-islist
co-list-islist(T) ==  {L:colist(T)| (is-list(L))↓

Lemma: co-list-islist_wf
[T:Type]. (co-list-islist(T) ∈ Type)

Lemma: member-co-list-islist
[T:Type]. ∀[L:colist(T)].  L ∈ co-list-islist(T) supposing (is-list(L))↓

Lemma: islist-iff-length-has-value
[T:Type]. ∀[t:colist(T)].  uiff((is-list(t))↓;(||t||)↓)

Lemma: co-list-islist-ext-list
[T:Type]. co-list-islist(T) ≡ List

Lemma: length-wf-co-list-islist
[T:Type]. ∀[t:co-list-islist(T)].  (||t|| ∈ ℕ)

Lemma: list_ind-wf-co-list-islist
[A,B:Type]. ∀[L:co-list-islist(A)]. ∀[x:B]. ∀[F:A ⟶ co-list-islist(A) ⟶ B ⟶ B].
  (rec-case(L) of
   [] => x
   h::t =>
    r.F[h;t;r] ∈ B)

Definition: conil
conil() ==  Ax

Lemma: conil_wf
[A:Type]. (conil() ∈ co-list-islist(A))

Definition: cocons
cocons(a;L) ==  <a, L>

Lemma: cocons_wf
[A:Type]. ∀[a:A]. ∀[L:co-list-islist(A)].  (cocons(a;L) ∈ co-list-islist(A))

Lemma: list_ind-wf-co-list-islist2
[A:Type]. ∀[B:co-list-islist(A) ⟶ Type]. ∀[L:co-list-islist(A)]. ∀[x:B[conil()]]. ∀[F:a:A
                                                                                        ⟶ L:co-list-islist(A)
                                                                                        ⟶ B[L]
                                                                                        ⟶ B[cocons(a;L)]].
  (rec-case(L) of
   [] => x
   h::t =>
    r.F[h;t;r] ∈ B[L])

Lemma: co-list-islist-induction1
[A:Type]. ∀[P:co-list-islist(A) ⟶ ℙ].
  (P[conil()]  (∀L:co-list-islist(A). ∀a:A.  (P[L]  P[cocons(a;L)]))  (∀L:co-list-islist(A). P[L]))

Lemma: co-list-islist-islist
[T:Type]. ∀[t:co-list-islist(T)].  islist(t)

Lemma: co-list-islist-ext-eq-list
[T:Type]. co-list-islist(T) ≡ List

Lemma: co-list-islist-islist-new-compactness-base
[T:Type]. ∀[t:co-list-islist(T)].  islist(t)

Definition: colist-unfold
colist-unfold(P;x)==r case of inl(u) => [] inr(v) => let a,b in [a colist-unfold(P;b)]

Lemma: colist-unfold_wf
[A,B:Type]. ∀[P:B ⟶ (Unit (A × B))]. ∀[x:B].  (colist-unfold(P;x) ∈ colist(A))

Definition: co-ones
co-ones() ==  fix((λt.<1, t>))

Lemma: co-ones_wf
co-ones() ∈ colist(ℤ)

Definition: co-alt
co-alt() ==  fix((λt.<1, 2, t>))

Lemma: co-alt_wf
co-alt() ∈ colist(ℤ)

Definition: step-function
step-function(T;transition;X) ==  {x:T| ∃y:T ⋂ X. (transition y)} 

Lemma: step-function_wf
[T:Type]. ∀[transition:T ⟶ T ⟶ ℙ]. ∀[X:Type].  (step-function(T;transition;X) ∈ Type)

Definition: step-function-example
step-function-example(X) ==
  step-function(ℕ+7;λx,y. (((x 1 ∈ ℤ) ∧ (y 2 ∈ ℤ))
                         ∨ ((x 2 ∈ ℤ) ∧ (y 3 ∈ ℤ))
                         ∨ ((x 2 ∈ ℤ) ∧ (y 4 ∈ ℤ))
                         ∨ ((x 3 ∈ ℤ) ∧ (y 6 ∈ ℤ))
                         ∨ ((x 4 ∈ ℤ) ∧ (y 2 ∈ ℤ))
                         ∨ ((x 5 ∈ ℤ) ∧ (y 3 ∈ ℤ)));X)

Lemma: step-function-example_wf
[X:Type]. (step-function-example(X) ∈ Type)

Lemma: step-function-example-monotone

Lemma: step-function-example-member
1 ∈ corec(X.step-function-example(X))

Definition: restart-function
restart-function(f) ==  fix((λR,n. if 0 <then <(n 1), {n}> else fi ))

Home Index