Nuprl Definition : same-binding
same-binding(vs;ws;v;w) ==
if vs is a pair then if ws is a pair then let a,as = vs
in let b,bs = ws
in case eq_var(a;v)
of inl(_) =>
eq_var(b;w)
| inr(_) =>
(¬beq_var(b;w)) ∧b same-binding(as;bs;v;w) otherwise ff
otherwise if ws is a pair then ff otherwise eq_var(v;w)
Definitions occuring in Statement :
eq_var: eq_var(a;b),
band: p ∧b q,
bnot: ¬bb,
bfalse: ff,
ispair: if z is a pair then a otherwise b,
spread: spread def,
decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :
spread: spread def,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
band: p ∧b q,
bnot: ¬bb,
ispair: if z is a pair then a otherwise b,
bfalse: ff,
eq_var: eq_var(a;b)
FDL editor aliases :
same-binding
Latex:
same-binding(vs;ws;v;w) ==
if vs is a pair then if ws is a pair then let a,as = vs
in let b,bs = ws
in case eq\_var(a;v)
of inl($_{}$) =>
eq\_var(b;w)
| inr($_{}$) =>
(\mneg{}\msubb{}eq\_var(b;w)) \mwedge{}\msubb{} same-binding(as;bs;v;w)
otherwise ff otherwise if ws is a pair then ff otherwise eq\_var(v;w)
Date html generated:
2020_05_19-PM-09_53_03
Last ObjectModification:
2020_03_09-PM-04_07_58
Theory : terms
Home
Index