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

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

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

About:
listaddsubtractless_thanuniverseequalimpliesandall

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