Step * 1 2 of Lemma list-decomp-no_repeats


1. Type
2. l1 List
3. l2 List
4. l3 List
5. l4 List
6. T
7. no_repeats(T;(l1 [x]) l2)
8. ((l1 [x]) l2) ((l3 [x]) l4) ∈ (T List)
9. ((||l1|| 1) ||l2||) ((||l3|| 1) ||l4||) ∈ ℤ
10. ∀i:ℕ(||l1|| 1) ||l2||. ((l1 [x]) l2[i] (l3 [x]) l4[i] ∈ T)
11. ||l1|| ||l3|| ∈ ℤ
12. : ℕ||l1||
⊢ l1[i] l3[i] ∈ T
BY
((InstHyp [⌜i⌝(-3)⋅ THENA Auto') THEN RepeatFor ((RWO "select_append_front" (-1) THENA Auto')) THEN Auto) }


Latex:


Latex:

1.  T  :  Type
2.  l1  :  T  List
3.  l2  :  T  List
4.  l3  :  T  List
5.  l4  :  T  List
6.  x  :  T
7.  no\_repeats(T;(l1  @  [x])  @  l2)
8.  ((l1  @  [x])  @  l2)  =  ((l3  @  [x])  @  l4)
9.  ((||l1||  +  1)  +  ||l2||)  =  ((||l3||  +  1)  +  ||l4||)
10.  \mforall{}i:\mBbbN{}(||l1||  +  1)  +  ||l2||.  ((l1  @  [x])  @  l2[i]  =  (l3  @  [x])  @  l4[i])
11.  ||l1||  =  ||l3||
12.  i  :  \mBbbN{}||l1||
\mvdash{}  l1[i]  =  l3[i]


By


Latex:
((InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto')
  THEN  RepeatFor  2  ((RWO  "select\_append\_front"  (-1)  THENA  Auto'))
  THEN  Auto)




Home Index