(13steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: no repeats append iff 4
1. T: Type
2. l1: T List
3. l2: T List
4. x:T. ((x l1) & (x l2))
5. i,j:. i < ||l1|| j < ||l1|| i = j l1[i] = l1[j]
6. i,j:. i < ||l2|| j < ||l2|| i = j l2[i] = l2[j]
7. i:
8. j:
9. i < ||l1 @ l2||
10. j < ||l1 @ l2||
11. i = j
(l1 @ l2)[i] = (l1 @ l2)[j]
By:
((All (RWO Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs|| )) THEN (Decide (i < ||l1||))) THENL [RW (AddrC [1;2] (LemmaC Thm* as,bs:T List, i:||as||. (as @ bs)[i] = as[i])) 0 ;RW (AddrC [1;2] (LemmaC Thm* as,bs:T List, i:{||as||..(||as||+||bs||)}. (as @ bs)[i] = bs[(i-||as||)])) 0]
THEN
(Decide (j < ||l1||)) THENL [RW (AddrC [1;3] (LemmaC Thm* as,bs:T List, i:||as||. (as @ bs)[i] = as[i])) 0 ;RW (AddrC [1;3] (LemmaC Thm* as,bs:T List, i:{||as||..(||as||+||bs||)}. (as @ bs)[i] = bs[(i-||as||)])) 0]
THEN
Try (BackThruSomeHyp THEN (Complete Auto))
Generated subgoals:

19. i < ||l1||+||l2||
10. j < ||l1||+||l2||
11. i = j
12. i < ||l1||
13. j < ||l1||
l1[i] = l2[(j-||l1||)]		3 steps
 
29. i < ||l1||+||l2||
10. j < ||l1||+||l2||
11. i = j
12. i < ||l1||
13. j < ||l1||
l2[(i-||l1||)] = l1[j]		3 steps

About:
listintnatural_numberaddsubtractless_thanuniverseequalimpliesandall

(13steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc