Logiweb aspects of system s in pyk

Up Help

The predefined "pyk" aspect

define pyk of system s as text unicode start of text unicode small s unicode small y unicode small s unicode small t unicode small e unicode small m unicode space unicode small s unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of system s as text unicode start of text unicode newline unicode capital s unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of system s as ( ( var a peano var peano plus ( var b peano var peano succ ) ) peano is ( ( var a peano var peano plus ( var b peano var ) ) peano succ ) ) rule plus ( ( all metavar var a end metavar indeed all metavar var b end metavar indeed ( ( ( peano not metavar var b end metavar ) peano imply peano not metavar var a end metavar ) peano imply ( ( ( peano not metavar var b end metavar ) peano imply metavar var a end metavar ) peano imply metavar var b end metavar ) ) ) rule plus ( ( ( var a peano var peano is ( var b peano var ) ) peano imply ( var a peano var peano succ peano is ( var b peano var peano succ ) ) ) rule plus ( ( all metavar var a end metavar indeed all metavar var b end metavar indeed ( ( metavar var a end metavar peano imply metavar var b end metavar ) infer ( metavar var a end metavar infer metavar var b end metavar ) ) ) rule plus ( ( ( var a peano var peano succ peano is ( var b peano var peano succ ) ) peano imply ( var a peano var peano is ( var b peano var ) ) ) rule plus ( ( all metavar var a end metavar indeed all metavar var b end metavar indeed ( metavar var a end metavar peano imply ( metavar var b end metavar peano imply metavar var a end metavar ) ) ) rule plus ( ( all metavar var x end metavar indeed all metavar var a end metavar indeed all metavar var b end metavar indeed ( peano nonfree metavar var x end metavar in metavar var a end metavar end nonfree endorse ( ( peano all metavar var x end metavar indeed ( metavar var a end metavar peano imply metavar var b end metavar ) ) peano imply ( metavar var a end metavar peano imply peano all metavar var x end metavar indeed metavar var b end metavar ) ) ) ) rule plus ( ( ( var a peano var peano times ( var b peano var peano succ ) ) peano is ( ( var a peano var peano times ( var b peano var ) ) peano plus ( var a peano var ) ) ) rule plus ( ( ( var a peano var peano plus peano zero ) peano is ( var a peano var ) ) rule plus ( ( all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed ( ( metavar var a end metavar peano imply ( metavar var b end metavar peano imply metavar var c end metavar ) ) peano imply ( ( metavar var a end metavar peano imply metavar var b end metavar ) peano imply ( metavar var a end metavar peano imply metavar var c end metavar ) ) ) ) rule plus ( ( ( var a peano var peano is ( var b peano var ) ) peano imply ( ( var a peano var peano is ( var c peano var ) ) peano imply ( var b peano var peano is ( var c peano var ) ) ) ) rule plus ( ( all metavar var a end metavar indeed all metavar var b end metavar indeed all metavar var c end metavar indeed all metavar var x end metavar indeed ( peano sub metavar var b end metavar is metavar var a end metavar where metavar var x end metavar is peano zero end sub endorse ( peano sub metavar var c end metavar is metavar var a end metavar where metavar var x end metavar is metavar var x end metavar peano succ end sub endorse ( metavar var b end metavar peano imply ( ( peano all metavar var x end metavar indeed ( metavar var a end metavar peano imply metavar var c end metavar ) ) peano imply peano all metavar var x end metavar indeed metavar var a end metavar ) ) ) ) ) rule plus ( ( not ( peano zero peano is ( var a peano var peano succ ) ) ) rule plus ( ( all metavar var x end metavar indeed all metavar var a end metavar indeed ( metavar var a end metavar infer peano all metavar var x end metavar indeed metavar var a end metavar ) ) rule plus ( ( all metavar var c end metavar indeed all metavar var a end metavar indeed all metavar var x end metavar indeed all metavar var b end metavar indeed ( peano sub quote metavar var a end metavar end quote is quote metavar var b end metavar end quote where quote metavar var x end metavar end quote is quote metavar var c end metavar end quote end sub endorse ( ( peano all metavar var x end metavar indeed metavar var b end metavar ) peano imply metavar var a end metavar ) ) ) rule plus ( ( var a peano var peano times peano zero ) peano is peano zero ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) end define