const Sigma : set (set set) set term setprod = \x:set.\y:set.Sigma x \z:set.y const In : set set prop term iIn = In infix iIn 2000 2000 const ap : set set set const Empty : set axiom ap0_Sigma: !x:set.!f:set set.!y:set.y iIn Sigma x f -> ap y Empty iIn x const ordsucc : set set axiom ap1_Sigma: !x:set.!f:set set.!y:set.y iIn Sigma x f -> ap y (ordsucc Empty) iIn f (ap y Empty) const Repl : set (set set) set axiom ReplE_impred: !x:set.!f:set set.!y:set.y iIn Repl x f -> !P:prop.(!z:set.z iIn x -> y = f z -> P) -> P const binunion : set set set axiom binunionE: !x:set.!y:set.!z:set.z iIn binunion x y -> z iIn x | z iIn y const If_i : prop set set set axiom tuple_2_setprod: !x:set.!y:set.!z:set.z iIn x -> !w:set.w iIn y -> Sigma (ordsucc (ordsucc Empty)) (\u:set.If_i (u = Empty) z w) iIn setprod x y axiom ReplI: !x:set.!f:set set.!y:set.y iIn x -> f y iIn Repl x f axiom tuple_2_1_eq: !x:set.!y:set.ap (Sigma (ordsucc (ordsucc Empty)) \z:set.If_i (z = Empty) x y) (ordsucc Empty) = y axiom tuple_2_0_eq: !x:set.!y:set.ap (Sigma (ordsucc (ordsucc Empty)) \z:set.If_i (z = Empty) x y) Empty = x axiom binunionI1: !x:set.!y:set.!z:set.z iIn x -> z iIn binunion x y axiom binunionI2: !x:set.!y:set.!z:set.z iIn y -> z iIn binunion x y const SNo : set prop const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 const SNoCut : set set set const SNoL : set set const add_SNo : set set set term + = add_SNo infix + 2281 2280 const minus_SNo : set set term - = minus_SNo const SNoR : set set axiom mul_SNo_eq: !x:set.SNo x -> !y:set.SNo y -> x * y = SNoCut (binunion (Repl (setprod (SNoL x) (SNoL y)) \z:set.ap z Empty * y + x * ap z (ordsucc Empty) + - ap z Empty * ap z (ordsucc Empty)) (Repl (setprod (SNoR x) (SNoR y)) \z:set.ap z Empty * y + x * ap z (ordsucc Empty) + - ap z Empty * ap z (ordsucc Empty))) (binunion (Repl (setprod (SNoL x) (SNoR y)) \z:set.ap z Empty * y + x * ap z (ordsucc Empty) + - ap z Empty * ap z (ordsucc Empty)) (Repl (setprod (SNoR x) (SNoL y)) \z:set.ap z Empty * y + x * ap z (ordsucc Empty) + - ap z Empty * ap z (ordsucc Empty))) claim !x:set.!y:set.SNo x -> SNo y -> !P:prop.(!z:set.!w:set.(!u:set.u iIn z -> !Q:prop.(!v:set.v iIn SNoL x -> !x2:set.x2 iIn SNoL y -> u = v * y + x * x2 + - v * x2 -> Q) -> (!v:set.v iIn SNoR x -> !x2:set.x2 iIn SNoR y -> u = v * y + x * x2 + - v * x2 -> Q) -> Q) -> (!u:set.u iIn SNoL x -> !v:set.v iIn SNoL y -> u * y + x * v + - u * v iIn z) -> (!u:set.u iIn SNoR x -> !v:set.v iIn SNoR y -> u * y + x * v + - u * v iIn z) -> (!u:set.u iIn w -> !Q:prop.(!v:set.v iIn SNoL x -> !x2:set.x2 iIn SNoR y -> u = v * y + x * x2 + - v * x2 -> Q) -> (!v:set.v iIn SNoR x -> !x2:set.x2 iIn SNoL y -> u = v * y + x * x2 + - v * x2 -> Q) -> Q) -> (!u:set.u iIn SNoL x -> !v:set.v iIn SNoR y -> u * y + x * v + - u * v iIn w) -> (!u:set.u iIn SNoR x -> !v:set.v iIn SNoL y -> u * y + x * v + - u * v iIn w) -> x * y = SNoCut z w -> P) -> P