Logiweb aspects of lemma (-1)*(-1)=1 in pyk

Up Help

The predefined "pyk" aspect

define pyk of lemma (-1)*(-1)=1 as text unicode start of text unicode small l unicode small e unicode small m unicode small m unicode small a unicode space unicode left parenthesis unicode hyphen unicode one unicode right parenthesis unicode asterisk unicode left parenthesis unicode hyphen unicode one unicode right parenthesis unicode equal sign unicode one unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of lemma (-1)*(-1)=1 as text unicode start of text unicode left parenthesis unicode hyphen unicode one unicode right parenthesis unicode asterisk unicode left parenthesis unicode hyphen unicode one unicode right parenthesis unicode equal sign unicode one unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of lemma (-1)*(-1)=1 as system Q infer - 1 * - 1 = 1 end define

The user defined "the proof aspect" aspect

define proof of lemma (-1)*(-1)=1 as lambda var c dot lambda var x dot proof expand quote system Q infer lemma x=x+(y-y) conclude - 1 * - 1 = - 1 * - 1 + 1 + - 1 cut axiom times1 conclude - 1 * 1 = - 1 cut lemma eqSymmetry modus ponens - 1 * 1 = - 1 conclude - 1 = - 1 * 1 cut lemma eqAdditionLeft modus ponens - 1 = - 1 * 1 conclude 1 + - 1 = 1 + - 1 * 1 cut lemma eqAdditionLeft modus ponens 1 + - 1 = 1 + - 1 * 1 conclude - 1 * - 1 + 1 + - 1 = - 1 * - 1 + 1 + - 1 * 1 cut axiom plusCommutativity conclude 1 + - 1 * 1 = - 1 * 1 + 1 cut lemma eqAdditionLeft modus ponens 1 + - 1 * 1 = - 1 * 1 + 1 conclude - 1 * - 1 + 1 + - 1 * 1 = - 1 * - 1 + - 1 * 1 + 1 cut axiom plusAssociativity conclude - 1 * - 1 + - 1 * 1 + 1 = - 1 * - 1 + - 1 * 1 + 1 cut lemma eqSymmetry modus ponens - 1 * - 1 + - 1 * 1 + 1 = - 1 * - 1 + - 1 * 1 + 1 conclude - 1 * - 1 + - 1 * 1 + 1 = - 1 * - 1 + - 1 * 1 + 1 cut lemma (-1)*(-1)+(-1)*1=0 conclude - 1 * - 1 + - 1 * 1 = 0 cut lemma eqAddition modus ponens - 1 * - 1 + - 1 * 1 = 0 conclude - 1 * - 1 + - 1 * 1 + 1 = 0 + 1 cut lemma plus0Left conclude 0 + 1 = 1 cut lemma eqTransitivity5 modus ponens - 1 * - 1 = - 1 * - 1 + 1 + - 1 modus ponens - 1 * - 1 + 1 + - 1 = - 1 * - 1 + 1 + - 1 * 1 modus ponens - 1 * - 1 + 1 + - 1 * 1 = - 1 * - 1 + - 1 * 1 + 1 modus ponens - 1 * - 1 + - 1 * 1 + 1 = - 1 * - 1 + - 1 * 1 + 1 conclude - 1 * - 1 = - 1 * - 1 + - 1 * 1 + 1 cut lemma eqTransitivity4 modus ponens - 1 * - 1 = - 1 * - 1 + - 1 * 1 + 1 modus ponens - 1 * - 1 + - 1 * 1 + 1 = 0 + 1 modus ponens 0 + 1 = 1 conclude - 1 * - 1 = 1 end quote state proof state cache var c end expand end define