Nuprl Lemma : append-tuple-shorten-tuple
∀[L:Type List]. ∀[x:tuple-type(L)]. ∀[n:ℕ||L||].
  (append-tuple(n;||L|| - n;fst(split-tuple(x;n));shorten-tuple(x;n)) ~ x)
Proof
Definitions occuring in Statement : 
append-tuple: append-tuple(n;m;x;y)
, 
shorten-tuple: shorten-tuple(x;n)
, 
split-tuple: split-tuple(x;n)
, 
tuple-type: tuple-type(L)
, 
length: ||as||
, 
list: T List
, 
int_seg: {i..j-}
, 
uall: ∀[x:A]. B[x]
, 
pi1: fst(t)
, 
subtract: n - m
, 
natural_number: $n
, 
universe: Type
, 
sqequal: s ~ t
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
subtype_rel: A ⊆r B
, 
uimplies: b supposing a
, 
le: A ≤ B
, 
and: P ∧ Q
, 
less_than': less_than'(a;b)
, 
false: False
, 
not: ¬A
, 
implies: P 
⇒ Q
, 
prop: ℙ
, 
top: Top
Lemmas referenced : 
append-tuple-split-tuple, 
int_seg_wf, 
length_wf, 
tuple-type_wf, 
list_wf, 
shorten-tuple-split-tuple, 
int_seg_subtype_nat, 
false_wf
Rules used in proof : 
cut, 
lemma_by_obid, 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation, 
hypothesis, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
hypothesisEquality, 
sqequalRule, 
natural_numberEquality, 
instantiate, 
universeEquality, 
applyEquality, 
independent_isectElimination, 
independent_pairFormation, 
lambdaFormation, 
isect_memberEquality, 
voidElimination, 
voidEquality
Latex:
\mforall{}[L:Type  List].  \mforall{}[x:tuple-type(L)].  \mforall{}[n:\mBbbN{}||L||].
    (append-tuple(n;||L||  -  n;fst(split-tuple(x;n));shorten-tuple(x;n))  \msim{}  x)
Date html generated:
2016_05_14-PM-03_59_02
Last ObjectModification:
2015_12_26-PM-07_21_37
Theory : tuples
Home
Index