Nuprl Lemma : per-close_wf
∀[Term:{T:Type| T ⊆r Base} ]. ∀[EQ:Term ⟶ Term ⟶ Term ⟶ Term]. ∀[ts:candidate-type-system{i:l, i:l}(Term)].
∀[T,T':Term]. ∀[eq:term-equality{i:l}(Term)].
(per-close{i:l}(Term;EQ;ts;T;T';eq) ∈ 𝕌')
Proof
Definitions occuring in Statement :
per-close: per-close{i:l}(Term;EQ;ts;T;T';eq),
candidate-type-system: candidate-type-system{i:l,j:l}(Term),
term-equality: term-equality{i:l}(Term),
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
member: t ∈ T,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
base: Base,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
per-close: per-close{i:l}(Term;EQ;ts;T;T';eq),
or: P ∨ Q,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
candidate-type-system: candidate-type-system{i:l,j:l}(Term),
prop: ℙ,
spreadn: spread4,
all: ∀x:A. B[x],
and: P ∧ Q,
exists: ∃x:A. B[x],
per-eq-def: per-eq-def{i:l}(Term;EQ;ts;T;T';eq),
guard: {T},
implies: P ⇒ Q,
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
so_apply: x[s],
term-equality: term-equality{i:l}(Term),
so_lambda: λ2x.t[x]
Lemmas referenced :
term-equality_wf,
candidate-type-system_wf,
istype-universe,
subtype_rel_wf,
base_wf,
subtype_rel_product,
per-computes-to_wf,
all_wf,
iff_wf,
subtype_base_sq,
or_wf,
per-eq-def_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
setElimination,
thin,
rename,
sqequalRule,
parameterizedRecEquality,
sqequalHypSubstitution,
hypothesis,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
universeIsType,
extract_by_obid,
isectElimination,
hypothesisEquality,
isect_memberEquality_alt,
isectIsTypeImplies,
inhabitedIsType,
instantiate,
functionIsType,
because_Cache,
setIsType,
universeEquality,
productEquality,
independent_isectElimination,
functionEquality,
independent_pairEquality,
applyEquality,
cumulativity,
lemma_by_obid,
productElimination,
lambdaEquality,
lambdaFormation,
unionElimination,
inlEquality,
inrEquality,
dependent_functionElimination,
sqequalIntensionalEquality,
dependent_set_memberEquality,
dependent_pairEquality
Latex:
\mforall{}[Term:\{T:Type| T \msubseteq{}r Base\} ]. \mforall{}[EQ:Term {}\mrightarrow{} Term {}\mrightarrow{} Term {}\mrightarrow{} Term]. \mforall{}[ts:candidate-type-system\{i:l,
i:l\}
(Term)]. \mforall{}[T,T':Term].
\mforall{}[eq:term-equality\{i:l\}(Term)].
(per-close\{i:l\}(Term;EQ;ts;T;T';eq) \mmember{} \mBbbU{}')
Date html generated:
2020_05_20-AM-07_47_58
Last ObjectModification:
2020_01_25-AM-09_35_26
Theory : parameterized!rec
Home
Index