Nuprl Lemma : per-eq-def_wf
∀[Term:Type]. ∀[EQ:Term ⟶ Term ⟶ Term ⟶ Term]. ∀[ts:candidate-type-system{i:l, i':l}(Term)]. ∀[T,T':Term].
∀[eq:term-equality{i:l}(Term)].
per-eq-def{i:l}(Term;EQ;ts;T;T';eq) ∈ 𝕌' supposing Term ⊆r Base
Proof
Definitions occuring in Statement :
per-eq-def: per-eq-def{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),
uimplies: b supposing a,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
member: t ∈ T,
function: x:A ⟶ B[x],
base: Base,
universe: Type
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
per-eq-def: per-eq-def{i:l}(Term;EQ;ts;T;T';eq),
member: t ∈ T,
so_lambda: λ2x.t[x],
prop: ℙ,
and: P ∧ Q,
subtype_rel: A ⊆r B,
candidate-type-system: candidate-type-system{i:l,j:l}(Term),
term-equality: term-equality{i:l}(Term),
so_apply: x[s],
iff: P ⇐⇒ Q,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
rev_implies: P ⇐ Q,
implies: P ⇒ Q
Lemmas referenced :
exists_wf,
term-equality_wf,
per-computes-to_wf,
subtype_rel_wf,
base_wf,
all_wf,
iff_wf,
subtype_base_sq,
candidate-type-system_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
cut,
thin,
instantiate,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
cumulativity,
hypothesisEquality,
sqequalRule,
lambdaEquality,
because_Cache,
hypothesis,
productEquality,
dependent_set_memberEquality,
applyEquality,
universeEquality,
sqequalIntensionalEquality,
independent_isectElimination,
functionEquality
Latex:
\mforall{}[Term:Type]. \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-eq-def\{i:l\}(Term;EQ;ts;T;T';eq) \mmember{} \mBbbU{}' supposing Term \msubseteq{}r Base
Date html generated:
2016_05_15-PM-01_49_11
Last ObjectModification:
2015_12_27-AM-00_11_57
Theory : parameterized!rec
Home
Index