Logiweb aspects of lemma set equality nec condition(1) in pyk

Up Help

The predefined "pyk" aspect

define pyk of lemma set equality nec condition(1) as text unicode start of text unicode small l unicode small e unicode small m unicode small m unicode small a unicode space unicode small s unicode small e unicode small t unicode space unicode small e unicode small q unicode small u unicode small a unicode small l unicode small i unicode small t unicode small y unicode space unicode small n unicode small e unicode small c unicode space unicode small c unicode small o unicode small n unicode small d unicode small i unicode small t unicode small i unicode small o unicode small n unicode left parenthesis unicode one unicode right parenthesis unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of lemma set equality nec condition(1) as text unicode start of text unicode capital s unicode capital e unicode capital n unicode capital c unicode one unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of lemma set equality nec condition(1) as system Q infer all metavar var fx end metavar indeed all metavar var rx end metavar indeed all metavar var ry end metavar indeed metavar var rx end metavar == metavar var ry end metavar infer metavar var fx end metavar in0 metavar var rx end metavar infer metavar var fx end metavar in0 metavar var ry end metavar end define

The user defined "the proof aspect" aspect

define proof of lemma set equality nec condition(1) as rule tactic end define