:: by Artur Korni{\l}owicz

::

:: Received February 10, 2004

:: Copyright (c) 2004-2012 Association of Mizar Users

begin

:: Projections

definition

let x be triple set ;

consider x1, x2, x3 being set such that

A1: x = [x1,x2,x3] by XTUPLE_0:def 5;

A2: [x1,x2,x3] `1_3 = x1 ;

A3: [x1,x2,x3] `2_3 = x2 ;

A4: [x1,x2,x3] `3_3 = x3 ;

for b_{1} being set holds

( b_{1} = x `1_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds

b_{1} = y1 )
by A1, A2, XTUPLE_0:3;

for b_{1} being set holds

( b_{1} = x `2_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds

b_{1} = y2 )
by A1, A3, XTUPLE_0:3;

for b_{1} being set holds

( b_{1} = x `3_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds

b_{1} = y3 )
by A1, A4, XTUPLE_0:3;

end;
consider x1, x2, x3 being set such that

A1: x = [x1,x2,x3] by XTUPLE_0:def 5;

A2: [x1,x2,x3] `1_3 = x1 ;

A3: [x1,x2,x3] `2_3 = x2 ;

A4: [x1,x2,x3] `3_3 = x3 ;

redefine func x `1_3 means :Def1: :: RECDEF_2:def 1

for y1, y2, y3 being set st x = [y1,y2,y3] holds

it = y1;

compatibility for y1, y2, y3 being set st x = [y1,y2,y3] holds

it = y1;

for b

( b

b

redefine func x `2_3 means :Def2: :: RECDEF_2:def 2

for y1, y2, y3 being set st x = [y1,y2,y3] holds

it = y2;

compatibility for y1, y2, y3 being set st x = [y1,y2,y3] holds

it = y2;

for b

( b

b

redefine func x `2 means :Def3: :: RECDEF_2:def 3

for y1, y2, y3 being set st x = [y1,y2,y3] holds

it = y3;

compatibility for y1, y2, y3 being set st x = [y1,y2,y3] holds

it = y3;

for b

( b

b

:: deftheorem Def1 defines `1_3 RECDEF_2:def 1 :

for x being triple set

for b_{2} being set holds

( b_{2} = x `1_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds

b_{2} = y1 );

for x being triple set

for b

( b

b

:: deftheorem Def2 defines `2_3 RECDEF_2:def 2 :

for x being triple set

for b_{2} being set holds

( b_{2} = x `2_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds

b_{2} = y2 );

for x being triple set

for b

( b

b

:: deftheorem Def3 defines `3_3 RECDEF_2:def 3 :

for x being triple set

for b_{2} being set holds

( b_{2} = x `3_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds

b_{2} = y3 );

for x being triple set

for b

( b

b

definition

let x be quadruple set ;

consider x1, x2, x3, x4 being set such that

A1: x = [x1,x2,x3,x4] by XTUPLE_0:def 9;

A2: [x1,x2,x3,x4] `1_4 = x1 ;

A3: [x1,x2,x3,x4] `2_4 = x2 ;

A4: [x1,x2,x3,x4] `3_4 = x3 ;

A5: [x1,x2,x3,x4] `4_4 = x4 ;

for b_{1} being set holds

( b_{1} = x `1_4 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds

b_{1} = y1 )
by A1, A2, XTUPLE_0:5;

for b_{1} being set holds

( b_{1} = x `2_4 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds

b_{1} = y2 )
by A1, A3, XTUPLE_0:5;

for b_{1} being set holds

( b_{1} = x `2_3 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds

b_{1} = y3 )
by A1, A4, XTUPLE_0:5;

for b_{1} being set holds

( b_{1} = x `3_3 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds

b_{1} = y4 )
by A1, A5, XTUPLE_0:5;

end;
consider x1, x2, x3, x4 being set such that

A1: x = [x1,x2,x3,x4] by XTUPLE_0:def 9;

A2: [x1,x2,x3,x4] `1_4 = x1 ;

A3: [x1,x2,x3,x4] `2_4 = x2 ;

A4: [x1,x2,x3,x4] `3_4 = x3 ;

A5: [x1,x2,x3,x4] `4_4 = x4 ;

redefine func x `1_4 means :Def4: :: RECDEF_2:def 4

for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds

it = y1;

compatibility for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds

it = y1;

for b

( b

b

redefine func x `2_4 means :Def5: :: RECDEF_2:def 5

for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds

it = y2;

compatibility for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds

it = y2;

for b

( b

b

redefine func x `2_3 means :Def6: :: RECDEF_2:def 6

for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds

it = y3;

compatibility for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds

it = y3;

for b

( b

b

redefine func x `2 means :Def7: :: RECDEF_2:def 7

for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds

it = y4;

compatibility for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds

it = y4;

for b

( b

b

:: deftheorem Def4 defines `1_4 RECDEF_2:def 4 :

for x being quadruple set

for b_{2} being set holds

( b_{2} = x `1_4 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds

b_{2} = y1 );

for x being quadruple set

for b

( b

b

:: deftheorem Def5 defines `2_4 RECDEF_2:def 5 :

for x being quadruple set

for b_{2} being set holds

( b_{2} = x `2_4 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds

b_{2} = y2 );

for x being quadruple set

for b

( b

b

:: deftheorem Def6 defines `2_3 RECDEF_2:def 6 :

for x being quadruple set

for b_{2} being set holds

( b_{2} = x `2_3 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds

b_{2} = y3 );

for x being quadruple set

for b

( b

b

:: deftheorem Def7 defines `3_3 RECDEF_2:def 7 :

for x being quadruple set

for b_{2} being set holds

( b_{2} = x `3_3 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds

b_{2} = y4 );

for x being quadruple set

for b

( b

b

theorem Th4: :: RECDEF_2:4

for z being set st ex a, b, c, d being set st z = [a,b,c,d] holds

z = [(z `1_4),(z `2_4),(z `3_4),(z `4_4)]

z = [(z `1_4),(z `2_4),(z `3_4),(z `4_4)]

proof end;

theorem :: RECDEF_2:5

for z, A, B, C, D being set st z in [:A,B,C,D:] holds

( z `1_4 in A & z `2_4 in B & z `3_4 in C & z `4_4 in D )

( z `1_4 in A & z `2_4 in B & z `3_4 in C & z `4_4 in D )

proof end;

definition

canceled;

canceled;

canceled;

canceled;

canceled;

end;
canceled;

canceled;

canceled;

canceled;

:: Conditional schemes

scheme :: RECDEF_2:sch 1

ExFunc3Cond{ F_{1}() -> set , P_{1}[ set ], P_{2}[ set ], P_{3}[ set ], F_{2}( set ) -> set , F_{3}( set ) -> set , F_{4}( set ) -> set } :

ExFunc3Cond{ F

ex f being Function st

( dom f = F_{1}() & ( for c being set st c in F_{1}() holds

( ( P_{1}[c] implies f . c = F_{2}(c) ) & ( P_{2}[c] implies f . c = F_{3}(c) ) & ( P_{3}[c] implies f . c = F_{4}(c) ) ) ) )

provided( dom f = F

( ( P

A1:
for c being set st c in F_{1}() holds

( ( P_{1}[c] implies not P_{2}[c] ) & ( P_{1}[c] implies not P_{3}[c] ) & ( P_{2}[c] implies not P_{3}[c] ) )
and

A2: for c being set holds

( not c in F_{1}() or P_{1}[c] or P_{2}[c] or P_{3}[c] )

( ( P

A2: for c being set holds

( not c in F

proof end;

scheme :: RECDEF_2:sch 2

ExFunc4Cond{ F_{1}() -> set , P_{1}[ set ], P_{2}[ set ], P_{3}[ set ], P_{4}[ set ], F_{2}( set ) -> set , F_{3}( set ) -> set , F_{4}( set ) -> set , F_{5}( set ) -> set } :

ExFunc4Cond{ F

ex f being Function st

( dom f = F_{1}() & ( for c being set st c in F_{1}() holds

( ( P_{1}[c] implies f . c = F_{2}(c) ) & ( P_{2}[c] implies f . c = F_{3}(c) ) & ( P_{3}[c] implies f . c = F_{4}(c) ) & ( P_{4}[c] implies f . c = F_{5}(c) ) ) ) )

provided( dom f = F

( ( P

A1:
for c being set st c in F_{1}() holds

( ( P_{1}[c] implies not P_{2}[c] ) & ( P_{1}[c] implies not P_{3}[c] ) & ( P_{1}[c] implies not P_{4}[c] ) & ( P_{2}[c] implies not P_{3}[c] ) & ( P_{2}[c] implies not P_{4}[c] ) & ( P_{3}[c] implies not P_{4}[c] ) )
and

A2: for c being set holds

( not c in F_{1}() or P_{1}[c] or P_{2}[c] or P_{3}[c] or P_{4}[c] )

( ( P

A2: for c being set holds

( not c in F

proof end;

:: 1 step

scheme :: RECDEF_2:sch 3

DoubleChoiceRec{ F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> Element of F_{1}(), F_{4}() -> Element of F_{2}(), P_{1}[ set , set , set , set , set ] } :

DoubleChoiceRec{ F

ex f being Function of NAT,F_{1}() ex g being Function of NAT,F_{2}() st

( f . 0 = F_{3}() & g . 0 = F_{4}() & ( for n being Element of NAT holds P_{1}[n,f . n,g . n,f . (n + 1),g . (n + 1)] ) )

provided( f . 0 = F

A1:
for n being Element of NAT

for x being Element of F_{1}()

for y being Element of F_{2}() ex x1 being Element of F_{1}() ex y1 being Element of F_{2}() st P_{1}[n,x,y,x1,y1]

for x being Element of F

for y being Element of F

proof end;

:: 2 steps

scheme :: RECDEF_2:sch 5

LambdaRec2ExD{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}() -> Element of F_{1}(), F_{4}( set , set , set ) -> Element of F_{1}() } :

LambdaRec2ExD{ F

ex f being Function of NAT,F_{1}() st

( f . 0 = F_{2}() & f . 1 = F_{3}() & ( for n being Element of NAT holds f . (n + 2) = F_{4}(n,(f . n),(f . (n + 1))) ) )

( f . 0 = F

proof end;

scheme :: RECDEF_2:sch 6

LambdaRec2Un{ F_{1}() -> set , F_{2}() -> set , F_{3}() -> Function, F_{4}() -> Function, F_{5}( set , set , set ) -> set } :

provided

LambdaRec2Un{ F

provided

A1:
dom F_{3}() = NAT
and

A2: ( F_{3}() . 0 = F_{1}() & F_{3}() . 1 = F_{2}() )
and

A3: for n being Element of NAT holds F_{3}() . (n + 2) = F_{5}(n,(F_{3}() . n),(F_{3}() . (n + 1)))
and

A4: dom F_{4}() = NAT
and

A5: ( F_{4}() . 0 = F_{1}() & F_{4}() . 1 = F_{2}() )
and

A6: for n being Element of NAT holds F_{4}() . (n + 2) = F_{5}(n,(F_{4}() . n),(F_{4}() . (n + 1)))

A2: ( F

A3: for n being Element of NAT holds F

A4: dom F

A5: ( F

A6: for n being Element of NAT holds F

proof end;

scheme :: RECDEF_2:sch 7

LambdaRec2UnD{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}() -> Element of F_{1}(), F_{4}() -> Function of NAT,F_{1}(), F_{5}() -> Function of NAT,F_{1}(), F_{6}( set , set , set ) -> Element of F_{1}() } :

provided

LambdaRec2UnD{ F

provided

A1:
( F_{4}() . 0 = F_{2}() & F_{4}() . 1 = F_{3}() )
and

A2: for n being Element of NAT holds F_{4}() . (n + 2) = F_{6}(n,(F_{4}() . n),(F_{4}() . (n + 1)))
and

A3: ( F_{5}() . 0 = F_{2}() & F_{5}() . 1 = F_{3}() )
and

A4: for n being Element of NAT holds F_{5}() . (n + 2) = F_{6}(n,(F_{5}() . n),(F_{5}() . (n + 1)))

A2: for n being Element of NAT holds F

A3: ( F

A4: for n being Element of NAT holds F

proof end;

:: 3 steps

scheme :: RECDEF_2:sch 8

LambdaRec3Ex{ F_{1}() -> set , F_{2}() -> set , F_{3}() -> set , F_{4}( set , set , set , set ) -> set } :

LambdaRec3Ex{ F

ex f being Function st

( dom f = NAT & f . 0 = F_{1}() & f . 1 = F_{2}() & f . 2 = F_{3}() & ( for n being Element of NAT holds f . (n + 3) = F_{4}(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )

( dom f = NAT & f . 0 = F

proof end;

scheme :: RECDEF_2:sch 9

LambdaRec3ExD{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}() -> Element of F_{1}(), F_{4}() -> Element of F_{1}(), F_{5}( set , set , set , set ) -> Element of F_{1}() } :

LambdaRec3ExD{ F

ex f being Function of NAT,F_{1}() st

( f . 0 = F_{2}() & f . 1 = F_{3}() & f . 2 = F_{4}() & ( for n being Element of NAT holds f . (n + 3) = F_{5}(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )

( f . 0 = F

proof end;

scheme :: RECDEF_2:sch 10

LambdaRec3Un{ F_{1}() -> set , F_{2}() -> set , F_{3}() -> set , F_{4}() -> Function, F_{5}() -> Function, F_{6}( set , set , set , set ) -> set } :

provided

LambdaRec3Un{ F

provided

A1:
dom F_{4}() = NAT
and

A2: ( F_{4}() . 0 = F_{1}() & F_{4}() . 1 = F_{2}() & F_{4}() . 2 = F_{3}() )
and

A3: for n being Element of NAT holds F_{4}() . (n + 3) = F_{6}(n,(F_{4}() . n),(F_{4}() . (n + 1)),(F_{4}() . (n + 2)))
and

A4: dom F_{5}() = NAT
and

A5: ( F_{5}() . 0 = F_{1}() & F_{5}() . 1 = F_{2}() & F_{5}() . 2 = F_{3}() )
and

A6: for n being Element of NAT holds F_{5}() . (n + 3) = F_{6}(n,(F_{5}() . n),(F_{5}() . (n + 1)),(F_{5}() . (n + 2)))

A2: ( F

A3: for n being Element of NAT holds F

A4: dom F

A5: ( F

A6: for n being Element of NAT holds F

proof end;

scheme :: RECDEF_2:sch 11

LambdaRec3UnD{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}() -> Element of F_{1}(), F_{4}() -> Element of F_{1}(), F_{5}() -> Function of NAT,F_{1}(), F_{6}() -> Function of NAT,F_{1}(), F_{7}( set , set , set , set ) -> Element of F_{1}() } :

provided

LambdaRec3UnD{ F

provided

A1:
( F_{5}() . 0 = F_{2}() & F_{5}() . 1 = F_{3}() & F_{5}() . 2 = F_{4}() )
and

A2: for n being Element of NAT holds F_{5}() . (n + 3) = F_{7}(n,(F_{5}() . n),(F_{5}() . (n + 1)),(F_{5}() . (n + 2)))
and

A3: ( F_{6}() . 0 = F_{2}() & F_{6}() . 1 = F_{3}() & F_{6}() . 2 = F_{4}() )
and

A4: for n being Element of NAT holds F_{6}() . (n + 3) = F_{7}(n,(F_{6}() . n),(F_{6}() . (n + 1)),(F_{6}() . (n + 2)))

A2: for n being Element of NAT holds F

A3: ( F

A4: for n being Element of NAT holds F

proof end;

:: 4 steps

scheme :: RECDEF_2:sch 12

LambdaRec4Un{ F_{1}() -> set , F_{2}() -> set , F_{3}() -> set , F_{4}() -> set , F_{5}() -> Function, F_{6}() -> Function, F_{7}( set , set , set , set , set ) -> set } :

provided

LambdaRec4Un{ F

provided

A1:
dom F_{5}() = NAT
and

A2: ( F_{5}() . 0 = F_{1}() & F_{5}() . 1 = F_{2}() & F_{5}() . 2 = F_{3}() & F_{5}() . 3 = F_{4}() )
and

A3: for n being Element of NAT holds F_{5}() . (n + 4) = F_{7}(n,(F_{5}() . n),(F_{5}() . (n + 1)),(F_{5}() . (n + 2)),(F_{5}() . (n + 3)))
and

A4: dom F_{6}() = NAT
and

A5: ( F_{6}() . 0 = F_{1}() & F_{6}() . 1 = F_{2}() & F_{6}() . 2 = F_{3}() & F_{6}() . 3 = F_{4}() )
and

A6: for n being Element of NAT holds F_{6}() . (n + 4) = F_{7}(n,(F_{6}() . n),(F_{6}() . (n + 1)),(F_{6}() . (n + 2)),(F_{6}() . (n + 3)))

A2: ( F

A3: for n being Element of NAT holds F

A4: dom F

A5: ( F

A6: for n being Element of NAT holds F

proof end;

scheme :: RECDEF_2:sch 13

LambdaRec4UnD{ F_{1}() -> non empty set , F_{2}() -> Element of F_{1}(), F_{3}() -> Element of F_{1}(), F_{4}() -> Element of F_{1}(), F_{5}() -> Element of F_{1}(), F_{6}() -> Function of NAT,F_{1}(), F_{7}() -> Function of NAT,F_{1}(), F_{8}( set , set , set , set , set ) -> Element of F_{1}() } :

provided

LambdaRec4UnD{ F

provided

A1:
( F_{6}() . 0 = F_{2}() & F_{6}() . 1 = F_{3}() & F_{6}() . 2 = F_{4}() & F_{6}() . 3 = F_{5}() )
and

A2: for n being Element of NAT holds F_{6}() . (n + 4) = F_{8}(n,(F_{6}() . n),(F_{6}() . (n + 1)),(F_{6}() . (n + 2)),(F_{6}() . (n + 3)))
and

A3: ( F_{7}() . 0 = F_{2}() & F_{7}() . 1 = F_{3}() & F_{7}() . 2 = F_{4}() & F_{7}() . 3 = F_{5}() )
and

A4: for n being Element of NAT holds F_{7}() . (n + 4) = F_{8}(n,(F_{7}() . n),(F_{7}() . (n + 1)),(F_{7}() . (n + 2)),(F_{7}() . (n + 3)))

A2: for n being Element of NAT holds F

A3: ( F

A4: for n being Element of NAT holds F

proof end;

begin

:: 2010.05.120, A.T.

theorem :: RECDEF_2:10

for x, y, X, Y, Z being set st x `1_3 = y `1_3 & x `2_3 = y `2_3 & x `3_3 = y `3_3 & y in [:X,Y,Z:] & x in [:X,Y,Z:] holds

x = y

x = y

proof end;