Logiweb aspects of lemma fromOrderedPair in pyk

Up Help

The predefined "pyk" aspect

define pyk of lemma fromOrderedPair 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 f unicode small r unicode small o unicode small m unicode capital o unicode small r unicode small d unicode small e unicode small r unicode small e unicode small d unicode capital p unicode small a unicode small i unicode small r unicode end of text end unicode text end text end define

The predefined "tex" aspect

define tex of lemma fromOrderedPair as text unicode start of text unicode capital f unicode small r unicode small o unicode small m unicode capital o unicode small r unicode small d unicode small e unicode small r unicode small e unicode small d unicode capital p unicode small a unicode small i unicode small r unicode end of text end unicode text end text end define

The user defined "the statement aspect" aspect

define statement of lemma fromOrderedPair 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 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 sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair infer not0 metavar var sx end metavar = metavar var sx1 end metavar imply not0 metavar var sy end metavar = metavar var sy1 end metavar end define

The user defined "the proof aspect" aspect

define proof of lemma fromOrderedPair 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 sx1 end metavar = 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 = zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair infer 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 = zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar 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 = zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair cut lemma eqReflexivity conclude metavar var sx1 end metavar = metavar var sx1 end metavar cut lemma same pair modus ponens metavar var sx1 end metavar = metavar var sx1 end metavar modus ponens metavar var sx1 end metavar = metavar var sy1 end metavar conclude zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair = zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair cut 1rule repetition modus ponens zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair = zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair conclude zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair = zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair cut lemma eqReflexivity conclude zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair = zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair cut lemma same pair modus ponens zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair = zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair modus ponens zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair = zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair conclude zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair end pair = zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair cut 1rule repetition modus ponens zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair end pair = zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair conclude zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair end pair = zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair cut lemma eqSymmetry modus ponens zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair end pair = zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair conclude zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair = zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair end pair cut lemma eqTransitivity 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 sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair modus ponens zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair = zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar 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 = zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair end pair cut lemma inPair(1) conclude zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair 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 cut lemma set equality nec condition(1) 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 sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair end pair modus ponens zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair 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 zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair in0 zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair end pair cut lemma fromSingleton modus ponens zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair in0 zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair end pair conclude zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair = zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair cut lemma fromSameSingleton modus ponens zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair = zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair conclude metavar var sx end metavar = metavar var sx1 end metavar cut lemma eqSymmetry modus ponens zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair = zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair conclude zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair = zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair cut lemma same singleton modus ponens zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair = zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair conclude zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sx1 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 sx end metavar end pair end pair cut lemma eqTransitivity 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 sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair end pair modus ponens zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sx1 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 sx end metavar 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 = 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 sx end metavar end pair end pair cut lemma inPair(2) conclude zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair 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 cut lemma set equality nec condition(1) 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 sx end metavar end pair end pair modus ponens zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair 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 zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair 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 sx end metavar end pair end pair cut lemma fromSingleton modus ponens zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair 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 sx end metavar end pair end pair conclude zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair = zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair cut lemma singletonmembersEqual modus ponens zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair = zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair conclude metavar var sx end metavar = metavar var sy end metavar cut lemma eqSymmetry modus ponens metavar var sx end metavar = metavar var sy end metavar conclude metavar var sy end metavar = metavar var sx end metavar cut lemma eqTransitivity4 modus ponens metavar var sy end metavar = metavar var sx end metavar modus ponens metavar var sx end metavar = metavar var sx1 end metavar modus ponens metavar var sx1 end metavar = metavar var sy1 end metavar conclude metavar var sy end metavar = metavar var sy1 end metavar cut prop lemma join conjuncts modus ponens metavar var sx end metavar = metavar var sx1 end metavar modus ponens metavar var sy end metavar = metavar var sy1 end metavar conclude not0 metavar var sx end metavar = metavar var sx1 end metavar imply not0 metavar var sy end metavar = metavar var sy1 end metavar 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 not0 metavar var sx1 end metavar = 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 = zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair infer 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 = zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar 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 = zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair cut lemma inPair(1) conclude zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair 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 cut lemma set equality nec condition(1) 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 sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair modus ponens zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair 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 zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair in0 zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair cut lemma pair2formula modus ponens zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair in0 zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair conclude not0 zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair = zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair imply zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair = zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair cut lemma unequalsNotInSingleton modus ponens not0 metavar var sx1 end metavar = metavar var sy1 end metavar conclude not0 zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair = zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair cut lemma neqSymmetry modus ponens not0 zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair = zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair conclude not0 zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair = zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair cut prop lemma negate second disjunct modus ponens not0 zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair = zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair imply zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair = zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair modus ponens not0 zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair = zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair conclude zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair = zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair cut lemma fromSameSingleton modus ponens zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair = zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair conclude metavar var sx end metavar = metavar var sx1 end metavar cut lemma inPair(2) conclude zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair in0 zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair cut lemma set equality nec condition(2) 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 sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair modus ponens zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair in0 zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair conclude zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair 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 cut lemma pair2formula modus ponens zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair 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 not0 zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair = zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair imply zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair = zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair cut prop lemma negate first disjunct modus ponens not0 zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair = zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair imply zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair = zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair modus ponens not0 zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair = zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair conclude zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair = zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair cut lemma inPair(2) conclude metavar var sy end metavar in0 zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair cut lemma set equality nec condition(2) modus ponens zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair = zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair modus ponens metavar var sy end metavar in0 zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair conclude metavar var sy end metavar in0 zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair cut lemma pair2formula modus ponens metavar var sy end metavar in0 zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair conclude not0 metavar var sy end metavar = metavar var sx1 end metavar imply metavar var sy end metavar = metavar var sy1 end metavar cut lemma unequalsNotInSingleton modus ponens not0 metavar var sx1 end metavar = metavar var sy1 end metavar conclude not0 zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair = zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair cut lemma subNeqLeft modus ponens zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair = zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair modus ponens not0 zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair = zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair conclude not0 zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair = zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair cut lemma nonsingletonmembersUnequal modus ponens not0 zermelo pair metavar var sx end metavar comma metavar var sy end metavar end pair = zermelo pair metavar var sx end metavar comma metavar var sx end metavar end pair conclude not0 metavar var sx end metavar = metavar var sy end metavar cut lemma subNeqLeft modus ponens metavar var sx end metavar = metavar var sx1 end metavar modus ponens not0 metavar var sx end metavar = metavar var sy end metavar conclude not0 metavar var sx1 end metavar = metavar var sy end metavar cut lemma neqSymmetry modus ponens not0 metavar var sx1 end metavar = metavar var sy end metavar conclude not0 metavar var sy end metavar = metavar var sx1 end metavar cut prop lemma negate first disjunct modus ponens not0 metavar var sy end metavar = metavar var sx1 end metavar imply metavar var sy end metavar = metavar var sy1 end metavar modus ponens not0 metavar var sy end metavar = metavar var sx1 end metavar conclude metavar var sy end metavar = metavar var sy1 end metavar cut prop lemma join conjuncts modus ponens metavar var sx end metavar = metavar var sx1 end metavar modus ponens metavar var sy end metavar = metavar var sy1 end metavar conclude not0 metavar var sx end metavar = metavar var sx1 end metavar imply not0 metavar var sy end metavar = metavar var sy1 end metavar 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 sx1 end metavar = 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 = zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair infer not0 metavar var sx end metavar = metavar var sx1 end metavar imply not0 metavar var sy end metavar = metavar var sy1 end metavar conclude metavar var sx1 end metavar = metavar var sy1 end metavar imply 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 sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair imply not0 metavar var sx end metavar = metavar var sx1 end metavar imply not0 metavar var sy end metavar = metavar var sy1 end metavar cut 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 not0 metavar var sx1 end metavar = 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 = zermelo pair zermelo pair metavar var sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair infer not0 metavar var sx end metavar = metavar var sx1 end metavar imply not0 metavar var sy end metavar = metavar var sy1 end metavar conclude not0 metavar var sx1 end metavar = metavar var sy1 end metavar imply 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 sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair imply not0 metavar var sx end metavar = metavar var sx1 end metavar imply not0 metavar var sy end metavar = metavar var sy1 end metavar cut 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 sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair infer prop lemma from negations modus ponens metavar var sx1 end metavar = metavar var sy1 end metavar imply 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 sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair imply not0 metavar var sx end metavar = metavar var sx1 end metavar imply not0 metavar var sy end metavar = metavar var sy1 end metavar modus ponens not0 metavar var sx1 end metavar = metavar var sy1 end metavar imply 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 sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair imply not0 metavar var sx end metavar = metavar var sx1 end metavar imply not0 metavar var sy end metavar = metavar var sy1 end metavar 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 sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair imply not0 metavar var sx end metavar = metavar var sx1 end metavar imply not0 metavar var sy end metavar = metavar var sy1 end metavar cut 1rule mp 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 sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair imply not0 metavar var sx end metavar = metavar var sx1 end metavar imply not0 metavar var sy end metavar = 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 sx1 end metavar comma metavar var sx1 end metavar end pair comma zermelo pair metavar var sx1 end metavar comma metavar var sy1 end metavar end pair end pair conclude not0 metavar var sx end metavar = metavar var sx1 end metavar imply not0 metavar var sy end metavar = metavar var sy1 end metavar end quote state proof state cache var c end expand end define