(3steps) PrintForm Definitions mb automata 4 Sections GenAutomata Doc

At: tc pred monotone

p1,p2:Fmla, ds1,ds2:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(). p2 p1 ds1 ds2 da1 da2 tc_pred(p1;ds1;da1;de) tc_pred(p2;ds2;da2;de)
By:
Unfold `tc_pred` 0
THEN
Try (Fold `pred` 0)
THEN
AllHyps (InstHyp [r])
Generated subgoals:

11. p1: Fmla
2. p2: Fmla
3. ds1: Collection(dec())
4. ds2: Collection(dec())
5. da1: Collection(SimpleType)
6. da2: Collection(SimpleType)
7. de: sig()
8. p2 p1
9. ds1 ds2
10. da1 da2
11. r:rel(). r p1 tc(r;ds1;da1;de)
12. r: rel()
13. r p2
r p1
21. p1: Fmla
2. p2: Fmla
3. ds1: Collection(dec())
4. ds2: Collection(dec())
5. da1: Collection(SimpleType)
6. da2: Collection(SimpleType)
7. de: sig()
8. p2 p1
9. ds1 ds2
10. da1 da2
11. r:rel(). r p1 tc(r;ds1;da1;de)
12. r: rel()
13. r p2
14. tc(r;ds1;da1;de)
tc(r;ds2;da2;de)

About:
impliesall

(3steps) PrintForm Definitions mb automata 4 Sections GenAutomata Doc