Nuprl Lemma : mFOL-proveable-formula-evidence-ext
Main Lemma. See mFOL-proveable-evidence also.⋅
∀[fmla:mFOL()]. (mFOL-proveable-formula(fmla) ⇒ mFOL-evidence(fmla))
Proof
Definitions occuring in Statement :
mFOL-proveable-formula: mFOL-proveable-formula(fmla),
mFOL-evidence: mFOL-evidence(fmla),
mFOL: mFOL(),
uall: ∀[x:A]. B[x],
implies: P ⇒ Q
Definitions unfolded in proof :
member: t ∈ T,
eq_atom: x =a y,
btrue: tt,
it: ⋅,
bfalse: ff,
ifthenelse: if b then t else f fi ,
int-deq: IntDeq,
mFOL-sequent-freevars: mFOL-sequent-freevars(s),
l-union: as ⋃ bs,
insert: insert(a;L),
eval_list: eval_list(t),
eq_bool: p =b q,
experimental: experimental{impliesFunctionality}(possibleextract),
experimental: experimental{allFunctionality}(possibleextract),
deq-witness: deq-witness(eq),
subtract: n - m,
experimental: experimental{orFunctionality}(possibleextract),
update-assignment: a[x := v],
deq-mFO: deq-mFO(),
eqof: eqof(d),
pi1: fst(t),
pi2: snd(t),
bnot: ¬bb,
null: null(as),
cons: [a / b],
all: ∀x:A. B[x],
top: Top,
mFOL-proveable-formula-evidence,
mFOL-proveable-evidence,
proof-tree-induction-ext,
any: any x,
FOLRule-induction-ext,
mFOL-sequent-evidence_and,
bool_cases_sqequal,
not-member-mFOL-sequent-freevars,
assert-bnot,
eqff_to_assert,
assert-deq-member,
mFOL-sequent-evidence_transitivity1,
union-contains,
eqtt_to_assert,
mFOL-sequent-evidence-trivial,
mFOL-sequent-evidence_transitivity2,
l_contains_transitivity,
select_member,
better-mFOL-sequent-evidence_transitivity1,
iff_weakening_equal,
cons_member,
bool_cases,
decidable__l_member,
decidable__equal_int,
l_all_iff,
member_filter,
iff_transitivity,
iff_weakening_uiff,
assert_of_bnot,
assert_of_eq_int,
list-cases,
sq_stable__correct_proof,
list_induction,
l_all_nil_iff,
member-union,
l_all_cons,
assert_of_bor,
safe-assert-deq,
decidable_functionality,
nil_member,
decidable__false,
decidable__or,
decidable__int_equal,
colist-cases,
member-insert,
decidable__assert,
iff_preserves_decidability,
colist-ext,
decidable-equal-deq
Lemmas referenced :
mFOL-proveable-formula-evidence,
length_of_cons_lemma,
mFOL-proveable-evidence,
proof-tree-induction-ext,
FOLRule-induction-ext,
mFOL-sequent-evidence_and,
bool_cases_sqequal,
not-member-mFOL-sequent-freevars,
assert-bnot,
eqff_to_assert,
assert-deq-member,
mFOL-sequent-evidence_transitivity1,
union-contains,
eqtt_to_assert,
mFOL-sequent-evidence-trivial,
mFOL-sequent-evidence_transitivity2,
l_contains_transitivity,
select_member,
better-mFOL-sequent-evidence_transitivity1,
iff_weakening_equal,
cons_member,
bool_cases,
decidable__l_member,
decidable__equal_int,
l_all_iff,
member_filter,
iff_transitivity,
iff_weakening_uiff,
assert_of_bnot,
assert_of_eq_int,
list-cases,
sq_stable__correct_proof,
list_induction,
l_all_nil_iff,
member-union,
l_all_cons,
assert_of_bor,
safe-assert-deq,
decidable_functionality,
nil_member,
decidable__false,
decidable__or,
decidable__int_equal,
colist-cases,
member-insert,
decidable__assert,
iff_preserves_decidability,
colist-ext,
decidable-equal-deq
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry,
dependent_functionElimination,
isect_memberEquality,
voidElimination,
voidEquality
Latex:
\mforall{}[fmla:mFOL()]. (mFOL-proveable-formula(fmla) {}\mRightarrow{} mFOL-evidence(fmla))
Date html generated:
2019_10_16-AM-11_43_33
Last ObjectModification:
2018_09_26-PM-09_31_59
Theory : minimal-first-order-logic
Home
Index