Nuprl Lemma : length-copath-cons

[b:Top]. ∀[p:Top × Top].  (copath-length(copath-cons(b;p)) copath-length(p) 1)


Proof




Definitions occuring in Statement :  copath-cons: copath-cons(b;x) copath-length: copath-length(p) uall: [x:A]. B[x] top: Top product: x:A × B[x] add: m natural_number: $n sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T copath-length: copath-length(p) pi1: fst(t) copath-cons: copath-cons(b;x)
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut productElimination thin sqequalRule hypothesis sqequalAxiom productEquality extract_by_obid sqequalHypSubstitution isect_memberEquality isectElimination hypothesisEquality because_Cache

Latex:
\mforall{}[b:Top].  \mforall{}[p:Top  \mtimes{}  Top].    (copath-length(copath-cons(b;p))  \msim{}  copath-length(p)  +  1)



Date html generated: 2018_07_25-PM-01_40_24
Last ObjectModification: 2018_06_01-AM-10_19_14

Theory : co-recursion


Home Index