Nuprl Lemma : K-assignment_subtype
∀[K:mKripkeStruct]. ∀[i,j:World].
∀vs1,vs2:ℤ List. FOAssignment(vs1,Dom(i)) ⊆r FOAssignment(vs2,Dom(j)) supposing vs2 ⊆ vs1 supposing i ≤ j
Proof
Definitions occuring in Statement :
K-dom: Dom(i),
K-le: i ≤ j,
K-world: World,
mFO-Kripke-struct: mKripkeStruct,
FOAssignment: FOAssignment(vs,Dom),
l_contains: A ⊆ B,
list: T List,
uimplies: b supposing a,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
int: ℤ
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
all: ∀x:A. B[x],
l_contains: A ⊆ B,
so_lambda: λ2x.t[x],
prop: ℙ,
so_apply: x[s],
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
FOAssignment: FOAssignment(vs,Dom),
subtype_rel: A ⊆r B
Lemmas referenced :
l_all_iff,
l_member_wf,
istype-int,
subtype_rel_dep_function,
K-dom_wf,
subtype_rel_sets,
K-dom_subtype,
l_contains_wf,
list_wf,
K-le_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
lambdaFormation_alt,
sqequalHypSubstitution,
extract_by_obid,
isectElimination,
thin,
intEquality,
dependent_functionElimination,
hypothesisEquality,
sqequalRule,
lambdaEquality_alt,
hypothesis,
setElimination,
rename,
closedConclusion,
setIsType,
universeIsType,
productElimination,
independent_functionElimination,
setEquality,
independent_isectElimination,
because_Cache,
axiomEquality,
inhabitedIsType,
isect_memberEquality_alt,
isectIsTypeImplies,
functionIsTypeImplies
Latex:
\mforall{}[K:mKripkeStruct]. \mforall{}[i,j:World].
\mforall{}vs1,vs2:\mBbbZ{} List. FOAssignment(vs1,Dom(i)) \msubseteq{}r FOAssignment(vs2,Dom(j)) supposing vs2 \msubseteq{} vs1
supposing i \mleq{} j
Date html generated:
2019_10_16-AM-11_44_39
Last ObjectModification:
2018_10_13-AM-10_17_46
Theory : minimal-first-order-logic
Home
Index