defpred S1[ set ] means In $1,NAT > 1;
defpred S2[ set ] means $1 = 1;
defpred S3[ set ] means $1 = 0 ;
deffunc H1( Nat, set ) -> set = [($2 `2_4 ),($2 `3_4 ),($2 `4_4 ),F4(($1 + 1),($2 `2_4 ),($2 `3_4 ),($2 `4_4 ))];
set r04 = F4(0 ,F1(),F2(),F3());
set r14 = F4(1,F2(),F3(),F4(0 ,F1(),F2(),F3()));
set r24 = F4(2,F3(),F4(0 ,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0 ,F1(),F2(),F3())));
deffunc H2( Nat, set ) -> set = H1($1 + 2,$2);
consider h being Function such that
dom h = NAT and
A1: h . 0 = [F3(),F4(0 ,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0 ,F1(),F2(),F3())),F4(2,F3(),F4(0 ,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0 ,F1(),F2(),F3())))] and
A2: for n being Nat holds h . (n + 1) = H2(n,h . n) from NAT_1:sch 11();
 deffunc H3( set ) -> set = h . ((In $1,NAT ) -' 2);
deffunc H4( set ) -> set = [F2(),F3(),F4(0 ,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0 ,F1(),F2(),F3()))];
deffunc H5( set ) -> set = [F1(),F2(),F3(),F4(0 ,F1(),F2(),F3())];
A3: for c being set holds
( not c in NAT or S3[c] or S2[c] or S1[c] )
proof
let c be set ; :: thesis: ( not c in NAT or S3[c] or S2[c] or S1[c] )
assume c in NAT ; :: thesis: ( S3[c] or S2[c] or S1[c] )
then In c,NAT = c by FUNCT_7:def 1;
hence ( S3[c] or S2[c] or S1[c] ) by NAT_1:26; :: thesis: verum
end;
A4: for c being set st c in NAT holds
( ( S3[c] implies not S2[c] ) & ( S3[c] implies not S1[c] ) & ( S2[c] implies not S1[c] ) )
proof
let c be set ; :: thesis: ( c in NAT implies ( ( S3[c] implies not S2[c] ) & ( S3[c] implies not S1[c] ) & ( S2[c] implies not S1[c] ) ) )
assume c in NAT ; :: thesis: ( ( S3[c] implies not S2[c] ) & ( S3[c] implies not S1[c] ) & ( S2[c] implies not S1[c] ) )
then In c,NAT = c by FUNCT_7:def 1;
hence ( ( S3[c] implies not S2[c] ) & ( S3[c] implies not S1[c] ) & ( S2[c] implies not S1[c] ) ) ; :: thesis: verum
end;
consider g being Function such that
dom g = NAT and
A5: for x being set st x in NAT holds
( ( S3[x] implies g . x = H5(x) ) & ( S2[x] implies g . x = H4(x) ) & ( S1[x] implies g . x = H3(x) ) ) from RECDEF_2:sch 1(A4, A3);
 A6: In 2,NAT = 2 by FUNCT_7:def 1;
then A7: g . 2 = H3(2) by A5
.= [F3(),F4(0 ,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0 ,F1(),F2(),F3())),F4(2,F3(),F4(0 ,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0 ,F1(),F2(),F3())))] by A1, A6, XREAL_1:234 ;
A8: for n being Element of NAT holds g . (n + 3) = H1(n + 2,g . (n + 2))
proof
let n be Element of NAT ; :: thesis: g . (n + 3) = H1(n + 2,g . (n + 2))
A9: In (n + 2),NAT = n + 2 by FUNCT_7:def 1;
0 + 1 < n + 2 by NAT_1:2, XREAL_1:10;
then A10: g . (n + 2) = H3(n + 2) by A5, A9
.= h . n by A9, NAT_D:34 ;
A11: In (n + 3),NAT = n + 3 by FUNCT_7:def 1;
A12: ( (n + 3) - 2 = n + (3 - 2) & 0 <= n + 1 ) by NAT_1:2;
0 + 1 < n + 3 by NAT_1:2, XREAL_1:10;
hence g . (n + 3) = H3(n + 3) by A5, A11
.= h . (n + 1) by A11, A12, XREAL_0:def 2
.= H1(n + 2,g . (n + 2)) by A2, A10 ;
:: thesis: verum
end;
A13: g . 1 = [F2(),F3(),F4(0 ,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0 ,F1(),F2(),F3()))] by A5;
then A14: (g . (0 + 1)) `3_4 = F4(0 ,F1(),F2(),F3()) by Def6
.= (g . (0 + 2)) `2_4 by A7, Def5 ;
A15: g . 0 = [F1(),F2(),F3(),F4(0 ,F1(),F2(),F3())] by A5;
then A16: (g . 0 ) `3_4 = F3() by Def6
.= (g . (0 + 1)) `2_4 by A13, Def5 ;
A17: (g . (0 + 1)) `4_4 = F4(1,F2(),F3(),F4(0 ,F1(),F2(),F3())) by A13, Def7
.= (g . (0 + 2)) `3_4 by A7, Def6 ;
A18: (g . 0 ) `4_4 = F4(0 ,F1(),F2(),F3()) by A15, Def7
.= (g . (0 + 1)) `3_4 by A13, Def6 ;
A19: (g . (0 + 1)) `1_4 = F2() by A13, Def4
.= (g . 0 ) `2_4 by A15, Def5 ;
deffunc H6( Element of NAT ) -> set = (g . $1) `1_4 ;
consider f being Function such that
A20: dom f = NAT and
A21: for x being Element of NAT holds f . x = H6(x) from FUNCT_1:sch 4();
 A22: f . (0 + 3) = (g . (0 + 3)) `1_4 by A21
.= H1(0 + 2,g . (0 + 2)) `1_4 by A8
.= (g . (0 + 2)) `2_4 by Def4 ;
take f ; :: thesis: ( 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))) ) )
thus dom f = NAT by A20; :: thesis: ( 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))) ) )
defpred S4[ Element of NAT ] means ( f . ($1 + 3) = (g . ($1 + 2)) `2_4 & (g . $1) `2_4 = (g . ($1 + 1)) `1_4 & (g . $1) `3_4 = (g . ($1 + 1)) `2_4 & (g . $1) `4_4 = (g . ($1 + 1)) `3_4 & (g . ($1 + 1)) `2_4 = (g . ($1 + 2)) `1_4 & (g . ($1 + 1)) `3_4 = (g . ($1 + 2)) `2_4 & (g . ($1 + 1)) `4_4 = (g . ($1 + 2)) `3_4 & (g . ($1 + 2)) `2_4 = (g . ($1 + 3)) `1_4 & f . ($1 + 3) = F4($1,(f . $1),(f . ($1 + 1)),(f . ($1 + 2))) );
A23: (g . (0 + 2)) `2_4 = H1(0 + 2,g . (0 + 2)) `1_4 by Def4
.= (g . (0 + 3)) `1_4 by A8 ;
thus A24: f . 0 = (g . 0 ) `1_4 by A21
.= F1() by A15, Def4 ; :: thesis: ( 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))) ) )
thus A25: f . 1 = (g . 1) `1_4 by A21
.= F2() by A13, Def4 ; :: thesis: ( f . 2 = F3() & ( for n being Element of NAT holds f . (n + 3) = F4(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )
thus A26: f . 2 = (g . 2) `1_4 by A21
.= F3() by A7, Def4 ; :: thesis: for n being Element of NAT holds f . (n + 3) = F4(n,(f . n),(f . (n + 1)),(f . (n + 2)))
A27: for x being Element of NAT st S4[x] holds
S4[x + 1]
proof
let x be Element of NAT ; :: thesis: ( S4[x] implies S4[x + 1] )
A28: (x + 1) + 2 = x + (1 + 2) ;
assume A29: S4[x] ; :: thesis: S4[x + 1]
then A30: f . ((x + 1) + 1) = (g . x) `3_4 by A21;
thus A31: f . ((x + 1) + 3) = (g . ((x + 1) + 3)) `1_4 by A21
.= H1((x + 1) + 2,g . ((x + 1) + 2)) `1_4 by A8
.= (g . ((x + 1) + 2)) `2_4 by Def4 ; :: thesis: ( (g . (x + 1)) `2_4 = (g . ((x + 1) + 1)) `1_4 & (g . (x + 1)) `3_4 = (g . ((x + 1) + 1)) `2_4 & (g . (x + 1)) `4_4 = (g . ((x + 1) + 1)) `3_4 & (g . ((x + 1) + 1)) `2_4 = (g . ((x + 1) + 2)) `1_4 & (g . ((x + 1) + 1)) `3_4 = (g . ((x + 1) + 2)) `2_4 & (g . ((x + 1) + 1)) `4_4 = (g . ((x + 1) + 2)) `3_4 & (g . ((x + 1) + 2)) `2_4 = (g . ((x + 1) + 3)) `1_4 & f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )
thus (g . ((x + 1) + 1)) `1_4 = (g . (x + 1)) `2_4 by A29; :: thesis: ( (g . (x + 1)) `3_4 = (g . ((x + 1) + 1)) `2_4 & (g . (x + 1)) `4_4 = (g . ((x + 1) + 1)) `3_4 & (g . ((x + 1) + 1)) `2_4 = (g . ((x + 1) + 2)) `1_4 & (g . ((x + 1) + 1)) `3_4 = (g . ((x + 1) + 2)) `2_4 & (g . ((x + 1) + 1)) `4_4 = (g . ((x + 1) + 2)) `3_4 & (g . ((x + 1) + 2)) `2_4 = (g . ((x + 1) + 3)) `1_4 & f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )
thus (g . (x + 1)) `3_4 = (g . ((x + 1) + 1)) `2_4 by A29; :: thesis: ( (g . (x + 1)) `4_4 = (g . ((x + 1) + 1)) `3_4 & (g . ((x + 1) + 1)) `2_4 = (g . ((x + 1) + 2)) `1_4 & (g . ((x + 1) + 1)) `3_4 = (g . ((x + 1) + 2)) `2_4 & (g . ((x + 1) + 1)) `4_4 = (g . ((x + 1) + 2)) `3_4 & (g . ((x + 1) + 2)) `2_4 = (g . ((x + 1) + 3)) `1_4 & f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )
thus (g . (x + 1)) `4_4 = (g . ((x + 1) + 1)) `3_4 by A29; :: thesis: ( (g . ((x + 1) + 1)) `2_4 = (g . ((x + 1) + 2)) `1_4 & (g . ((x + 1) + 1)) `3_4 = (g . ((x + 1) + 2)) `2_4 & (g . ((x + 1) + 1)) `4_4 = (g . ((x + 1) + 2)) `3_4 & (g . ((x + 1) + 2)) `2_4 = (g . ((x + 1) + 3)) `1_4 & f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )
thus (g . ((x + 1) + 1)) `2_4 = H1(x + 2,g . (x + 2)) `1_4 by Def4
.= (g . ((x + 1) + 2)) `1_4 by A8, A28 ; :: thesis: ( (g . ((x + 1) + 1)) `3_4 = (g . ((x + 1) + 2)) `2_4 & (g . ((x + 1) + 1)) `4_4 = (g . ((x + 1) + 2)) `3_4 & (g . ((x + 1) + 2)) `2_4 = (g . ((x + 1) + 3)) `1_4 & f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )
thus (g . ((x + 1) + 1)) `3_4 = H1(x + 2,g . (x + 2)) `2_4 by Def5
.= (g . ((x + 1) + 2)) `2_4 by A8, A28 ; :: thesis: ( (g . ((x + 1) + 1)) `4_4 = (g . ((x + 1) + 2)) `3_4 & (g . ((x + 1) + 2)) `2_4 = (g . ((x + 1) + 3)) `1_4 & f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )
thus (g . ((x + 1) + 1)) `4_4 = H1(x + 2,g . (x + 2)) `3_4 by Def6
.= (g . ((x + 1) + 2)) `3_4 by A8, A28 ; :: thesis: ( (g . ((x + 1) + 2)) `2_4 = (g . ((x + 1) + 3)) `1_4 & f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )
thus (g . ((x + 1) + 2)) `2_4 = H1((x + 1) + 2,g . ((x + 1) + 2)) `1_4 by Def4
.= (g . ((x + 1) + 3)) `1_4 by A8 ; :: thesis: f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)))
per cases ( ( x <= 1 & x <> 1 ) or x = 1 or 1 < x ) ;
suppose ( x <= 1 & x <> 1 ) ; :: thesis: f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)))
then A32: x = 0 by NAT_1:26;
hence f . ((x + 1) + 3) = (g . (1 + 3)) `1_4 by A21
.= H1(1 + 2,g . (1 + 2)) `1_4 by A8
.= (g . (0 + 3)) `2_4 by Def4
.= H1(0 + 2,g . (0 + 2)) `2_4 by A8
.= (g . (0 + 2)) `3_4 by Def5
.= F4(1,F2(),F3(),F4(0 ,F1(),F2(),F3())) by A7, Def6
.= F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) by A15, A25, A26, A29, A32, Def7 ;
:: thesis: verum
end;
suppose A33: x = 1 ; :: thesis: f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)))
then A34: ( f . ((x + 1) + 1) = F4(0 ,F1(),F2(),F3()) & f . ((x + 1) + 2) = F4(1,F2(),F3(),F4(0 ,F1(),F2(),F3())) ) by A13, A29, A30, Def6, Def7;
thus f . ((x + 1) + 3) = (g . ((1 + 1) + 3)) `1_4 by A21, A33
.= H1(2 + 2,g . (2 + 2)) `1_4 by A8
.= (g . (1 + 3)) `2_4 by Def4
.= H1(1 + 2,g . (1 + 2)) `2_4 by A8
.= (g . (0 + 3)) `3_4 by Def5
.= H1(0 + 2,g . (0 + 2)) `3_4 by A8
.= (g . (0 + 2)) `4_4 by Def6
.= F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) by A7, A26, A33, A34, Def7 ; :: thesis: verum
end;
suppose A35: 1 < x ; :: thesis: f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)))
then 1 - 1 <= x - 1 by XREAL_1:15;
then A36: x - 1 = x -' 1 by XREAL_0:def 2;
A37: 1 + 1 <= x by A35, NAT_1:13;
then A38: (x -' 2) + 2 = x by XREAL_1:237;
2 - 2 <= x - 2 by A37, XREAL_1:15;
then A39: x - 2 = x -' 2 by XREAL_0:def 2;
A40: x + 1 = (x - 1) + 2 ;
thus f . ((x + 1) + 3) = (g . (x + (1 + 2))) `2_4 by A31
.= H1(x + 2,g . (x + 2)) `2_4 by A8
.= (g . ((x -' 1) + 3)) `3_4 by A36, Def5
.= H1(x + 1,g . (x + 1)) `3_4 by A8, A36, A40
.= (g . ((x -' 2) + 3)) `4_4 by A39, Def6
.= H1((x -' 2) + 2,g . ((x -' 2) + 2)) `4_4 by A8
.= F4((x + 1),((g . x) `2_4 ),((g . x) `3_4 ),((g . x) `4_4 )) by A38, Def7
.= F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) by A21, A29, A30 ; :: thesis: verum
end;
end;
end;
(g . (0 + 1)) `2_4 = F3() by A13, Def5
.= (g . (0 + 2)) `1_4 by A7, Def4 ;
then A41: S4[ 0 ] by A7, A24, A25, A26, A22, A19, A16, A18, A14, A17, A23, Def5;
for x being Element of NAT holds S4[x] from NAT_1:sch 1(A41, A27);
 hence for n being Element of NAT holds f . (n + 3) = F4(n,(f . n),(f . (n + 1)),(f . (n + 2))) ; :: thesis: verum