Nuprl - Pf trace consistent pred addprime 1

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

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)')

By: Auto THEN Unfold `rel_addprime` 0 THEN ParallelOp -1 THEN Reduce 0 THEN RWO "map_length" 0 THEN ParallelOp -1 THEN Subst' (map(t.(t)';r@0.args)[i] = (r@0.args[i])') 0 THEN Try (RWO "map_length" 0) THEN Try ((RWO "map_select" 0) THEN (Reduce 0)) THEN MoveToConcl -1 THEN GenConcl (r@0.args[i] = t) THEN Lemmaize []

Generated subgoal:

1 da:Collection(dec()), rho:Decl, te:(LabelLabel), t:Term. trace_consistent(rho;da;te;t) trace_consistent(rho;da;te;(t)')

About:

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