:: by Artur Korni{\l}owicz

::

:: Received February 10, 2004

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

:: Projections

definition

let x be triple object ;

consider x1, x2, x3 being object such that

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

for b_{1} being object holds

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

b_{1} = y1 )
by A1;

for b_{1} being object holds

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

b_{1} = y2 )
by A1;

for b_{1} being object holds

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

b_{1} = y3 )
by A1;

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

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

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

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

it = y1;

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

it = y1;

for b

( b

b

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

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

it = y2;

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

it = y2;

for b

( b

b

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

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

it = y3;

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

it = y3;

for b

( b

b

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

for x being triple object

for b_{2} being object holds

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

b_{2} = y1 );

for x being triple object

for b

( b

b

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

for x being triple object

for b_{2} being object holds

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

b_{2} = y2 );

for x being triple object

for b

( b

b

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

for x being triple object

for b_{2} being object holds

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

b_{2} = y3 );

for x being triple object

for b

( b

b

::$CT

theorem :: RECDEF_2:2

for z being object

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

( z `1_3 in A & z `2_3 in B & z `3_3 in C )

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

( z `1_3 in A & z `2_3 in B & z `3_3 in C )

proof end;

definition

let x be quadruple object ;

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

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

for b_{1} being object holds

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

b_{1} = y1 )
by A1;

for b_{1} being object holds

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

b_{1} = y2 )
by A1;

for b_{1} being object holds

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

b_{1} = y3 )
by A1;

for b_{1} being object holds

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

b_{1} = y4 )
by A1;

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

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

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

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

it = y1;

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

it = y1;

for b

( b

b

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

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

it = y2;

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

it = y2;

for b

( b

b

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

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

it = y3;

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

it = y3;

for b

( b

b

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

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

it = y4;

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

it = y4;

for b

( b

b

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

for x being quadruple object

for b_{2} being object holds

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

b_{2} = y1 );

for x being quadruple object

for b

( b

b

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

for x being quadruple object

for b_{2} being object holds

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

b_{2} = y2 );

for x being quadruple object

for b

( b

b

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

for x being quadruple object

for b_{2} being object holds

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

b_{2} = y3 );

for x being quadruple object

for b

( b

b

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

for x being quadruple object

for b_{2} being object holds

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

b_{2} = y4 );

for x being quadruple object

for b

( b

b

::$CT

theorem :: RECDEF_2:5

for z being object

for 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 )

for 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 )

proof end;

theorem :: RECDEF_2:6

for z being object

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

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

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

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

proof end;

definition
end;

::$CD 5

::$CD 5

::$CD 5

scheme :: RECDEF_2:sch 1

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

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}[ object ], P_{2}[ object ], P_{3}[ object ], P_{4}[ object ], F_{2}( object ) -> object , F_{3}( object ) -> object , F_{4}( object ) -> object , F_{5}( object ) -> object } :

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}[ object , object , object , object , object ] } :

DoubleChoiceRec{ F

ex f being sequence of F_{1}() ex g being sequence of F_{2}() st

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

provided( f . 0 = F

A1:
for n being 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;

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}( object , object , object ) -> Element of F_{1}() } :

LambdaRec2ExD{ F

ex f being sequence of F_{1}() st

( f . 0 = F_{2}() & f . 1 = F_{3}() & ( for n being 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}() -> object , F_{2}() -> object , F_{3}() -> Function, F_{4}() -> Function, F_{5}( object , object , object ) -> object } :

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 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 Nat holds F_{4}() . (n + 2) = F_{5}(n,(F_{4}() . n),(F_{4}() . (n + 1)))

A2: ( F

A3: for n being Nat holds F

A4: dom F

A5: ( F

A6: for n being 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}() -> sequence of F_{1}(), F_{5}() -> sequence of F_{1}(), F_{6}( object , object , object ) -> Element of F_{1}() } :

provided

LambdaRec2UnD{ F

provided

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

A2: for n being 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 Nat holds F_{5}() . (n + 2) = F_{6}(n,(F_{5}() . n),(F_{5}() . (n + 1)))

A2: for n being Nat holds F

A3: ( F

A4: for n being Nat holds F

proof end;

scheme :: RECDEF_2:sch 8

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

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 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}( object , object , object , object ) -> Element of F_{1}() } :

LambdaRec3ExD{ F

ex f being sequence of F_{1}() st

( f . 0 = F_{2}() & f . 1 = F_{3}() & f . 2 = F_{4}() & ( for n being 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}() -> object , F_{2}() -> object , F_{3}() -> object , F_{4}() -> Function, F_{5}() -> Function, F_{6}( object , object , object , object ) -> object } :

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 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 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 Nat holds F

A4: dom F

A5: ( F

A6: for n being 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}() -> sequence of F_{1}(), F_{6}() -> sequence of F_{1}(), F_{7}( object , object , object , object ) -> 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 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 Nat holds F_{6}() . (n + 3) = F_{7}(n,(F_{6}() . n),(F_{6}() . (n + 1)),(F_{6}() . (n + 2)))

A2: for n being Nat holds F

A3: ( F

A4: for n being Nat holds F

proof end;

scheme :: RECDEF_2:sch 12

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

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 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 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 Nat holds F

A4: dom F

A5: ( F

A6: for n being 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}() -> sequence of F_{1}(), F_{7}() -> sequence of F_{1}(), F_{8}( object , object , object , object , object ) -> 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 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 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 Nat holds F

A3: ( F

A4: for n being Nat holds F

proof end;

:: 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;