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)


Proof




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

Latex:
\mforall{}z,f:Top.
    (accumulate  (with  value  x  and  list  item  y):
        f[x;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