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

At: unequal termlists 1 2
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])

termlist_eq([u / v];[u1 / v1]) ||v||+1 = ||v1||+1 (i:. i < ||v||+1 & [u / v][i] = [u1 / v1][i])
By:
RecUnfold `termlist_eq` 0
THEN
Reduce 0
THEN
RW assert_pushdownC 0
THEN
Decide term_eq(u;u1)
Generated subgoals:

19. term_eq(u;u1)
10. (term_eq(u;u1) & termlist_eq(v;v1))
11. ||v||+1 = ||v1||+1
i:. i < ||v||+1 & [u / v][i] = [u1 / v1][i]
29. term_eq(u;u1)
10. (term_eq(u;u1) & termlist_eq(v;v1))
11. ||v||+1 = ||v1||+1
i:. i < ||v||+1 & [u / v][i] = [u1 / v1][i]

About:
listconsassertnatural_numberaddless_thanequalimpliesallexists

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