defpred S1[ set ] means $1 = 0 ;
deffunc H1( Nat, set ) -> object = [($2 `2_3),($2 `3_3),F3(($1 + 1),($2 `2_3),($2 `3_3))];
set r03 = F3(0,F1(),F2());
set r13 = F3(1,F2(),F3(0,F1(),F2()));
deffunc H2( Nat, set ) -> object = H1($1 + 1,$2);
consider h being Function such that
dom h = NAT
and
A1:
h . 0 = [F2(),F3(0,F1(),F2()),F3(1,F2(),F3(0,F1(),F2()))]
and
A2:
for n being Nat holds h . (n + 1) = H2(n,h . n)
from NAT_1:sch 11();
deffunc H3( Nat) -> set = h . ($1 -' 1);
deffunc H4( set ) -> object = [F1(),F2(),F3(0,F1(),F2())];
consider g being Function such that
dom g = NAT
and
A3:
for x being Element of NAT holds
( ( S1[x] implies g . x = H4(x) ) & ( not S1[x] implies g . x = H3(x) ) )
from PARTFUN1:sch 4();
deffunc H5( object ) -> object = (g . $1) `1_3 ;
consider f being Function such that
A4:
dom f = NAT
and
A5:
for x being object st x in NAT holds
f . x = H5(x)
from FUNCT_1:sch 3();
defpred S2[ Nat] means ( f . ($1 + 2) = (g . ($1 + 1)) `2_3 & (g . ($1 + 1)) `1_3 = (g . $1) `2_3 & (g . ($1 + 2)) `1_3 = (g . $1) `3_3 & (g . ($1 + 2)) `1_3 = (g . ($1 + 1)) `2_3 & (g . ($1 + 2)) `2_3 = (g . ($1 + 1)) `3_3 & f . ($1 + 2) = F3($1,(f . $1),(f . ($1 + 1))) );
A6:
g . 0 = [F1(),F2(),F3(0,F1(),F2())]
by A3;
A7:
for n being Nat holds g . (n + 2) = H1(n + 1,g . (n + 1))
then A10: (g . (0 + 2)) `2_3 =
H1(0 + 1,g . (0 + 1)) `2_3
.=
(g . (0 + 1)) `3_3
;
take
f
; ( dom f = NAT & f . 0 = F1() & f . 1 = F2() & ( for n being Nat holds f . (n + 2) = F3(n,(f . n),(f . (n + 1))) ) )
thus
dom f = NAT
by A4; ( f . 0 = F1() & f . 1 = F2() & ( for n being Nat holds f . (n + 2) = F3(n,(f . n),(f . (n + 1))) ) )
thus A11: f . 0 =
(g . 0) `1_3
by A5
.=
F1()
by A6
; ( f . 1 = F2() & ( for n being Nat holds f . (n + 2) = F3(n,(f . n),(f . (n + 1))) ) )
A12: g . 1 =
H3(1)
by A3
.=
[F2(),F3(0,F1(),F2()),F3(1,F2(),F3(0,F1(),F2()))]
by A1, XREAL_1:232
;
then A13: (g . (0 + 1)) `1_3 =
F2()
.=
(g . 0) `2_3
by A6
;
A14:
for x being Nat st S2[x] holds
S2[x + 1]
proof
let x be
Nat;
( S2[x] implies S2[x + 1] )
assume A15:
S2[
x]
;
S2[x + 1]
then A16:
f . (x + 1) = (g . x) `2_3
by A5;
thus A17:
f . ((x + 1) + 2) =
(g . ((x + 1) + 2)) `1_3
by A5
.=
H1(
(x + 1) + 1,
g . ((x + 1) + 1))
`1_3
by A7
.=
(g . ((x + 1) + 1)) `2_3
;
( (g . ((x + 1) + 1)) `1_3 = (g . (x + 1)) `2_3 & (g . ((x + 1) + 2)) `1_3 = (g . (x + 1)) `3_3 & (g . ((x + 1) + 2)) `1_3 = (g . ((x + 1) + 1)) `2_3 & (g . ((x + 1) + 2)) `2_3 = (g . ((x + 1) + 1)) `3_3 & f . ((x + 1) + 2) = F3((x + 1),(f . (x + 1)),(f . ((x + 1) + 1))) )
thus
(g . ((x + 1) + 1)) `1_3 = (g . (x + 1)) `2_3
by A15;
( (g . ((x + 1) + 2)) `1_3 = (g . (x + 1)) `3_3 & (g . ((x + 1) + 2)) `1_3 = (g . ((x + 1) + 1)) `2_3 & (g . ((x + 1) + 2)) `2_3 = (g . ((x + 1) + 1)) `3_3 & f . ((x + 1) + 2) = F3((x + 1),(f . (x + 1)),(f . ((x + 1) + 1))) )
thus (g . ((x + 1) + 2)) `1_3 =
H1(
(x + 1) + 1,
g . ((x + 1) + 1))
`1_3
by A7
.=
(g . (x + 1)) `3_3
by A15
;
( (g . ((x + 1) + 2)) `1_3 = (g . ((x + 1) + 1)) `2_3 & (g . ((x + 1) + 2)) `2_3 = (g . ((x + 1) + 1)) `3_3 & f . ((x + 1) + 2) = F3((x + 1),(f . (x + 1)),(f . ((x + 1) + 1))) )
hence
(g . ((x + 1) + 2)) `1_3 = (g . ((x + 1) + 1)) `2_3
by A15;
( (g . ((x + 1) + 2)) `2_3 = (g . ((x + 1) + 1)) `3_3 & f . ((x + 1) + 2) = F3((x + 1),(f . (x + 1)),(f . ((x + 1) + 1))) )
thus (g . ((x + 1) + 2)) `2_3 =
H1(
(x + 1) + 1,
g . ((x + 1) + 1))
`2_3
by A7
.=
(g . ((x + 1) + 1)) `3_3
;
f . ((x + 1) + 2) = F3((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)))
per cases
( x = 0 or x <> 0 )
;
suppose A18:
x = 0
;
f . ((x + 1) + 2) = F3((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)))hence f . ((x + 1) + 2) =
(g . (1 + 2)) `1_3
by A5
.=
H1(1
+ 1,
g . (1 + 1))
`1_3
by A7
.=
(g . (0 + 1)) `3_3
by A15, A18
.=
F3(1,
F2(),
F3(
0,
F1(),
F2()))
by A12
.=
F3(
(0 + 1),
F2(),
((g . 0) `3_3))
by A6
.=
F3(
(x + 1),
(f . (x + 1)),
(f . ((x + 1) + 1)))
by A6, A15, A16, A18
;
verum end; end;
end;
A22: f . (0 + 2) =
(g . (0 + 2)) `1_3
by A5
.=
H1(0 + 1,g . (0 + 1)) `1_3
by A7
.=
(g . (0 + 1)) `2_3
;
thus A23: f . 1 =
(g . 1) `1_3
by A5
.=
F2()
by A12
; for n being Nat holds f . (n + 2) = F3(n,(f . n),(f . (n + 1)))
A24: (g . (0 + 2)) `1_3 =
H1(0 + 1,g . (0 + 1)) `1_3
by A7
.=
(g . 1) `2_3
.=
F3(0,F1(),F2())
by A12
.=
(g . 0) `3_3
by A6
;
then (g . (0 + 2)) `1_3 =
F3(0,F1(),F2())
by A6
.=
(g . (0 + 1)) `2_3
by A12
;
then A25:
S2[ 0 ]
by A12, A11, A23, A22, A13, A24, A10;
for x being Nat holds S2[x]
from NAT_1:sch 2(A25, A14);
hence
for n being Nat holds f . (n + 2) = F3(n,(f . n),(f . (n + 1)))
; verum