Nuprl Lemma : ifthenelse_wf-partial

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


Proof




Definitions occuring in Statement :  partial: partial(T) value-type: value-type(T) ifthenelse: if then else fi  bool: 𝔹 all: x:A. B[x] implies:  Q member: t ∈ T universe: Type
Definitions unfolded in proof :  all: x:A. B[x] implies:  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: supposing a bool: 𝔹 subtype_rel: A ⊆B so_lambda: λ2y.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: ⇐⇒ Q rev_implies:  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