### 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