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

At: tc pred unprime 2
1. P: Fmla
2. ds: Collection(dec())
3. da: Collection(SimpleType)
4. de: sig()
5. r:rel(). r pred_unprime(P) tc(r;ds;da;de)
6. r: rel()
7. r P

tc(r;ds;da;de)
By:
RWO "tc_unprime" 0
THEN
BackThruSomeHyp
Generated subgoal:

1 rel_unprime(r) pred_unprime(P)

About:
impliesall

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