begin
scheme
Ind{
P1[
Nat] } :
provided
A1:
P1[
0 ]
and A2:
for
k being
Element of
NAT st
P1[
k] holds
P1[
k + 1]
scheme
NatInd{
P1[
Nat] } :
for
k being
Nat holds
P1[
k]
provided
A1:
P1[
0 ]
and A2:
for
k being
Nat st
P1[
k] holds
P1[
k + 1]
theorem
for
i,
j,
h being
Nat st
i <= j holds
i * h <= j * h
theorem
for
i being
Nat holds
0 < i + 1
theorem Th6:
for
i being
Nat holds
(
i = 0 or ex
k being
Nat st
i = k + 1 )
theorem Th7:
for
i,
j being
Nat st
i + j = 0 holds
(
i = 0 &
j = 0 )
scheme
DefbyInd{
F1()
-> Nat,
F2(
Nat,
Nat)
-> Nat,
P1[
Nat,
Nat] } :
( ( for
k being
Nat ex
n being
Nat st
P1[
k,
n] ) & ( for
k,
n,
m being
Nat st
P1[
k,
n] &
P1[
k,
m] holds
n = m ) )
provided
A1:
for
k,
n being
Nat holds
(
P1[
k,
n] iff ( (
k = 0 &
n = F1() ) or ex
m,
l being
Nat st
(
k = m + 1 &
P1[
m,
l] &
n = F2(
k,
l) ) ) )
theorem Th8:
for
i,
j being
Nat holds
( not
i <= j + 1 or
i <= j or
i = j + 1 )
theorem Th9:
for
i,
j being
Nat st
i <= j &
j <= i + 1 & not
i = j holds
j = i + 1
theorem Th10:
for
i,
j being
Nat st
i <= j holds
ex
k being
Nat st
j = i + k
theorem Th11:
for
i,
j being
Nat holds
i <= i + j
scheme
CompInd{
P1[
Nat] } :
for
k being
Nat holds
P1[
k]
provided
A1:
for
k being
Nat st ( for
n being
Nat st
n < k holds
P1[
n] ) holds
P1[
k]
scheme
Min{
P1[
Nat] } :
ex
k being
Nat st
(
P1[
k] & ( for
n being
Nat st
P1[
n] holds
k <= n ) )
provided
A1:
ex
k being
Nat st
P1[
k]
scheme
Max{
P1[
Nat],
F1()
-> Nat } :
ex
k being
Nat st
(
P1[
k] & ( for
n being
Nat st
P1[
n] holds
n <= k ) )
provided
A1:
for
k being
Nat st
P1[
k] holds
k <= F1()
and A2:
ex
k being
Nat st
P1[
k]
theorem Th12:
for
i,
j,
h being
Nat st
i <= j holds
i <= j + h
theorem Th13:
for
i,
j being
Nat holds
(
i < j + 1 iff
i <= j )
theorem Th14:
for
j being
Nat st
j < 1 holds
j = 0
theorem
for
i,
j being
Nat st
i * j = 1 holds
i = 1
theorem Th16:
for
k,
n being
Nat st
k <> 0 holds
n < n + k
scheme
Regr{
P1[
Nat] } :
provided
A1:
ex
k being
Nat st
P1[
k]
and A2:
for
k being
Nat st
k <> 0 &
P1[
k] holds
ex
n being
Nat st
(
n < k &
P1[
n] )
theorem
for
m being
Nat st
0 < m holds
for
n being
Nat ex
k,
t being
Nat st
(
n = (m * k) + t &
t < m )
theorem
for
n,
m,
k,
t,
k1,
t1 being
Nat st
n = (m * k) + t &
t < m &
n = (m * k1) + t1 &
t1 < m holds
(
k = k1 &
t = t1 )
theorem
for
k,
n being
Nat holds
(
k < k + n iff 1
<= n )
begin
theorem Th22:
for
m,
n being
Nat holds
( not
m < n + 1 or
m < n or
m = n )
theorem
for
k being
Nat holds
( not
k < 2 or
k = 0 or
k = 1 )
theorem
for
i,
h,
j being
Nat st
i <> 0 &
h = j * i holds
j <= h
scheme
Ind1{
F1()
-> Nat,
P1[
Nat] } :
for
i being
Nat st
F1()
<= i holds
P1[
i]
provided
A1:
P1[
F1()]
and A2:
for
j being
Nat st
F1()
<= j &
P1[
j] holds
P1[
j + 1]
scheme
CompInd1{
F1()
-> Nat,
P1[
Nat] } :
for
k being
Nat st
k >= F1() holds
P1[
k]
provided
A1:
for
k being
Nat st
k >= F1() & ( for
n being
Nat st
n >= F1() &
n < k holds
P1[
n] ) holds
P1[
k]
theorem Th25:
for
n being
Nat holds
( not
n <= 1 or
n = 0 or
n = 1 )
theorem Th26:
for
n being
Nat holds
( not
n <= 2 or
n = 0 or
n = 1 or
n = 2 )
theorem Th27:
for
n being
Nat holds
( not
n <= 3 or
n = 0 or
n = 1 or
n = 2 or
n = 3 )
theorem Th28:
for
n being
Nat holds
( not
n <= 4 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 )
theorem Th29:
for
n being
Nat holds
( not
n <= 5 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 or
n = 5 )
theorem Th30:
for
n being
Nat holds
( not
n <= 6 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 or
n = 5 or
n = 6 )
theorem Th31:
for
n being
Nat holds
( not
n <= 7 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 or
n = 5 or
n = 6 or
n = 7 )
theorem Th32:
for
n being
Nat holds
( not
n <= 8 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 or
n = 5 or
n = 6 or
n = 7 or
n = 8 )
theorem Th33:
for
n being
Nat holds
( not
n <= 9 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 or
n = 5 or
n = 6 or
n = 7 or
n = 8 or
n = 9 )
theorem Th34:
for
n being
Nat holds
( not
n <= 10 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 or
n = 5 or
n = 6 or
n = 7 or
n = 8 or
n = 9 or
n = 10 )
theorem Th35:
for
n being
Nat holds
( not
n <= 11 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 or
n = 5 or
n = 6 or
n = 7 or
n = 8 or
n = 9 or
n = 10 or
n = 11 )
theorem Th36:
for
n being
Nat holds
( not
n <= 12 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 or
n = 5 or
n = 6 or
n = 7 or
n = 8 or
n = 9 or
n = 10 or
n = 11 or
n = 12 )
theorem Th37:
for
n being
Nat holds
( not
n <= 13 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 or
n = 5 or
n = 6 or
n = 7 or
n = 8 or
n = 9 or
n = 10 or
n = 11 or
n = 12 or
n = 13 )
scheme
Indfrom1{
P1[
Nat] } :
provided
A1:
P1[1]
and A2:
for
k being non
empty Nat st
P1[
k] holds
P1[
k + 1]
theorem Th39:
for
n,
m being
Nat holds
(
n <= m iff
n c= m )
theorem
for
k,
n being
Nat holds
(
k in n iff
k < n )
theorem
for
n being
Nat holds
n in n + 1
theorem
for
k,
n being
Nat st
k <= n holds
k = k /\ n
scheme
RecUn{
F1()
-> set ,
F2()
-> Function,
F3()
-> Function,
P1[
set ,
set ,
set ] } :
provided
A1:
dom F2()
= NAT
and A2:
F2()
. 0 = F1()
and A3:
for
n being
Nat holds
P1[
n,
F2()
. n,
F2()
. (n + 1)]
and A4:
dom F3()
= NAT
and A5:
F3()
. 0 = F1()
and A6:
for
n being
Nat holds
P1[
n,
F3()
. n,
F3()
. (n + 1)]
and A7:
for
n being
Nat for
x,
y1,
y2 being
set st
P1[
n,
x,
y1] &
P1[
n,
x,
y2] holds
y1 = y2
scheme
RecUnD{
F1()
-> non
empty set ,
F2()
-> Element of
F1(),
P1[
set ,
set ,
set ],
F3()
-> Function of
NAT,
F1(),
F4()
-> Function of
NAT,
F1() } :
provided
A1:
F3()
. 0 = F2()
and A2:
for
n being
Nat holds
P1[
n,
F3()
. n,
F3()
. (n + 1)]
and A3:
F4()
. 0 = F2()
and A4:
for
n being
Nat holds
P1[
n,
F4()
. n,
F4()
. (n + 1)]
and A5:
for
n being
Nat for
x,
y1,
y2 being
Element of
F1() st
P1[
n,
x,
y1] &
P1[
n,
x,
y2] holds
y1 = y2
scheme
MinIndex{
F1(
Nat)
-> Nat } :
ex
k being
Nat st
(
F1(
k)
= 0 & ( for
n being
Nat st
F1(
n)
= 0 holds
k <= n ) )
provided
A1:
for
k being
Nat holds
(
F1(
(k + 1))
< F1(
k) or
F1(
k)
= 0 )
Lm1:
for s being ManySortedSet of NAT
for k being Nat holds rng (s ^\ k) c= rng s
theorem
for
n being
Nat holds
(
n is
zero or
n = 1 or
n > 1 )
theorem Th56:
for
n being
Nat for
m being
Nat st
n <= m &
m <= n + 2 & not
m = n & not
m = n + 1 holds
m = n + 2
theorem Th57:
for
n being
Nat for
m being
Nat st
n <= m &
m <= n + 3 & not
m = n & not
m = n + 1 & not
m = n + 2 holds
m = n + 3
theorem
for
n being
Nat for
m being
Nat st
n <= m &
m <= n + 4 & not
m = n & not
m = n + 1 & not
m = n + 2 & not
m = n + 3 holds
m = n + 4
theorem
for
n being
Nat holds
( not
n <= 14 or
n = 0 or
n = 1 or
n = 2 or
n = 3 or
n = 4 or
n = 5 or
n = 6 or
n = 7 or
n = 8 or
n = 9 or
n = 10 or
n = 11 or
n = 12 or
n = 13 or
n = 14 )