Nuprl - Proof: no repeats append iff 1

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

1. T: Type
2. l1: T List
3. l2: T List
4. i,j:. i < ||l1 @ l2|| j < ||l1 @ l2|| i = j (l1 @ l2)[i] = (l1 @ l2)[j]
5. x: T

((x l1) & (x l2))

By: RWO Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs|| 4 THEN Unfold `l_member` 0 THEN Analyze 0 THEN ExRepD THEN InstHyp [i1;i+||l1||] 4 THEN Analyze -1

Generated subgoal:

1 4. i,j:. i < ||l1||+||l2|| j < ||l1||+||l2|| i = j (l1 @ l2)[i] = (l1 @ l2)[j]
5. x: T
6. i1:
7. i1 < ||l1||
8. x = l1[i1]
9. i:
10. i < ||l2||
11. x = l2[i]
(l1 @ l2)[i1] = (l1 @ l2)[(i+||l1||)] 2 steps

About:

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