Nuprl Definition : alpha-aux
alpha-aux(opr;vs;ws;a;b) ==
case a
of inl(v) =>
case b of inl(w) => ↑same-binding(vs;ws;v;w) | inr(p) => False
| inr(p) =>
case b
of inl(w) =>
False
| inr(q) =>
let opa,abts = p
in let opb,bbts = q
in if abts is a pair then if bbts is a pair then let bta,morea = abts
in let btb,moreb = bbts
in let as,x = bta
in let bs,y = btb
in (||as|| = ||bs|| ∈ ℤ)
∧ alpha-aux(opr;rev(as) + vs;rev(bs) + ws;x;y)
∧ alpha-aux(opr;vs;ws;mkterm(opa;morea);mkterm(opb;moreb))
otherwise False otherwise if bbts is a pair then False otherwise opa = opb ∈ opr
Definitions occuring in Statement :
mkterm: mkterm(opr;bts),
same-binding: same-binding(vs;ws;v;w),
length: ||as||,
rev-append: rev(as) + bs,
assert: ↑b,
ispair: if z is a pair then a otherwise b,
and: P ∧ Q,
false: False,
spread: spread def,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
assert: ↑b,
same-binding: same-binding(vs;ws;v;w),
decide: case b of inl(x) => s[x] | inr(y) => t[y],
spread: spread def,
and: P ∧ Q,
int: ℤ,
length: ||as||,
rev-append: rev(as) + bs,
mkterm: mkterm(opr;bts),
ispair: if z is a pair then a otherwise b,
false: False,
equal: s = t ∈ T
FDL editor aliases :
alpha-aux
Latex:
alpha-aux(opr;vs;ws;a;b) ==
case a
of inl(v) =>
case b of inl(w) => \muparrow{}same-binding(vs;ws;v;w) | inr(p) => False
| inr(p) =>
case b
of inl(w) =>
False
| inr(q) =>
let opa,abts = p
in let opb,bbts = q
in if abts is a pair
then if bbts is a pair
then let bta,morea = abts
in let btb,moreb = bbts
in let as,x = bta
in let bs,y = btb
in (||as|| = ||bs||) \mwedge{} alpha-aux(opr;rev(as) + vs;rev(bs) + ws;x;y)
\mwedge{} alpha-aux(opr;vs;ws;mkterm(opa;morea);mkterm(opb;moreb)) otherwise False
otherwise if bbts is a pair then False otherwise opa = opb
Date html generated:
2020_05_19-PM-09_55_20
Last ObjectModification:
2020_03_09-PM-04_08_52
Theory : terms
Home
Index