Logiweb aspects of hlplem6 in pyk

Up Help

The predefined "pyk" aspect

define pyk of hlplem6 as text unicode start of text unicode small h unicode small l unicode small p unicode small l unicode small e unicode small m unicode six unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of hlplem6 as pred calc infer all metavar var x end metavar indeed all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var h 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 exists metavar var x end metavar dot metavar var f end metavar end exists end define

The user defined "the proof aspect" aspect

define proof of hlplem6 as lambda var c dot lambda var x dot proof expand quote pred calc infer all metavar var x end metavar indeed all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var h 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 forallelim 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 metavar var h end metavar cut existsintro 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 metavar var h end metavar conclude exists metavar var x end metavar dot metavar var f end metavar end exists end quote state proof state cache var c end expand end define