Logiweb aspects of pred calc in pyk

Up Help

The predefined "pyk" aspect

define pyk of pred calc as text unicode start of text unicode small p unicode small r unicode small e unicode small d unicode space unicode small c unicode small a unicode small l unicode small c unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of pred calc as all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar land metavar var g end metavar imply metavar var f end metavar rule plus all metavar var f end metavar indeed lnot lnot metavar var f end metavar imply metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var h end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar imply metavar var g end metavar imply metavar var h end metavar imply metavar var f end metavar imply metavar var h end metavar rule plus all metavar var x end metavar indeed all metavar var r end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed 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 r end metavar end quote end sub endorse metavar var h end metavar imply exists metavar var x end metavar dot metavar var f end metavar end exists rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var f end metavar lor metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var h end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var h end metavar imply metavar var g end metavar imply metavar var f end metavar lor metavar var h end metavar imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var x end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse metavar var f end metavar imply metavar var g end metavar infer exists metavar var x end metavar dot metavar var f end metavar end exists imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar infer metavar var f end metavar imply metavar var g end metavar infer metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar lor metavar var f end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar imply lnot metavar var g end metavar imply lnot metavar var f end metavar rule plus all metavar var a end metavar indeed all metavar var b end metavar indeed lambda var x dot deduction zero quote metavar var a end metavar end quote conclude quote metavar var b end metavar end quote end deduction endorse metavar var a end metavar infer metavar var b end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar rule plus all metavar var x end metavar indeed all metavar var r end metavar indeed all metavar var g end metavar indeed all metavar var f end metavar indeed 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 r end metavar end quote end sub endorse forall metavar var x end metavar dot metavar var f end metavar end forall imply metavar var h end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar imply metavar var g end metavar imply metavar var f end metavar land metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed metavar var f end metavar land metavar var g end metavar imply metavar var g end metavar rule plus all metavar var f end metavar indeed all metavar var g end metavar indeed all metavar var x end metavar indeed quote metavar var x end metavar end quote avoid zero quote metavar var g end metavar end quote endorse metavar var g end metavar imply metavar var f end metavar infer metavar var g end metavar imply forall metavar var x end metavar dot metavar var f end metavar end forall end define