const In : set set prop term iIn = In infix iIn 2000 2000 term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y const SNo : set prop const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 axiom SNo_mul_SNo: !x:set.!y:set.SNo x -> SNo y -> SNo (x * y) const SNoLt : set set prop term < = SNoLt infix < 2020 2020 const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 axiom SNoLtLe: !x:set.!y:set.x < y -> x <= y const omega : set const nat_p : set prop axiom omega_nat_p: !x:set.x iIn omega -> nat_p x const ordinal : set prop axiom nat_p_ordinal: !x:set.nat_p x -> ordinal x const Empty : set axiom SNo_0: SNo Empty const ordsucc : set set axiom nat_0_in_ordsucc: !x:set.nat_p x -> Empty iIn ordsucc x const SNoLev : set set axiom SNoLev_0: SNoLev Empty = Empty axiom ordinal_SNoLev_max_2: !x:set.ordinal x -> !y:set.SNo y -> SNoLev y iIn ordsucc x -> y <= x axiom mul_SNo_assoc: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> x * y * z = (x * y) * z axiom mul_SNo_oneR: !x:set.SNo x -> x * ordsucc Empty = x axiom SNoLe_tra: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> x <= y -> y <= z -> x <= z const exp_SNo_nat : set set set lemma !x:set.!y:set.!z:set.SNo x -> SNo (exp_SNo_nat (ordsucc (ordsucc Empty)) y) -> ordsucc Empty <= exp_SNo_nat (ordsucc (ordsucc Empty)) y * x -> z iIn omega -> SNo z -> Empty <= z -> z * ordsucc Empty <= z * exp_SNo_nat (ordsucc (ordsucc Empty)) y * x var x:set var y:set var z:set var w:set hyp SNo x hyp SNo (exp_SNo_nat (ordsucc (ordsucc Empty)) z) hyp ordsucc Empty <= exp_SNo_nat (ordsucc (ordsucc Empty)) z * x hyp SNo y hyp w iIn omega hyp y < w hyp SNo w claim SNo (w * exp_SNo_nat (ordsucc (ordsucc Empty)) z) -> y <= (w * exp_SNo_nat (ordsucc (ordsucc Empty)) z) * x