Nuprl Lemma : colist-fix-ap-partial

  (∀[T:Type]. ∀[f:⋂L:Type. ((L ⟶ partial(A)) ⟶ (Unit ⋃ (T × L)) ⟶ partial(A))]. ∀[L:colist(T)].
     (fix(f) L ∈ partial(A))) supposing 
     (mono(A) and 


Definitions occuring in Statement :  colist: colist(T) partial: partial(T) mono: mono(T) value-type: value-type(T) b-union: A ⋃ B uimplies: supposing a uall: [x:A]. B[x] unit: Unit member: t ∈ T apply: a fix: fix(F) isect: x:A. B[x] function: x:A ⟶ B[x] product: x:A × B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a member: t ∈ T prop:
Lemmas referenced :  colist-fix-partial colist_wf partial_wf b-union_wf unit_wf2 mono_wf value-type_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_isectElimination hypothesis isectEquality universeEquality cumulativity functionEquality productEquality applyEquality

    (\mforall{}[T:Type].  \mforall{}[f:\mcap{}L:Type.  ((L  {}\mrightarrow{}  partial(A))  {}\mrightarrow{}  (Unit  \mcup{}  (T  \mtimes{}  L))  {}\mrightarrow{}  partial(A))].  \mforall{}[L:colist(T)].
          (fix(f)  L  \mmember{}  partial(A)))  supposing 
          (mono(A)  and 

Date html generated: 2016_05_14-AM-06_25_27
Last ObjectModification: 2015_12_26-PM-00_42_29

Theory : list_0

Home Index