("factorial" |factorial| |factorial_pos| "" (INDUCT "n" 1) (("1" (GRIND) NIL NIL) ("2" (SKOSIMP*) (("2" (EXPAND "factorial" 1) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)