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

At: rel mentions iff 1 2 2 2

1. r: rel()
2. x: Label
3. l: Term List
4. u: Term
5. v: Term List
6. (i:. i < ||v|| & (x term_vars(v[i]))) (x reduce(t,vs. term_vars(t) @ vs;nil;v))
7. (i:. i < ||v|| & (x term_vars(v[i]))) (x reduce(t,vs. term_vars(t) @ vs;nil;v))
8. (x reduce(t,vs. term_vars(t) @ vs;nil;v))

i:. i < ||v||+1 & (x term_vars([u / v][i]))

By:
ThinTrivial
THEN
ExRepD
THEN
InstConcl [i+1]
THEN
Reduce 0


Generated subgoal:

16. (x reduce(t,vs. term_vars(t) @ vs;nil;v))
7. i:
8. i < ||v||
9. (x term_vars(v[i]))
10. (x reduce(t,vs. term_vars(t) @ vs;nil;v))
(x term_vars([u / v][(i+1)]))

About:
listconsnilnatural_numberaddless_thanlambdaimpliesexists

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