### Nuprl Lemma : decide_wf

`∀[T1,T2,T3:Type]. ∀[x:T1 + T2]. ∀[l:T1 ⟶ T3]. ∀[r:T2 ⟶ T3].  (case x of inl(a) => l[a] | inr(b) => r[b] ∈ T3)`

Proof

Definitions occuring in Statement :  uall: `∀[x:A]. B[x]` so_apply: `x[s]` member: `t ∈ T` function: `x:A ⟶ B[x]` decide: `case b of inl(x) => s[x] | inr(y) => t[y]` union: `left + right` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` implies: `P `` Q` so_apply: `x[s]` prop: `ℙ`
Lemmas referenced :  equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesisEquality equalityTransitivity hypothesis equalitySymmetry thin unionEquality lambdaFormation unionElimination sqequalRule applyEquality extract_by_obid sqequalHypSubstitution isectElimination dependent_functionElimination independent_functionElimination axiomEquality functionEquality isect_memberEquality because_Cache universeEquality

Latex:
\mforall{}[T1,T2,T3:Type].  \mforall{}[x:T1  +  T2].  \mforall{}[l:T1  {}\mrightarrow{}  T3].  \mforall{}[r:T2  {}\mrightarrow{}  T3].
(case  x  of  inl(a)  =>  l[a]  |  inr(b)  =>  r[b]  \mmember{}  T3)

Date html generated: 2019_10_15-AM-11_06_47
Last ObjectModification: 2018_08_21-PM-01_58_34

Theory : general

Home Index