Nuprl - Pf assert termlist eq

(13steps) PrintForm Definitions Lemmas mb automata 2 Sections GenAutomata Doc

a,b:Term List. termlist_eq(a;b) a = b

By: Analyze 0 THEN ListInd -1 THEN Analyze 0 THEN ListInd -1 THEN RecUnfold `termlist_eq` 0 THEN Reduce 0 THEN let T ((ApFunToHypEquands `z' ||z|| -1) THEN (Reduce -1)) THEN (Complete Auto) in Try T

Generated subgoals:

1 1. a: Term List
2. u: Term
3. v: Term List
4. b:Term List. termlist_eq(v;b) v = b
5. b: Term List
6. u1: Term
7. v1: Term List
8. termlist_eq([u / v];v1) [u / v] = v1
9. termlist_eq([u / v];v1) ([u / v] = v1)
10. term_eq(u;u1)termlist_eq(v;v1)
[u / v] = [u1 / v1]

2 1. a: Term List
2. u: Term
3. v: Term List
4. b:Term List. termlist_eq(v;b) v = b
5. b: Term List
6. u1: Term
7. v1: Term List
8. termlist_eq([u / v];v1) [u / v] = v1
9. termlist_eq([u / v];v1) ([u / v] = v1)
10. [u / v] = [u1 / v1]
term_eq(u;u1)termlist_eq(v;v1)

About:

(13steps) PrintForm Definitions Lemmas mb automata 2 Sections GenAutomata Doc

1	1. `a:` `Term List` 2. `u:` `Term` 3. `v:` `Term List` 4. `b:Term List. termlist_eq(v;b) v = b` 5. `b:` `Term List` 6. `u1:` `Term` 7. `v1:` `Term List` 8. `termlist_eq([u / v];v1) [u / v] = v1` 9. `termlist_eq([u / v];v1) ([u / v] = v1)` 10. `term_eq(u;u1)termlist_eq(v;v1)` `[u / v] = [u1 / v1]`
2	1. `a:` `Term List` 2. `u:` `Term` 3. `v:` `Term List` 4. `b:Term List. termlist_eq(v;b) v = b` 5. `b:` `Term List` 6. `u1:` `Term` 7. `v1:` `Term List` 8. `termlist_eq([u / v];v1) [u / v] = v1` 9. `termlist_eq([u / v];v1) ([u / v] = v1)` 10. `[u / v] = [u1 / v1]` `term_eq(u;u1)termlist_eq(v;v1)`