:: Recursive Definitions. {P}art {II}
:: 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 ;
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 b1 being set holds
( b1 = x `1_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds
b1 = y1 ) by A1, A2, XTUPLE_0:3;
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 b1 being set holds
( b1 = x `2_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds
b1 = y2 ) by A1, A3, XTUPLE_0:3;
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 b1 being set holds
( b1 = x `3_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds
b1 = y3 ) by A1, A4, XTUPLE_0:3;
end;

:: deftheorem Def1 defines `1_3 RECDEF_2:def 1 :
for x being triple set
for b2 being set holds
( b2 = x `1_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds
b2 = y1 );

:: deftheorem Def2 defines `2_3 RECDEF_2:def 2 :
for x being triple set
for b2 being set holds
( b2 = x `2_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds
b2 = y2 );

:: deftheorem Def3 defines `3_3 RECDEF_2:def 3 :
for x being triple set
for b2 being set holds
( b2 = x `3_3 iff for y1, y2, y3 being set st x = [y1,y2,y3] holds
b2 = y3 );

theorem Th1: :: RECDEF_2:1
for z being set st ex a, b, c being set st z = [a,b,c] holds
z = [(z `1_3),(z `2_3),(z `3_3)]
proof end;

theorem :: RECDEF_2:2
for z, 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;

theorem Th3: :: RECDEF_2:3
for z, A, B, C being set st z in [:A,B,C:] holds
z = [(z `1_3),(z `2_3),(z `3_3)]
proof end;

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 ;
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 b1 being set holds
( b1 = x `1_4 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b1 = y1 ) by A1, A2, XTUPLE_0:5;
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 b1 being set holds
( b1 = x `2_4 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b1 = y2 ) by A1, A3, XTUPLE_0:5;
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 b1 being set holds
( b1 = x `2_3 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b1 = y3 ) by A1, A4, XTUPLE_0:5;
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 b1 being set holds
( b1 = x `3_3 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b1 = y4 ) by A1, A5, XTUPLE_0:5;
end;

:: deftheorem Def4 defines `1_4 RECDEF_2:def 4 :
for x being quadruple set
for b2 being set holds
( b2 = x `1_4 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b2 = y1 );

:: deftheorem Def5 defines `2_4 RECDEF_2:def 5 :
for x being quadruple set
for b2 being set holds
( b2 = x `2_4 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b2 = y2 );

:: deftheorem Def6 defines `2_3 RECDEF_2:def 6 :
for x being quadruple set
for b2 being set holds
( b2 = x `2_3 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b2 = y3 );

:: deftheorem Def7 defines `3_3 RECDEF_2:def 7 :
for x being quadruple set
for b2 being set holds
( b2 = x `3_3 iff for y1, y2, y3, y4 being set st x = [y1,y2,y3,y4] holds
b2 = y4 );

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)]
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 )
proof end;

theorem :: RECDEF_2:6
for z, 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
canceled;
canceled;
canceled;
canceled;
canceled;
end;

:: deftheorem RECDEF_2:def 8 :
canceled;

:: deftheorem RECDEF_2:def 9 :
canceled;

:: deftheorem RECDEF_2:def 10 :
canceled;

:: deftheorem RECDEF_2:def 11 :
canceled;

:: deftheorem RECDEF_2:def 12 :
canceled;

theorem :: RECDEF_2:7
canceled;

theorem :: RECDEF_2:8
canceled;

theorem :: RECDEF_2:9
canceled;

:: Conditional schemes
scheme :: RECDEF_2:sch 1
ExFunc3Cond{ F1() -> set , P1[ set ], P2[ set ], P3[ set ], F2( set ) -> set , F3( set ) -> set , F4( set ) -> set } :
ex f being Function st
( dom f = F1() & ( for c being set st c in F1() holds
( ( P1[c] implies f . c = F2(c) ) & ( P2[c] implies f . c = F3(c) ) & ( P3[c] implies f . c = F4(c) ) ) ) )
provided
A1: for c being set st c in F1() holds
( ( P1[c] implies not P2[c] ) & ( P1[c] implies not P3[c] ) & ( P2[c] implies not P3[c] ) ) and
A2: for c being set holds
( not c in F1() or P1[c] or P2[c] or P3[c] )
proof end;

scheme :: RECDEF_2:sch 2
ExFunc4Cond{ F1() -> set , P1[ set ], P2[ set ], P3[ set ], P4[ set ], F2( set ) -> set , F3( set ) -> set , F4( set ) -> set , F5( set ) -> set } :
ex f being Function st
( dom f = F1() & ( for c being set st c in F1() holds
( ( P1[c] implies f . c = F2(c) ) & ( P2[c] implies f . c = F3(c) ) & ( P3[c] implies f . c = F4(c) ) & ( P4[c] implies f . c = F5(c) ) ) ) )
provided
A1: for c being set st c in F1() holds
( ( P1[c] implies not P2[c] ) & ( P1[c] implies not P3[c] ) & ( P1[c] implies not P4[c] ) & ( P2[c] implies not P3[c] ) & ( P2[c] implies not P4[c] ) & ( P3[c] implies not P4[c] ) ) and
A2: for c being set holds
( not c in F1() or P1[c] or P2[c] or P3[c] or P4[c] )
proof end;

:: 1 step
scheme :: RECDEF_2:sch 3
DoubleChoiceRec{ F1() -> non empty set , F2() -> non empty set , F3() -> Element of F1(), F4() -> Element of F2(), P1[ set , set , set , set , set ] } :
ex f being Function of NAT,F1() ex g being Function of NAT,F2() st
( f . 0 = F3() & g . 0 = F4() & ( for n being Element of NAT holds P1[n,f . n,g . n,f . (n + 1),g . (n + 1)] ) )
provided
A1: for n being Element of NAT
for x being Element of F1()
for y being Element of F2() ex x1 being Element of F1() ex y1 being Element of F2() st P1[n,x,y,x1,y1]
proof end;

:: 2 steps
scheme :: RECDEF_2:sch 4
LambdaRec2Ex{ F1() -> set , F2() -> set , F3( set , set , set ) -> set } :
ex f being Function st
( dom f = NAT & f . 0 = F1() & f . 1 = F2() & ( for n being Element of NAT holds f . (n + 2) = F3(n,(f . n),(f . (n + 1))) ) )
proof end;

scheme :: RECDEF_2:sch 5
LambdaRec2ExD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Element of F1(), F4( set , set , set ) -> Element of F1() } :
ex f being Function of NAT,F1() st
( f . 0 = F2() & f . 1 = F3() & ( for n being Element of NAT holds f . (n + 2) = F4(n,(f . n),(f . (n + 1))) ) )
proof end;

scheme :: RECDEF_2:sch 6
LambdaRec2Un{ F1() -> set , F2() -> set , F3() -> Function, F4() -> Function, F5( set , set , set ) -> set } :
F3() = F4()
provided
A1: dom F3() = NAT and
A2: ( F3() . 0 = F1() & F3() . 1 = F2() ) and
A3: for n being Element of NAT holds F3() . (n + 2) = F5(n,(F3() . n),(F3() . (n + 1))) and
A4: dom F4() = NAT and
A5: ( F4() . 0 = F1() & F4() . 1 = F2() ) and
A6: for n being Element of NAT holds F4() . (n + 2) = F5(n,(F4() . n),(F4() . (n + 1)))
proof end;

scheme :: RECDEF_2:sch 7
LambdaRec2UnD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Element of F1(), F4() -> Function of NAT,F1(), F5() -> Function of NAT,F1(), F6( set , set , set ) -> Element of F1() } :
F4() = F5()
provided
A1: ( F4() . 0 = F2() & F4() . 1 = F3() ) and
A2: for n being Element of NAT holds F4() . (n + 2) = F6(n,(F4() . n),(F4() . (n + 1))) and
A3: ( F5() . 0 = F2() & F5() . 1 = F3() ) and
A4: for n being Element of NAT holds F5() . (n + 2) = F6(n,(F5() . n),(F5() . (n + 1)))
proof end;

:: 3 steps
scheme :: RECDEF_2:sch 8
LambdaRec3Ex{ F1() -> set , F2() -> set , F3() -> set , F4( set , set , set , set ) -> set } :
ex f being Function st
( dom f = NAT & f . 0 = F1() & f . 1 = F2() & f . 2 = F3() & ( for n being Element of NAT holds f . (n + 3) = F4(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )
proof end;

scheme :: RECDEF_2:sch 9
LambdaRec3ExD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Element of F1(), F4() -> Element of F1(), F5( set , set , set , set ) -> Element of F1() } :
ex f being Function of NAT,F1() st
( f . 0 = F2() & f . 1 = F3() & f . 2 = F4() & ( for n being Element of NAT holds f . (n + 3) = F5(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )
proof end;

scheme :: RECDEF_2:sch 10
LambdaRec3Un{ F1() -> set , F2() -> set , F3() -> set , F4() -> Function, F5() -> Function, F6( set , set , set , set ) -> set } :
F4() = F5()
provided
A1: dom F4() = NAT and
A2: ( F4() . 0 = F1() & F4() . 1 = F2() & F4() . 2 = F3() ) and
A3: for n being Element of NAT holds F4() . (n + 3) = F6(n,(F4() . n),(F4() . (n + 1)),(F4() . (n + 2))) and
A4: dom F5() = NAT and
A5: ( F5() . 0 = F1() & F5() . 1 = F2() & F5() . 2 = F3() ) and
A6: for n being Element of NAT holds F5() . (n + 3) = F6(n,(F5() . n),(F5() . (n + 1)),(F5() . (n + 2)))
proof end;

scheme :: RECDEF_2:sch 11
LambdaRec3UnD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Element of F1(), F4() -> Element of F1(), F5() -> Function of NAT,F1(), F6() -> Function of NAT,F1(), F7( set , set , set , set ) -> Element of F1() } :
F5() = F6()
provided
A1: ( F5() . 0 = F2() & F5() . 1 = F3() & F5() . 2 = F4() ) and
A2: for n being Element of NAT holds F5() . (n + 3) = F7(n,(F5() . n),(F5() . (n + 1)),(F5() . (n + 2))) and
A3: ( F6() . 0 = F2() & F6() . 1 = F3() & F6() . 2 = F4() ) and
A4: for n being Element of NAT holds F6() . (n + 3) = F7(n,(F6() . n),(F6() . (n + 1)),(F6() . (n + 2)))
proof end;

:: 4 steps
scheme :: RECDEF_2:sch 12
LambdaRec4Un{ F1() -> set , F2() -> set , F3() -> set , F4() -> set , F5() -> Function, F6() -> Function, F7( set , set , set , set , set ) -> set } :
F5() = F6()
provided
A1: dom F5() = NAT and
A2: ( F5() . 0 = F1() & F5() . 1 = F2() & F5() . 2 = F3() & F5() . 3 = F4() ) and
A3: for n being Element of NAT holds F5() . (n + 4) = F7(n,(F5() . n),(F5() . (n + 1)),(F5() . (n + 2)),(F5() . (n + 3))) and
A4: dom F6() = NAT and
A5: ( F6() . 0 = F1() & F6() . 1 = F2() & F6() . 2 = F3() & F6() . 3 = F4() ) and
A6: for n being Element of NAT holds F6() . (n + 4) = F7(n,(F6() . n),(F6() . (n + 1)),(F6() . (n + 2)),(F6() . (n + 3)))
proof end;

scheme :: RECDEF_2:sch 13
LambdaRec4UnD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Element of F1(), F4() -> Element of F1(), F5() -> Element of F1(), F6() -> Function of NAT,F1(), F7() -> Function of NAT,F1(), F8( set , set , set , set , set ) -> Element of F1() } :
F6() = F7()
provided
A1: ( F6() . 0 = F2() & F6() . 1 = F3() & F6() . 2 = F4() & F6() . 3 = F5() ) and
A2: for n being Element of NAT holds F6() . (n + 4) = F8(n,(F6() . n),(F6() . (n + 1)),(F6() . (n + 2)),(F6() . (n + 3))) and
A3: ( F7() . 0 = F2() & F7() . 1 = F3() & F7() . 2 = F4() & F7() . 3 = F5() ) and
A4: for n being Element of NAT holds F7() . (n + 4) = F8(n,(F7() . n),(F7() . (n + 1)),(F7() . (n + 2)),(F7() . (n + 3)))
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
proof end;