Nuprl Lemma : assert-ctt-term-is
∀s:Atom. ∀t:CttTerm.
((↑ctt-term-is(s;t))
⇒ {(¬↑isvarterm(t))
∧ (term-opr(t) = <"opid", s> ∈ CttOp)
∧ (||term-bts(t)|| = ||ctt-opid-arity(s)|| ∈ ℤ)
∧ (∀i:ℕ||term-bts(t)||
((||fst(term-bts(t)[i])|| = (fst(ctt-opid-arity(s)[i])) ∈ ℤ)
∧ (ctt-kind(snd(term-bts(t)[i])) = (snd(ctt-opid-arity(s)[i])) ∈ ℤ)))
∧ (t ~ mkwfterm(term-opr(t);term-bts(t)))})
Proof
Definitions occuring in Statement :
ctt-term-is: ctt-term-is(s;t),
ctt-term: CttTerm,
ctt-opid-arity: ctt-opid-arity(t),
ctt-kind: ctt-kind(t),
ctt-op: CttOp,
mkwfterm: mkwfterm(f;bts),
term-bts: term-bts(t),
term-opr: term-opr(t),
isvarterm: isvarterm(t),
select: L[n],
length: ||as||,
int_seg: {i..j-},
assert: ↑b,
guard: {T},
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
pair: <a, b>,
natural_number: $n,
int: ℤ,
token: "$token",
atom: Atom,
sqequal: s ~ t,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
ctt-term: CttTerm,
wfterm: wfterm(opr;sort;arity),
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
sq_type: SQType(T),
implies: P ⇒ Q,
guard: {T},
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
true: True,
subtype_rel: A ⊆r B,
coterm-fun: coterm-fun(opr;T),
isvarterm: isvarterm(t),
ctt-term-is: ctt-term-is(s;t),
isl: isl(x),
bnot: ¬bb,
bfalse: ff,
band: p ∧b q,
false: False,
mkterm: mkterm(opr;bts),
uiff: uiff(P;Q),
and: P ∧ Q,
not: ¬A,
ctt-op: CttOp,
term-opr: term-opr(t),
pi1: fst(t),
outr: outr(x),
sq_stable: SqStable(P),
squash: ↓T,
iff: P ⇐⇒ Q,
or: P ∨ Q,
eq_atom: x =a y,
ctt-arity: ctt-arity(x),
term-bts: term-bts(t),
mkwfterm: mkwfterm(f;bts),
pi2: snd(t),
cand: A c∧ B
Lemmas referenced :
assert_elim,
wf-term_wf,
ctt-op_wf,
ctt-kind_wf,
ctt-arity_wf,
subtype_base_sq,
bool_wf,
bool_subtype_base,
term-ext,
subtype_rel_weakening,
term_wf,
coterm-fun_wf,
ext-eq_inversion,
istype-void,
istype-assert,
assert-wf-mkterm,
ctt-term-is_wf,
ctt-term_wf,
istype-atom,
term-opr_wf,
isvarterm_wf,
sq_stable__l_member,
decidable__atom_equal,
cons_wf,
nil_wf,
cons_member,
atom_subtype_base,
ctt-tokens_wf,
assert_of_eq_atom,
int_seg_wf,
length_wf,
list_wf,
varname_wf,
member_singleton
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
sqequalHypSubstitution,
setElimination,
thin,
rename,
cut,
hypothesis,
introduction,
extract_by_obid,
isectElimination,
instantiate,
lambdaEquality_alt,
hypothesisEquality,
inhabitedIsType,
universeIsType,
independent_isectElimination,
cumulativity,
dependent_functionElimination,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
natural_numberEquality,
applyEquality,
sqequalRule,
unionElimination,
voidElimination,
productElimination,
dependent_set_memberEquality_alt,
equalityIstype,
atomEquality,
tokenEquality,
imageMemberEquality,
baseClosed,
imageElimination,
because_Cache,
independent_pairFormation,
productEquality,
independent_pairEquality,
functionIsTypeImplies,
axiomEquality,
axiomSqEquality,
equalityElimination
Latex:
\mforall{}s:Atom. \mforall{}t:CttTerm.
((\muparrow{}ctt-term-is(s;t))
{}\mRightarrow{} \{(\mneg{}\muparrow{}isvarterm(t))
\mwedge{} (term-opr(t) = <"opid", s>)
\mwedge{} (||term-bts(t)|| = ||ctt-opid-arity(s)||)
\mwedge{} (\mforall{}i:\mBbbN{}||term-bts(t)||
((||fst(term-bts(t)[i])|| = (fst(ctt-opid-arity(s)[i])))
\mwedge{} (ctt-kind(snd(term-bts(t)[i])) = (snd(ctt-opid-arity(s)[i])))))
\mwedge{} (t \msim{} mkwfterm(term-opr(t);term-bts(t)))\})
Date html generated:
2020_05_20-PM-08_23_13
Last ObjectModification:
2020_02_25-PM-02_45_17
Theory : cubical!type!theory
Home
Index