Nuprl Lemma : radd_list_nil_lemma
radd-list([]) ~ r0
Proof
Definitions occuring in Statement :
radd-list: radd-list(L),
int-to-real: r(n),
nil: [],
natural_number: $n,
sqequal: s ~ t
Definitions unfolded in proof :
radd-list: radd-list(L),
callbyvalueall: callbyvalueall,
evalall: evalall(t),
nil: [],
it: ⋅,
length: ||as||,
list_ind: list_ind,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
btrue: tt,
int-to-real: r(n)
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalTransitivity,
computationStep,
sqequalReflexivity
Latex:
radd-list([]) \msim{} r0
Date html generated:
2016_05_18-AM-06_50_49
Last ObjectModification:
2015_12_28-AM-00_29_13
Theory : reals
Home
Index