begin
theorem Th1:
theorem Th2:
theorem
theorem
theorem Th5:
theorem Th6:
theorem
theorem Th8:
theorem
theorem Th10:
theorem
theorem Th12:
theorem
theorem Th14:
:: deftheorem Def1 defines "increasing STIRL2_1:def 1 :
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem
theorem
theorem Th23:
theorem Th24:
theorem Th25:
:: deftheorem defines block STIRL2_1:def 2 :
theorem Th26:
theorem Th27:
theorem
theorem Th29:
theorem
theorem Th31:
theorem Th32:
theorem
for
k,
n being
Nat holds
( ( ( 1
<= k &
k <= n ) or
k = n ) iff
n block k > 0 )
scheme
Sch2{
F1()
-> set ,
F2()
-> set ,
F3()
-> set ,
F4()
-> set ,
F5()
-> Function of
F1(),
F2(),
F6(
set )
-> set } :
ex
h being
Function of
F3(),
F4() st
(
h | F1()
= F5() & ( for
x being
set st
x in F3()
\ F1() holds
h . x = F6(
x) ) )
provided
A1:
for
x being
set st
x in F3()
\ F1() holds
F6(
x)
in F4()
and A2:
(
F1()
c= F3() &
F2()
c= F4() )
and A3:
(
F2() is
empty implies
F1() is
empty )
scheme
Sch3{
F1()
-> set ,
F2()
-> set ,
F3()
-> set ,
F4()
-> set ,
F5(
set )
-> set ,
P1[
set ,
set ,
set ] } :
card { f where f is Function of F1(),F2() : P1[f,F1(),F2()] } = card { f where f is Function of F3(),F4() : ( P1[f,F3(),F4()] & rng (f | F1()) c= F2() & ( for x being set st x in F3() \ F1() holds
f . x = F5(x) ) ) }
provided
A1:
for
x being
set st
x in F3()
\ F1() holds
F5(
x)
in F4()
and A2:
(
F1()
c= F3() &
F2()
c= F4() )
and A3:
(
F2() is
empty implies
F1() is
empty )
and A4:
for
f being
Function of
F3(),
F4() st ( for
x being
set st
x in F3()
\ F1() holds
F5(
x)
= f . x ) holds
(
P1[
f,
F3(),
F4()] iff
P1[
f | F1(),
F1(),
F2()] )
scheme
Sch4{
F1()
-> set ,
F2()
-> set ,
F3()
-> set ,
F4()
-> set ,
P1[
set ,
set ,
set ] } :
provided
A1:
(
F2() is
empty implies
F1() is
empty )
and A2:
not
F3()
in F1()
and A3:
for
f being
Function of
(F1() \/ {F3()}),
(F2() \/ {F4()}) st
f . F3()
= F4() holds
(
P1[
f,
F1()
\/ {F3()},
F2()
\/ {F4()}] iff
P1[
f | F1(),
F1(),
F2()] )
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
Lm1:
for k, n being Nat st k < n holds
n \/ {k} = n
theorem Th42:
theorem Th43:
definition
canceled;
end;
:: deftheorem STIRL2_1:def 3 :
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
definition
canceled;
end;
:: deftheorem STIRL2_1:def 4 :
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
Lm2:
for n being Nat holds n |^ 3 = (n * n) * n
theorem
theorem Th60:
theorem Th61:
theorem Th62:
theorem
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
Lm3:
for X being finite set
for x being set st x in X holds
card (X \ {x}) < card X
theorem Th70:
Lm4:
for n being Element of NAT
for N being finite Subset of NAT
for F being Function of N,(card N) st n in N & F is bijective & ( for n, k being Nat st n in dom F & k in dom F & n < k holds
F . n < F . k ) holds
ex P being Permutation of N st
for k being Nat st k in N holds
( ( k < n implies P . k = (F " ) . ((F . k) + 1) ) & ( k = n implies P . k = (F " ) . 0 ) & ( k > n implies P . k = k ) )
theorem Th71:
:: deftheorem Def5 defines "increasing STIRL2_1:def 5 :
theorem Th72:
theorem
theorem Th74:
theorem