Logiweb(TM)

8.4.8 Blocks

Prev Up Next Page 323 of 800 Search internet


The following construct allows to group a sequence of proof lines into a block:

   line L1 : Block >> Begin ; B line L2 : Block >> End ; N

The construct above is used for expressing Line L02 and L08 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

In the example above, Line L03-L07 constitute the body B of the block and Line L09-L10 constitute the 'next' argument N of the block.

The block construct generates two lines (Line L02 and Line L08 in the example above). Both lines have a line number. The first of the two line numbers (L02 in the example above) is purely decorative.

Blocks can be used both in T proofs and plain proofs. After a block you can refer to the end line of the block but not to any line inside the block.

Blocks can be nested. The 'use' rendering aspect of blocks does indentation.

Prev Up Next Page 323 of 800 Search logiweb.eu

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