Nuprl Lemma : accumulate_abort_nil_lemma
∀s,F:Top. (accumulate_abort(x,y.F[x;y];s;[]) ~ s)
Proof
Definitions occuring in Statement :
accumulate_abort: accumulate_abort(x,sofar.F[x; sofar];s;L),
nil: [],
top: Top,
so_apply: x[s1;s2],
all: ∀x:A. B[x],
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
accumulate_abort: accumulate_abort(x,sofar.F[x; sofar];s;L),
eager-accum: eager-accum(x,a.f[x; a];y;l),
nil: [],
it: ⋅,
member: t ∈ T
Lemmas referenced :
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :lambdaFormation_alt,
cut,
sqequalRule,
hypothesis,
Error :inhabitedIsType,
hypothesisEquality,
introduction,
extract_by_obid
Latex:
\mforall{}s,F:Top. (accumulate\_abort(x,y.F[x;y];s;[]) \msim{} s)
Date html generated:
2019_06_20-PM-00_44_41
Last ObjectModification:
2019_01_29-AM-10_24_18
Theory : omega
Home
Index