Nuprl - Pf trace consistent pred addprime

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

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:

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