:: 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 b₁ being object holds
( b₁ = x `1_3 iff for y1, y2, y3 being object st x = [y1,y2,y3] holds
b₁ = 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 b₁ being object holds
( b₁ = x `2_3 iff for y1, y2, y3 being object st x = [y1,y2,y3] holds
b₁ = 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 b₁ being object holds
( b₁ = x `3_3 iff for y1, y2, y3 being object st x = [y1,y2,y3] holds
b₁ = y3 ) by A1;

end;

:: deftheorem defines `1_3 RECDEF_2:def 1 :
for x being triple object
for b<sub>2</sub> being object holds
( b<sub>2</sub> = x `1_3 iff for y1, y2, y3 being object st x = [y1,y2,y3] holds
b₂ = y1 );

:: deftheorem defines `2_3 RECDEF_2:def 2 :
for x being triple object
for b<sub>2</sub> being object holds
( b<sub>2</sub> = x `2_3 iff for y1, y2, y3 being object st x = [y1,y2,y3] holds
b₂ = y2 );

:: deftheorem defines `3_3 RECDEF_2:def 3 :
for x being triple object
for b<sub>2</sub> being object holds
( b<sub>2</sub> = x `3_3 iff for y1, y2, y3 being object st x = [y1,y2,y3] holds
b₂ = 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 b₁ being object holds
( b₁ = x `1_4 iff for y1, y2, y3, y4 being object st x = [y1,y2,y3,y4] holds
b₁ = 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 b₁ being object holds
( b₁ = x `2_4 iff for y1, y2, y3, y4 being object st x = [y1,y2,y3,y4] holds
b₁ = 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 b₁ being object holds
( b₁ = x `2_3 iff for y1, y2, y3, y4 being object st x = [y1,y2,y3,y4] holds
b₁ = 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 b₁ being object holds
( b₁ = x `3_3 iff for y1, y2, y3, y4 being object st x = [y1,y2,y3,y4] holds
b₁ = y4 ) by A1;

end;

:: deftheorem defines `1_4 RECDEF_2:def 4 :
for x being quadruple object
for b<sub>2</sub> being object holds
( b<sub>2</sub> = x `1_4 iff for y1, y2, y3, y4 being object st x = [y1,y2,y3,y4] holds
b₂ = y1 );

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

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

:: deftheorem defines `3_3 RECDEF_2:def 7 :
for x being quadruple object
for b<sub>2</sub> being object holds
( b<sub>2</sub> = x `3_3 iff for y1, y2, y3, y4 being object st x = [y1,y2,y3,y4] holds
b₂ = 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{ F₁() -> set , P₁[ object ], P₂[ object ], P₃[ object ], F₂( object ) -> object , F₃( object ) -> object , F₄( object ) -> object } :

ex f being Function st
( dom f = F₁() & ( for c being set st c in F₁() holds
( ( P₁[c] implies f . c = F₂(c) ) & ( P₂[c] implies f . c = F₃(c) ) & ( P₃[c] implies f . c = F₄(c) ) ) ) )

provided

A1: for c being set st c in F₁() holds
( ( P₁[c] implies not P₂[c] ) & ( P₁[c] implies not P₃[c] ) & ( P₂[c] implies not P₃[c] ) ) and
A2: for c being set holds
( not c in F₁() or P₁[c] or P₂[c] or P₃[c] )

proof end;

scheme :: RECDEF_2:sch 2
ExFunc4Cond{ F₁() -> set , P₁[ object ], P₂[ object ], P₃[ object ], P₄[ object ], F₂( object ) -> object , F₃( object ) -> object , F₄( object ) -> object , F₅( object ) -> object } :

ex f being Function st
( dom f = F₁() & ( for c being set st c in F₁() holds
( ( P₁[c] implies f . c = F₂(c) ) & ( P₂[c] implies f . c = F₃(c) ) & ( P₃[c] implies f . c = F₄(c) ) & ( P₄[c] implies f . c = F₅(c) ) ) ) )

provided

A1: for c being set st c in F₁() holds
( ( P₁[c] implies not P₂[c] ) & ( P₁[c] implies not P₃[c] ) & ( P₁[c] implies not P₄[c] ) & ( P₂[c] implies not P₃[c] ) & ( P₂[c] implies not P₄[c] ) & ( P₃[c] implies not P₄[c] ) ) and
A2: for c being set holds
( not c in F₁() or P₁[c] or P₂[c] or P₃[c] or P₄[c] )

proof end;

:: 1 step

scheme :: RECDEF_2:sch 3
DoubleChoiceRec{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> Element of F₁(), F₄() -> Element of F₂(), P₁[ object , object , object , object , object ] } :

ex f being sequence of F₁() ex g being sequence of F₂() st
( f . 0 = F₃() & g . 0 = F₄() & ( for n being Nat holds P₁[n,f . n,g . n,f . (n + 1),g . (n + 1)] ) )

provided

A1: for n being Nat
for x being Element of F₁()
for y being Element of F₂() ex x1 being Element of F₁() ex y1 being Element of F₂() st P₁[n,x,y,x1,y1]

proof end;

:: 2 steps

scheme :: RECDEF_2:sch 4
LambdaRec2Ex{ F₁() -> set , F₂() -> set , F₃( object , object , object ) -> object } :

ex f being Function st
( dom f = NAT & f . 0 = F₁() & f . 1 = F₂() & ( for n being Nat holds f . (n + 2) = F₃(n,(f . n),(f . (n + 1))) ) )

proof end;

scheme :: RECDEF_2:sch 5
LambdaRec2ExD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄( object , object , object ) -> Element of F₁() } :

ex f being sequence of F₁() st
( f . 0 = F₂() & f . 1 = F₃() & ( for n being Nat holds f . (n + 2) = F₄(n,(f . n),(f . (n + 1))) ) )

proof end;

scheme :: RECDEF_2:sch 6
LambdaRec2Un{ F₁() -> object , F₂() -> object , F₃() -> Function, F₄() -> Function, F₅( object , object , object ) -> object } :

F₃() = F₄()

provided

A1: dom F₃() = NAT and
A2: ( F₃() . 0 = F₁() & F₃() . 1 = F₂() ) and
A3: for n being Nat holds F₃() . (n + 2) = F₅(n,(F₃() . n),(F₃() . (n + 1))) and
A4: dom F₄() = NAT and
A5: ( F₄() . 0 = F₁() & F₄() . 1 = F₂() ) and
A6: for n being Nat holds F₄() . (n + 2) = F₅(n,(F₄() . n),(F₄() . (n + 1)))

proof end;

scheme :: RECDEF_2:sch 7
LambdaRec2UnD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄() -> sequence of F₁(), F₅() -> sequence of F₁(), F₆( object , object , object ) -> Element of F₁() } :

F₄() = F₅()

provided

A1: ( F₄() . 0 = F₂() & F₄() . 1 = F₃() ) and
A2: for n being Nat holds F₄() . (n + 2) = F₆(n,(F₄() . n),(F₄() . (n + 1))) and
A3: ( F₅() . 0 = F₂() & F₅() . 1 = F₃() ) and
A4: for n being Nat holds F₅() . (n + 2) = F₆(n,(F₅() . n),(F₅() . (n + 1)))

proof end;

:: 3 steps

scheme :: RECDEF_2:sch 8
LambdaRec3Ex{ F₁() -> set , F₂() -> set , F₃() -> set , F₄( object , object , object , object ) -> object } :

ex f being Function st
( dom f = NAT & f . 0 = F₁() & f . 1 = F₂() & f . 2 = F₃() & ( for n being Nat holds f . (n + 3) = F₄(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )

proof end;

scheme :: RECDEF_2:sch 9
LambdaRec3ExD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄() -> Element of F₁(), F₅( object , object , object , object ) -> Element of F₁() } :

ex f being sequence of F₁() st
( f . 0 = F₂() & f . 1 = F₃() & f . 2 = F₄() & ( for n being Nat holds f . (n + 3) = F₅(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )

proof end;

scheme :: RECDEF_2:sch 10
LambdaRec3Un{ F₁() -> object , F₂() -> object , F₃() -> object , F₄() -> Function, F₅() -> Function, F₆( object , object , object , object ) -> object } :

F₄() = F₅()

provided

A1: dom F₄() = NAT and
A2: ( F₄() . 0 = F₁() & F₄() . 1 = F₂() & F₄() . 2 = F₃() ) and
A3: for n being Nat holds F₄() . (n + 3) = F₆(n,(F₄() . n),(F₄() . (n + 1)),(F₄() . (n + 2))) and
A4: dom F₅() = NAT and
A5: ( F₅() . 0 = F₁() & F₅() . 1 = F₂() & F₅() . 2 = F₃() ) and
A6: for n being Nat holds F₅() . (n + 3) = F₆(n,(F₅() . n),(F₅() . (n + 1)),(F₅() . (n + 2)))

proof end;

scheme :: RECDEF_2:sch 11
LambdaRec3UnD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄() -> Element of F₁(), F₅() -> sequence of F₁(), F₆() -> sequence of F₁(), F₇( object , object , object , object ) -> Element of F₁() } :

F₅() = F₆()

provided

A1: ( F₅() . 0 = F₂() & F₅() . 1 = F₃() & F₅() . 2 = F₄() ) and
A2: for n being Nat holds F₅() . (n + 3) = F₇(n,(F₅() . n),(F₅() . (n + 1)),(F₅() . (n + 2))) and
A3: ( F₆() . 0 = F₂() & F₆() . 1 = F₃() & F₆() . 2 = F₄() ) and
A4: for n being Nat holds F₆() . (n + 3) = F₇(n,(F₆() . n),(F₆() . (n + 1)),(F₆() . (n + 2)))

proof end;

:: 4 steps

scheme :: RECDEF_2:sch 12
LambdaRec4Un{ F₁() -> object , F₂() -> object , F₃() -> object , F₄() -> object , F₅() -> Function, F₆() -> Function, F₇( object , object , object , object , object ) -> object } :

F₅() = F₆()

provided

A1: dom F₅() = NAT and
A2: ( F₅() . 0 = F₁() & F₅() . 1 = F₂() & F₅() . 2 = F₃() & F₅() . 3 = F₄() ) and
A3: for n being Nat holds F₅() . (n + 4) = F₇(n,(F₅() . n),(F₅() . (n + 1)),(F₅() . (n + 2)),(F₅() . (n + 3))) and
A4: dom F₆() = NAT and
A5: ( F₆() . 0 = F₁() & F₆() . 1 = F₂() & F₆() . 2 = F₃() & F₆() . 3 = F₄() ) and
A6: for n being Nat holds F₆() . (n + 4) = F₇(n,(F₆() . n),(F₆() . (n + 1)),(F₆() . (n + 2)),(F₆() . (n + 3)))

proof end;

scheme :: RECDEF_2:sch 13
LambdaRec4UnD{ F₁() -> non empty set , F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄() -> Element of F₁(), F₅() -> Element of F₁(), F₆() -> sequence of F₁(), F₇() -> sequence of F₁(), F₈( object , object , object , object , object ) -> Element of F₁() } :

F₆() = F₇()

provided

A1: ( F₆() . 0 = F₂() & F₆() . 1 = F₃() & F₆() . 2 = F₄() & F₆() . 3 = F₅() ) and
A2: for n being Nat holds F₆() . (n + 4) = F₈(n,(F₆() . n),(F₆() . (n + 1)),(F₆() . (n + 2)),(F₆() . (n + 3))) and
A3: ( F₇() . 0 = F₂() & F₇() . 1 = F₃() & F₇() . 2 = F₄() & F₇() . 3 = F₅() ) and
A4: for n being Nat holds F₇() . (n + 4) = F₈(n,(F₇() . n),(F₇() . (n + 1)),(F₇() . (n + 2)),(F₇() . (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;