---

Step * 1 of Lemma append-tuple-one-one


1. L1 : Type List
2. L2 : Type List
3. 0 < ||L2||
4. x1 : tuple-type(L1)
5. x2 : tuple-type(L1)
6. y1 : tuple-type(L2)
7. y2 : tuple-type(L2)
8. append-tuple(||L1||;||L2||;x1;y1) = append-tuple(||L1||;||L2||;x2;y2) ∈ tuple-type(L1 @ L2)
9. <x1, y1> = <x2, y2> ∈ (tuple-type(firstn(||L1||;L1 @ L2)) × tuple-type(nth_tl(||L1||;L1 @ L2)))
⊢ {(x1 = x2 ∈ tuple-type(L1)) ∧ (y1 = y2 ∈ tuple-type(L2))}
BY
{ (SimpHyp (-1) THEN D 0 THEN Auto) }

1
1. L1 : Type List
2. L2 : Type List
3. 0 < ||L2||
4. x1 : tuple-type(L1)
5. x2 : tuple-type(L1)
6. y1 : tuple-type(L2)
7. y2 : tuple-type(L2)
8. append-tuple(||L1||;||L2||;x1;y1) = append-tuple(||L1||;||L2||;x2;y2) ∈ tuple-type(L1 @ L2)
9. x1 = x2 ∈ tuple-type(firstn(||L1||;L1 @ L2))
10. y1 = y2 ∈ tuple-type(nth_tl(||L1||;L1 @ L2))
⊢ x1 = x2 ∈ tuple-type(L1)

---

Latex:

---

Latex:

1.  L1  :  Type  List
2.  L2  :  Type  List
3.  0  <  ||L2||
4.  x1  :  tuple-type(L1)
5.  x2  :  tuple-type(L1)
6.  y1  :  tuple-type(L2)
7.  y2  :  tuple-type(L2)
8.  append-tuple(||L1||;||L2||;x1;y1)  =  append-tuple(||L1||;||L2||;x2;y2)
9.  <x1,  y1>  =  <x2,  y2>
\mvdash{}  \{(x1  =  x2)  \mwedge{}  (y1  =  y2)\}


By

---

Latex:
(SimpHyp  (-1)  THEN  D  0  THEN  Auto)

---

Home Index