Nuprl 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))))

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, apply: f a, sqequal: s ~ t, axiom: Ax
Definitions occuring in definition : exists: ∃x:A. B[x], term-equality: term-equality{i:l}(Term), per-computes-to: per-computes-to(Term;a;b), all: ∀x:A. B[x], iff: P ⇐⇒ Q, and: P ∧ Q, sqequal: s ~ t, axiom: Ax, apply: f a
FDL editor aliases : per-eq-def

Latex:
per-eq-def\{i:l\}(Term;EQ;ts;T;T';eq) == \mexists{}A,B,a1,a2,b1,b2:Term \mexists{}eqa:term-equality\{i:l\}(Term) (per-computes-to(Term;T;EQ A a1 a2) \mwedge{} per-computes-to(Term;T';EQ B b1 b2) \mwedge{} (ts A B eqa) \mwedge{} (eqa a1 b1) \mwedge{} (eqa a2 b2) \mwedge{} (\mforall{}t,t':Term. (eq t t' \mLeftarrow{}{}\mRightarrow{} (t \msim{} Ax) \mwedge{} (t' \msim{} Ax) \mwedge{} (eqa a1 a2)))) Date html generated: 2016_05_15-PM-01_49_10 Last ObjectModification: 2015_09_23-AM-07_37_16 Theory : parameterized!rec Home Index