Nuprl - Pf unequal termlists 1 2 1 2 1

(10steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc

1. a: Term List
2. u: Term
3. v: Term List
4. b:Term List. termlist_eq(v;b) ||v|| = ||b|| (i:. i < ||v|| & v[i] = b[i])
5. b: Term List
6. u1: Term
7. v1: Term List
8. termlist_eq([u / v];v1) ||[u / v]|| = ||v1|| (i:. i < ||[u / v]|| & [u / v][i] = v1[i])
9. term_eq(u;u1)
10. (term_eq(u;u1) & termlist_eq(v;v1))
11. ||v||+1 = ||v1||+1
12. i:
13. i < ||v||
14. v[i] = v1[i]

i+1 < ||v||+1 & [u / v][(i+1)] = [u1 / v1][(i+1)]

By: Auto THEN RWW "select_cons_tl" 0 THEN ArithSimp 0

Generated subgoals:

None

About:

(10steps) PrintForm Definitions mb automata 2 Sections GenAutomata Doc