At:
tc pred monotone
2
1.
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)
By:
Easy
Generated subgoals:
None
About:
