Nuprl Lemma : mFOL-sequent-evidence_and
From uniform evidence that hyps ⇒ x and
uniform evidence that (y ∧ hyps) ⇒ y
we construct uniform evidence that hyps ⇒ x ∧ y⋅
∀hyps:mFOL() List. ∀[x,y:mFOL()]. (mFOL-sequent-evidence(<hyps, x>) ⇒ mFOL-sequent-evidence(<hyps, y>) ⇒ mFOL-sequent\000C-evidence(<hyps, x ∧ y>))
Proof
Definitions occuring in Statement :
mFOL-sequent-evidence: mFOL-sequent-evidence(s),
mFOconnect: mFOconnect(knd;left;right),
mFOL: mFOL(),
list: T List,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
pair: <a, b>,
token: "$token"
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
mFOL-sequent-evidence: mFOL-sequent-evidence(s),
mFO-uniform-evidence: mFO-uniform-evidence(vs;fmla),
and: P ∧ Q,
cand: A c∧ B,
member: t ∈ T,
subtype_rel: A ⊆r B,
uimplies: b supposing a,
mFOL-freevars: mFOL-freevars(fmla),
mFOconnect: mFOconnect(knd;left;right),
mFOL_ind: mFOL_ind,
mFOL-sequent-abstract: mFOL-sequent-abstract(s),
FOSatWith: Dom,S,a |= fmla,
mFOL-abstract: mFOL-abstract(fmla),
FOConnective: FOConnective(knd),
eq_atom: x =a y,
ifthenelse: if b then t else f fi ,
btrue: tt,
let: let,
mFOL-sequent: mFOL-sequent()
Lemmas referenced :
subtype_rel_FOAssignment,
mFOL-sequent-freevars_wf,
mFOconnect_wf,
mFOL-sequent-freevars-subset-3,
val-union-l-union,
int-deq_wf,
mFOL-freevars_wf,
int-valueall-type,
union-contains,
union-contains2,
tuple-type_wf,
mFOL-hyps-meaning_wf,
FOAssignment_wf,
FOStruct_wf,
mFOL-sequent-evidence_wf,
list_wf,
mFOL_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
isect_memberFormation,
cut,
sqequalHypSubstitution,
hypothesis,
isectElimination,
thin,
hypothesisEquality,
dependent_functionElimination,
applyEquality,
lemma_by_obid,
independent_pairEquality,
tokenEquality,
because_Cache,
sqequalRule,
independent_isectElimination,
independent_functionElimination,
intEquality,
independent_pairFormation,
productElimination,
universeEquality,
lambdaEquality,
productEquality
Latex:
\mforall{}hyps:mFOL() List. \mforall{}[x,y:mFOL()]. (mFOL-sequent-evidence(<hyps, x>) {}\mRightarrow{} mFOL-sequent-evidence(<hyps,\000C y>) {}\mRightarrow{} mFOL-sequent-evidence(<hyps, x \mwedge{} y>))
Date html generated:
2016_07_08-PM-05_21_59
Last ObjectModification:
2015_12_27-PM-06_25_33
Theory : minimal-first-order-logic
Home
Index