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

At: no repeats append iff 4 1
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
12. i < ||l1||
13. j < ||l1||
l1[i] = l2[(j-||l1||)]
By:
InstHyp [l1[i]] 4
THEN
ParallelOp -1
Generated subgoals:

114. l1[i] = l2[(j-||l1||)]
(l1[i] l1)		1 step
 
214. l1[i] = l2[(j-||l1||)]
(l1[i] l2)		1 step

About:
listaddsubtractless_thanuniverseequalimpliesandall

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