Logiweb aspects of prop three two g rt hyp in pyk

Up Help

The predefined "pyk" aspect

define pyk of prop three two g rt hyp as text unicode start of text unicode small p unicode small r unicode small o unicode small p unicode space unicode small t unicode small h unicode small r unicode small e unicode small e unicode space unicode small t unicode small w unicode small o unicode space unicode small g unicode space unicode small r unicode small t unicode space unicode small h unicode small y unicode small p unicode space unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of prop three two g rt hyp as text unicode start of text unicode backslash unicode small m unicode small a unicode small t unicode small h unicode small i unicode small t unicode left brace unicode capital m unicode small e unicode small n unicode small d unicode small e unicode small l unicode small s unicode small o unicode small n unicode space unicode backslash unicode semicolon unicode space unicode three unicode period unicode two unicode left parenthesis unicode small g unicode right parenthesis unicode underscore unicode small h unicode left parenthesis unicode backslash unicode small d unicode small o unicode small t unicode left brace unicode small r unicode right brace unicode comma unicode backslash unicode small d unicode small o unicode small t unicode left brace unicode small t unicode right brace unicode right parenthesis unicode right brace unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of prop three two g rt hyp as system prime s infer all metavar var h end metavar indeed ( metavar var h end metavar peano imply ( ( var r peano var peano succ peano plus ( var t peano var ) ) peano is ( ( var r peano var peano plus ( var t peano var ) ) peano succ ) ) ) end define

The user defined "the proof aspect" aspect

define proof of prop three two g rt hyp as lambda var c dot lambda var x dot proof expand quote system prime s infer all metavar var h end metavar indeed ( ( prop three two g conclude peano all var r peano var indeed peano all var t peano var indeed ( ( var r peano var peano succ peano plus ( var t peano var ) ) peano is ( ( var r peano var peano plus ( var t peano var ) ) peano succ ) ) ) cut ( ( ( axiom prime a four at ( var r peano var ) ) conclude ( ( peano all var r peano var indeed peano all var t peano var indeed ( ( var r peano var peano succ peano plus ( var t peano var ) ) peano is ( ( var r peano var peano plus ( var t peano var ) ) peano succ ) ) ) peano imply peano all var t peano var indeed ( ( var r peano var peano succ peano plus ( var t peano var ) ) peano is ( ( var r peano var peano plus ( var t peano var ) ) peano succ ) ) ) ) cut ( ( ( ( rule prime mp modus ponens ( ( peano all var r peano var indeed peano all var t peano var indeed ( ( var r peano var peano succ peano plus ( var t peano var ) ) peano is ( ( var r peano var peano plus ( var t peano var ) ) peano succ ) ) ) peano imply peano all var t peano var indeed ( ( var r peano var peano succ peano plus ( var t peano var ) ) peano is ( ( var r peano var peano plus ( var t peano var ) ) peano succ ) ) ) ) modus ponens peano all var r peano var indeed peano all var t peano var indeed ( ( var r peano var peano succ peano plus ( var t peano var ) ) peano is ( ( var r peano var peano plus ( var t peano var ) ) peano succ ) ) ) conclude peano all var t peano var indeed ( ( var r peano var peano succ peano plus ( var t peano var ) ) peano is ( ( var r peano var peano plus ( var t peano var ) ) peano succ ) ) ) cut ( ( ( axiom prime a four at ( var t peano var ) ) conclude ( ( peano all var t peano var indeed ( ( var r peano var peano succ peano plus ( var t peano var ) ) peano is ( ( var r peano var peano plus ( var t peano var ) ) peano succ ) ) ) peano imply ( ( var r peano var peano succ peano plus ( var t peano var ) ) peano is ( ( var r peano var peano plus ( var t peano var ) ) peano succ ) ) ) ) cut ( ( ( ( rule prime mp modus ponens ( ( peano all var t peano var indeed ( ( var r peano var peano succ peano plus ( var t peano var ) ) peano is ( ( var r peano var peano plus ( var t peano var ) ) peano succ ) ) ) peano imply ( ( var r peano var peano succ peano plus ( var t peano var ) ) peano is ( ( var r peano var peano plus ( var t peano var ) ) peano succ ) ) ) ) modus ponens peano all var t peano var indeed ( ( var r peano var peano succ peano plus ( var t peano var ) ) peano is ( ( var r peano var peano plus ( var t peano var ) ) peano succ ) ) ) conclude ( ( var r peano var peano succ peano plus ( var t peano var ) ) peano is ( ( var r peano var peano plus ( var t peano var ) ) peano succ ) ) ) cut ( ( hypothesize modus ponens ( ( var r peano var peano succ peano plus ( var t peano var ) ) peano is ( ( var r peano var peano plus ( var t peano var ) ) peano succ ) ) ) conclude ( metavar var h end metavar peano imply ( ( var r peano var peano succ peano plus ( var t peano var ) ) peano is ( ( var r peano var peano plus ( var t peano var ) ) peano succ ) ) ) ) ) ) ) ) ) end quote state proof state cache var c end expand end define