Logiweb(TM)

8.5.5 The init operator

Prev Up Next Page 330 of 800 Search internet


One of the things an argumentation can contain is explicit mentioning of a previous proof line:

Prop lemma M1.8e : #x imply #x end lemma

prepare proof indentation,proof of M1.8e : line L01 : Premise >> Prop ; line L02 : A2 >> ( #x imply ( #y imply #x ) imply #x ) imply newline ( #x imply #y imply #x ) imply #x imply #x ; line L03 : A1 >> #x imply ( #y imply #x ) imply #x ; line L04 : MP ponens L02 ponens L03 >> ( #x imply #y imply #x ) imply #x imply #x ; line L05 : A1 >> #x imply #y imply #x ; line L06 : MP ponens L04 ponens ( #x imply #y imply #x ) Init >> #x imply #x qed

In Line L06 above, ( #x imply #y imply #x ) Init replaces a reference to Line L05. In general, A Init can be used to state that A holds because it is proved 'elsewhere'. 'Elsewhere' covers previous proof lines and certain other situations as described various places later on.

Prev Up Next Page 330 of 800 Search logiweb.eu

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