Nuprl Lemma : K-uforces-umonotone
∀K:mKripkeStruct. ∀fmla:mFOL(). ∀i:World.
∀[j:World]
∀a:FOAssignment(mFOL-freevars(fmla),Dom(i)). ((K-uforces(K;fmla) i a) ⊆r (K-uforces(K;fmla) j a)) supposing i ≤ j
Proof
Definitions occuring in Statement :
K-uforces: K-uforces(K;fmla),
K-dom: Dom(i),
K-le: i ≤ j,
K-world: World,
mFO-Kripke-struct: mKripkeStruct,
mFOL-freevars: mFOL-freevars(fmla),
mFOL: mFOL(),
FOAssignment: FOAssignment(vs,Dom),
uimplies: b supposing a,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
apply: f a
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
uimplies: b supposing a,
prop: ℙ,
subtype_rel: A ⊆r B,
so_apply: x[s],
implies: P ⇒ Q,
top: Top,
guard: {T},
mFO-Kripke-struct: mKripkeStruct,
spreadn: spread4,
K-dom: Dom(i),
mFOL-freevars: mFOL-freevars(fmla),
FOAssignment: FOAssignment(vs,Dom),
mFOatomic: name(vars),
mFOL_ind: mFOL_ind,
pi1: fst(t),
pi2: snd(t),
K-le: i ≤ j,
K-sat: i,a |= fmla,
mFOL-abstract: mFOL-abstract(fmla),
K-struct: K-struct(K;i),
FOSatWith: Dom,S,a |= fmla,
AbstractFOAtomic: AbstractFOAtomic(n;L),
and: P ∧ Q,
K-world: World,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
istype: istype(T),
mFOconnect: mFOconnect(knd;left;right),
not: ¬A,
false: False,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
uiff: uiff(P;Q),
ifthenelse: if b then t else f fi ,
bfalse: ff,
or: P ∨ Q,
l_contains: A ⊆ B,
mFOquant: mFOquant(isall;var;body),
filter: filter(P;l),
reduce: reduce(f;k;as),
list_ind: list_ind,
exists: ∃x:A. B[x]
Lemmas referenced :
mFOL_wf,
mFO-Kripke-struct_wf,
mFOL-induction,
all_wf,
K-world_wf,
uall_wf,
isect_wf,
K-le_wf,
FOAssignment_wf,
mFOL-freevars_wf,
K-dom_wf,
subtype_rel_wf,
K-uforces_wf,
K-assignment_subtype,
l_contains_weakening,
K_uforces_atomic_lemma,
istype-void,
mFOatomic_wf,
list_wf,
istype-atom,
K_uforces_connect_lemma,
mFOconnect_wf,
K_uforces_quant_lemma,
mFOquant_wf,
istype-int,
bool_wf,
subtype_rel_self,
list-subtype,
map_wf,
l_member_wf,
subtype_rel_dep_function,
remove-repeats_wf,
int-deq_wf,
subtype_rel_sets,
member-remove-repeats,
K-le_reflexive,
val-union-l-union,
int-valueall-type,
union-contains,
union-contains2,
eq_atom_wf,
equal-wf-base,
atom_subtype_base,
assert_wf,
bnot_wf,
not_wf,
istype-assert,
uiff_transitivity,
eqtt_to_assert,
assert_of_eq_atom,
iff_transitivity,
iff_weakening_uiff,
eqff_to_assert,
assert_of_bnot,
subtype_rel_product,
subtype_rel_union,
K-le_transitivity,
l_all_iff,
filter_wf5,
eq_int_wf,
btrue_wf,
bool_subtype_base,
update-assignment_wf,
K-dom_subtype,
K-uforces-monotone
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation_alt,
universeIsType,
cut,
introduction,
extract_by_obid,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
sqequalRule,
lambdaEquality_alt,
hypothesisEquality,
because_Cache,
applyEquality,
independent_isectElimination,
dependent_functionElimination,
intEquality,
inhabitedIsType,
independent_functionElimination,
isect_memberFormation_alt,
isect_memberEquality_alt,
voidElimination,
axiomEquality,
functionIsTypeImplies,
isectIsTypeImplies,
functionIsType,
isectIsType,
productElimination,
closedConclusion,
equalityTransitivity,
equalitySymmetry,
setEquality,
setElimination,
rename,
setIsType,
equalityIsType1,
tokenEquality,
baseApply,
baseClosed,
atomEquality,
equalityIsType4,
unionElimination,
equalityElimination,
independent_pairFormation,
instantiate,
universeEquality
Latex:
\mforall{}K:mKripkeStruct. \mforall{}fmla:mFOL(). \mforall{}i:World.
\mforall{}[j:World]
\mforall{}a:FOAssignment(mFOL-freevars(fmla),Dom(i))
((K-uforces(K;fmla) i a) \msubseteq{}r (K-uforces(K;fmla) j a))
supposing i \mleq{} j
Date html generated:
2019_10_16-AM-11_46_19
Last ObjectModification:
2018_10_16-PM-01_25_20
Theory : minimal-first-order-logic
Home
Index