Page 317 of 800
| Page 317 of 800 | Search internet |
The most common lines in proofs are ones which argue in favor of a conclusion. The construct for lines reads:
line L : A >> C ; N
The construct above uses the argumentation A to prove the conclusion C. It contains a line number L which allows to refer to the conclusion C later on in the proof. The construct also has a 'next' argument N which is supposed to contain all proof lines following the given line. The notion of an argumentation is explained later.
The construct above is used for expressing Line L01, L04, L05, L06, and L09 of the multzero proof:
The body of the proof above has form
line L01 : S7 >> 0 * 0 = 0 ; ...
where the ellipsis ... comprises Line L02-L10.
| Page 317 of 800 | Search logiweb.eu |