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

At: trace consistent pred addprime


da:Collection(dec()), P:Fmla, rho:Decl, te:(LabelLabel). trace_consistent_pred(rho;da;te;P) trace_consistent_pred(rho;da;te;(P)')

By:
Auto
THEN
RepeatFor 2 (ParallelOp -1)
THEN
Unfold `pred_addprime` 0
THEN
RW ColMemberC 0
THEN
Try (Fold `pred` 0)
THEN
ExRepD
THEN
SubstFor r 0
THEN
AllHyps (InstHyp [r@0])
THEN
Lemmaize [-1]


Generated subgoal:

1 da:Collection(dec()), rho:Decl, te:(LabelLabel), r@0:rel(). trace_consistent_rel(rho;da;te;r@0) trace_consistent_rel(rho;da;te;(r@0)')

About:
boolfunctionimpliesall

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