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