define pyk of lemma equivalence class is subset 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 e unicode small q unicode small u unicode small i unicode small v unicode small a unicode small l unicode small e unicode small n unicode small c unicode small e unicode space unicode small c unicode small l unicode small a unicode small s unicode small s unicode space unicode small i unicode small s unicode space unicode small s unicode small u unicode small b unicode small s unicode small e unicode small t unicode end of text end unicode text end text end define
define tex of lemma equivalence class is subset as text unicode start of text unicode capital e unicode small q unicode capital c unicode small l unicode small a unicode small s unicode small s unicode capital i unicode small s unicode capital s unicode small u unicode small b unicode small s unicode small e unicode small t unicode end of text end unicode text end text end define
define statement of lemma equivalence class is subset as system zf infer all metavar var r end metavar indeed all metavar var s end metavar indeed all metavar var x end metavar indeed all metavar var big set end metavar indeed metavar var s end metavar zermelo in 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 metavar var x end metavar end pair end pair zermelo in metavar var r end metavar end set imply metavar var s end metavar zermelo in metavar var big set end metavar end define
define proof of lemma equivalence class is subset as lambda var c dot lambda var x dot proof expand quote system zf infer all metavar var r end metavar indeed all metavar var s end metavar indeed all metavar var x end metavar indeed all metavar var big set end metavar indeed metavar var s end metavar zermelo in 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 metavar var x end metavar end pair end pair zermelo in metavar var r end metavar end set infer lemma separation2formula modus ponens metavar var s end metavar zermelo in 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 metavar var x end metavar end pair end pair zermelo in metavar var r end metavar end set conclude not0 metavar var s end metavar zermelo in metavar var big set end metavar imply not0 zermelo pair zermelo pair metavar var s end metavar comma metavar var s end metavar end pair comma zermelo pair metavar var s end metavar comma metavar var x end metavar end pair end pair zermelo in metavar var r end metavar cut prop lemma first conjunct modus ponens not0 metavar var s end metavar zermelo in metavar var big set end metavar imply not0 zermelo pair zermelo pair metavar var s end metavar comma metavar var s end metavar end pair comma zermelo pair metavar var s end metavar comma metavar var x end metavar end pair end pair zermelo in metavar var r end metavar conclude metavar var s end metavar zermelo in metavar var big set end metavar cut all metavar var r end metavar indeed all metavar var s end metavar indeed all metavar var x end metavar indeed all metavar var big set end metavar indeed 1rule deduction modus ponens all metavar var r end metavar indeed all metavar var s end metavar indeed all metavar var x end metavar indeed all metavar var big set end metavar indeed metavar var s end metavar zermelo in 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 metavar var x end metavar end pair end pair zermelo in metavar var r end metavar end set infer metavar var s end metavar zermelo in metavar var big set end metavar conclude metavar var s end metavar zermelo in 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 metavar var x end metavar end pair end pair zermelo in metavar var r end metavar end set imply metavar var s end metavar zermelo in metavar var big set end metavar end quote state proof state cache var c end expand end define
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,