environ
vocabularies HIDDEN, NUMBERS, NAT_1, INT_1, RELAT_1, ARYTM_3, CARD_1, XXREAL_0, SUBSET_1, ARYTM_1, INT_2, COMPLEX1, ZFMISC_1, XBOOLE_0, FINSET_1, ORDINAL1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, FINSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, INT_1, NAT_1, INT_2;
definitions ;
theorems ORDINAL1, XCMPLX_1, XREAL_1, XXREAL_0, NAT_1, INT_1, INT_2, ABSVALUE, XREAL_0, CARD_1, ZFMISC_1, COMPLEX1, XCMPLX_0, TARSKI;
schemes NAT_1;
registrations XXREAL_0, XREAL_0, NAT_1, INT_1, ORDINAL1, CARD_1;
constructors HIDDEN, XXREAL_0, NAT_1, INT_2, REAL_1, FINSET_1, CARD_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities ;
expansions ;
scheme
Euklides{
F1(
Nat)
-> Nat,
F2()
-> Nat,
F3()
-> Nat } :
ex
n being
Nat st
(
F1(
n)
= F2()
gcd F3() &
F1(
(n + 1))
= 0 )
provided
A1:
(
0 < F3() &
F3()
< F2() )
and A2:
(
F1(
0)
= F2() &
F1(1)
= F3() )
and A3:
for
n being
Nat holds
F1(
(n + 2))
= F1(
n)
mod F1(
(n + 1))