Nuprl Lemma : FOL-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()]. (FOL-sequent-evidence{i:l}(<hyps, x>) ⇒ FOL-sequent-evidence{i:l}(<hyps, y>) ⇒ FOL-\000Csequent-evidence{i:l}(<hyps, x ∧ y>))
Proof
Definitions occuring in Statement :
FOL-sequent-evidence: FOL-sequent-evidence{i:l}(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,
FOL-sequent-evidence: FOL-sequent-evidence{i:l}(s),
FO-uniform-evidence: FO-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,
FOL-sequent-abstract: FOL-sequent-abstract(s),
FOSatWith+: Dom,S,a +|= fmla,
FOL-abstract: FOL-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(),
pi2: snd(t),
prop: ℙ,
FOStruct+: FOStruct+{i:l}(Dom),
FOStruct: FOStruct(Dom)
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,
FOL-hyps-meaning_wf,
FOAssignment_wf,
FOStruct+_wf,
FOL-sequent-evidence_wf,
list_wf,
mFOL_wf,
mFOL-sequent-freevars-subset-1,
subtype_rel_b-union-left,
FOSatWith+_wf,
mFOL-sequent-freevars-contains-concl,
FOL-abstract_wf,
nil_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,
introduction,
cumulativity,
setElimination,
rename
Latex:
\mforall{}hyps:mFOL() List
\mforall{}[x,y:mFOL()]. (FOL-sequent-evidence\{i:l\}(<hyps, x>) {}\mRightarrow{} FOL-sequent-evidence\{i:l\}(<hyps, y>) {}\mRightarrow{} F\000COL-sequent-evidence\{i:l\}(<hyps, x \mwedge{} y>))
Date html generated:
2016_07_08-PM-05_22_10
Last ObjectModification:
2015_12_27-PM-06_25_49
Theory : minimal-first-order-logic
Home
Index