Nuprl Lemma : list_accum_nil_lemma

z,f:Top.  (accumulate (with value and list item y): f[x;y]over list:  []with starting value: z) z)


Definitions occuring in Statement :  list_accum: list_accum nil: [] top: Top so_apply: x[s1;s2] all: x:A. B[x] sqequal: t
Definitions unfolded in proof :  list_accum: list_accum nil: [] it: all: x:A. B[x] member: t ∈ T
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep callbyvalueReduce sqleReflexivity lambdaFormation cut introduction extract_by_obid hypothesis

    (accumulate  (with  value  x  and  list  item  y):
      over  list:
      with  starting  value:
        z)  \msim{}  z)

Date html generated: 2018_05_21-PM-00_18_38
Last ObjectModification: 2018_05_19-AM-06_58_48

Theory : list_0

Home Index