Nuprl Lemma : list_accum_nil_lemma
∀z,f:Top. (accumulate (with value x 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: s ~ 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