---

{ [T,V:Type]. [A,B:T  ]. [dcd_A:t:T  Dec(A t)]. [f:{t:T| A t}   V].
  [g:{t:T| B t}   V]. [t:{t:T| (A t)  (B t)} ].
    (([A? f : g] t) = (f t) supposing A t
     ([A? f : g] t) = (g t) supposing (A t)) }

{ Proof }

---

Definitions occuring in Statement :  conditional: [P? f : g],  decidable: Dec(P),  uimplies: b supposing a,  uall: [x:A]. B[x],  prop: ,  not: A,  or: P  Q,  and: P  Q,  set: {x:A| B[x]} ,  apply: f a,  function: x:A  B[x],  universe: Type,  equal: s = t
Definitions :  uall: [x:A]. B[x],  prop: ,  or: P  Q,  and: P  Q,  uimplies: b supposing a,  conditional: [P? f : g],  branch: if p:P then A[p] else B fi ,  member: t  T,  all: x:A. B[x],  implies: P  Q,  decidable: Dec(P),  not: A,  false: False
Lemmas :  decidable_wf,  not_wf

---

\mforall{}[T,V:Type].  \mforall{}[A,B:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[dcd$_{A}$:t:T  {}\mrightarrow{}  Dec(A  t)].  \mforall{}[f:\{t:T|  A  t\}    {}\mrightarrow{}  V].\000C  \mforall{}[g:\{t:T|  B  t\}    {}\mrightarrow{}  V].
\mforall{}[t:\{t:T|  (A  t)  \mvee{}  (B  t)\}  ].
    (([A?  f  :  g]  t)  =  (f  t)  supposing  A  t  \mwedge{}  ([A?  f  :  g]  t)  =  (g  t)  supposing  \mneg{}(A  t))


Date html generated: 2011_08_16-AM-11_06_25
Last ObjectModification: 2011_06_18-AM-09_38_44

Home Index