Nuprl Lemma : conditional-ifthenelse
[T,V:Type]. [A,B:T 
]. [f:{x:T| 
(A x)} V]. [g:{x:T| (B x)} V].
((
x.if A x then f x else g x fi ) = [x.((A x))? f : g])
Proof not projected
Definitions occuring in Statement :
conditional: [P? f : g],
assert: b,
ifthenelse: if b then t else f fi ,
bool: ,
uall: [x:A]. B[x],
or: P 
Q,
set: {x:A| B[x]} ,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
universe: Type,
equal: s = t,
bool-decider: bool-decider(b)
Definitions :
member: t 
T,
uall: [x:A]. B[x],
conditional: [P? f : g],
so_lambda: 
x.t[x],
all: x:A. B[x],
or: P Q,
bfalse: ff,
btrue: tt,
implies: P 
Q,
top: Top,
ifthenelse: if b then t else f fi ,
prop: 
,
false: False,
so_apply: x[s],
not: 
A,
and: P 
Q,
uiff: uiff(P;Q),
uimplies: b supposing a,
unit: Unit,
bool: ,
iff: P 
Q,
decidable: Dec(P),
it: 
Lemmas :
bool_wf,
assert_wf,
not_wf,
bool-decider_wf,
branch_wf2,
or_wf,
assert_of_bnot,
eqff_to_assert,
bnot_wf,
equal_wf,
uiff_transitivity,
eqtt_to_assert,
branch-ifthenelse,
iff_weakening_uiff,
decidable__assert,
decidable__or
\mforall{}[T,V:Type]. \mforall{}[A,B:T {}\mrightarrow{} \mBbbB{}]. \mforall{}[f:\{x:T| \muparrow{}(A x)\} {}\mrightarrow{} V]. \mforall{}[g:\{x:T| \muparrow{}(B x)\} {}\mrightarrow{} V].
((\mlambda{}x.if A x then f x else g x fi ) = [\mlambda{}x.(\muparrow{}(A x))? f : g])
Date html generated:
2012_01_23-PM-12_14_39
Last ObjectModification:
2011_12_13-PM-12_48_05
Home
Index