Logiweb aspects of lemma 0<1Helper in pyk

Up Help

The predefined "pyk" aspect

define pyk of lemma 0<1Helper as text unicode start of text unicode small l unicode small e unicode small m unicode small m unicode small a unicode space unicode zero unicode less than unicode one unicode capital h unicode small e unicode small l unicode small p unicode small e unicode small r unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of lemma 0<1Helper as text unicode start of text unicode zero unicode less than unicode one unicode capital h unicode small e unicode small l unicode small p unicode small e unicode small r unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of lemma 0<1Helper as system Q infer 1 <= 0 imply 0 <= 1 end define

The user defined "the proof aspect" aspect

define proof of lemma 0<1Helper as lambda var c dot lambda var x dot proof expand quote system Q infer 1 <= 0 infer lemma leqAddition modus ponens 1 <= 0 conclude 1 + - 1 <= 0 + - 1 cut axiom negative conclude 1 + - 1 = 0 cut lemma subLeqLeft modus ponens 1 + - 1 = 0 modus ponens 1 + - 1 <= 0 + - 1 conclude 0 <= 0 + - 1 cut lemma plus0Left conclude 0 + - 1 = - 1 cut lemma subLeqRight modus ponens 0 + - 1 = - 1 modus ponens 0 <= 0 + - 1 conclude 0 <= - 1 cut lemma leqMultiplication modus ponens 0 <= - 1 modus ponens 0 <= - 1 conclude 0 * - 1 <= - 1 * - 1 cut lemma x*0=0 conclude - 1 * 0 = 0 cut axiom timesCommutativity conclude 0 * - 1 = - 1 * 0 cut lemma eqTransitivity modus ponens 0 * - 1 = - 1 * 0 modus ponens - 1 * 0 = 0 conclude 0 * - 1 = 0 cut lemma subLeqLeft modus ponens 0 * - 1 = 0 modus ponens 0 * - 1 <= - 1 * - 1 conclude 0 <= - 1 * - 1 cut lemma (-1)*(-1)=1 conclude - 1 * - 1 = 1 cut lemma subLeqRight modus ponens - 1 * - 1 = 1 modus ponens 0 <= - 1 * - 1 conclude 0 <= 1 cut 1rule deduction modus ponens 1 <= 0 infer 0 <= 1 conclude 1 <= 0 imply 0 <= 1 end quote state proof state cache var c end expand end define