Nuprl Lemma : FOStruct-false-subtype-evidence
∀Dom:Type. ∀S:FOStruct+{i:l}(Dom). ∀fmla:mFOL(). ∀a:FOAssignment(mFOL-freevars(fmla),Dom).
((S "false" []) ⊆r Dom,S,a +|= FOL-abstract(fmla))
Proof
Definitions occuring in Statement :
FOL-abstract: FOL-abstract(fmla),
mFOL-freevars: mFOL-freevars(fmla),
mFOL: mFOL(),
FOSatWith+: Dom,S,a +|= fmla,
FOStruct+: FOStruct+{i:l}(Dom),
FOAssignment: FOAssignment(vs,Dom),
nil: [],
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
apply: f a,
token: "$token",
universe: Type
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
so_lambda: λ2x.t[x],
member: t ∈ T,
FOStruct+: FOStruct+{i:l}(Dom),
FOStruct: FOStruct(Dom),
subtype_rel: A ⊆r B,
prop: ℙ,
so_apply: x[s],
implies: P ⇒ Q,
FOL-abstract: FOL-abstract(fmla),
mFOL-freevars: mFOL-freevars(fmla),
mFOatomic: name(vars),
mFOL_ind: mFOL_ind,
AbstractFOAtomic+: AbstractFOAtomic+(n;L),
FOSatWith+: Dom,S,a +|= fmla,
mFOconnect: mFOconnect(knd;left;right),
FOConnective+: FOConnective+(knd),
uimplies: b supposing a,
AbstractFOFormula+: AbstractFOFormula+(vs),
mFOquant: mFOquant(isall;var;body),
FOQuantifier+: FOQuantifier+(isall),
guard: {T},
FOAssignment: FOAssignment(vs,Dom),
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
let: let,
ifthenelse: if b then t else f fi ,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
uiff: uiff(P;Q),
or: P ∨ Q,
bfalse: ff,
exists: ∃x:A. B[x],
sq_type: SQType(T),
bnot: ¬bb,
assert: ↑b,
false: False
Lemmas referenced :
mFOL-induction,
all_wf,
FOAssignment_wf,
mFOL-freevars_wf,
subtype_rel_wf,
nil_wf,
FOSatWith+_wf,
FOL-abstract_wf,
mFOL_wf,
remove-repeats_wf,
int-deq_wf,
list_wf,
val-union_wf,
int-valueall-type,
AbstractFOFormula+_wf,
filter_wf5,
bnot_wf,
eq_int_wf,
l_member_wf,
bool_wf,
FOStruct+_wf,
list-subtype,
subtype_rel_b-union-right,
map_wf,
subtype_rel_dep_function,
subtype_rel_sets,
member-remove-repeats,
set_wf,
val-union-l-union,
eq_atom_wf,
eqtt_to_assert,
assert_of_eq_atom,
subtype_rel_FOAssignment,
l-union_wf,
union-contains,
union-contains2,
or_wf,
equal_wf,
eqff_to_assert,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
neg_assert_of_eq_atom,
update-assignment_wf,
exists_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
sqequalRule,
lambdaEquality,
hypothesisEquality,
hypothesis,
cumulativity,
applyEquality,
setElimination,
rename,
tokenEquality,
universeEquality,
independent_functionElimination,
intEquality,
atomEquality,
independent_isectElimination,
because_Cache,
setEquality,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
productElimination,
unionElimination,
equalityElimination,
productEquality,
dependent_pairFormation,
promote_hyp,
instantiate,
voidElimination,
functionEquality
Latex:
\mforall{}Dom:Type. \mforall{}S:FOStruct+\{i:l\}(Dom). \mforall{}fmla:mFOL(). \mforall{}a:FOAssignment(mFOL-freevars(fmla),Dom).
((S "false" []) \msubseteq{}r Dom,S,a +|= FOL-abstract(fmla))
Date html generated:
2018_05_21-PM-10_34_28
Last ObjectModification:
2017_07_26-PM-06_42_03
Theory : minimal-first-order-logic
Home
Index