Nuprl - Pf trace consistent pred unprime 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;rel_unprime(r@0))

By: Auto THEN Unfold `rel_unprime` 0 THEN ParallelOp -1 THEN Reduce 0 THEN RWO "map_length" 0 THEN ParallelOp -1 THEN Subst' (map(t.unprime(t);r@0.args)[i] = unprime(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;unprime(t))

About:

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