[Clear, Push [0, 0], CreateIndHyp, Clear, Push [0, 1, 0, 0, 1], Pop [0, 1, 0, 0, 1], Push [0, 1, 0], Narrow 0 False, Clear, Push [0, 1, 0, 0, 1], Pop [0, 1, 0, 0, 1], Push [0, 1, 0, 0, 1, 0], Narrow 0 False, Clear, Simplify 2 True, Clear, Push [0, 1, 1, 0, 0, 0, 0], ApplyTheorem False (F "<===" [F "=" [F "$" [F "$" [F "loop" [F "F" []], V "N0"], F "F" [V "X0"]], F "F" [F "$" [F "$" [F "loop" [F "F" []], V "N0"], V "X0"]]], F "&" [F "Nat" [V "N0"], F ">>" [V "!N", V "N0"]]]), Clear, Push [0, 1, 1, 0, 0, 0, 1, 0], Narrow 0 False, Clear, Simplify 4 True, Clear, Push [1, 1, 0, 0], Narrow 0 False, Clear, Simplify 1 True, Clear, Push [0], Narrow 0 False, Clear, Simplify 1 True, Clear]