Nuprl Definition : equiv-substs
equiv-substs(opr;s1;s2) ==
∀x:varname()
(isl(apply-alist(VarDeq;s1;x)) = isl(apply-alist(VarDeq;s2;x))
∧ ((↑isl(apply-alist(VarDeq;s1;x)))
⇒ alpha-eq-terms(opr;outl(apply-alist(VarDeq;s1;x));outl(apply-alist(VarDeq;s2;x)))))
Definitions occuring in Statement :
alpha-eq-terms: alpha-eq-terms(opr;a;b),
var-deq: VarDeq,
varname: varname(),
apply-alist: apply-alist(eq;L;x),
outl: outl(x),
assert: ↑b,
isl: isl(x),
bool: 𝔹,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
equal: s = t ∈ T
Definitions occuring in definition :
all: ∀x:A. B[x],
and: P ∧ Q,
equal: s = t ∈ T,
bool: 𝔹,
implies: P ⇒ Q,
assert: ↑b,
isl: isl(x),
alpha-eq-terms: alpha-eq-terms(opr;a;b),
outl: outl(x),
apply-alist: apply-alist(eq;L;x),
var-deq: VarDeq
FDL editor aliases :
equiv-substs
Latex:
equiv-substs(opr;s1;s2) ==
\mforall{}x:varname()
(isl(apply-alist(VarDeq;s1;x)) = isl(apply-alist(VarDeq;s2;x))
\mwedge{} ((\muparrow{}isl(apply-alist(VarDeq;s1;x)))
{}\mRightarrow{} alpha-eq-terms(opr;outl(apply-alist(VarDeq;s1;x));outl(apply-alist(VarDeq;s2;x)))))
Date html generated:
2020_05_19-PM-09_57_34
Last ObjectModification:
2020_03_09-PM-04_09_50
Theory : terms
Home
Index