Nuprl - Proof: no repeats append iff 3

(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. i:
6. j:
7. i < ||l2||
8. j < ||l2||
9. i = j

l2[i] = l2[j]

By: RWO Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs|| 4 THEN InstHyp [i+||l1||;j+||l1||] 4 THEN RWO Thm* as,bs:T List, i:{||as||..(||as||+||bs||)}. (as @ bs)[i] = bs[(i-||as||)] -1 THEN NthHypSq -1 THEN Repeat Analyze

Generated subgoals:

None

About:

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