defpred S₁[ set ] means In $1,NAT > 2;
defpred S₂[ set ] means $1 = 2;
defpred S₃[ set ] means $1 = 1;
defpred S₄[ set ] means $1 = 0 ;
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 ))];
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₂( 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();
deffunc H₃( set ) -> set = h . ((In $1,NAT ) -' 3);
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 = [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₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())];
A3: 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: ( not c in NAT or S₄[c] or S₃[c] or S₂[c] or S₁[c] )
assume c in NAT ; :: thesis: ( S₄[c] or S₃[c] or S₂[c] or S₁[c] )
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: verum

end;

A4: 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: ( c in NAT implies ( ( 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] ) ) )
assume c in NAT ; :: thesis: ( ( 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] ) )
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: verum

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(A4, A3);
A6: In 3,NAT = 3 by FUNCT_7:def 1;
then A7: 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, A6, XREAL_1:234 ;
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;
then A9: (g . (0 + 2)) `3_5 = F<sub>5</sub>(0 ,F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>()) by Def10
.= (g . (0 + 3)) `2_5 by A7, Def9 ;
A10: g . 1 = [F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()),F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄()))] by A5;
then A11: (g . (0 + 1)) `2_5 = F<sub>3</sub>() by Def9
.= (g . (0 + 2)) `1_5 by A8, Def8 ;
A12: g . 0 = [F₁(),F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())] by A5;
then A13: (g . 0 ) `3_5 = F<sub>3</sub>() by Def10
.= (g . (0 + 1)) `2_5 by A10, Def9 ;
A14: (g . (0 + 2)) `5_5 = F<sub>5</sub>(2,F<sub>3</sub>(),F<sub>4</sub>(),F<sub>5</sub>(0 ,F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>()),F<sub>5</sub>(1,F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>(),F<sub>5</sub>(0 ,F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>()))) by A8, Def12
.= (g . (0 + 3)) `4_5 by A7, Def11 ;
A15: (g . (0 + 2)) `4_5 = F<sub>5</sub>(1,F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>(),F<sub>5</sub>(0 ,F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>())) by A8, Def11
.= (g . (0 + 3)) `3_5 by A7, Def10 ;
A16: (g . (0 + 1)) `4_5 = F<sub>5</sub>(0 ,F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>()) by A10, Def11
.= (g . (0 + 2)) `3_5 by A8, Def10 ;
A17: (g . (0 + 1)) `3_5 = F<sub>4</sub>() by A10, Def10
.= (g . (0 + 2)) `2_5 by A8, Def9 ;
A18: (g . (0 + 1)) `5_5 = F<sub>5</sub>(1,F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>(),F<sub>5</sub>(0 ,F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>())) by A10, Def12
.= (g . (0 + 2)) `4_5 by A8, Def11 ;
A19: (g . 0 ) `5_5 = F<sub>5</sub>(0 ,F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>()) by A12, Def12
.= (g . (0 + 1)) `4_5 by A10, Def11 ;
A20: (g . 0 ) `4_5 = F<sub>4</sub>() by A12, Def11
.= (g . (0 + 1)) `3_5 by A10, Def10 ;
A21: (g . (0 + 1)) `1_5 = F<sub>2</sub>() by A10, Def8
.= (g . 0 ) `2_5 by A12, Def9 ;
A22: for n being Element of NAT holds g . (n + 4) = H₁(n + 3,g . (n + 3))

proof

let n be Element of NAT ; :: thesis: g . (n + 4) = H₁(n + 3,g . (n + 3))
A23: In (n + 3),NAT = n + 3 by FUNCT_7:def 1;
0 + 2 < n + 3 by NAT_1:2, XREAL_1:10;
then A24: g . (n + 3) = H₃(n + 3) by A5, A23
.= h . n by A23, NAT_D:34 ;
A25: In (n + 4),NAT = n + 4 by FUNCT_7:def 1;
A26: ( (n + 4) - 3 = n + (4 - 3) & 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, A25
.= h . (n + 1) by A25, A26, XREAL_0:def 2
.= H₁(n + 3,g . (n + 3)) by A2, A24 ;
:: thesis: verum

end;

deffunc H₇( Element of NAT ) -> set = (g . $1) `1_5 ;
consider f being Function such that
A27: dom f = NAT and
A28: for x being Element of NAT holds f . x = H<sub>7</sub>(x) from FUNCT_1:sch 4();
A29: f . (0 + 4) = (g . (0 + 4)) `1_5 by A28
.= H₁(0 + 3,g . (0 + 3)) `1_5 by A22
.= (g . (0 + 3)) `2_5 by Def8 ;
take f ; :: thesis: ( dom f = NAT & f . 0 = F₁() & f . 1 = F₂() & f . 2 = F₃() & f . 3 = F₄() & ( for n being Element of NAT holds f . (n + 4) = F₅(n,(f . n),(f . (n + 1)),(f . (n + 2)),(f . (n + 3))) ) )
thus dom f = NAT by A27; :: thesis: ( f . 0 = F₁() & f . 1 = F₂() & f . 2 = F₃() & f . 3 = F₄() & ( for n being Element of NAT holds f . (n + 4) = F₅(n,(f . n),(f . (n + 1)),(f . (n + 2)),(f . (n + 3))) ) )
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<sub>5</sub>($1,(f . $1),(f . ($1 + 1)),(f . ($1 + 2)),(f . ($1 + 3))) );
A30: (g . (0 + 3)) `2_5 = H₁(0 + 3,g . (0 + 3)) `1_5 by Def8
.= (g . (0 + 4)) `1_5 by A22 ;
thus A31: f . 0 = (g . 0 ) `1_5 by A28
.= F<sub>1</sub>() by A12, Def8 ; :: thesis: ( f . 1 = F<sub>2</sub>() & f . 2 = F<sub>3</sub>() & f . 3 = F<sub>4</sub>() & ( for n being Element of NAT holds f . (n + 4) = F<sub>5</sub>(n,(f . n),(f . (n + 1)),(f . (n + 2)),(f . (n + 3))) ) )
thus A32: f . 1 = (g . 1) `1_5 by A28
.= F₂() by A10, Def8 ; :: thesis: ( f . 2 = F₃() & f . 3 = F₄() & ( for n being Element of NAT holds f . (n + 4) = F₅(n,(f . n),(f . (n + 1)),(f . (n + 2)),(f . (n + 3))) ) )
thus A33: f . 2 = (g . 2) `1_5 by A28
.= F<sub>3</sub>() by A8, Def8 ; :: thesis: ( f . 3 = F<sub>4</sub>() & ( for n being Element of NAT holds f . (n + 4) = F<sub>5</sub>(n,(f . n),(f . (n + 1)),(f . (n + 2)),(f . (n + 3))) ) )
thus A34: f . 3 = (g . 3) `1_5 by A28
.= F₄() by A7, Def8 ; :: thesis: for n being Element of NAT holds f . (n + 4) = F₅(n,(f . n),(f . (n + 1)),(f . (n + 2)),(f . (n + 3)))
A35: for x being Element of NAT st S₅[x] holds
S₅[x + 1]

proof

let x be Element of NAT ; :: thesis: ( S₅[x] implies S₅[x + 1] )
assume A36: S₅[x] ; :: thesis: S₅[x + 1]
then A37: f . ((x + 1) + 1) = (g . x) `3_5 by A28;
thus A38: f . ((x + 1) + 4) = (g . ((x + 1) + 4)) `1_5 by A28
.= H₁((x + 1) + 3,g . ((x + 1) + 3)) `1_5 by A22
.= (g . ((x + 1) + 3)) `2_5 by Def8 ; :: thesis: ( (g . (x + 1)) `2_5 = (g . ((x + 1) + 1)) `1_5 & (g . (x + 1)) `3_5 = (g . ((x + 1) + 1)) `2_5 & (g . (x + 1)) `4_5 = (g . ((x + 1) + 1)) `3_5 & (g . (x + 1)) `5_5 = (g . ((x + 1) + 1)) `4_5 & (g . ((x + 1) + 1)) `2_5 = (g . ((x + 1) + 2)) `1_5 & (g . ((x + 1) + 1)) `3_5 = (g . ((x + 1) + 2)) `2_5 & (g . ((x + 1) + 1)) `4_5 = (g . ((x + 1) + 2)) `3_5 & (g . ((x + 1) + 1)) `5_5 = (g . ((x + 1) + 2)) `4_5 & (g . ((x + 1) + 2)) `2_5 = (g . ((x + 1) + 3)) `1_5 & (g . ((x + 1) + 2)) `3_5 = (g . ((x + 1) + 3)) `2_5 & (g . ((x + 1) + 2)) `4_5 = (g . ((x + 1) + 3)) `3_5 & (g . ((x + 1) + 2)) `5_5 = (g . ((x + 1) + 3)) `4_5 & (g . ((x + 1) + 3)) `2_5 = (g . ((x + 1) + 4)) `1_5 & (g . ((x + 1) + 3)) `3_5 = (g . ((x + 1) + 4)) `2_5 & (g . ((x + 1) + 3)) `4_5 = (g . ((x + 1) + 4)) `3_5 & (g . ((x + 1) + 3)) `5_5 = (g . ((x + 1) + 4)) `4_5 & f . ((x + 1) + 4) = F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) )
thus (g . ((x + 1) + 1)) `1_5 = (g . (x + 1)) `2_5 by A36; :: thesis: ( (g . (x + 1)) `3_5 = (g . ((x + 1) + 1)) `2_5 & (g . (x + 1)) `4_5 = (g . ((x + 1) + 1)) `3_5 & (g . (x + 1)) `5_5 = (g . ((x + 1) + 1)) `4_5 & (g . ((x + 1) + 1)) `2_5 = (g . ((x + 1) + 2)) `1_5 & (g . ((x + 1) + 1)) `3_5 = (g . ((x + 1) + 2)) `2_5 & (g . ((x + 1) + 1)) `4_5 = (g . ((x + 1) + 2)) `3_5 & (g . ((x + 1) + 1)) `5_5 = (g . ((x + 1) + 2)) `4_5 & (g . ((x + 1) + 2)) `2_5 = (g . ((x + 1) + 3)) `1_5 & (g . ((x + 1) + 2)) `3_5 = (g . ((x + 1) + 3)) `2_5 & (g . ((x + 1) + 2)) `4_5 = (g . ((x + 1) + 3)) `3_5 & (g . ((x + 1) + 2)) `5_5 = (g . ((x + 1) + 3)) `4_5 & (g . ((x + 1) + 3)) `2_5 = (g . ((x + 1) + 4)) `1_5 & (g . ((x + 1) + 3)) `3_5 = (g . ((x + 1) + 4)) `2_5 & (g . ((x + 1) + 3)) `4_5 = (g . ((x + 1) + 4)) `3_5 & (g . ((x + 1) + 3)) `5_5 = (g . ((x + 1) + 4)) `4_5 & f . ((x + 1) + 4) = F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) )
thus (g . (x + 1)) `3_5 = (g . ((x + 1) + 1)) `2_5 by A36; :: thesis: ( (g . (x + 1)) `4_5 = (g . ((x + 1) + 1)) `3_5 & (g . (x + 1)) `5_5 = (g . ((x + 1) + 1)) `4_5 & (g . ((x + 1) + 1)) `2_5 = (g . ((x + 1) + 2)) `1_5 & (g . ((x + 1) + 1)) `3_5 = (g . ((x + 1) + 2)) `2_5 & (g . ((x + 1) + 1)) `4_5 = (g . ((x + 1) + 2)) `3_5 & (g . ((x + 1) + 1)) `5_5 = (g . ((x + 1) + 2)) `4_5 & (g . ((x + 1) + 2)) `2_5 = (g . ((x + 1) + 3)) `1_5 & (g . ((x + 1) + 2)) `3_5 = (g . ((x + 1) + 3)) `2_5 & (g . ((x + 1) + 2)) `4_5 = (g . ((x + 1) + 3)) `3_5 & (g . ((x + 1) + 2)) `5_5 = (g . ((x + 1) + 3)) `4_5 & (g . ((x + 1) + 3)) `2_5 = (g . ((x + 1) + 4)) `1_5 & (g . ((x + 1) + 3)) `3_5 = (g . ((x + 1) + 4)) `2_5 & (g . ((x + 1) + 3)) `4_5 = (g . ((x + 1) + 4)) `3_5 & (g . ((x + 1) + 3)) `5_5 = (g . ((x + 1) + 4)) `4_5 & f . ((x + 1) + 4) = F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) )
thus (g . (x + 1)) `4_5 = (g . ((x + 1) + 1)) `3_5 by A36; :: thesis: ( (g . (x + 1)) `5_5 = (g . ((x + 1) + 1)) `4_5 & (g . ((x + 1) + 1)) `2_5 = (g . ((x + 1) + 2)) `1_5 & (g . ((x + 1) + 1)) `3_5 = (g . ((x + 1) + 2)) `2_5 & (g . ((x + 1) + 1)) `4_5 = (g . ((x + 1) + 2)) `3_5 & (g . ((x + 1) + 1)) `5_5 = (g . ((x + 1) + 2)) `4_5 & (g . ((x + 1) + 2)) `2_5 = (g . ((x + 1) + 3)) `1_5 & (g . ((x + 1) + 2)) `3_5 = (g . ((x + 1) + 3)) `2_5 & (g . ((x + 1) + 2)) `4_5 = (g . ((x + 1) + 3)) `3_5 & (g . ((x + 1) + 2)) `5_5 = (g . ((x + 1) + 3)) `4_5 & (g . ((x + 1) + 3)) `2_5 = (g . ((x + 1) + 4)) `1_5 & (g . ((x + 1) + 3)) `3_5 = (g . ((x + 1) + 4)) `2_5 & (g . ((x + 1) + 3)) `4_5 = (g . ((x + 1) + 4)) `3_5 & (g . ((x + 1) + 3)) `5_5 = (g . ((x + 1) + 4)) `4_5 & f . ((x + 1) + 4) = F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) )
thus (g . (x + 1)) `5_5 = (g . ((x + 1) + 1)) `4_5 by A36; :: thesis: ( (g . ((x + 1) + 1)) `2_5 = (g . ((x + 1) + 2)) `1_5 & (g . ((x + 1) + 1)) `3_5 = (g . ((x + 1) + 2)) `2_5 & (g . ((x + 1) + 1)) `4_5 = (g . ((x + 1) + 2)) `3_5 & (g . ((x + 1) + 1)) `5_5 = (g . ((x + 1) + 2)) `4_5 & (g . ((x + 1) + 2)) `2_5 = (g . ((x + 1) + 3)) `1_5 & (g . ((x + 1) + 2)) `3_5 = (g . ((x + 1) + 3)) `2_5 & (g . ((x + 1) + 2)) `4_5 = (g . ((x + 1) + 3)) `3_5 & (g . ((x + 1) + 2)) `5_5 = (g . ((x + 1) + 3)) `4_5 & (g . ((x + 1) + 3)) `2_5 = (g . ((x + 1) + 4)) `1_5 & (g . ((x + 1) + 3)) `3_5 = (g . ((x + 1) + 4)) `2_5 & (g . ((x + 1) + 3)) `4_5 = (g . ((x + 1) + 4)) `3_5 & (g . ((x + 1) + 3)) `5_5 = (g . ((x + 1) + 4)) `4_5 & f . ((x + 1) + 4) = F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) )
thus (g . ((x + 1) + 1)) `2_5 = (g . ((x + 1) + 2)) `1_5 by A36; :: thesis: ( (g . ((x + 1) + 1)) `3_5 = (g . ((x + 1) + 2)) `2_5 & (g . ((x + 1) + 1)) `4_5 = (g . ((x + 1) + 2)) `3_5 & (g . ((x + 1) + 1)) `5_5 = (g . ((x + 1) + 2)) `4_5 & (g . ((x + 1) + 2)) `2_5 = (g . ((x + 1) + 3)) `1_5 & (g . ((x + 1) + 2)) `3_5 = (g . ((x + 1) + 3)) `2_5 & (g . ((x + 1) + 2)) `4_5 = (g . ((x + 1) + 3)) `3_5 & (g . ((x + 1) + 2)) `5_5 = (g . ((x + 1) + 3)) `4_5 & (g . ((x + 1) + 3)) `2_5 = (g . ((x + 1) + 4)) `1_5 & (g . ((x + 1) + 3)) `3_5 = (g . ((x + 1) + 4)) `2_5 & (g . ((x + 1) + 3)) `4_5 = (g . ((x + 1) + 4)) `3_5 & (g . ((x + 1) + 3)) `5_5 = (g . ((x + 1) + 4)) `4_5 & f . ((x + 1) + 4) = F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) )
thus (g . ((x + 1) + 1)) `3_5 = (g . ((x + 1) + 2)) `2_5 by A36; :: thesis: ( (g . ((x + 1) + 1)) `4_5 = (g . ((x + 1) + 2)) `3_5 & (g . ((x + 1) + 1)) `5_5 = (g . ((x + 1) + 2)) `4_5 & (g . ((x + 1) + 2)) `2_5 = (g . ((x + 1) + 3)) `1_5 & (g . ((x + 1) + 2)) `3_5 = (g . ((x + 1) + 3)) `2_5 & (g . ((x + 1) + 2)) `4_5 = (g . ((x + 1) + 3)) `3_5 & (g . ((x + 1) + 2)) `5_5 = (g . ((x + 1) + 3)) `4_5 & (g . ((x + 1) + 3)) `2_5 = (g . ((x + 1) + 4)) `1_5 & (g . ((x + 1) + 3)) `3_5 = (g . ((x + 1) + 4)) `2_5 & (g . ((x + 1) + 3)) `4_5 = (g . ((x + 1) + 4)) `3_5 & (g . ((x + 1) + 3)) `5_5 = (g . ((x + 1) + 4)) `4_5 & f . ((x + 1) + 4) = F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) )
thus (g . ((x + 1) + 1)) `4_5 = (g . ((x + 1) + 2)) `3_5 by A36; :: thesis: ( (g . ((x + 1) + 1)) `5_5 = (g . ((x + 1) + 2)) `4_5 & (g . ((x + 1) + 2)) `2_5 = (g . ((x + 1) + 3)) `1_5 & (g . ((x + 1) + 2)) `3_5 = (g . ((x + 1) + 3)) `2_5 & (g . ((x + 1) + 2)) `4_5 = (g . ((x + 1) + 3)) `3_5 & (g . ((x + 1) + 2)) `5_5 = (g . ((x + 1) + 3)) `4_5 & (g . ((x + 1) + 3)) `2_5 = (g . ((x + 1) + 4)) `1_5 & (g . ((x + 1) + 3)) `3_5 = (g . ((x + 1) + 4)) `2_5 & (g . ((x + 1) + 3)) `4_5 = (g . ((x + 1) + 4)) `3_5 & (g . ((x + 1) + 3)) `5_5 = (g . ((x + 1) + 4)) `4_5 & f . ((x + 1) + 4) = F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) )
thus (g . ((x + 1) + 1)) `5_5 = (g . ((x + 1) + 2)) `4_5 by A36; :: thesis: ( (g . ((x + 1) + 2)) `2_5 = (g . ((x + 1) + 3)) `1_5 & (g . ((x + 1) + 2)) `3_5 = (g . ((x + 1) + 3)) `2_5 & (g . ((x + 1) + 2)) `4_5 = (g . ((x + 1) + 3)) `3_5 & (g . ((x + 1) + 2)) `5_5 = (g . ((x + 1) + 3)) `4_5 & (g . ((x + 1) + 3)) `2_5 = (g . ((x + 1) + 4)) `1_5 & (g . ((x + 1) + 3)) `3_5 = (g . ((x + 1) + 4)) `2_5 & (g . ((x + 1) + 3)) `4_5 = (g . ((x + 1) + 4)) `3_5 & (g . ((x + 1) + 3)) `5_5 = (g . ((x + 1) + 4)) `4_5 & f . ((x + 1) + 4) = F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) )
thus (g . ((x + 1) + 2)) `2_5 = (g . ((x + 1) + 3)) `1_5 by A36; :: thesis: ( (g . ((x + 1) + 2)) `3_5 = (g . ((x + 1) + 3)) `2_5 & (g . ((x + 1) + 2)) `4_5 = (g . ((x + 1) + 3)) `3_5 & (g . ((x + 1) + 2)) `5_5 = (g . ((x + 1) + 3)) `4_5 & (g . ((x + 1) + 3)) `2_5 = (g . ((x + 1) + 4)) `1_5 & (g . ((x + 1) + 3)) `3_5 = (g . ((x + 1) + 4)) `2_5 & (g . ((x + 1) + 3)) `4_5 = (g . ((x + 1) + 4)) `3_5 & (g . ((x + 1) + 3)) `5_5 = (g . ((x + 1) + 4)) `4_5 & f . ((x + 1) + 4) = F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) )
thus (g . ((x + 1) + 2)) `3_5 = (g . ((x + 1) + 3)) `2_5 by A36; :: thesis: ( (g . ((x + 1) + 2)) `4_5 = (g . ((x + 1) + 3)) `3_5 & (g . ((x + 1) + 2)) `5_5 = (g . ((x + 1) + 3)) `4_5 & (g . ((x + 1) + 3)) `2_5 = (g . ((x + 1) + 4)) `1_5 & (g . ((x + 1) + 3)) `3_5 = (g . ((x + 1) + 4)) `2_5 & (g . ((x + 1) + 3)) `4_5 = (g . ((x + 1) + 4)) `3_5 & (g . ((x + 1) + 3)) `5_5 = (g . ((x + 1) + 4)) `4_5 & f . ((x + 1) + 4) = F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) )
thus (g . ((x + 1) + 2)) `4_5 = (g . ((x + 1) + 3)) `3_5 by A36; :: thesis: ( (g . ((x + 1) + 2)) `5_5 = (g . ((x + 1) + 3)) `4_5 & (g . ((x + 1) + 3)) `2_5 = (g . ((x + 1) + 4)) `1_5 & (g . ((x + 1) + 3)) `3_5 = (g . ((x + 1) + 4)) `2_5 & (g . ((x + 1) + 3)) `4_5 = (g . ((x + 1) + 4)) `3_5 & (g . ((x + 1) + 3)) `5_5 = (g . ((x + 1) + 4)) `4_5 & f . ((x + 1) + 4) = F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) )
thus (g . ((x + 1) + 2)) `5_5 = (g . ((x + 1) + 3)) `4_5 by A36; :: thesis: ( (g . ((x + 1) + 3)) `2_5 = (g . ((x + 1) + 4)) `1_5 & (g . ((x + 1) + 3)) `3_5 = (g . ((x + 1) + 4)) `2_5 & (g . ((x + 1) + 3)) `4_5 = (g . ((x + 1) + 4)) `3_5 & (g . ((x + 1) + 3)) `5_5 = (g . ((x + 1) + 4)) `4_5 & f . ((x + 1) + 4) = F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) )
thus (g . ((x + 1) + 3)) `2_5 = H<sub>1</sub>((x + 1) + 3,g . ((x + 1) + 3)) `1_5 by Def8
.= (g . ((x + 1) + 4)) `1_5 by A22 ; :: thesis: ( (g . ((x + 1) + 3)) `3_5 = (g . ((x + 1) + 4)) `2_5 & (g . ((x + 1) + 3)) `4_5 = (g . ((x + 1) + 4)) `3_5 & (g . ((x + 1) + 3)) `5_5 = (g . ((x + 1) + 4)) `4_5 & f . ((x + 1) + 4) = F<sub>5</sub>((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) )
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 A22 ; :: thesis: ( (g . ((x + 1) + 3)) `4_5 = (g . ((x + 1) + 4)) `3_5 & (g . ((x + 1) + 3)) `5_5 = (g . ((x + 1) + 4)) `4_5 & f . ((x + 1) + 4) = F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) )
thus (g . ((x + 1) + 3)) `4_5 = H<sub>1</sub>((x + 1) + 3,g . ((x + 1) + 3)) `3_5 by Def10
.= (g . ((x + 1) + 4)) `3_5 by A22 ; :: thesis: ( (g . ((x + 1) + 3)) `5_5 = (g . ((x + 1) + 4)) `4_5 & f . ((x + 1) + 4) = F<sub>5</sub>((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) )
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 A22 ; :: thesis: f . ((x + 1) + 4) = F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3)))
A39: f . ((x + 1) + 2) = (g . x) `4_5 by A28, A36;

per cases ( x <= 2 or 2 < x ) ;

suppose A40: x <= 2 ; :: thesis: f . ((x + 1) + 4) = F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3)))

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

proof

per cases ( x = 0 or x = 1 or x = 2 ) by A40, NAT_1:27;

suppose A41: x = 0 ; :: thesis: f . ((x + 1) + 4) = F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3)))

hence f . ((x + 1) + 4) = (g . (1 + 4)) `1_5 by A28
.= H<sub>1</sub>(1 + 3,g . (1 + 3)) `1_5 by A22
.= (g . (0 + 4)) `2_5 by Def8
.= H<sub>1</sub>(0 + 3,g . (0 + 3)) `2_5 by A22
.= (g . (0 + 3)) `3_5 by Def9
.= F<sub>5</sub>(1,F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>(),F<sub>5</sub>(0 ,F<sub>1</sub>(),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>())) by A7, Def10
.= F<sub>5</sub>((0 + 1),F<sub>2</sub>(),F<sub>3</sub>(),F<sub>4</sub>(),((g . 0 ) `5_5 )) by A12, Def12
.= F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) by A12, A32, A33, A36, A39, A41, Def11 ;
:: thesis: verum

end;

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

then A43: f . ((x + 1) + 3) = F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())) by A10, A36, Def12;
A44: ( f . ((x + 1) + 1) = F₄() & f . ((x + 1) + 2) = F₅(0 ,F₁(),F₂(),F₃(),F₄()) ) by A10, A37, A39, A42, Def10, Def11;
thus f . ((x + 1) + 4) = (g . ((1 + 1) + 4)) `1_5 by A28, A42
.= H<sub>1</sub>(2 + 3,g . (2 + 3)) `1_5 by A22
.= (g . (1 + 4)) `2_5 by Def8
.= H<sub>1</sub>(1 + 3,g . (1 + 3)) `2_5 by A22
.= (g . (0 + 4)) `3_5 by Def9
.= H<sub>1</sub>(0 + 3,g . (0 + 3)) `3_5 by A22
.= (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 A7, A33, A42, A44, A43, Def11 ; :: thesis: verum

end;

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

then A46: 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, A36, Def12;
A47: ( f . ((x + 1) + 1) = F₅(0 ,F₁(),F₂(),F₃(),F₄()) & f . ((x + 1) + 2) = F₅(1,F₂(),F₃(),F₄(),F₅(0 ,F₁(),F₂(),F₃(),F₄())) ) by A8, A37, A39, A45, Def10, Def11;
thus f . ((x + 1) + 4) = (g . ((2 + 1) + 4)) `1_5 by A28, A45
.= H<sub>1</sub>(3 + 3,g . (3 + 3)) `1_5 by A22
.= (g . (2 + 4)) `2_5 by Def8
.= H<sub>1</sub>(2 + 3,g . (2 + 3)) `2_5 by A22
.= (g . (1 + 4)) `3_5 by Def9
.= H<sub>1</sub>(1 + 3,g . (1 + 3)) `3_5 by A22
.= (g . (0 + 4)) `4_5 by Def10
.= H<sub>1</sub>(0 + 3,g . (0 + 3)) `4_5 by A22
.= (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 A7, A34, A45, A47, A46, Def12 ; :: thesis: verum

end;

end;

end;

end;

suppose A48: 2 < x ; :: thesis: f . ((x + 1) + 4) = F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3)))

then 1 < x by XXREAL_0:2;
then 1 - 1 <= x - 1 by XREAL_1:15;
then A49: x - 1 = x -' 1 by XREAL_0:def 2;
A50: 2 - 2 <= x - 2 by A48, XREAL_1:15;
then A51: x - 2 = x -' 2 by XREAL_0:def 2;
A52: (x -' 2) + 3 = (x - 2) + 3 by A50, XREAL_0:def 2
.= x + 1 ;
A53: 1 + 2 <= x by A48, NAT_1:13;
then A54: (x -' 3) + 3 = x by XREAL_1:237;
3 - 3 <= x - 3 by A53, XREAL_1:15;
then A55: x - 3 = x -' 3 by XREAL_0:def 2;
A56: x + 2 = (x - 1) + 3 ;
thus f . ((x + 1) + 4) = (g . (x + (1 + 3))) `2_5 by A38
.= H<sub>1</sub>(x + 3,g . (x + 3)) `2_5 by A22
.= (g . ((x -' 1) + 4)) `3_5 by A49, Def9
.= H<sub>1</sub>(x + 2,g . (x + 2)) `3_5 by A22, A49, A56
.= (g . ((x -' 2) + 4)) `4_5 by A51, Def10
.= H<sub>1</sub>(x + 1,g . (x + 1)) `4_5 by A22, A52
.= (g . ((x -' 3) + 4)) `5_5 by A55, Def11
.= H<sub>1</sub>((x -' 3) + 3,g . ((x -' 3) + 3)) `5_5 by A22
.= F₅((x + 1),((g . x) `2_5 ),((g . x) `3_5 ),((g . x) `4_5 ),((g . x) `5_5 )) by A54, Def12
.= F₅((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)),(f . ((x + 1) + 3))) by A28, A36, A37, A39 ; :: thesis: verum

end;

end;

end;

A57: (g . (0 + 3)) `5_5 = H<sub>1</sub>(0 + 3,g . (0 + 3)) `4_5 by Def11
.= (g . (0 + 4)) `4_5 by A22 ;
A58: (g . (0 + 3)) `4_5 = H₁(0 + 3,g . (0 + 3)) `3_5 by Def10
.= (g . (0 + 4)) `3_5 by A22 ;
A59: (g . (0 + 3)) `3_5 = H<sub>1</sub>(0 + 3,g . (0 + 3)) `2_5 by Def9
.= (g . (0 + 4)) `2_5 by A22 ;
(g . (0 + 2)) `2_5 = F₄() by A8, Def9
.= (g . (0 + 3)) `1_5 by A7, Def8 ;
then A60: S₅[ 0 ] by A7, A31, A32, A33, A34, A29, A21, A13, A20, A19, A11, A17, A16, A18, A9, A15, A14, A30, A59, A58, A57, Def9;
for x being Element of NAT holds S₅[x] from NAT_1:sch 1(A60, A35);
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: verum