Nuprl Lemma : copath_length_nil_lemma
copath-length(()) ~ 0
Proof
Definitions occuring in Statement :
copath-nil: (),
copath-length: copath-length(p),
natural_number: $n,
sqequal: s ~ t
Definitions unfolded in proof :
copath-nil: (),
pi1: fst(t),
copath-length: copath-length(p)
Rules used in proof :
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalRule,
sqequalSubstitution
Latex:
copath-length(()) \msim{} 0
Date html generated:
2018_07_25-PM-01_39_33
Last ObjectModification:
2018_06_26-AM-00_26_01
Theory : co-recursion
Home
Index