Nuprl - Pf trace consistent pred addprime 1 1 1

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

At: trace consistent pred addprime 1 1 1

t:Term, g:Label. term_mentions_guard(g;(t)') term_mentions_guard(g;t)

By: Auto THEN MoveToConcl -1 THEN Unfold `addprime` 0 THEN TermInd 1 THEN All Reduce THEN AllHyps (Fold `addprime`) THEN All (RW assert_pushdownC) THEN ParallelOp -1 THEN EasyHyp

Generated subgoals:

None

About:

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