Logiweb aspects of goal2 in pyk

Up Help

The predefined "pyk" aspect

define pyk of goal2 as text unicode start of text unicode small g unicode small o unicode small a unicode small l unicode two unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of goal2 as pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var x end metavar indeed all metavar var h end metavar indeed all metavar var k end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse quote metavar var x end metavar end quote avoid zero quote metavar var h end metavar end quote endorse sub zero quote metavar var h end metavar end quote is quote metavar var f end metavar end quote where quote metavar var x end metavar end quote is quote metavar var g end metavar end quote end sub endorse forall metavar var x end metavar dot metavar var f end metavar end forall infer lnot exists metavar var x end metavar dot metavar var f end metavar end exists imply metavar var k end metavar end define

The user defined "the proof aspect" aspect

define proof of goal2 as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var x end metavar indeed all metavar var h end metavar indeed all metavar var k end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse quote metavar var x end metavar end quote avoid zero quote metavar var h end metavar end quote endorse sub zero quote metavar var h end metavar end quote is quote metavar var f end metavar end quote where quote metavar var x end metavar end quote is quote metavar var g end metavar end quote end sub endorse forall metavar var x end metavar dot metavar var f end metavar end forall infer hlplem6 modus probans quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote modus probans quote metavar var x end metavar end quote avoid zero quote metavar var h end metavar end quote modus probans sub zero quote metavar var h end metavar end quote is quote metavar var f end metavar end quote where quote metavar var x end metavar end quote is quote metavar var g end metavar end quote end sub modus ponens forall metavar var x end metavar dot metavar var f end metavar end forall conclude exists metavar var x end metavar dot metavar var f end metavar end exists cut all metavar var f end metavar indeed all metavar var x end metavar indeed all metavar var k end metavar indeed exists metavar var x end metavar dot metavar var f end metavar end exists infer lnot exists metavar var x end metavar dot metavar var f end metavar end exists infer andintro modus ponens exists metavar var x end metavar dot metavar var f end metavar end exists modus ponens lnot exists metavar var x end metavar dot metavar var f end metavar end exists conclude exists metavar var x end metavar dot metavar var f end metavar end exists land lnot exists metavar var x end metavar dot metavar var f end metavar end exists cut bottomelim modus ponens exists metavar var x end metavar dot metavar var f end metavar end exists land lnot exists metavar var x end metavar dot metavar var f end metavar end exists conclude metavar var k end metavar cut pcdeduction modus ponens all metavar var f end metavar indeed all metavar var x end metavar indeed all metavar var k end metavar indeed exists metavar var x end metavar dot metavar var f end metavar end exists infer lnot exists metavar var x end metavar dot metavar var f end metavar end exists infer metavar var k end metavar conclude exists metavar var x end metavar dot metavar var f end metavar end exists imply lnot exists metavar var x end metavar dot metavar var f end metavar end exists imply metavar var k end metavar cut pcmp modus ponens exists metavar var x end metavar dot metavar var f end metavar end exists modus ponens exists metavar var x end metavar dot metavar var f end metavar end exists imply lnot exists metavar var x end metavar dot metavar var f end metavar end exists imply metavar var k end metavar conclude lnot exists metavar var x end metavar dot metavar var f end metavar end exists imply metavar var k end metavar end quote state proof state cache var c end expand end define