(7steps)
PrintForm
Definitions
mb
automata
3
Sections
GenAutomata
Doc
At:
rel
mentions
trace
iff
1
2
1.
r:
rel()
2.
L:
Term List
3.
u:
Term
4.
v:
Term List
5.
reduce(
x,y. mentions_trace(x)
y;false
;v)
(
i:
. i < ||v|| & mentions_trace(v[i]))
6.
reduce(
x,y. mentions_trace(x)
y;false
;v)
(
i:
. i < ||v|| & mentions_trace(v[i]))
7.
i:
8.
i < ||v||+1
9.
mentions_trace([u / v][i])
mentions_trace(u)
reduce(
x,y. mentions_trace(x)
y;false
;v)
By:
(CaseNat 0 `i') THENL [Sel 1 (Analyze 0);Sel 2 (Analyze 0)]
Generated subgoals:
1
10.
i = 0
mentions_trace(u)
2
10.
i = 0
reduce(
x,y. mentions_trace(x)
y;false
;v)
About:
(7steps)
PrintForm
Definitions
mb
automata
3
Sections
GenAutomata
Doc