Logiweb aspects of conclude two * proves * cache * end conclude in pyk

Up Help

The predefined "pyk" aspect

define pyk of conclude two var a proves var t cache var c end conclude as text unicode start of text unicode small c unicode small o unicode small n unicode small c unicode small l unicode small u unicode small d unicode small e unicode space unicode small t unicode small w unicode small o unicode space unicode asterisk unicode space unicode small p unicode small r unicode small o unicode small v unicode small e unicode small s unicode space unicode asterisk unicode space unicode small c unicode small a unicode small c unicode small h unicode small e unicode space unicode asterisk unicode space unicode small e unicode small n unicode small d unicode space unicode small c unicode small o unicode small n unicode small c unicode small l unicode small u unicode small d unicode small e unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of conclude two var a proves var t cache var c end conclude as text unicode start of text unicode newline unicode small c unicode small o unicode small n unicode small c unicode small l unicode small u unicode small d unicode small e unicode underscore unicode two unicode space unicode left parenthesis unicode space unicode number sign unicode one unicode period unicode newline unicode comma unicode space unicode number sign unicode two unicode period unicode newline unicode comma unicode space unicode number sign unicode three unicode period unicode newline unicode right parenthesis unicode end of text end unicode text end text end define

The predefined "value" aspect

define value of conclude two var a proves var t cache var c end conclude as var t tagged guard newline tagged if var a term root equal quote var x modus ponens var y end quote then conclude two var a first proves var a color var t modus ponens ( var a second ) end color cache var c end conclude else newline tagged if var a term root equal quote var x modus probans var y end quote then conclude two var a first proves var a color var t modus probans ( var a second ) end color cache var c end conclude else newline tagged if var a term root equal quote var x at var y end quote then conclude two var a first proves var a color var t at ( var a second ) end color cache var c end conclude else newline tagged if aspect the proof aspect term var a cache var c end aspect then error two quote unicode start of text unicode capital l unicode small e unicode small m unicode small m unicode small a unicode space unicode small e unicode small x unicode small p unicode small e unicode small c unicode small t unicode small e unicode small d unicode end of text end unicode text end quote term var a end error else newline let one lambda var d dot newline conclude three var a color conclude four var a init modus dereference modus lemma var d third second end conclude end color proves var t lemma parameter term var d third second stack true seed one end parameter substitution true end conclude apply aspect the statement aspect term var a cache var c end aspect end let end if end if end if end if end define