Logiweb aspects of conclude three {MissingArg} proves {MissingArg} lemma {MissingArg} substitution {MissingArg} end conclude in pyk

Up Help

The predefined "pyk" aspect

define pyk of conclude three x proves x lemma x substitution x 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 h unicode small r unicode small e unicode small e unicode space unicode quotation mark unicode space unicode small p unicode small r unicode small o unicode small v unicode small e unicode small s unicode space unicode quotation mark unicode space unicode small l unicode small e unicode small m unicode small m unicode small a unicode space unicode quotation mark unicode space unicode small s unicode small u unicode small b unicode small s unicode small t unicode small i unicode small t unicode small u unicode small t unicode small i unicode small o unicode small n unicode space unicode quotation mark 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 three var a proves var t lemma var l substitution var s 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 three 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 comma unicode space unicode number sign unicode four 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 three var a proves var t lemma var l substitution var s end conclude as var a tagged guard var t tagged guard var l tagged guard var s tagged guard newline tagged if var l term root equal quote var x infer var y end quote then newline var t term root equal quote var x modus ponens var y end quote select conclude three var a modus proves var t first lemma var l second substitution unify var l first with var t second substitution var s end unify end conclude else conclude three var a modus proves var t lemma var l second substitution var s end conclude end select else newline tagged if var l term root equal quote var x endorse var y end quote then newline var t term root equal quote var x modus probans var y end quote select conclude three var a modus proves var t first lemma var l second substitution unify var l first with var t second substitution var s end unify end conclude else conclude three var a verify proves var t lemma var l second substitution var s end conclude end select else newline tagged if var l term root equal quote all var x indeed var y end quote then newline var t term root equal quote var x at var y end quote select conclude three var a at var t second proves var t first lemma var l second substitution unify var l first with var t second substitution var s end unify end conclude else conclude three var a at var l first proves var t lemma var l second substitution var s end conclude end select else newline let one lambda var s dot newline tagged if var s is cardinal then var s else newline instantiate var a with var s end instantiate end if apply unify var l with var t substitution var s end unify end let end if end if end if end define