### Nuprl Lemma : ifthenelse_wf-partial

`∀T:Type. (value-type(T) `` (∀c1,c2:partial(T). ∀b:partial(𝔹).  (if b then c1 else c2 fi  ∈ partial(T))))`

Proof

Definitions occuring in Statement :  partial: `partial(T)` value-type: `value-type(T)` ifthenelse: `if b then t else f fi ` bool: `𝔹` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` partial: `partial(T)` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` uall: `∀[x:A]. B[x]` prop: `ℙ` base-partial: `base-partial(T)` uimplies: `b supposing a` bool: `𝔹` subtype_rel: `A ⊆r B` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` per-partial: `per-partial(T;x;y)` uiff: `uiff(P;Q)` sq_type: `SQType(T)` guard: `{T}` not: `¬A` false: `False` squash: `↓T` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  base-partial_wf bool_wf per-partial_wf equal_wf equal-wf-base partial_wf value-type_wf has-value_wf-partial union-value-type unit_wf2 subtype_quotient per-partial-equiv_rel is-exception_wf subtype_base_sq bool_subtype_base base-partial-not-exception sqle_wf_base squash_wf true_wf base_wf iff_weakening_equal ifthenelse_wf-partial-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalHypSubstitution pointwiseFunctionalityForEquality because_Cache sqequalRule pertypeElimination productElimination thin equalityTransitivity hypothesis equalitySymmetry introduction extract_by_obid isectElimination rename setElimination hypothesisEquality dependent_functionElimination independent_functionElimination productEquality cumulativity universeEquality sqequalSqle divergentSqle independent_isectElimination applyEquality lambdaEquality instantiate sqleReflexivity voidElimination imageElimination natural_numberEquality imageMemberEquality baseClosed

Latex:
\mforall{}T:Type
(value-type(T)  {}\mRightarrow{}  (\mforall{}c1,c2:partial(T).  \mforall{}b:partial(\mBbbB{}).    (if  b  then  c1  else  c2  fi    \mmember{}  partial(T))))

Date html generated: 2017_04_14-AM-07_41_08
Last ObjectModification: 2017_02_27-PM-03_13_10

Theory : partial_1

Home Index