set r05 = F₅(0 ,F₁(),F₂(),F₃(),F₄());
set r15 = F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()));
set r25 = F₅(2,F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())));
set r35 = F₅(3,F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())),F₅(2,F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()))));
deffunc H₁( Element of NAT , set ) -> set = [($2 `2_5 ),($2 `3_5 ),($2 `4_5 ),($2 `5_5 ),F₅(($1 + 1),($2 `2_5 ),($2 `3_5 ),($2 `4_5 ),($2 `5_5 ))];
deffunc H₂( Nat, set ) -> set = H₁($1 + 3,$2);
consider h being Function such that
dom h = NAT and
A1: h . 0 = [F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())),F₅(2,F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()))),F₅(3,F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())),F₅(2,F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()))))] and
A2: for n being Nat holds h . (n + 1) = H₂(n,h . n) from NAT_1:sch 11();
defpred S₁[ set ] means $1 = 0 ;
defpred S₂[ set ] means $1 = 1;
defpred S₃[ set ] means $1 = 2;
defpred S₄[ set ] means In $1,NAT > 2;
deffunc H₃( set ) -> set = [F₁(),F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())];
deffunc H₄( set ) -> set = [F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()))];
deffunc H₅( set ) -> set = [F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())),F₅(2,F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())))];
deffunc H₆( set ) -> set = h . ((In $1,NAT ) -' 3);
A3: for c being set st c in NAT holds
( ( S₁[c] implies not S₂[c] ) & ( S₁[c] implies not S₃[c] ) & ( S₁[c] implies not S₄[c] ) & ( S₂[c] implies not S₃[c] ) & ( S₂[c] implies not S₄[c] ) & ( S₃[c] implies not S₄[c] ) )

proof

let c be set ; :: thesis:
assume c in NAT ; :: thesis:
then In c,NAT = c by FUNCT_7:def 1;
hence ( ( S₁[c] implies not S₂[c] ) & ( S₁[c] implies not S₃[c] ) & ( S₁[c] implies not S₄[c] ) & ( S₂[c] implies not S₃[c] ) & ( S₂[c] implies not S₄[c] ) & ( S₃[c] implies not S₄[c] ) ) ; :: thesis:

end;

A4: for c being set holds
( not c in NAT or S₁[c] or S₂[c] or S₃[c] or S₄[c] )

proof

let c be set ; :: thesis:
assume c in NAT ; :: thesis:
then In c,NAT = c by FUNCT_7:def 1;
hence ( S₁[c] or S₂[c] or S₃[c] or S₄[c] ) by NAT_1:27; :: thesis:

end;

consider g being Function such that
dom g = NAT and
A5: for x being set st x in NAT holds
( ( S₁[x] implies g . x = H₃(x) ) & ( S₂[x] implies g . x = H₄(x) ) & ( S₃[x] implies g . x = H₅(x) ) & ( S₄[x] implies g . x = H₆(x) ) ) from RECDEF_2:sch 2(A3, A4);
A6: g . 0 = [F₁(),F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())] by A5;
A7: g . 1 = [F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()))] by A5;
A8: g . 2 = [F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())),F₅(2,F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())))] by A5;
A9: In 3,NAT = 3 by FUNCT_7:def 1;
then A10: g . 3 = H₆(3) by A5
.= [F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())),F₅(2,F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()))),F₅(3,F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())),F₅(2,F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()))))] by A1, A9, XREAL_1:234 ;
A11: for n being Element of NAT holds g . (n + 4) = H₁(n + 3,g . (n + 3))

proof

let n be Element of NAT ; :: thesis:
A12: ( In (n + 3),NAT = n + 3 & In (n + 4),NAT = n + 4 & In n,NAT = n & In (n + 1),NAT = n + 1 ) by FUNCT_7:def 1;
0 + 2 < n + 3 by NAT_1:2, XREAL_1:10;
then A13: g . (n + 3) = H₆(n + 3) by A5, A12
.= h . n by A12, NAT_D:34 ;
A14: (n + 4) - 3 = n + (4 - 3) ;
A15: 0 <= n + 1 by NAT_1:2;
0 + 2 < n + 4 by NAT_1:2, XREAL_1:10;
hence g . (n + 4) = H₆(n + 4) by A5, A12
.= h . (n + 1) by A12, A14, A15, XREAL_0:def 2
.= H₁(n + 3,g . (n + 3)) by A2, A13 ;
:: thesis:

end;

deffunc H₇( Element of NAT ) -> set = (g . $1) `1_5 ;
consider f being Function such that
A16: dom f = NAT and
A17: for x being Element of NAT holds f . x = H₇(x) from FUNCT_1:sch 4();
take f ; :: thesis:
thus dom f = NAT by A16; :: thesis:
thus A18: f . 0 = (g . 0 ) `1_5 by A17
.= F₁() by A6, Def8 ; :: thesis:
thus A19: f . 1 = (g . 1) `1_5 by A17
.= F₂() by A7, Def8 ; :: thesis:
thus A20: f . 2 = (g . 2) `1_5 by A17
.= F₃() by A8, Def8 ; :: thesis:
thus A21: f . 3 = (g . 3) `1_5 by A17
.= F₄() by A10, Def8 ; :: thesis:
defpred S₅[ Element of NAT ] means ( f . ($1 + 4) = (g . ($1 + 3)) `2_5 & (g . $1) `2_5 = (g . ($1 + 1)) `1_5 & (g . $1) `3_5 = (g . ($1 + 1)) `2_5 & (g . $1) `4_5 = (g . ($1 + 1)) `3_5 & (g . $1) `5_5 = (g . ($1 + 1)) `4_5 & (g . ($1 + 1)) `2_5 = (g . ($1 + 2)) `1_5 & (g . ($1 + 1)) `3_5 = (g . ($1 + 2)) `2_5 & (g . ($1 + 1)) `4_5 = (g . ($1 + 2)) `3_5 & (g . ($1 + 1)) `5_5 = (g . ($1 + 2)) `4_5 & (g . ($1 + 2)) `2_5 = (g . ($1 + 3)) `1_5 & (g . ($1 + 2)) `3_5 = (g . ($1 + 3)) `2_5 & (g . ($1 + 2)) `4_5 = (g . ($1 + 3)) `3_5 & (g . ($1 + 2)) `5_5 = (g . ($1 + 3)) `4_5 & (g . ($1 + 3)) `2_5 = (g . ($1 + 4)) `1_5 & (g . ($1 + 3)) `3_5 = (g . ($1 + 4)) `2_5 & (g . ($1 + 3)) `4_5 = (g . ($1 + 4)) `3_5 & (g . ($1 + 3)) `5_5 = (g . ($1 + 4)) `4_5 & f . ($1 + 4) = F₅($1,(f . $1),(f . ($1 + 1)),(f . ($1 + 2)),(f . ($1 + 3))) );
A22: S₅[ 0 ]

proof

thus A23: f . (0 + 4) = (g . (0 + 4)) `1_5 by A17
.= H₁(0 + 3,g . (0 + 3)) `1_5 by A11
.= (g . (0 + 3)) `2_5 by Def8 ; :: thesis:
thus (g . (0 + 1)) `1_5 = F₂() by A7, Def8
.= (g . 0 ) `2_5 by A6, Def9 ; :: thesis:
thus (g . 0 ) `3_5 = F₃() by A6, Def10
.= (g . (0 + 1)) `2_5 by A7, Def9 ; :: thesis:
thus (g . 0 ) `4_5 = F₄() by A6, Def11
.= (g . (0 + 1)) `3_5 by A7, Def10 ; :: thesis:
thus (g . 0 ) `5_5 = F₅(0 ,F₁(),F₂(),F₃(),F₄()) by A6, Def12
.= (g . (0 + 1)) `4_5 by A7, Def11 ; :: thesis:
thus (g . (0 + 1)) `2_5 = F₃() by A7, Def9
.= (g . (0 + 2)) `1_5 by A8, Def8 ; :: thesis:
thus (g . (0 + 1)) `3_5 = F₄() by A7, Def10
.= (g . (0 + 2)) `2_5 by A8, Def9 ; :: thesis:
thus (g . (0 + 1)) `4_5 = F₅(0 ,F₁(),F₂(),F₃(),F₄()) by A7, Def11
.= (g . (0 + 2)) `3_5 by A8, Def10 ; :: thesis:
thus (g . (0 + 1)) `5_5 = F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())) by A7, Def12
.= (g . (0 + 2)) `4_5 by A8, Def11 ; :: thesis:
thus (g . (0 + 2)) `2_5 = F₄() by A8, Def9
.= (g . (0 + 3)) `1_5 by A10, Def8 ; :: thesis:
thus (g . (0 + 2)) `3_5 = F₅(0 ,F₁(),F₂(),F₃(),F₄()) by A8, Def10
.= (g . (0 + 3)) `2_5 by A10, Def9 ; :: thesis:
thus (g . (0 + 2)) `4_5 = F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())) by A8, Def11
.= (g . (0 + 3)) `3_5 by A10, Def10 ; :: thesis:
thus (g . (0 + 2)) `5_5 = F₅(2,F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()))) by A8, Def12
.= (g . (0 + 3)) `4_5 by A10, Def11 ; :: thesis:
thus (g . (0 + 3)) `2_5 = H₁(0 + 3,g . (0 + 3)) `1_5 by Def8
.= (g . (0 + 4)) `1_5 by A11 ; :: thesis:
thus (g . (0 + 3)) `3_5 = H₁(0 + 3,g . (0 + 3)) `2_5 by Def9
.= (g . (0 + 4)) `2_5 by A11 ; :: thesis:
thus (g . (0 + 3)) `4_5 = H₁(0 + 3,g . (0 + 3)) `3_5 by Def10
.= (g . (0 + 4)) `3_5 by A11 ; :: thesis:
thus (g . (0 + 3)) `5_5 = H₁(0 + 3,g . (0 + 3)) `4_5 by Def11
.= (g . (0 + 4)) `4_5 by A11 ; :: thesis:
thus f . (0 + 4) = F₅(0 ,(f . 0 ),(f . (0 + 1)),(f . (0 + 2)),(f . (0 + 3))) by A10, A18, A19, A20, A21, A23, Def9; :: thesis:

end;

A24: for x being Element of NAT st S₅[x] holds
S₅[x + 1]

proof

let x be Element of NAT ; :: thesis:
assume A25: S₅[x] ; :: thesis:
thus A26: f . ((x + 1) + 4) = (g . ((x + 1) + 4)) `1_5 by A17
.= H₁((x + 1) + 3,g . ((x + 1) + 3)) `1_5 by A11
.= (g . ((x + 1) + 3)) `2_5 by Def8 ; :: thesis:
thus (g . ((x + 1) + 1)) `1_5 = (g . (x + 1)) `2_5 by A25; :: thesis:
thus (g . (x + 1)) `3_5 = (g . ((x + 1) + 1)) `2_5 by A25; :: thesis:
thus (g . (x + 1)) `4_5 = (g . ((x + 1) + 1)) `3_5 by A25; :: thesis:
thus (g . (x + 1)) `5_5 = (g . ((x + 1) + 1)) `4_5 by A25; :: thesis:
thus (g . ((x + 1) + 1)) `2_5 = (g . ((x + 1) + 2)) `1_5 by A25; :: thesis:
thus (g . ((x + 1) + 1)) `3_5 = (g . ((x + 1) + 2)) `2_5 by A25; :: thesis:
thus (g . ((x + 1) + 1)) `4_5 = (g . ((x + 1) + 2)) `3_5 by A25; :: thesis:
thus (g . ((x + 1) + 1)) `5_5 = (g . ((x + 1) + 2)) `4_5 by A25; :: thesis:
thus (g . ((x + 1) + 2)) `2_5 = (g . ((x + 1) + 3)) `1_5 by A25; :: thesis:
A27: f . ((x + 1) + 1) = (g . x) `3_5 by A17, A25;
A28: f . ((x + 1) + 2) = (g . x) `4_5 by A17, A25;
thus (g . ((x + 1) + 2)) `3_5 = (g . ((x + 1) + 3)) `2_5 by A25; :: thesis:
thus (g . ((x + 1) + 2)) `4_5 = (g . ((x + 1) + 3)) `3_5 by A25; :: thesis:
thus (g . ((x + 1) + 2)) `5_5 = (g . ((x + 1) + 3)) `4_5 by A25; :: thesis:
thus (g . ((x + 1) + 3)) `2_5 = H₁((x + 1) + 3,g . ((x + 1) + 3)) `1_5 by Def8
.= (g . ((x + 1) + 4)) `1_5 by A11 ; :: thesis:
thus (g . ((x + 1) + 3)) `3_5 = H₁((x + 1) + 3,g . ((x + 1) + 3)) `2_5 by Def9
.= (g . ((x + 1) + 4)) `2_5 by A11 ; :: thesis:
thus (g . ((x + 1) + 3)) `4_5 = H₁((x + 1) + 3,g . ((x + 1) + 3)) `3_5 by Def10
.= (g . ((x + 1) + 4)) `3_5 by A11 ; :: thesis:
thus (g . ((x + 1) + 3)) `5_5 = H₁((x + 1) + 3,g . ((x + 1) + 3)) `4_5 by Def11
.= (g . ((x + 1) + 4)) `4_5 by A11 ; :: thesis:

per cases ;

suppose A29: x <= 2 ; :: thesis:

thus f . ((x + 1) + 4) = F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) :: thesis:

proof

per cases by A29, NAT_1:27;

suppose A30: x = 0 ; :: thesis:

hence f . ((x + 1) + 4) = (g . (1 + 4)) `1_5 by A17
.= H₁(1 + 3,g . (1 + 3)) `1_5 by A11
.= (g . (0 + 4)) `2_5 by Def8
.= H₁(0 + 3,g . (0 + 3)) `2_5 by A11
.= (g . (0 + 3)) `3_5 by Def9
.= F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())) by A10, Def10
.= F₅((0 + 1),F₂(),F₃(),F₄(),((g . 0 ) `5_5 )) by A6, Def12
.= F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) by A6, A19, A20, A25, A28, A30, Def11 ;
:: thesis:

end;

suppose A31: x = 1 ; :: thesis:

then A32: f . ((x + 1) + 1) = F₄() by A7, A27, Def10;
A33: f . ((x + 1) + 2) = F₅(0 ,F₁(),F₂(),F₃(),F₄()) by A7, A28, A31, Def11;
A34: f . ((x + 1) + 3) = F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())) by A7, A25, A31, Def12;
thus f . ((x + 1) + 4) = (g . ((1 + 1) + 4)) `1_5 by A17, A31
.= H₁(2 + 3,g . (2 + 3)) `1_5 by A11
.= (g . (1 + 4)) `2_5 by Def8
.= H₁(1 + 3,g . (1 + 3)) `2_5 by A11
.= (g . (0 + 4)) `3_5 by Def9
.= H₁(0 + 3,g . (0 + 3)) `3_5 by A11
.= (g . (0 + 3)) `4_5 by Def10
.= F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) by A10, A20, A31, A32, A33, A34, Def11 ; :: thesis:

end;

suppose A35: x = 2 ; :: thesis:

then A36: f . ((x + 1) + 1) = F₅(0 ,F₁(),F₂(),F₃(),F₄()) by A8, A27, Def10;
A37: f . ((x + 1) + 2) = F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())) by A8, A28, A35, Def11;
A38: f . ((x + 1) + 3) = F₅(2,F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()))) by A8, A25, A35, Def12;
thus f . ((x + 1) + 4) = (g . ((2 + 1) + 4)) `1_5 by A17, A35
.= H₁(3 + 3,g . (3 + 3)) `1_5 by A11
.= (g . (2 + 4)) `2_5 by Def8
.= H₁(2 + 3,g . (2 + 3)) `2_5 by A11
.= (g . (1 + 4)) `3_5 by Def9
.= H₁(1 + 3,g . (1 + 3)) `3_5 by A11
.= (g . (0 + 4)) `4_5 by Def10
.= H₁(0 + 3,g . (0 + 3)) `4_5 by A11
.= (g . (0 + 3)) `5_5 by Def11
.= F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) by A10, A21, A35, A36, A37, A38, Def12 ; :: thesis:

end;

suppose A39: 2 < x ; :: thesis:

then A40: 1 + 2 <= x by NAT_1:13;
then 3 - 3 <= x - 3 by XREAL_1:15;
then A41: x - 3 = x -' 3 by XREAL_0:def 2;
A42: 2 - 2 <= x - 2 by A39, XREAL_1:15;
then A43: x - 2 = x -' 2 by XREAL_0:def 2;
1 < x by A39, XXREAL_0:2;
then 1 - 1 <= x - 1 by XREAL_1:15;
then A44: x - 1 = x -' 1 by XREAL_0:def 2;
A45: (x -' 3) + 3 = x by A40, XREAL_1:237;
A46: x + 2 = (x - 1) + 3 ;
A47: (x -' 2) + 3 = (x - 2) + 3 by A42, XREAL_0:def 2
.= x + 1 ;
thus f . ((x + 1) + 4) = (g . (x + (1 + 3))) `2_5 by A26
.= H₁(x + 3,g . (x + 3)) `2_5 by A11
.= (g . ((x -' 1) + 4)) `3_5 by A44, Def9
.= H₁(x + 2,g . (x + 2)) `3_5 by A11, A44, A46
.= (g . ((x -' 2) + 4)) `4_5 by A43, Def10
.= H₁(x + 1,g . (x + 1)) `4_5 by A11, A47
.= (g . ((x -' 3) + 4)) `5_5 by A41, Def11
.= H₁((x -' 3) + 3,g . ((x -' 3) + 3)) `5_5 by A11
.= F₅((x + 1),((g . x) `2_5 ),((g . x) `3_5 ),((g . x) `4_5 ),((g . x) `5_5 )) by A45, Def12
.= F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) by A17, A25, A27, A28 ; :: thesis:

end;

for x being Element of NAT holds S₅[x] from NAT_1:sch 1(A22, A24);
hence for n being Element of NAT holds f . (n + 4) = F₅(n,(f . n),(f . (n + 1)),(f . (n + 2)),(f . (n + 3))) ; :: thesis: