---

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