Nuprl Definition : ctt-subterm-context
ctt-subterm-context{i:l}(ctxt;f;n;vs;m) ==
if (ctt-opr-is(f;"pi") ∨bctt-opr-is(f;"sigma") ∨bctt-opr-is(f;"fst") ∨bctt-opr-is(f;"snd") ∨bctt-opr-is(f;"lambda"))
∧b (n =z 1)
then ctxt; hd(vs):fst(m)
if ctt-opr-is(f;"case") ∧b ((n =z 2) ∨b(n =z 3)) then restrict-cubical-context{i:l}(ctxt;m)
if ctt-opr-is(f;"Glue") then if (n =z 2) ∨b(n =z 3) then restrict-cubical-context{i:l}(ctxt;m) else OK(ctxt) fi
if (ctt-opr-is(f;"pair") ∨bctt-opr-is(f;"apply")) ∧b (n =z 1) then ctxt; hd(vs):fst(m)
if ctt-opr-is(f;"pathabs") ∧b (n =z 1) then ctxt; hd(vs):OK(<0, 𝕀>)
if ctt-opr-is(f;"comp")
then if (n =z 1) then ctxt; hd(vs):OK(<0, 𝕀>)
if (n =z 2) then restrict-cubical-context{i:l}(ctxt;m),hd(vs):I
else OK(ctxt)
fi
if ctt-opr-is(f;"glue") ∧b ((n =z 2) ∨b(n =z 3)) then restrict-cubical-context{i:l}(ctxt;m)
if ctt-opr-is(f;"unglue") ∧b ((n =z 2) ∨b(n =z 3)) then restrict-cubical-context{i:l}(ctxt;m)
else OK(ctxt)
fi
Definitions occuring in Statement :
ctt-opr-is: ctt-opr-is(f;s),
restrict-cubical-context: restrict-cubical-context{i:l}(ctxt;trm),
update-cubical-context2: ctxt; v:fst(T),
update-cubical-context: ctxt; v:T,
update-provisional-context-I: X,v:I,
interval-type: 𝕀,
hd: hd(l),
bor: p ∨bq,
band: p ∧b q,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
true: True,
pair: <a, b>,
natural_number: $n,
token: "$token",
provision: provision(ok; v)
Definitions occuring in definition :
token: "$token",
ctt-opr-is: ctt-opr-is(f;s),
band: p ∧b q,
ifthenelse: if b then t else f fi ,
restrict-cubical-context: restrict-cubical-context{i:l}(ctxt;trm),
natural_number: $n,
eq_int: (i =z j),
bor: p ∨bq,
true: True,
provision: provision(ok; v),
hd: hd(l),
update-provisional-context-I: X,v:I,
interval-type: 𝕀,
pair: <a, b>,
update-cubical-context: ctxt; v:T,
update-cubical-context2: ctxt; v:fst(T)
FDL editor aliases :
ctt-subterm-context
Latex:
ctt-subterm-context\{i:l\}(ctxt;f;n;vs;m) ==
if (ctt-opr-is(f;"pi")
\mvee{}\msubb{}ctt-opr-is(f;"sigma")
\mvee{}\msubb{}ctt-opr-is(f;"fst")
\mvee{}\msubb{}ctt-opr-is(f;"snd")
\mvee{}\msubb{}ctt-opr-is(f;"lambda"))
\mwedge{}\msubb{} (n =\msubz{} 1)
then ctxt; hd(vs):fst(m)
if ctt-opr-is(f;"case") \mwedge{}\msubb{} ((n =\msubz{} 2) \mvee{}\msubb{}(n =\msubz{} 3)) then restrict-cubical-context\{i:l\}(ctxt;m)
if ctt-opr-is(f;"Glue")
then if (n =\msubz{} 2) \mvee{}\msubb{}(n =\msubz{} 3) then restrict-cubical-context\{i:l\}(ctxt;m) else OK(ctxt) fi
if (ctt-opr-is(f;"pair") \mvee{}\msubb{}ctt-opr-is(f;"apply")) \mwedge{}\msubb{} (n =\msubz{} 1) then ctxt; hd(vs):fst(m)
if ctt-opr-is(f;"pathabs") \mwedge{}\msubb{} (n =\msubz{} 1) then ctxt; hd(vs):OK(ɘ, \mBbbI{}>)
if ctt-opr-is(f;"comp")
then if (n =\msubz{} 1) then ctxt; hd(vs):OK(ɘ, \mBbbI{}>)
if (n =\msubz{} 2) then restrict-cubical-context\{i:l\}(ctxt;m),hd(vs):I
else OK(ctxt)
fi
if ctt-opr-is(f;"glue") \mwedge{}\msubb{} ((n =\msubz{} 2) \mvee{}\msubb{}(n =\msubz{} 3)) then restrict-cubical-context\{i:l\}(ctxt;m)
if ctt-opr-is(f;"unglue") \mwedge{}\msubb{} ((n =\msubz{} 2) \mvee{}\msubb{}(n =\msubz{} 3)) then restrict-cubical-context\{i:l\}(ctxt;m)
else OK(ctxt)
fi
Date html generated:
2020_05_21-AM-10_36_50
Last ObjectModification:
2020_05_18-AM-10_31_23
Theory : cubical!type!theory
Home
Index