Logiweb aspects of lemma doubleMinus in pyk

Up Help

The predefined "pyk" aspect

define pyk of lemma doubleMinus as text unicode start of text unicode small l unicode small e unicode small m unicode small m unicode small a unicode space unicode small d unicode small o unicode small u unicode small b unicode small l unicode small e unicode capital m unicode small i unicode small n unicode small u unicode small s unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of lemma doubleMinus as text unicode start of text unicode capital d unicode small o unicode small u unicode small b unicode small l unicode small e unicode capital m unicode small i unicode small n unicode small u unicode small s unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of lemma doubleMinus as system Q infer all metavar var x end metavar indeed - - metavar var x end metavar = metavar var x end metavar end define

The user defined "the proof aspect" aspect

define proof of lemma doubleMinus as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var x end metavar indeed axiom negative conclude - metavar var x end metavar + - - metavar var x end metavar = 0 cut lemma x+y=zBackwards modus ponens - metavar var x end metavar + - - metavar var x end metavar = 0 conclude 0 = - - metavar var x end metavar + - metavar var x end metavar cut lemma negativeToLeft(Eq) modus ponens 0 = - - metavar var x end metavar + - metavar var x end metavar conclude 0 + metavar var x end metavar = - - metavar var x end metavar cut lemma plus0Left conclude 0 + metavar var x end metavar = metavar var x end metavar cut lemma equality modus ponens 0 + metavar var x end metavar = - - metavar var x end metavar modus ponens 0 + metavar var x end metavar = metavar var x end metavar conclude - - metavar var x end metavar = metavar var x end metavar end quote state proof state cache var c end expand end define