376 \<exists>f fj sj. M(f) & M(fj) & M(sj) & |
376 \<exists>f fj sj. M(f) & M(fj) & M(sj) & |
377 successor(M,j,sj) & is_omult_fun(M,i,sj,f) & |
377 successor(M,j,sj) & is_omult_fun(M,i,sj,f) & |
378 fun_apply(M,f,j,fj) & fj = k" |
378 fun_apply(M,f,j,fj) & fj = k" |
379 |
379 |
380 |
380 |
381 locale M_ord_arith = M_axioms + |
381 locale (open) M_ord_arith = M_axioms + |
382 assumes oadd_strong_replacement: |
382 assumes oadd_strong_replacement: |
383 "[| M(i); M(j) |] ==> |
383 "[| M(i); M(j) |] ==> |
384 strong_replacement(M, |
384 strong_replacement(M, |
385 \<lambda>x z. \<exists>y[M]. pair(M,x,y,z) & |
385 \<lambda>x z. \<exists>y[M]. pair(M,x,y,z) & |
386 (\<exists>f[M]. \<exists>fx[M]. is_oadd_fun(M,i,j,x,f) & |
386 (\<exists>f[M]. \<exists>fx[M]. is_oadd_fun(M,i,j,x,f) & |