Nuprl Lemma : weak-antecedent-conditional
∀es:EO
  ∀[P1,Q1,P2,Q2:E ⟶ ℙ].
    ∀dcd_P1:e:E ⟶ Dec(P1 e). ∀f:{e:E| P1 e}  ⟶ {e:E| Q1 e} . ∀g:{e:E| P2 e}  ⟶ {e:E| Q2 e} .
      ((Q1 ←==f== P1 ∧ Q2 ←==g== P2) 
⇒ λe.((Q1 e) ∨ (Q2 e)) ←==[P1? f : g]== λe.((P1 e) ∨ (P2 e)))
Proof
Definitions occuring in Statement : 
weak-antecedent-function: Q ←==f== P
, 
conditional: [P? f : g]
, 
es-E: E
, 
event_ordering: EO
, 
decidable: Dec(P)
, 
uall: ∀[x:A]. B[x]
, 
prop: ℙ
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
or: P ∨ Q
, 
and: P ∧ Q
, 
set: {x:A| B[x]} 
, 
apply: f a
, 
lambda: λx.A[x]
, 
function: x:A ⟶ B[x]
Definitions unfolded in proof : 
all: ∀x:A. B[x]
, 
uall: ∀[x:A]. B[x]
, 
implies: P 
⇒ Q
, 
and: P ∧ Q
, 
member: t ∈ T
, 
prop: ℙ
, 
subtype_rel: A ⊆r B
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s]
, 
uimplies: b supposing a
, 
weak-antecedent-function: Q ←==f== P
, 
cand: A c∧ B
, 
or: P ∨ Q
, 
conditional: [P? f : g]
, 
branch: if p:P then A[p] else B fi 
, 
decidable: Dec(P)
, 
not: ¬A
, 
false: False
, 
guard: {T}
Latex:
\mforall{}es:EO
    \mforall{}[P1,Q1,P2,Q2:E  {}\mrightarrow{}  \mBbbP{}].
        \mforall{}dcd$_{P1}$:e:E  {}\mrightarrow{}  Dec(P1  e).  \mforall{}f:\{e:E|  P1  e\}    {}\mrightarrow{}  \{e:E|  Q1  e\}  .  \mforall{}g:\{e:E|  P2  e\000C\}    {}\mrightarrow{}  \{e:E|  Q2  e\}  .
            ((Q1  \mleftarrow{}==f==  P1  \mwedge{}  Q2  \mleftarrow{}==g==  P2)  {}\mRightarrow{}  \mlambda{}e.((Q1  e)  \mvee{}  (Q2  e))  \mleftarrow{}==[P1?  f  :  g]==  \mlambda{}e.((P1  e)  \mvee{}  (P2  e)))
Date html generated:
2016_05_16-AM-10_16_33
Last ObjectModification:
2015_12_28-PM-09_29_05
Theory : new!event-ordering
Home
Index