Nuprl 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'))))
per-univi{i:l}(Term;UNIV;i;T;T';eq) ==
  fix((λper-univi,i,T,T',eq. 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 - 1) T T' eq); t; t'; eq')))\000C))) 
  i 
  T 
  T' 
  eq


Definitions occuring in Statement :  per-computes-to: per-computes-to(Term;a;b),  term-equality: term-equality{i:l}(Term),  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  iff: P ⇐⇒ Q,  and: P ∧ Q,  false: False,  int_eq: if a=b  then c  else d,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  int_eq: if a=b  then c  else d,  false: False,  and: P ∧ Q,  per-computes-to: per-computes-to(Term;a;b),  all: ∀x:A. B[x],  iff: P ⇐⇒ Q,  exists: ∃x:A. B[x],  term-equality: term-equality{i:l}(Term),  lambda: λx.A[x],  apply: f a,  subtract: n - m,  natural_number: $n
FDL editor aliases :  per-univi
Latex:
per-univi\{i:l\}(Term;UNIV;i;T;T';eq)
==r  if  i=0
              then  False
              else  (per-computes-to(Term;T;UNIV  i)
                        \mwedge{}  per-computes-to(Term;T';UNIV  i)
                        \mwedge{}  (\mforall{}t,t':Term.
                                  (eq  t  t'
                                  \mLeftarrow{}{}\mRightarrow{}  \mexists{}eq':term-equality\{i:l\}(Term)
                                            per-close\{i:l\}(Term;  \mlambda{}T,T',eq.  per-univi\{i:l\}(Term;UNIV;i  -  1;T;T';eq);  t;  t';\000C  eq'))))
Latex:
per-univi\{i:l\}(Term;UNIV;i;T;T';eq)  ==
    fix((\mlambda{}per-univi,i,T,T',eq.  if  i=0
                                                                then  False
                                                                else  (per-computes-to(Term;T;UNIV  i)
                                                                          \mwedge{}  per-computes-to(Term;T';UNIV  i)
                                                                          \mwedge{}  (\mforall{}t,t':Term.
                                                                                    (eq  t  t'
                                                                                    \mLeftarrow{}{}\mRightarrow{}  \mexists{}eq':term-equality\{i:l\}(Term)
                                                                                              per-close\{i:l\}(Term;
                                                                                                                            \mlambda{}T,T',eq.  (per-univi  (i  -  1)  T  T'  eq);
                                                                                                                            t;
                                                                                                                            t';
                                                                                                                            eq')))))) 
    i 
    T 
    T' 
    eq


Date html generated: 2016_05_15-PM-01_49_19
Last ObjectModification: 2015_09_23-AM-07_37_17

Theory : parameterized!rec


Home Index