Nuprl Lemma : shorten-tuple-simplify

[p:Top × Top × Top]. (fst(shorten-tuple(p;1)) fst(snd(p)))


Proof




Definitions occuring in Statement :  shorten-tuple: shorten-tuple(x;n) uall: [x:A]. B[x] top: Top pi1: fst(t) pi2: snd(t) product: x:A × B[x] natural_number: $n sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T shorten-tuple: shorten-tuple(x;n) le_int: i ≤j lt_int: i <j bnot: ¬bb ifthenelse: if then else fi  btrue: tt pi2: snd(t) subtract: m bfalse: ff pi1: fst(t)
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut productElimination thin sqequalRule sqequalAxiom hypothesis productEquality lemma_by_obid

Latex:
\mforall{}[p:Top  \mtimes{}  Top  \mtimes{}  Top].  (fst(shorten-tuple(p;1))  \msim{}  fst(snd(p)))



Date html generated: 2016_05_14-PM-03_59_06
Last ObjectModification: 2015_12_26-PM-07_21_34

Theory : tuples


Home Index