Nuprl Lemma : repeat-on-success_wf

[A,B:Type].
  (∀[C:Type]. ∀[f:A ⟶ (C?)]. ∀[g:(ℕ × C) ⟶ (A List) ⟶ (A List)].
     ∀[h:(ℕ × C) ⟶ B ⟶ B]. ∀[as:A List]. ∀[b:B].  (repeat-on-success(f;g;h;as;b) ∈ List × B) 
     supposing ∃m:(A List) ⟶ ℕ
                ∀as:A List. ∀c:C. ∀j:ℕ.
                  ((first-success(f;as) (inl <j, c>) ∈ (ℕ × C?))  (g <j, c> as) < as)) supposing 
     (value-type(B) and 
     valueall-type(A))


Proof




Definitions occuring in Statement :  repeat-on-success: repeat-on-success(f;g;h;as;b) first-success: first-success(f;L) list: List nat: valueall-type: valueall-type(T) value-type: value-type(T) less_than: a < b uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] exists: x:A. B[x] implies:  Q unit: Unit member: t ∈ T apply: a function: x:A ⟶ B[x] pair: <a, b> product: x:A × B[x] inl: inl x union: left right universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a exists: x:A. B[x] all: x:A. B[x] nat: implies:  Q false: False ge: i ≥  guard: {T} prop: subtype_rel: A ⊆B squash: T decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q and: P ∧ Q not: ¬A rev_implies:  Q uiff: uiff(P;Q) subtract: m top: Top le: A ≤ B less_than': less_than'(a;b) true: True repeat-on-success: repeat-on-success(f;g;h;as;b) so_lambda: λ2x.t[x] so_apply: x[s] sq_stable: SqStable(P) has-value: (a)↓
Lemmas referenced :  nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf list_wf nat_wf subtype_rel-equal base_wf le_weakening equal_wf decidable__le subtract_wf false_wf not-ge-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-one-mul-top minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel first-success_wf int_seg_wf length_wf unit_wf2 add_nat_wf le_wf sq_stable__le decidable__lt not-lt-2 add-mul-special zero-mul exists_wf all_wf subtype_rel_union subtype_rel_product int_seg_subtype_nat value-type_wf valueall-type_wf evalall-reduce list-valueall-type value-type-has-value list-value-type equal_functionality_wrt_subtype_rel2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin lambdaFormation extract_by_obid isectElimination hypothesisEquality hypothesis setElimination rename sqequalRule intWeakElimination natural_numberEquality independent_isectElimination independent_functionElimination voidElimination lambdaEquality dependent_functionElimination isect_memberEquality axiomEquality equalityTransitivity equalitySymmetry applyEquality functionExtensionality cumulativity because_Cache dependent_pairFormation sqequalIntensionalEquality applyLambdaEquality imageMemberEquality baseClosed promote_hyp unionElimination independent_pairFormation addEquality minusEquality voidEquality intEquality unionEquality productEquality dependent_set_memberEquality imageElimination multiplyEquality functionEquality inlEquality independent_pairEquality universeEquality callbyvalueReduce

Latex:
\mforall{}[A,B:Type].
    (\mforall{}[C:Type].  \mforall{}[f:A  {}\mrightarrow{}  (C?)].  \mforall{}[g:(\mBbbN{}  \mtimes{}  C)  {}\mrightarrow{}  (A  List)  {}\mrightarrow{}  (A  List)].
          \mforall{}[h:(\mBbbN{}  \mtimes{}  C)  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[as:A  List].  \mforall{}[b:B].    (repeat-on-success(f;g;h;as;b)  \mmember{}  A  List  \mtimes{}  B) 
          supposing  \mexists{}m:(A  List)  {}\mrightarrow{}  \mBbbN{}
                                \mforall{}as:A  List.  \mforall{}c:C.  \mforall{}j:\mBbbN{}.
                                    ((first-success(f;as)  =  (inl  <j,  c>))  {}\mRightarrow{}  m  (g  <j,  c>  as)  <  m  as))  supposing 
          (value-type(B)  and 
          valueall-type(A))



Date html generated: 2017_04_14-AM-08_39_46
Last ObjectModification: 2017_02_27-PM-03_30_28

Theory : list_0


Home Index