Nuprl Lemma : imax-list-as-reduce

[L:ℤ List]
  imax-list(L) outl(reduce(λx,y. case of inl(z) => inl imax(x;z) inr(z) => inl x;inr ⋅ ;L)) ∈ ℤ supposing 0 < ||L|\000C|


Definitions occuring in Statement :  imax-list: imax-list(L) length: ||as|| reduce: reduce(f;k;as) list: List imax: imax(a;b) outl: outl(x) less_than: a < b it: uimplies: supposing a uall: [x:A]. B[x] lambda: λx.A[x] decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a so_apply: x[s1;s2] assoc: Assoc(T;op) infix_ap: y squash: T prop: true: True subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q comm: Comm(T;op) sq_type: SQType(T) all: x:A. B[x] imax-list: imax-list(L)
Lemmas referenced :  combine-list-as-reduce imax_wf equal_wf squash_wf true_wf imax_assoc iff_weakening_equal imax_com subtype_base_sq int_subtype_base imax-list_wf less_than_wf length_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin intEquality lambdaEquality hypothesisEquality hypothesis independent_isectElimination sqequalRule applyEquality imageElimination equalityTransitivity equalitySymmetry universeEquality natural_numberEquality imageMemberEquality baseClosed productElimination independent_functionElimination because_Cache isect_memberEquality axiomEquality instantiate cumulativity dependent_functionElimination

\mforall{}[L:\mBbbZ{}  List]
    imax-list(L)  =  outl(reduce(\mlambda{}x,y.  case  y  of  inl(z)  =>  inl  imax(x;z)  |  inr(z)  =>  inl  x;inr  \mcdot{}  ;L)) 
    supposing  0  <  ||L||

Date html generated: 2017_04_17-AM-07_39_59
Last ObjectModification: 2017_02_27-PM-04_12_41

Theory : list_1

Home Index