(4steps)
PrintForm
Definitions
mb
automata
2
Sections
GenAutomata
Doc
At:
term
primed
vars
term
vars
2
1.
x:
Label
2.
u:
Term
3.
u1:
Term
Type{i'}
4.
w:
u:{v:Term| u1(v) }
(x
term_primed_vars(u))
(x
term_vars(u))
5.
y1:
{v:Term| u1(v) }
6.
y2:
{v:Term| u1(v) }
7.
(x
term_primed_vars(y1) @ term_primed_vars(y2))
(x
term_vars(y1) @ term_vars(y2))
By:
All (RWO "member_append")
Generated subgoal:
1
7.
(x
term_primed_vars(y1))
(x
term_primed_vars(y2))
(x
term_vars(y1))
(x
term_vars(y2))
About:
(4steps)
PrintForm
Definitions
mb
automata
2
Sections
GenAutomata
Doc