Nuprl - Pf ptn_atom_wf3 1 1

(3steps) PrintForm Definitions mb label Sections GenAutomata Doc

At: ptn atom wf3 1 1

1. x: Atom

ground_ptn(ptn_atom(x))

By: RecUnfold `ground_ptn` 0 THEN Reduce 0 THEN Trivial

Generated subgoals:

None

About:

(3steps) PrintForm Definitions mb label Sections GenAutomata Doc