(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:
1
6.
(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:
(15steps)
PrintForm
Definitions
mb
automata
2
Sections
GenAutomata
Doc