Nuprl Definition : provisional-subterm-context
provisional-subterm-context{i:l}(X;f;vs;L) ==
bind-provision(X;ctxt.ctt-subterm-context{i:l}(ctxt;f;||L||;vs;if (ctt-opr-is(f;"Glue")
∧b ((||L|| =z 2) ∨b(||L|| =z 3)))
∨b(ctt-opr-is(f;"case") ∧b (||L|| =z 3))
∨b(ctt-opr-is(f;"unglue")
∧b ((||L|| =z 2) ∨b(||L|| =z 3)))
then snd(snd(L[1]))
else snd(snd(L[0]))
fi ))
Definitions occuring in Statement :
ctt-subterm-context: ctt-subterm-context{i:l}(ctxt;f;n;vs;m),
ctt-opr-is: ctt-opr-is(f;s),
select: L[n],
length: ||as||,
bor: p ∨bq,
band: p ∧b q,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
pi2: snd(t),
natural_number: $n,
token: "$token",
bind-provision: bind-provision(x;t.f[t])
Definitions occuring in definition :
bind-provision: Error :bind-provision,
ctt-subterm-context: ctt-subterm-context{i:l}(ctxt;f;n;vs;m),
ifthenelse: if b then t else f fi ,
band: p ∧b q,
ctt-opr-is: ctt-opr-is(f;s),
token: "$token",
bor: p ∨bq,
eq_int: (i =z j),
length: ||as||,
pi2: snd(t),
select: L[n],
natural_number: $n
FDL editor aliases :
provisional-subterm-context
Latex:
provisional-subterm-context\{i:l\}(X;f;vs;L) ==
bind-provision(X;ctxt.ctt-subterm-context\{i:l\}(ctxt;f;||L||;vs;if (ctt-opr-is(f;"Glue")
\mwedge{}\msubb{} ((||L|| =\msubz{} 2)
\mvee{}\msubb{}(||L|| =\msubz{} 3)))
\mvee{}\msubb{}(ctt-opr-is(f;"case")
\mwedge{}\msubb{} (||L|| =\msubz{} 3))
\mvee{}\msubb{}(ctt-opr-is(f;"unglue")
\mwedge{}\msubb{} ((||L|| =\msubz{} 2)
\mvee{}\msubb{}(||L|| =\msubz{} 3)))
then snd(snd(L[1]))
else snd(snd(L[0]))
fi ))
Date html generated:
2020_05_21-AM-10_37_24
Last ObjectModification:
2020_03_17-PM-03_35_31
Theory : cubical!type!theory
Home
Index