defpred S1[ object ] means In ($1,NAT) > 1;
defpred S2[ object ] means $1 = 1;
defpred S3[ object ] means $1 = 0 ;
deffunc H1( Nat, set ) -> object = [($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 ) -> object = 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( object ) -> set = h . ((In ($1,NAT)) -' 2);
deffunc H4( object ) -> object = [F2(),F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3()))];
deffunc H5( object ) -> object = [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 SUBSET_1:def 8;
hence ( S3[c] or S2[c] or S1[c] ) by NAT_1:25; :: 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] ) ) ;
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: 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, XREAL_1:232 ;
A7: for n being Nat holds g . (n + 3) = H1(n + 2,g . (n + 2))
proof
let n be Nat; :: thesis: g . (n + 3) = H1(n + 2,g . (n + 2))
0 + 1 < n + 2 by XREAL_1:8;
then A8: g . (n + 2) = H3(n + 2) by A5
.= h . n by NAT_D:34 ;
A9: ( (n + 3) - 2 = n + (3 - 2) & 0 <= n + 1 ) ;
0 + 1 < n + 3 by XREAL_1:8;
hence g . (n + 3) = H3(n + 3) by A5
.= h . (n + 1) by A9, XREAL_0:def 2
.= H1(n + 2,g . (n + 2)) by A2, A8 ;
:: thesis: verum
end;
A10: g . 1 = [F2(),F3(),F4(0,F1(),F2(),F3()),F4(1,F2(),F3(),F4(0,F1(),F2(),F3()))] by A5;
then A11: (g . (0 + 1)) `3_4 = F4(0,F1(),F2(),F3())
.= (g . (0 + 2)) `2_4 by A6 ;
A12: g . 0 = [F1(),F2(),F3(),F4(0,F1(),F2(),F3())] by A5;
then A13: (g . 0) `3_4 = F3()
.= (g . (0 + 1)) `2_4 by A10 ;
A14: (g . (0 + 1)) `4_4 = F4(1,F2(),F3(),F4(0,F1(),F2(),F3())) by A10
.= (g . (0 + 2)) `3_4 by A6 ;
A15: (g . 0) `4_4 = F4(0,F1(),F2(),F3()) by A12
.= (g . (0 + 1)) `3_4 by A10 ;
A16: (g . (0 + 1)) `1_4 = F2() by A10
.= (g . 0) `2_4 by A12 ;
deffunc H6( Nat) -> object = (g . $1) `1_4 ;
consider f being Function such that
A17: dom f = NAT and
A18: for x being Element of NAT holds f . x = H6(x) from FUNCT_1:sch 4();
 A19: f . (0 + 3) = (g . (0 + 3)) `1_4 by A18
.= H1(0 + 2,g . (0 + 2)) `1_4 by A7
.= (g . (0 + 2)) `2_4 ;
take f ; :: thesis: ( 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))) ) )
thus dom f = NAT by A17; :: thesis: ( 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))) ) )
defpred S4[ 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))) );
A20: (g . (0 + 2)) `2_4 = H1(0 + 2,g . (0 + 2)) `1_4
.= (g . (0 + 3)) `1_4 by A7 ;
thus A21: f . 0 = (g . 0) `1_4 by A18
.= F1() by A12 ; :: thesis: ( f . 1 = F2() & f . 2 = F3() & ( for n being Nat holds f . (n + 3) = F4(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )
thus A22: f . 1 = (g . 1) `1_4 by A18
.= F2() by A10 ; :: thesis: ( f . 2 = F3() & ( for n being Nat holds f . (n + 3) = F4(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )
thus A23: f . 2 = (g . 2) `1_4 by A18
.= F3() by A6 ; :: thesis: for n being Nat holds f . (n + 3) = F4(n,(f . n),(f . (n + 1)),(f . (n + 2)))
A24: for x being Nat st S4[x] holds
S4[x + 1]
proof
let x be Nat; :: thesis: ( S4[x] implies S4[x + 1] )
A25: (x + 1) + 2 = x + (1 + 2) ;
assume A26: S4[x] ; :: thesis: S4[x + 1]
then A27: f . ((x + 1) + 1) = (g . x) `3_4 by A18;
thus A28: f . ((x + 1) + 3) = (g . ((x + 1) + 3)) `1_4 by A18
.= H1((x + 1) + 2,g . ((x + 1) + 2)) `1_4 by A7
.= (g . ((x + 1) + 2)) `2_4 ; :: 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 A26; :: 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 A26; :: 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 A26; :: 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
.= (g . ((x + 1) + 2)) `1_4 by A7, A25 ; :: 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
.= (g . ((x + 1) + 2)) `2_4 by A7, A25 ; :: 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
.= (g . ((x + 1) + 2)) `3_4 by A7, A25 ; :: 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
.= (g . ((x + 1) + 3)) `1_4 by A7 ; :: 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 A29: x = 0 by NAT_1:25;
hence f . ((x + 1) + 3) = (g . (1 + 3)) `1_4 by A18
.= H1(1 + 2,g . (1 + 2)) `1_4 by A7
.= (g . (0 + 3)) `2_4
.= H1(0 + 2,g . (0 + 2)) `2_4 by A7
.= (g . (0 + 2)) `3_4
.= F4(1,F2(),F3(),F4(0,F1(),F2(),F3())) by A6
.= F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) by A12, A22, A23, A26, A29 ;
:: thesis: verum
end;
suppose A30: x = 1 ; :: thesis: f . ((x + 1) + 3) = F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)))
then A31: ( f . ((x + 1) + 1) = F4(0,F1(),F2(),F3()) & f . ((x + 1) + 2) = F4(1,F2(),F3(),F4(0,F1(),F2(),F3())) ) by A10, A26, A27;
thus f . ((x + 1) + 3) = (g . ((1 + 1) + 3)) `1_4 by A18, A30
.= H1(2 + 2,g . (2 + 2)) `1_4 by A7
.= (g . (1 + 3)) `2_4
.= H1(1 + 2,g . (1 + 2)) `2_4 by A7
.= (g . (0 + 3)) `3_4
.= H1(0 + 2,g . (0 + 2)) `3_4 by A7
.= (g . (0 + 2)) `4_4
.= F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) by A6, A23, A30, A31 ; :: thesis: verum
end;
suppose A32: 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:13;
then A33: x - 1 = x -' 1 by XREAL_0:def 2;
A34: 1 + 1 <= x by A32, NAT_1:13;
then A35: (x -' 2) + 2 = x by XREAL_1:235;
2 - 2 <= x - 2 by A34, XREAL_1:13;
then A36: x - 2 = x -' 2 by XREAL_0:def 2;
A37: x + 1 = (x - 1) + 2 ;
thus f . ((x + 1) + 3) = (g . (x + (1 + 2))) `2_4 by A28
.= H1(x + 2,g . (x + 2)) `2_4 by A7
.= (g . ((x -' 1) + 3)) `3_4 by A33
.= H1(x + 1,g . (x + 1)) `3_4 by A7, A33, A37
.= (g . ((x -' 2) + 3)) `4_4 by A36
.= H1((x -' 2) + 2,g . ((x -' 2) + 2)) `4_4 by A7
.= F4((x + 1),((g . x) `2_4),((g . x) `3_4),((g . x) `4_4)) by A35
.= F4((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) by A18, A26, A27 ; :: thesis: verum
end;
end;
end;
(g . (0 + 1)) `2_4 = F3() by A10
.= (g . (0 + 2)) `1_4 by A6 ;
then A38: S4[ 0 ] by A6, A21, A22, A23, A19, A16, A13, A15, A11, A14, A20;
for x being Nat holds S4[x] from NAT_1:sch 2(A38, A24);
 hence for n being Nat holds f . (n + 3) = F4(n,(f . n),(f . (n + 1)),(f . (n + 2))) ; :: thesis: verum