PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc

At: tc closed pred

p:Fmla, ds:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(). closed_pred(p) tc_pred(p;ds;da1;de) tc_pred(p;ds;da2;de)
By:
Unfolds [`pred`;`closed_pred`;`tc_pred`] 0
THEN
Using [`da1',da1] (BackThru Thm* r:rel(), ds:Collection(dec()), da1,da2:Collection(SimpleType), de:sig(). closed_rel(r) tc(r;ds;da1;de) tc(r;ds;da2;de))
THEN
BackThruSomeHyp
Generated subgoals:

None

About:
impliesall

PrintForm Definitions Lemmas mb automata 4 Sections GenAutomata Doc