Nuprl Lemma : list_accum_cons_lemma
∀y,x,z,f:Top.
(accumulate (with value a and list item b):
f[a;b]
over list:
[x / y]
with starting value:
z) ~ accumulate (with value a and list item b):
f[a;b]
over list:
y
with starting value:
f[z;x]))
Proof
Definitions occuring in Statement :
list_accum: list_accum,
cons: [a / b],
top: Top,
so_apply: x[s1;s2],
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
list_accum: list_accum,
cons: [a / b],
member: t ∈ T
Lemmas referenced :
top_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalRule,
hypothesis,
introduction,
extract_by_obid
Latex:
\mforall{}y,x,z,f:Top.
(accumulate (with value a and list item b):
f[a;b]
over list:
[x / y]
with starting value:
z) \msim{} accumulate (with value a and list item b):
f[a;b]
over list:
y
with starting value:
f[z;x]))
Date html generated:
2018_05_21-PM-00_18_42
Last ObjectModification:
2018_05_19-AM-06_58_52
Theory : list_0
Home
Index