define pyk of axiom reciprocalF as text unicode start of text unicode small a unicode small x unicode small i unicode small o unicode small m unicode space unicode small r unicode small e unicode small c unicode small i unicode small p unicode small r unicode small o unicode small c unicode small a unicode small l unicode capital f unicode end of text end unicode text end text end define
define tex of axiom reciprocalF as text unicode start of text unicode capital r unicode small e unicode small c unicode small i unicode small p unicode small r unicode small o unicode small c unicode small a unicode small l unicode capital f unicode end of text end unicode text end text end define
define statement of axiom reciprocalF as system Q infer all metavar var m end metavar indeed all metavar var fx end metavar indeed [ the set of ph in the set of ph in power power U( zermelo pair N comma Q 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 N imply not0 object var var op2 end var in0 Q 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 such that not0 for all objects metavar var m end metavar indeed not0 not0 not0 not0 [ metavar var fx end metavar ; metavar var m end metavar ] = 0 imply not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma 1/ [ metavar var fx end metavar ; metavar var m end metavar ] end pair end pair imply not0 [ metavar var fx end metavar ; metavar var m end metavar ] = 0 imply not0 placeholder-var var f end var = zermelo pair zermelo pair metavar var m end metavar comma metavar var m end metavar end pair comma zermelo pair metavar var m end metavar comma 0 end pair end pair end set ; metavar var m end metavar ] = if( [ metavar var fx end metavar ; metavar var m end metavar ] = 0 , 0 , 1/ [ metavar var fx end metavar ; metavar var m end metavar ] ) end define
define proof of axiom reciprocalF as rule tactic end define
The pyk compiler, version 0.grue.20060417+ by Klaus Grue,