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) ≤ 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 u = t in if u is a pair then is-list (snd(u)) otherwise if u = 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) ==
(∀x:Base
((F x)↓
⇒ ((∀a,b:Base. (if x is a pair then a otherwise b ~ a)) ∨ (∀a,b:Base. (if x = Ax then a otherwise b ~ a)))))
∧ (∃G:Base. ((∀x,y:Base. (F <x, y> ~ G (F y) x 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]. (¬A + 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]. (¬ℤ ⋂ T + S)
Lemma: int-atom-disjoint
¬ℤ ⋂ Atom
Lemma: union-atom-disjoint
∀[T,S:Type]. (¬T + 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 t ~ <fst(t), snd(t)> else t ~ 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
∀t:ListLike
((t)↓
⇒ (((↑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 t is a pair then T (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) ⊆r 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 t ~ <fst(t), snd(t)> else t ~ 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 ≤ t @ [] supposing (t)↓ ⇒ (is-list(t))↓
Lemma: sqle-append-nil-if-has-value4
∀[t:ListLike]. (t ≤ 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 u = t in
if u is a pair then let a,b = u
in ev-list b (λc.(f <a, c>)) otherwise if u = Ax then f Ax otherwise ⊥))
t
f
Lemma: co-list-ext
∀[T:Type]. colist(T) ≡ Unit ⋃ (T × colist(T))
Lemma: co-list-subtype
∀[T:Type]. (colist(T) ⊆r (Unit ⋃ (T × colist(T))))
Lemma: co-list-subtype2
∀[T:Type]. ((Unit ⋃ (T × colist(T))) ⊆r colist(T))
Lemma: unit-subtype-co-list
∀[T:Type]. (Unit ⊆r colist(T))
Lemma: product-subtype-co-list
∀[T:Type]. ((T × colist(T)) ⊆r 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
∀[T:Type]
∀x:colist(T)
(((↑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 × B 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 u = t in if u is a pair then is-list (snd(u)) otherwise if u = 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> ~ f (snd(<a, b>)))
Lemma: is_list_fun_axiom_lemma
∀f:Top. (is-list-fun() f 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) x ~ ⊥)
Lemma: is-list-approx-step
∀j:ℕ+. ∀[x:Top]. (is-list-approx(j) x ~ 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|| ~ n supposing ||t|| = n ∈ partial(ℤ)
Lemma: has-value-is-list-approx-is-type
∀[T:Type]. ∀[t:colist(T)]. ∀[n:ℕ].
((λis-list,t. eval u = t in if u is a pair then is-list (snd(u)) otherwise if u = 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) ≡ 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) ≡ 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 P x of inl(u) => [] | inr(v) => let a,b = v 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 x 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
Monotone(T.step-function-example(T))
Lemma: step-function-example-member
1 ∈ corec(X.step-function-example(X))
Definition: restart-function
restart-function(f) == fix((λR,n. if 0 <z n then <R (n - 1), {n}> else f 0 fi ))
Home
Index