Nuprl Lemma : seq-nil-len
||seq-nil()|| ~ 0
Proof
Definitions occuring in Statement :
seq-nil: seq-nil(),
seq-len: ||s||,
natural_number: $n,
sqequal: s ~ t
Definitions unfolded in proof :
seq-nil: seq-nil(),
pi1: fst(t),
seq-len: ||s||
Rules used in proof :
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalRule,
sqequalSubstitution
Latex:
||seq-nil()|| \msim{} 0
Date html generated:
2018_07_25-PM-01_29_27
Last ObjectModification:
2018_06_18-PM-02_00_36
Theory : arithmetic
Home
Index