Logiweb(TM)

8.4.3 End lines

Prev Up Next Page 318 of 800 Search internet

The following constructs allow to express the last line of a proof:

   line L : A >> C ;
   line L : A >> C qed

The two constructs are identical except that the former is rendered with a terminating semicolon and the latter is rendered with a terminating box. The former is used in Line L07 and the latter in Line L10 of the multzero proof:

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 line number L of end lines is purely decorative and is discarded during macro expansion.

Prev Up Next Page 318 of 800 Search logiweb.eu

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