Nuprl Lemma : Q-R-pre-preserving-conditional
∀es:EO
∀[P1,P2:E ⟶ ℙ]. ∀[Q1,R1,Q2,R2:E ⟶ E ⟶ ℙ].
∀dcd_P1:e:E ⟶ Dec(P1 e). ∀f1:{e:E| P1 e} ⟶ E. ∀f2:{e:E| P2 e} ⟶ E.
(f1 is Q1-R1-pre-preserving on P1
⇒ f2 is Q2-R2-pre-preserving on P2
⇒ [P1? f1 : f2] is Q1 ∨ Q2-R1 ∨ R2-pre-preserving on P1 ∨ P2) supposing
((∀e:{e:E| P1 e} . ∀e':{e:E| P2 e} .
((¬(Q1 (f1 e) (f2 e'))) ∧ (¬(Q1 (f2 e') (f1 e))) ∧ (¬(Q2 (f1 e) (f2 e'))) ∧ (¬(Q2 (f2 e') (f1 e))))) and
(∀e,e':{e:E| P2 e} . (¬(Q1 (f2 e) (f2 e')))) and
(∀e,e':{e:E| P1 e} . (¬(Q2 (f1 e) (f1 e')))))
Proof
Definitions occuring in Statement :
Q-R-pre-preserving: f is Q-R-pre-preserving on P,
conditional: [P? f : g],
es-E: E,
event_ordering: EO,
predicate_or: P1 ∨ P2,
rel_or: R1 ∨ R2,
decidable: Dec(P),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
prop: ℙ,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x]
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
uimplies: b supposing a,
member: t ∈ T,
not: ¬A,
implies: P ⇒ Q,
false: False,
subtype_rel: A ⊆r B,
prop: ℙ,
and: P ∧ Q,
Q-R-pre-preserving: f is Q-R-pre-preserving on P,
predicate_or: P1 ∨ P2,
so_apply: x[s],
so_lambda: λ2x.t[x],
or: P ∨ Q,
conditional: [P? f : g],
branch: if p:P then A[p] else B fi ,
exists: ∃x:A. B[x],
decidable: Dec(P),
rel_or: R1 ∨ R2,
infix_ap: x f y,
guard: {T},
cand: A c∧ B
Latex:
\mforall{}es:EO
\mforall{}[P1,P2:E {}\mrightarrow{} \mBbbP{}]. \mforall{}[Q1,R1,Q2,R2:E {}\mrightarrow{} E {}\mrightarrow{} \mBbbP{}].
\mforall{}dcd$_{P1}$:e:E {}\mrightarrow{} Dec(P1 e). \mforall{}f1:\{e:E| P1 e\} {}\mrightarrow{} E. \mforall{}f2:\{e:E| P2 e\} {}\mrightarrow{} E.
(f1 is Q1-R1-pre-preserving on P1
{}\mRightarrow{} f2 is Q2-R2-pre-preserving on P2
{}\mRightarrow{} [P1? f1 : f2] is Q1 \mvee{} Q2-R1 \mvee{} R2-pre-preserving on P1 \mvee{} P2) supposing
((\mforall{}e:\{e:E| P1 e\} . \mforall{}e':\{e:E| P2 e\} .
((\mneg{}(Q1 (f1 e) (f2 e')))
\mwedge{} (\mneg{}(Q1 (f2 e') (f1 e)))
\mwedge{} (\mneg{}(Q2 (f1 e) (f2 e')))
\mwedge{} (\mneg{}(Q2 (f2 e') (f1 e))))) and
(\mforall{}e,e':\{e:E| P2 e\} . (\mneg{}(Q1 (f2 e) (f2 e')))) and
(\mforall{}e,e':\{e:E| P1 e\} . (\mneg{}(Q2 (f1 e) (f1 e')))))
Date html generated:
2016_05_16-AM-10_19_41
Last ObjectModification:
2015_12_28-PM-09_33_53
Theory : new!event-ordering
Home
Index