const SNo : set prop const ordsucc : set set const Empty : set axiom SNo_2: SNo (ordsucc (ordsucc Empty)) axiom SNo_1: SNo (ordsucc Empty) const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 axiom mul_SNo_oneR: !x:set.SNo x -> x * ordsucc Empty = x const exp_SNo_nat : set set set axiom exp_SNo_nat_0: !x:set.SNo x -> exp_SNo_nat x Empty = ordsucc Empty const eps_ : set set axiom eps_0_1: eps_ Empty = ordsucc Empty const nat_p : set prop axiom nat_ordsucc: !x:set.nat_p x -> nat_p (ordsucc x) const In : set set prop term iIn = In infix iIn 2000 2000 const omega : set axiom nat_p_omega: !x:set.nat_p x -> x iIn omega axiom SNo_eps_: !x:set.x iIn omega -> SNo (eps_ x) axiom exp_SNo_nat_S: !x:set.SNo x -> !y:set.nat_p y -> exp_SNo_nat x (ordsucc y) = x * exp_SNo_nat x y axiom nat_ind: !p:set prop.p Empty -> (!x:set.nat_p x -> p x -> p (ordsucc x)) -> !x:set.nat_p x -> p x lemma !x:set.nat_p x -> eps_ x * exp_SNo_nat (ordsucc (ordsucc Empty)) x = ordsucc Empty -> SNo (eps_ (ordsucc x)) -> eps_ (ordsucc x) * ordsucc (ordsucc Empty) * exp_SNo_nat (ordsucc (ordsucc Empty)) x = ordsucc Empty claim !x:set.nat_p x -> eps_ x * exp_SNo_nat (ordsucc (ordsucc Empty)) x = ordsucc Empty