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 not projected

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, 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], rel_or: R1

R2, predicate_or: P1

P2
Definitions : so_lambda:

x.t[x], so_apply: x[s], or: P

Q, false: False, member: t

T, predicate_or: P1

P2, conditional: [P? f : g], Q-R-pre-preserving: f is Q-R-pre-preserving on P, implies: P

Q, and: P

Q, not:

A, uimplies: b supposing a, prop:

, uall:

[x:A]. B[x], all:

x:A. B[x], exists:

x:A. B[x], infix_ap: x f y, rel_or: R1

R2, guard: {T}, cand: A c

B, branch: if p:P then A[p] else B fi , decidable: Dec(P)
Lemmas : conditional_wf2, event_ordering_wf, decidable_wf, not_wf, and_wf, all_wf, Q-R-pre-preserving_wf, or_wf, rel_or_wf, es-E_wf, branch_wf2, equal_wf

\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: 2012_01_23-PM-12_14_48 Last ObjectModification: 2011_12_13-PM-12_32_13 Home Index