:: Recursive Definitions. {P}art {II}
:: by Artur Korni{\l}owicz
::
:: Received February 10, 2004
:: Copyright (c) 2004-2021 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;
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 b1 being object holds
( b1 = x `1_3 iff for y1, y2, y3 being object st x = [y1,y2,y3] holds
b1 = y1 )
by A1;
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 b1 being object holds
( b1 = x `2_3 iff for y1, y2, y3 being object st x = [y1,y2,y3] holds
b1 = y2 )
by A1;
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 b1 being object holds
( b1 = x `3_3 iff for y1, y2, y3 being object st x = [y1,y2,y3] holds
b1 = y3 )
by A1;
end;

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

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

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

theorem :: RECDEF_2:1
canceled;

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

theorem Th3: :: RECDEF_2:3
for z being object
for 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 object ;
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 b1 being object holds
( b1 = x `1_4 iff for y1, y2, y3, y4 being object st x = [y1,y2,y3,y4] holds
b1 = y1 )
by A1;
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 b1 being object holds
( b1 = x `2_4 iff for y1, y2, y3, y4 being object st x = [y1,y2,y3,y4] holds
b1 = y2 )
by A1;
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 b1 being object holds
( b1 = x `2_3 iff for y1, y2, y3, y4 being object st x = [y1,y2,y3,y4] holds
b1 = y3 )
by A1;
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 b1 being object holds
( b1 = x `3_3 iff for y1, y2, y3, y4 being object st x = [y1,y2,y3,y4] holds
b1 = y4 )
by A1;
end;

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

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

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

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

theorem :: RECDEF_2:4
canceled;

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

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

::$CD 5
theorem :: RECDEF_2:7
canceled;

::$CD 5
theorem :: RECDEF_2:8
canceled;

::$CD 5
theorem :: RECDEF_2:9
canceled;

::$CT 3
:: Conditional schemes
scheme :: RECDEF_2:sch 1
ExFunc3Cond{ F1() -> set , P1[ object ], P2[ object ], P3[ object ], F2( object ) -> object , F3( object ) -> object , F4( object ) -> object } :
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[ object ], P2[ object ], P3[ object ], P4[ object ], F2( object ) -> object , F3( object ) -> object , F4( object ) -> object , F5( object ) -> object } :
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[ object , object , object , object , object ] } :
ex f being sequence of F1() ex g being sequence of F2() st
( f . 0 = F3() & g . 0 = F4() & ( for n being Nat holds P1[n,f . n,g . n,f . (n + 1),g . (n + 1)] ) )
provided
A1: for n being 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( object , object , object ) -> object } :
ex f being Function st
( dom f = NAT & f . 0 = F1() & f . 1 = F2() & ( for n being 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( object , object , object ) -> Element of F1() } :
ex f being sequence of F1() st
( f . 0 = F2() & f . 1 = F3() & ( for n being Nat holds f . (n + 2) = F4(n,(f . n),(f . (n + 1))) ) )
proof end;

scheme :: RECDEF_2:sch 6
LambdaRec2Un{ F1() -> object , F2() -> object , F3() -> Function, F4() -> Function, F5( object , object , object ) -> object } :
F3() = F4()
provided
A1: dom F3() = NAT and
A2: ( F3() . 0 = F1() & F3() . 1 = F2() ) and
A3: for n being 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 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() -> sequence of F1(), F5() -> sequence of F1(), F6( object , object , object ) -> Element of F1() } :
F4() = F5()
provided
A1: ( F4() . 0 = F2() & F4() . 1 = F3() ) and
A2: for n being 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 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( object , object , object , object ) -> object } :
ex f being Function st
( dom f = NAT & f . 0 = F1() & f . 1 = F2() & f . 2 = F3() & ( for n being 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( object , object , object , object ) -> Element of F1() } :
ex f being sequence of F1() st
( f . 0 = F2() & f . 1 = F3() & f . 2 = F4() & ( for n being Nat holds f . (n + 3) = F5(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )
proof end;

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