(4steps)
PrintForm
Definitions
mb
automata
4
Sections
GenAutomata
Doc
At:
tc
pred
addprime
P:Fmla, ds:Collection(dec()), da:Collection(SimpleType), de:sig(). tc_pred(P;ds;da;de)
tc_pred((P)';ds;da;de)
By:
Unfold `tc_pred` 0
THEN
Try (Fold `pred` 0)
Generated subgoals:
1
1.
P:
Fmla
2.
ds:
Collection(dec())
3.
da:
Collection(SimpleType)
4.
de:
sig()
5.
r:rel(). r
P
tc(r;ds;da;de)
6.
r:
rel()
7.
r
(P)'
tc(r;ds;da;de)
2
1.
P:
Fmla
2.
ds:
Collection(dec())
3.
da:
Collection(SimpleType)
4.
de:
sig()
5.
r:rel(). r
(P)'
tc(r;ds;da;de)
6.
r:
rel()
7.
r
P
tc(r;ds;da;de)
About:
(4steps)
PrintForm
Definitions
mb
automata
4
Sections
GenAutomata
Doc