Logiweb aspects of lemma toCartProd in pyk

Up Help

The predefined "pyk" aspect

define pyk of lemma toCartProd 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 t unicode small o unicode capital c unicode small a unicode small r unicode small t unicode capital p unicode small r unicode small o unicode small d unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of lemma toCartProd as text unicode start of text unicode capital t unicode small o unicode capital c unicode small a unicode small r unicode small t unicode capital p unicode small r unicode small o unicode small d unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of lemma toCartProd as system Q infer all metavar var sx end metavar indeed all metavar var sx1 end metavar indeed all metavar var sy end metavar indeed all metavar var sy1 end metavar indeed metavar var sx end metavar in0 metavar var sx1 end metavar infer metavar var sy end metavar in0 metavar var sy1 end metavar infer zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair in0 the set of ph in power power U( zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 metavar var sx1 end metavar imply not0 object var var op2 end var in0 metavar var sy1 end metavar imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set end define

The user defined "the proof aspect" aspect

define proof of lemma toCartProd as lambda var c dot lambda var x dot proof expand quote system Q infer all metavar var sx end metavar indeed all metavar var sx1 end metavar indeed all metavar var sy end metavar indeed all metavar var sy1 end metavar indeed metavar var sx end metavar in0 metavar var sx1 end metavar infer metavar var sy end metavar in0 metavar var sy1 end metavar infer object var var s1 end var in0 zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair infer lemma toCartProd helper modus ponens metavar var sx end metavar in0 metavar var sx1 end metavar modus ponens metavar var sy end metavar in0 metavar var sy1 end metavar modus ponens object var var s1 end var in0 zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair conclude for all objects object var var s1 end var indeed object var var s1 end var in0 object var var s1 end var imply object var var s1 end var in0 U( zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair ) cut lemma formula2power modus ponens for all objects object var var s1 end var indeed object var var s1 end var in0 object var var s1 end var imply object var var s1 end var in0 U( zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair ) conclude object var var s1 end var in0 power U( zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair ) end power cut all metavar var sx end metavar indeed all metavar var sx1 end metavar indeed all metavar var sy end metavar indeed all metavar var sy1 end metavar indeed 1rule deduction modus ponens all metavar var sx end metavar indeed all metavar var sx1 end metavar indeed all metavar var sy end metavar indeed all metavar var sy1 end metavar indeed metavar var sx end metavar in0 metavar var sx1 end metavar infer metavar var sy end metavar in0 metavar var sy1 end metavar infer object var var s1 end var in0 zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair infer object var var s1 end var in0 power U( zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair ) end power conclude metavar var sx end metavar in0 metavar var sx1 end metavar imply metavar var sy end metavar in0 metavar var sy1 end metavar imply object var var s1 end var in0 zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair imply object var var s1 end var in0 power U( zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair ) end power cut metavar var sx end metavar in0 metavar var sx1 end metavar infer metavar var sy end metavar in0 metavar var sy1 end metavar infer prop lemma mp2 modus ponens metavar var sx end metavar in0 metavar var sx1 end metavar imply metavar var sy end metavar in0 metavar var sy1 end metavar imply object var var s1 end var in0 zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair imply object var var s1 end var in0 power U( zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair ) end power modus ponens metavar var sx end metavar in0 metavar var sx1 end metavar modus ponens metavar var sy end metavar in0 metavar var sy1 end metavar conclude object var var s1 end var in0 zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair imply object var var s1 end var in0 power U( zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair ) end power cut 1rule gen modus ponens object var var s1 end var in0 zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair imply object var var s1 end var in0 power U( zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair ) end power conclude for all objects object var var s1 end var indeed object var var s1 end var in0 zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair imply object var var s1 end var in0 power U( zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair ) end power cut 1rule repetition modus ponens for all objects object var var s1 end var indeed object var var s1 end var in0 zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair imply object var var s1 end var in0 power U( zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair ) end power conclude for all objects object var var s1 end var indeed object var var s1 end var in0 zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair imply object var var s1 end var in0 power U( zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair ) end power cut lemma formula2power modus ponens for all objects object var var s1 end var indeed object var var s1 end var in0 zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair imply object var var s1 end var in0 power U( zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair ) end power conclude zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair in0 power power U( zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair ) end power end power cut lemma eqReflexivity conclude zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair = zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair cut prop lemma join conjuncts modus ponens metavar var sx end metavar in0 metavar var sx1 end metavar modus ponens metavar var sy end metavar in0 metavar var sy1 end metavar conclude not0 metavar var sx end metavar in0 metavar var sx1 end metavar imply not0 metavar var sy end metavar in0 metavar var sy1 end metavar cut prop lemma join conjuncts modus ponens not0 metavar var sx end metavar in0 metavar var sx1 end metavar imply not0 metavar var sy end metavar in0 metavar var sy1 end metavar modus ponens zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair = zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair conclude not0 not0 metavar var sx end metavar in0 metavar var sx1 end metavar imply not0 metavar var sy end metavar in0 metavar var sy1 end metavar imply not0 zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair = zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair cut pred lemma intro exist at metavar var sy end metavar modus ponens not0 not0 metavar var sx end metavar in0 metavar var sx1 end metavar imply not0 metavar var sy end metavar in0 metavar var sy1 end metavar imply not0 zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair = zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair conclude not0 for all objects object var var op2 end var indeed not0 not0 not0 metavar var sx end metavar in0 metavar var sx1 end metavar imply not0 object var var op2 end var in0 metavar var sy1 end metavar imply not0 zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair = zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma object var var op2 end var end pair end pair cut pred lemma intro exist at metavar var sx end metavar modus ponens not0 for all objects object var var op2 end var indeed not0 not0 not0 metavar var sx end metavar in0 metavar var sx1 end metavar imply not0 object var var op2 end var in0 metavar var sy1 end metavar imply not0 zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair = zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma object var var op2 end var end pair end pair conclude not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 metavar var sx1 end metavar imply not0 object var var op2 end var in0 metavar var sy1 end metavar imply not0 zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair cut 1rule repetition modus ponens not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 metavar var sx1 end metavar imply not0 object var var op2 end var in0 metavar var sy1 end metavar imply not0 zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair conclude not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 metavar var sx1 end metavar imply not0 object var var op2 end var in0 metavar var sy1 end metavar imply not0 zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair cut lemma formula2separation modus ponens zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair in0 power power U( zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair ) end power end power modus ponens not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 metavar var sx1 end metavar imply not0 object var var op2 end var in0 metavar var sy1 end metavar imply not0 zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair conclude zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair in0 the set of ph in power power U( zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 metavar var sx1 end metavar imply not0 object var var op2 end var in0 metavar var sy1 end metavar imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set cut 1rule repetition modus ponens zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair in0 the set of ph in power power U( zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 metavar var sx1 end metavar imply not0 object var var op2 end var in0 metavar var sy1 end metavar imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set conclude zermelo pair zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair comma zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair end pair in0 the set of ph in power power U( zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair ) end power end power such that not0 for all objects object var var op1 end var indeed not0 not0 for all objects object var var op2 end var indeed not0 not0 not0 object var var op1 end var in0 metavar var sx1 end metavar imply not0 object var var op2 end var in0 metavar var sy1 end metavar imply not0 placeholder-var var a end var = zermelo pair zermelo pair object var var op1 end var comma object var var op1 end var end pair comma zermelo pair object var var op1 end var comma object var var op2 end var end pair end pair end set end quote state proof state cache var c end expand end define