Nuprl - Proof: no repeats reverse 1

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

1. T: Type
2. L: T List
3. u: T
4. v: T List
5. no_repeats(T;rev(v)) no_repeats(T;v)

no_repeats(T;rev(v) @ [u]) no_repeats(T;[u / v])

By: RWO Thm* l:T List, x:T. no_repeats(T;[x / l]) no_repeats(T;l) & (x l) 0 THEN RWO Thm* l1,l2:T List. no_repeats(T;l1 @ l2) l_disjoint(T;l1;l2) & no_repeats(T;l1) & no_repeats(T;l2) 0 THEN RWO Thm* a,b:T List, t:T. l_disjoint(T;b;[t / a]) (t b) & l_disjoint(T;b;a) 0 THEN RWO Thm* x:T, L:T List. (x rev(L)) (x L) 0

Generated subgoal:

1 (u v) & l_disjoint(T;rev(v);nil) & no_repeats(T;rev(v)) & no_repeats(T;[u]) no_repeats(T;v) & (u v) 1 step

About:

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