define pyk of cheating axiom all disjoint as text unicode start of text unicode small c unicode small h unicode small e unicode small a unicode small t unicode small i unicode small n unicode small g unicode space unicode small a unicode small x unicode small i unicode small o unicode small m unicode space unicode small a unicode small l unicode small l unicode space unicode small d unicode small i unicode small s unicode small j unicode small o unicode small i unicode small n unicode small t unicode end of text end unicode text end text end define
define tex of cheating axiom all disjoint as text unicode start of text unicode capital c unicode small h unicode small e unicode small a unicode small t unicode capital a unicode small l unicode small l unicode capital d unicode small i unicode small s unicode small j unicode small o unicode small i unicode small n unicode small t unicode end of text end unicode text end text end define
define statement of cheating axiom all disjoint as system zf infer all metavar var r end metavar indeed all metavar var x end metavar indeed all metavar var y end metavar indeed all metavar var big set end metavar indeed not0 not0 for all objects object var var s end var indeed object var var s end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var s end var end pair end pair zermelo in metavar var r end metavar imply not0 for all objects object var var s end var indeed for all objects object var var t end var indeed for all objects object var var u end var indeed object var var s end var zermelo in metavar var big set end metavar imply object var var t end var zermelo in metavar var big set end metavar imply object var var u end var zermelo in metavar var big set end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var t end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var t end var comma object var var t end var end pair comma zermelo pair object var var t end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar imply zermelo pair zermelo pair object var var s end var comma object var var s end var end pair comma zermelo pair object var var s end var comma object var var u end var end pair end pair zermelo in metavar var r end metavar infer metavar var x end metavar zermelo in the set of ph in power metavar var big set end metavar end power such that not0 existential var var t end var zermelo in metavar var big set end metavar imply not0 the set of ph in metavar var big set end metavar such that zermelo pair zermelo pair placeholder-var var a end var comma placeholder-var var a end var end pair comma zermelo pair placeholder-var var a end var comma existential var var t end var end pair end pair zermelo in metavar var r end metavar end set zermelo is placeholder-var var b end var end set infer metavar var y end metavar zermelo in the set of ph in power metavar var big set end metavar end power such that not0 existential var var t end var zermelo in metavar var big set end metavar imply not0 the set of ph in metavar var big set end metavar such that zermelo pair zermelo pair placeholder-var var a end var comma placeholder-var var a end var end pair comma zermelo pair placeholder-var var a end var comma existential var var t end var end pair end pair zermelo in metavar var r end metavar end set zermelo is placeholder-var var b end var end set infer not0 metavar var x end metavar zermelo is metavar var y end metavar infer the set of ph in union zermelo pair zermelo pair metavar var x end metavar comma metavar var x end metavar end pair comma zermelo pair metavar var y end metavar comma metavar var y end metavar end pair end pair end union such that not0 placeholder-var var c end var zermelo in metavar var x end metavar imply not0 placeholder-var var c end var zermelo in metavar var y end metavar end set zermelo is zermelo empty set end define
define proof of cheating axiom all disjoint as rule tactic end define
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,