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

At: tc pred addprime 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)
By:
RWO "tc_addprime" 0
THEN
BackThruSomeHyp
Generated subgoal:

1 (r)' (P)'

About:
impliesall

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