Nuprl Lemma : provisional-subterm-context_wf
∀[X:?CubicalContext]. ∀[f:CttOp]. ∀[vs:varname() List]. ∀[L:{L:(a:?CubicalContext
× bt:varname() List × CttTerm
× [[a;snd(bt)]]) List|
||L|| < ||ctt-arity(f)||
∧ (||vs|| = (fst(ctt-arity(f)[||L||])) ∈ ℤ)
∧ (∀i:ℕ||L||
(ctt-kind(snd(fst(snd(L[i]))))
= (snd(ctt-arity(f)[i]))
∈ ℤ))
∧ ((||L|| = 1 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"pi"))
∨ (↑ctt-opr-is(f;"sigma"))
∨ (↑ctt-opr-is(f;"lambda"))
∨ (↑ctt-opr-is(f;"apply"))
∨ (↑ctt-opr-is(f;"pair"))
∨ (↑ctt-opr-is(f;"fst"))
∨ (↑ctt-opr-is(f;"snd")))
⇒ ((fst(L[0])) = X ∈ ?CubicalContext))
∧ ((||L|| = 2 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"Glue"))
∨ (↑ctt-opr-is(f;"case"))
∨ (↑ctt-opr-is(f;"comp"))
∨ (↑ctt-opr-is(f;"unglue"))
∨ (↑ctt-opr-is(f;"glue")))
⇒ ((fst(L[0])) = X ∈ ?CubicalContext))
∧ ((||L|| = 2 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"Glue")) ∨ (↑ctt-opr-is(f;"unglue")))
⇒ ((fst(L[1])) = X ∈ ?CubicalContext))
∧ ((||L|| = 3 ∈ ℤ)
⇒ ((↑ctt-opr-is(f;"Glue"))
∨ (↑ctt-opr-is(f;"case"))
∨ (↑ctt-opr-is(f;"unglue")))
⇒ ((fst(L[1])) = X ∈ ?CubicalContext))
∧ ((||L|| = 3 ∈ ℤ)
⇒ (↑ctt-opr-is(f;"glue"))
⇒ ((fst(L[0])) = X ∈ ?CubicalContext))
∧ ((||L|| = 4 ∈ ℤ)
⇒ (↑ctt-opr-is(f;"glue"))
⇒ ((fst(L[0])) = X ∈ ?CubicalContext))} ].
(provisional-subterm-context{i:l}(X;f;vs;L) ∈ ?CubicalContext)
Proof
Definitions occuring in Statement :
provisional-subterm-context: provisional-subterm-context{i:l}(X;f;vs;L),
ctt_meaning: [[ctxt;t]],
ctt-opr-is: ctt-opr-is(f;s),
ctt-term: CttTerm,
ctt-arity: ctt-arity(x),
ctt-kind: ctt-kind(t),
ctt-op: CttOp,
cubical-context: ?CubicalContext,
varname: varname(),
select: L[n],
length: ||as||,
list: T List,
int_seg: {i..j-},
assert: ↑b,
less_than: a < b,
uall: ∀[x:A]. B[x],
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
product: x:A × B[x],
natural_number: $n,
int: ℤ,
token: "$token",
equal: s = t ∈ T
Definitions unfolded in proof :
cubical-context: ?CubicalContext,
uall: ∀[x:A]. B[x],
member: t ∈ T,
provisional-subterm-context: provisional-subterm-context{i:l}(X;f;vs;L),
and: P ∧ Q,
so_lambda: λ2x.t[x],
so_apply: x[s],
subtype_rel: A ⊆r B,
nat: ℕ,
uimplies: b supposing a,
all: ∀x:A. B[x],
implies: P ⇒ Q,
pi1: fst(t),
pi2: snd(t),
int_seg: {i..j-},
lelt: i ≤ j < k,
le: A ≤ B,
or: P ∨ Q,
less_than': less_than'(a;b),
false: False,
not: ¬A,
decidable: Dec(P),
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
prop: ℙ,
sq_type: SQType(T),
guard: {T},
eq_int: (i =z j),
btrue: tt,
bor: p ∨bq,
ifthenelse: if b then t else f fi ,
assert: ↑b,
bfalse: ff,
isect2: T1 ⋂ T2,
bool: 𝔹,
unit: Unit,
it: ⋅,
uiff: uiff(P;Q),
band: p ∧b q,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
bnot: ¬bb,
cand: A c∧ B,
squash: ↓T,
true: True,
context-set: context-set(ctxt),
cubical_context: CubicalContext,
context-ok: context-ok(ctxt),
allowed: allowed(x),
usquash: usquash(T),
ctt-term: CttTerm,
wfterm: wfterm(opr;sort;arity),
less_than: a < b,
select: L[n],
ctt-arity: ctt-arity(x),
eq_atom: x =a y,
ctt-opid-arity: ctt-opid-arity(t),
cons: [a / b],
subtract: n - m,
ctt-op: CttOp,
sq_stable: SqStable(P),
ctt-tokens: ctt-tokens(),
ctt-opr-is: ctt-opr-is(f;s)
Lemmas referenced :
cubical_context_wf,
list_wf,
provisional-type_wf,
varname_wf,
ctt-term_wf,
ctt_meaning_wf,
pi2_wf,
istype-less_than,
length_wf,
nat_wf,
ctt-arity_wf,
istype-int,
length_wf_nat,
set_subtype_base,
le_wf,
int_subtype_base,
int_seg_wf,
ctt-kind_wf,
istype-assert,
ctt-opr-is_wf,
select_wf,
istype-false,
decidable__lt,
full-omega-unsat,
intformand_wf,
intformnot_wf,
intformless_wf,
itermConstant_wf,
itermVar_wf,
intformeq_wf,
int_formula_prop_and_lemma,
int_formula_prop_not_lemma,
int_formula_prop_less_lemma,
int_term_value_constant_lemma,
int_term_value_var_lemma,
int_formula_prop_eq_lemma,
int_formula_prop_wf,
ctt-op_wf,
allowed_wf,
allow_wf,
bind-provision_wf,
ctt-subterm-context_wf,
subtype_rel_self,
decidable__equal_int,
subtype_base_sq,
band_tt,
bor_wf,
band_ff,
istype-void,
bool_wf,
bool_subtype_base,
eq_int_eq_false_intro,
bfalse_wf,
bool_cases,
eqtt_to_assert,
band_wf,
btrue_wf,
eq_int_wf,
assert_wf,
equal-wf-base,
iff_transitivity,
or_wf,
iff_weakening_uiff,
assert_of_bor,
assert_of_band,
assert_of_eq_int,
equal-wf-T-base,
bnot_wf,
bool_cases_sqequal,
eqff_to_assert,
assert-bnot,
not_wf,
assert_of_bnot,
uiff_transitivity,
bnot_thru_bor,
iff_weakening_equal,
equal_wf,
squash_wf,
true_wf,
istype-universe,
decidable__le,
intformle_wf,
int_formula_prop_le_lemma,
istype-le,
assert-ctt-opr-is,
pi1_wf_top,
cubical_set_wf,
ctt-kind-0,
istype-nat,
less_than_wf,
subtype_rel_wf,
ctt-term-meaning_wf,
subtype_rel_universe1,
ctt-kind-1,
provisional-subtype,
ctt-type-meaning_wf,
ctt-type-meaning1_wf,
ctt-type-meaning-subtype,
subtype_rel_transitivity,
ctt-term-meaning-subtype2,
sq_stable__l_member,
decidable__atom_equal,
cons_wf,
nil_wf,
cons_member,
atom_subtype_base,
ctt-tokens_wf,
bor-bfalse,
member_singleton
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
cut,
introduction,
extract_by_obid,
hypothesis,
setElimination,
thin,
rename,
sqequalHypSubstitution,
productElimination,
setIsType,
universeIsType,
instantiate,
isectElimination,
productEquality,
cumulativity,
sqequalRule,
hypothesisEquality,
lambdaEquality_alt,
inhabitedIsType,
productIsType,
equalityIstype,
applyEquality,
intEquality,
natural_numberEquality,
independent_isectElimination,
because_Cache,
lambdaFormation_alt,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
independent_functionElimination,
sqequalBase,
functionIsType,
baseClosed,
unionIsType,
tokenEquality,
closedConclusion,
independent_pairFormation,
unionElimination,
approximateComputation,
dependent_pairFormation_alt,
int_eqEquality,
Error :memTop,
voidElimination,
isect_memberEquality_alt,
equalityElimination,
unionEquality,
inlFormation_alt,
inrFormation_alt,
promote_hyp,
imageElimination,
imageMemberEquality,
universeEquality,
dependent_set_memberEquality_alt,
independent_pairEquality,
hyp_replacement,
applyLambdaEquality,
sqequalIntensionalEquality,
atomEquality
Latex:
\mforall{}[X:?CubicalContext]. \mforall{}[f:CttOp]. \mforall{}[vs:varname() List]. \mforall{}[L:\{L:(a:?CubicalContext
\mtimes{} bt:varname() List \mtimes{} CttTerm
\mtimes{} [[a;snd(bt)]]) List|
||L|| < ||ctt-arity(f)||
\mwedge{} (||vs|| = (fst(ctt-arity(f)[||L||])))
\mwedge{} (\mforall{}i:\mBbbN{}||L||
(ctt-kind(snd(fst(snd(L[i]))))
= (snd(ctt-arity(f)[i]))))
\mwedge{} ((||L|| = 1)
{}\mRightarrow{} ((\muparrow{}ctt-opr-is(f;"pi"))
\mvee{} (\muparrow{}ctt-opr-is(f;"sigma"))
\mvee{} (\muparrow{}ctt-opr-is(f;"lambda"))
\mvee{} (\muparrow{}ctt-opr-is(f;"apply"))
\mvee{} (\muparrow{}ctt-opr-is(f;"pair"))
\mvee{} (\muparrow{}ctt-opr-is(f;"fst"))
\mvee{} (\muparrow{}ctt-opr-is(f;"snd")))
{}\mRightarrow{} ((fst(L[0])) = X))
\mwedge{} ((||L|| = 2)
{}\mRightarrow{} ((\muparrow{}ctt-opr-is(f;"Glue"))
\mvee{} (\muparrow{}ctt-opr-is(f;"case"))
\mvee{} (\muparrow{}ctt-opr-is(f;"comp"))
\mvee{} (\muparrow{}ctt-opr-is(f;"unglue"))
\mvee{} (\muparrow{}ctt-opr-is(f;"glue")))
{}\mRightarrow{} ((fst(L[0])) = X))
\mwedge{} ((||L|| = 2)
{}\mRightarrow{} ((\muparrow{}ctt-opr-is(f;"Glue"))
\mvee{} (\muparrow{}ctt-opr-is(f;"unglue")))
{}\mRightarrow{} ((fst(L[1])) = X))
\mwedge{} ((||L|| = 3)
{}\mRightarrow{} ((\muparrow{}ctt-opr-is(f;"Glue"))
\mvee{} (\muparrow{}ctt-opr-is(f;"case"))
\mvee{} (\muparrow{}ctt-opr-is(f;"unglue")))
{}\mRightarrow{} ((fst(L[1])) = X))
\mwedge{} ((||L|| = 3)
{}\mRightarrow{} (\muparrow{}ctt-opr-is(f;"glue"))
{}\mRightarrow{} ((fst(L[0])) = X))
\mwedge{} ((||L|| = 4)
{}\mRightarrow{} (\muparrow{}ctt-opr-is(f;"glue"))
{}\mRightarrow{} ((fst(L[0])) = X))\} ].
(provisional-subterm-context\{i:l\}(X;f;vs;L) \mmember{} ?CubicalContext)
Date html generated:
2020_05_21-AM-10_37_49
Last ObjectModification:
2020_05_18-AM-10_19_19
Theory : cubical!type!theory
Home
Index