---

Definition: co-value
co-value() ==  corec(L.atomic-values() ⋃ (L × L) ⋃ (L + L))

Lemma: co-value_wf
co-value() ∈ Type

Lemma: continuous-monotone-co-value
ContinuousMonotone(T.atomic-values() ⋃ (T × T) ⋃ (T + T))

Lemma: co-value-ext
co-value() ≡ atomic-values() ⋃ (co-value() × co-value()) ⋃ (co-value() + co-value())

Definition: co-value-height
co-value-height(t)
==r if t is a pair then let a,b = t 
                        in 1 + co-value-height(a) + co-value-height(b) otherwise if t is inl then 1
                                                                                 + co-value-height(outl(t))
                                                                                 else if t is inr then 1
                                                                                      + co-value-height(outr(t))
                                                                                      else 0

Lemma: co-value-height_wf
∀[t:co-value()]. (co-value-height(t) ∈ partial(ℕ))

Definition: rec-value
rec-value() ==  {v:co-value()| (co-value-height(v))↓} 

Lemma: rec-value_wf
rec-value() ∈ Type

Definition: rec-value-height
rec-value-height(v) ==  co-value-height(v)

Lemma: rec-value-height_wf
∀[v:rec-value()]. (rec-value-height(v) ∈ ℕ)

Lemma: rec-value-ext
rec-value() ≡ atomic-values() ⋃ (rec-value() × rec-value()) ⋃ (rec-value() + rec-value())

Lemma: atomic-values-evalall
∀[x:Base]. (evalall(x))↓ supposing x ∈ atomic-values()

Lemma: rec-value-evalall
∀[x:Base]. uiff((evalall(x))↓;x ∈ rec-value())

Lemma: rec-value-valueall-type
valueall-type(rec-value())

Lemma: rec-value-value-type
value-type(rec-value())

Lemma: rec-value_subype_base
rec-value() ⊆r Base

Lemma: rec-value-list-is-rec-value
∀[x:rec-value() List]. (x ∈ rec-value())

Lemma: evalall-append-implies-list
∀[a,b:Base].  a ∈ rec-value() List supposing (evalall(a @ b))↓

Lemma: evalall-append-implies-rec-value
∀[a,b:Base].  b ∈ rec-value() supposing (evalall(a @ b))↓



Home Index