Nuprl Lemma : list_accum'_wf

[A,B:Type].
  ∀[f:B ⟶ {L:A List| 0 < ||L||}  ⟶ B]. ∀[L:A List]. ∀[v:B].  (list_accum'(f;v;L) ∈ B) supposing valueall-type(B)


Proof




Definitions occuring in Statement :  list_accum': list_accum'(f;v;L) length: ||as|| list: List valueall-type: valueall-type(T) less_than: a < b uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T set: {x:A| B[x]}  function: x:A ⟶ B[x] natural_number: $n universe: Type
Definitions unfolded in proof :  nat_plus: + has-valueall: has-valueall(a) has-value: (a)↓ callbyvalueall: callbyvalueall exists: x:A. B[x] bfalse: ff less_than: a < b sq_type: SQType(T) so_apply: x[s] so_lambda: λ2x.t[x] it: nil: [] subtract: m rev_implies:  Q iff: ⇐⇒ Q decidable: Dec(P) true: True less_than': less_than'(a;b) not: ¬A le: A ≤ B and: P ∧ Q uiff: uiff(P;Q) sq_stable: SqStable(P) squash: T so_apply: x[s1;s2] top: Top so_lambda: λ2y.t[x; y] colength: colength(L) cons: [a b] btrue: tt ifthenelse: if then else fi  list_accum': list_accum'(f;v;L) or: P ∨ Q subtype_rel: A ⊆B prop: guard: {T} ge: i ≥  false: False implies:  Q nat: all: x:A. B[x] uimplies: supposing a member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  decidable__lt omega-shadow minus-zero not-lt-2 zero-mul mul-distributes-right two-mul add-mul-special one-mul le_reflexive valueall-type_wf list_wf evalall-reduce length_wf cons_wf length_wf_nat non_neg_length length_of_cons_lemma valueall-type-has-valueall null_cons_lemma int_subtype_base set_subtype_base subtype_base_sq add-swap minus-minus less-iff-le not-ge-2 subtract_wf equal_wf le_wf add-commutes minus-one-mul-top minus-one-mul minus-add condition-implies-le not-le-2 false_wf decidable__le le-add-cancel zero-add add-zero add-associates add_functionality_wrt_le le_antisymmetry_iff sq_stable__le spread_cons_lemma product_subtype_list null_nil_lemma list-cases colength_wf_list nat_wf equal-wf-T-base less_than_wf ge_wf less_than_irreflexivity less_than_transitivity1 nat_properties
Rules used in proof :  multiplyEquality universeEquality setEquality functionEquality callbyvalueReduce sqequalIntensionalEquality dependent_pairFormation functionExtensionality instantiate intEquality minusEquality independent_pairFormation dependent_set_memberEquality addEquality imageElimination baseClosed imageMemberEquality applyLambdaEquality voidEquality productElimination hypothesis_subsumption promote_hyp unionElimination because_Cache applyEquality cumulativity equalitySymmetry equalityTransitivity axiomEquality isect_memberEquality dependent_functionElimination lambdaEquality voidElimination independent_functionElimination independent_isectElimination natural_numberEquality intWeakElimination sqequalRule rename setElimination hypothesis hypothesisEquality isectElimination sqequalHypSubstitution extract_by_obid lambdaFormation thin cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[A,B:Type].
    \mforall{}[f:B  {}\mrightarrow{}  \{L:A  List|  0  <  ||L||\}    {}\mrightarrow{}  B].  \mforall{}[L:A  List].  \mforall{}[v:B].    (list\_accum'(f;v;L)  \mmember{}  B) 
    supposing  valueall-type(B)



Date html generated: 2017_04_14-AM-08_48_31
Last ObjectModification: 2017_04_10-PM-10_33_51

Theory : list_0


Home Index