environ
vocabularies HIDDEN, ORDINAL1, FUNCT_1, XBOOLE_0, TARSKI, ZFMISC_1, RELAT_1, SETFAM_1, SUBSET_1, FUNCOP_1, ORDINAL2, NAT_1, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, SETFAM_1, FUNCOP_1;
definitions ORDINAL1, TARSKI, XBOOLE_0;
theorems TARSKI, ORDINAL1, SETFAM_1, ZFMISC_1, FUNCT_1, RELAT_1, XBOOLE_1, FUNCOP_1, XTUPLE_0;
schemes XBOOLE_0, FUNCT_1, ORDINAL1;
registrations SUBSET_1, FUNCT_1, ORDINAL1, FUNCOP_1;
constructors HIDDEN, SETFAM_1, ORDINAL1, FUNCOP_1;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities ORDINAL1, XBOOLE_0;
expansions ORDINAL1, TARSKI, XBOOLE_0;
Lm1:
1 = succ 0
;
scheme
OmegaInd{
F1()
-> Nat,
P1[
object ] } :
provided
A1:
P1[
0 ]
and A2:
for
a being
Nat st
P1[
a] holds
P1[
succ a]
scheme
RecUn{
F1()
-> set ,
F2()
-> Function,
F3()
-> Function,
P1[
set ,
set ,
set ] } :
provided
A1:
dom F2()
= omega
and A2:
F2()
. 0 = F1()
and A3:
for
n being
Nat holds
P1[
n,
F2()
. n,
F2()
. (succ n)]
and A4:
dom F3()
= omega
and A5:
F3()
. 0 = F1()
and A6:
for
n being
Nat holds
P1[
n,
F3()
. n,
F3()
. (succ n)]
and A7:
for
n being
Nat for
x,
y1,
y2 being
set st
P1[
n,
x,
y1] &
P1[
n,
x,
y2] holds
y1 = y2