Nuprl Definition : wf-term
wf-term(arity;sort;t) ==
case t
of inl(v) =>
tt
| inr(p) =>
let f,bts = p
in eval nms = arity f in
(||nms|| =z ||bts||)
∧b (∀nm_bt∈zip(nms;bts).let nm,bt = nm_bt
in let vs,b = bt
in (fst(nm) =z ||vs||) ∧b (sort b =z snd(nm)) ∧b wf-term(arity;sort;b))_b
Definitions occuring in Statement :
zip: zip(as;bs),
bl-all: (∀x∈L.P[x])_b,
length: ||as||,
band: p ∧b q,
callbyvalue: callbyvalue,
eq_int: (i =z j),
btrue: tt,
pi1: fst(t),
pi2: snd(t),
apply: f a,
spread: spread def,
decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :
decide: case b of inl(x) => s[x] | inr(y) => t[y],
btrue: tt,
callbyvalue: callbyvalue,
bl-all: (∀x∈L.P[x])_b,
zip: zip(as;bs),
spread: spread def,
pi1: fst(t),
length: ||as||,
band: p ∧b q,
eq_int: (i =z j),
apply: f a,
pi2: snd(t)
FDL editor aliases :
wf-term
Latex:
wf-term(arity;sort;t) ==
case t
of inl(v) =>
tt
| inr(p) =>
let f,bts = p
in eval nms = arity f in
(||nms|| =\msubz{} ||bts||)
\mwedge{}\msubb{} (\mforall{}nm$_{bt}$\mmember{}zip(nms;bts).let nm,bt = nm$_{bt}$
in let vs,b = bt
in (fst(nm) =\msubz{} ||vs||)
\mwedge{}\msubb{} (sort b =\msubz{} snd(nm))
\mwedge{}\msubb{} wf-term(arity;sort;b))\_b
Date html generated:
2020_05_19-PM-09_58_12
Last ObjectModification:
2020_03_09-PM-04_10_10
Theory : terms
Home
Index