Logiweb(TM)

8.4.1 Proof line constructors

Prev Up Next Page 316 of 800 Search internet

Recall the following proof from the multzero page:

prepare proof indentation,PA proof of 3.2l : line L01 : S7 >> 0 * 0 = 0 ; line L02 : Block >> Begin ; line L03 : Hypothesis >> 0 * x = 0 ; line L04 : S8 >> 0 * x suc = 0 * x + 0 ; line L05 : S5 >> 0 * x + 0 = 0 * x ; line L06 : 3.2c mp L04 mp L05 >> 0 * x suc = 0 * x ; line L07 : 3.2c mp L06 mp L03 >> 0 * x suc = 0 ; line L08 : Block >> End ; line L09 : Induction at x ponens L01 ponens L08 >> 0 * x = 0 ; line L10 : Gen1 ponens L09 >> all x : 0 * x = 0 qed

The body of the proof comprises ten proof lines. The proof line constructors defined on the check and Peano pages are described in the following.

Prev Up Next Page 316 of 800 Search logiweb.eu

Copyright © 2010 Klaus Grue, GRD-2010-01-05