Nuprl Definition : ctt-binder-context
ctt-binder-context ==
λX,vs,f,trs,bt. if ||trs|| <z ||ctt-arity(f)||
∧b (||fst(bt)|| =z fst(ctt-arity(f)[||trs||]))
∧b bdd-all(||trs||;i.(ctt-kind(snd(fst(snd(trs[i])))) =z snd(ctt-arity(f)[i])))
then provisional-subterm-context{i:l}(X;f;fst(bt);trs)
else X
fi
Definitions occuring in Statement :
provisional-subterm-context: provisional-subterm-context{i:l}(X;f;vs;L),
ctt-arity: ctt-arity(x),
ctt-kind: ctt-kind(t),
select: L[n],
length: ||as||,
bdd-all: bdd-all(n;i.P[i]),
band: p ∧b q,
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
eq_int: (i =z j),
pi1: fst(t),
pi2: snd(t),
lambda: λx.A[x]
Definitions occuring in definition :
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
band: p ∧b q,
bdd-all: bdd-all(n;i.P[i]),
length: ||as||,
eq_int: (i =z j),
ctt-kind: ctt-kind(t),
pi2: snd(t),
select: L[n],
ctt-arity: ctt-arity(x),
provisional-subterm-context: provisional-subterm-context{i:l}(X;f;vs;L),
pi1: fst(t)
FDL editor aliases :
ctt-binder-context
Latex:
ctt-binder-context ==
\mlambda{}X,vs,f,trs,bt. if ||trs|| <z ||ctt-arity(f)||
\mwedge{}\msubb{} (||fst(bt)|| =\msubz{} fst(ctt-arity(f)[||trs||]))
\mwedge{}\msubb{} bdd-all(||trs||;i.(ctt-kind(snd(fst(snd(trs[i])))) =\msubz{} snd(ctt-arity(f)[i])))
then provisional-subterm-context\{i:l\}(X;f;fst(bt);trs)
else X
fi
Date html generated:
2020_05_21-AM-10_38_07
Last ObjectModification:
2020_03_13-AM-11_13_34
Theory : cubical!type!theory
Home
Index