Definition: parameterized-rec
`pRec(C;x.B[x];c) ==  PRIMITIVE`

Definition: term-equality
`term-equality{i:l}(Term) ==  Term ⟶ Term ⟶ Type`

Lemma: term-equality_wf
`∀[Term:Type]. (term-equality{i:l}(Term) ∈ 𝕌')`

Definition: candidate-type-system
`candidate-type-system{i:l,j:l}(Term) ==  Term ⟶ Term ⟶ term-equality{i:l}(Term) ⟶ 𝕌{j}`

Lemma: candidate-type-system_wf
`∀[Term:Type]. (candidate-type-system{i:l,j:l}(Term) ∈ 𝕌{[i' | j']})`

Definition: per-computes-to
`per-computes-to(Term;a;b) ==  a ~ b`

Lemma: per-computes-to_wf
`∀[Term:{T:Type| T ⊆r Base} ]. ∀[a,b:Term].  (per-computes-to(Term;a;b) ∈ Type)`

Definition: per-eq-def
`per-eq-def{i:l}(Term;EQ;ts;T;T';eq) ==`
`  ∃A,B,a1,a2,b1,b2:Term`
`   ∃eqa:term-equality{i:l}(Term)`
`    (per-computes-to(Term;T;EQ A a1 a2)`
`    ∧ per-computes-to(Term;T';EQ B b1 b2)`
`    ∧ (ts A B eqa)`
`    ∧ (eqa a1 b1)`
`    ∧ (eqa a2 b2)`
`    ∧ (∀t,t':Term.  (eq t t' `⇐⇒` (t ~ Ax) ∧ (t' ~ Ax) ∧ (eqa a1 a2))))`

Lemma: per-eq-def_wf
`∀[Term:Type]. ∀[EQ:Term ⟶ Term ⟶ Term ⟶ Term]. ∀[ts:candidate-type-system{i:l, i':l}(Term)]. ∀[T,T':Term].`
`∀[eq:term-equality{i:l}(Term)].`
`  per-eq-def{i:l}(Term;EQ;ts;T;T';eq) ∈ 𝕌' supposing Term ⊆r Base`

Definition: per-close
`per-close{i:l}(Term;EQ;ts;T;T';eq) ==`
`  pRec(candidate-type-system{i:l, i:l}(Term)`
`  × Term`
`  × Term`
`  × term-equality{i:l}(Term);close.λp.let ts,T,T',eq = p `
`                                      in (ts T T' eq) ∨ per-eq-def{i:l}(Term;EQ;λT,T',eq. (close <ts, T, T', eq>);T;T';e\000Cq)  ;<ts`
`                                                                                                               , T`
`                                                                                                               , T'`
`                                                                                                               , eq>)`

Lemma: per-close_wf
`∀[Term:{T:Type| T ⊆r Base} ]. ∀[EQ:Term ⟶ Term ⟶ Term ⟶ Term]. ∀[ts:candidate-type-system{i:l, i:l}(Term)].`
`∀[T,T':Term]. ∀[eq:term-equality{i:l}(Term)].`
`  (per-close{i:l}(Term;EQ;ts;T;T';eq) ∈ 𝕌')`

Definition: per-univi
`per-univi{i:l}(Term;UNIV;i;T;T';eq)`
`==r if i=0`
`    then False`
`    else (per-computes-to(Term;T;UNIV i)`
`         ∧ per-computes-to(Term;T';UNIV i)`
`         ∧ (∀t,t':Term.`
`              (eq t t'`
`              `⇐⇒` ∃eq':term-equality{i:l}(Term)`
`                   per-close{i:l}(Term; λT,T',eq. per-univi{i:l}(Term;UNIV;i - 1;T;T';eq); t; t'; eq'))))`

Home Index