set r04 = F₄(0 ,F₁(),F₂(),F₃());
set r14 = F₄(1,F₂(),F₃(),F₄(0 ,F₁(),F₂(),F₃()));
set r24 = F₄(2,F₃(),F₄(0 ,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0 ,F₁(),F₂(),F₃())));
deffunc H₁( Nat, set ) -> set = [($2 `2_4 ),($2 `3_4 ),($2 `4_4 ),F<sub>4</sub>(($1 + 1),($2 `2_4 ),($2 `3_4 ),($2 `4_4 ))];
deffunc H₂( Nat, set ) -> set = H₁($1 + 2,$2);
consider h being Function such that
dom h = NAT and
A1: h . 0 = [F₃(),F₄(0 ,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0 ,F₁(),F₂(),F₃())),F₄(2,F₃(),F₄(0 ,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0 ,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 In $1,NAT > 1;
deffunc H₃( set ) -> set = [F₁(),F₂(),F₃(),F₄(0 ,F₁(),F₂(),F₃())];
deffunc H₄( set ) -> set = [F₂(),F₃(),F₄(0 ,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0 ,F₁(),F₂(),F₃()))];
deffunc H₅( set ) -> set = h . ((In $1,NAT ) -' 2);
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] ) )

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

end;

A4: for c being set holds
( not c in NAT 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] )
assume c in NAT ; :: thesis: ( 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] ) by NAT_1:26; :: 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) ) ) from RECDEF_2:sch 1(A3, A4);
A6: g . 0 = [F₁(),F₂(),F₃(),F₄(0 ,F₁(),F₂(),F₃())] by A5;
A7: g . 1 = [F₂(),F₃(),F₄(0 ,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0 ,F₁(),F₂(),F₃()))] by A5;
A8: In 2,NAT = 2 by FUNCT_7:def 1;
then A9: g . 2 = H₅(2) by A5
.= [F₃(),F₄(0 ,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0 ,F₁(),F₂(),F₃())),F₄(2,F₃(),F₄(0 ,F₁(),F₂(),F₃()),F₄(1,F₂(),F₃(),F₄(0 ,F₁(),F₂(),F₃())))] by A1, A8, XREAL_1:234 ;
A10: for n being Element of NAT holds g . (n + 3) = H₁(n + 2,g . (n + 2))

proof

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

end;

deffunc H₆( Element of NAT ) -> set = (g . $1) `1_4 ;
consider f being Function such that
A15: dom f = NAT and
A16: for x being Element of NAT holds f . x = H<sub>6</sub>(x) from FUNCT_1:sch 4();
take f ; :: thesis: ( dom f = NAT & f . 0 = F<sub>1</sub>() & f . 1 = F<sub>2</sub>() & f . 2 = F<sub>3</sub>() & ( for n being Element of NAT holds f . (n + 3) = F<sub>4</sub>(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )
thus dom f = NAT by A15; :: thesis: ( f . 0 = F<sub>1</sub>() & f . 1 = F<sub>2</sub>() & f . 2 = F<sub>3</sub>() & ( for n being Element of NAT holds f . (n + 3) = F<sub>4</sub>(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )
thus A17: f . 0 = (g . 0 ) `1_4 by A16
.= F₁() by A6, Def4 ; :: thesis: ( f . 1 = F₂() & f . 2 = F₃() & ( for n being Element of NAT holds f . (n + 3) = F₄(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )
thus A18: f . 1 = (g . 1) `1_4 by A16
.= F<sub>2</sub>() by A7, Def4 ; :: thesis: ( f . 2 = F<sub>3</sub>() & ( for n being Element of NAT holds f . (n + 3) = F<sub>4</sub>(n,(f . n),(f . (n + 1)),(f . (n + 2))) ) )
thus A19: f . 2 = (g . 2) `1_4 by A16
.= F₃() by A9, Def4 ; :: thesis: for n being Element of NAT holds f . (n + 3) = F₄(n,(f . n),(f . (n + 1)),(f . (n + 2)))
defpred S₄[ 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) = F₄($1,(f . $1),(f . ($1 + 1)),(f . ($1 + 2))) );
A20: S₄[ 0 ]

proof

thus A21: f . (0 + 3) = (g . (0 + 3)) `1_4 by A16
.= H<sub>1</sub>(0 + 2,g . (0 + 2)) `1_4 by A10
.= (g . (0 + 2)) `2_4 by Def4 ; :: thesis: ( (g . 0 ) `2_4 = (g . (0 + 1)) `1_4 & (g . 0 ) `3_4 = (g . (0 + 1)) `2_4 & (g . 0 ) `4_4 = (g . (0 + 1)) `3_4 & (g . (0 + 1)) `2_4 = (g . (0 + 2)) `1_4 & (g . (0 + 1)) `3_4 = (g . (0 + 2)) `2_4 & (g . (0 + 1)) `4_4 = (g . (0 + 2)) `3_4 & (g . (0 + 2)) `2_4 = (g . (0 + 3)) `1_4 & f . (0 + 3) = F<sub>4</sub>(0 ,(f . 0 ),(f . (0 + 1)),(f . (0 + 2))) )
thus (g . (0 + 1)) `1_4 = F₂() by A7, Def4
.= (g . 0 ) `2_4 by A6, Def5 ; :: thesis: ( (g . 0 ) `3_4 = (g . (0 + 1)) `2_4 & (g . 0 ) `4_4 = (g . (0 + 1)) `3_4 & (g . (0 + 1)) `2_4 = (g . (0 + 2)) `1_4 & (g . (0 + 1)) `3_4 = (g . (0 + 2)) `2_4 & (g . (0 + 1)) `4_4 = (g . (0 + 2)) `3_4 & (g . (0 + 2)) `2_4 = (g . (0 + 3)) `1_4 & f . (0 + 3) = F<sub>4</sub>(0 ,(f . 0 ),(f . (0 + 1)),(f . (0 + 2))) )
thus (g . 0 ) `3_4 = F₃() by A6, Def6
.= (g . (0 + 1)) `2_4 by A7, Def5 ; :: thesis: ( (g . 0 ) `4_4 = (g . (0 + 1)) `3_4 & (g . (0 + 1)) `2_4 = (g . (0 + 2)) `1_4 & (g . (0 + 1)) `3_4 = (g . (0 + 2)) `2_4 & (g . (0 + 1)) `4_4 = (g . (0 + 2)) `3_4 & (g . (0 + 2)) `2_4 = (g . (0 + 3)) `1_4 & f . (0 + 3) = F<sub>4</sub>(0 ,(f . 0 ),(f . (0 + 1)),(f . (0 + 2))) )
thus (g . 0 ) `4_4 = F₄(0 ,F₁(),F₂(),F₃()) by A6, Def7
.= (g . (0 + 1)) `3_4 by A7, Def6 ; :: thesis: ( (g . (0 + 1)) `2_4 = (g . (0 + 2)) `1_4 & (g . (0 + 1)) `3_4 = (g . (0 + 2)) `2_4 & (g . (0 + 1)) `4_4 = (g . (0 + 2)) `3_4 & (g . (0 + 2)) `2_4 = (g . (0 + 3)) `1_4 & f . (0 + 3) = F<sub>4</sub>(0 ,(f . 0 ),(f . (0 + 1)),(f . (0 + 2))) )
thus (g . (0 + 1)) `2_4 = F₃() by A7, Def5
.= (g . (0 + 2)) `1_4 by A9, Def4 ; :: thesis: ( (g . (0 + 1)) `3_4 = (g . (0 + 2)) `2_4 & (g . (0 + 1)) `4_4 = (g . (0 + 2)) `3_4 & (g . (0 + 2)) `2_4 = (g . (0 + 3)) `1_4 & f . (0 + 3) = F<sub>4</sub>(0 ,(f . 0 ),(f . (0 + 1)),(f . (0 + 2))) )
thus (g . (0 + 1)) `3_4 = F₄(0 ,F₁(),F₂(),F₃()) by A7, Def6
.= (g . (0 + 2)) `2_4 by A9, Def5 ; :: thesis: ( (g . (0 + 1)) `4_4 = (g . (0 + 2)) `3_4 & (g . (0 + 2)) `2_4 = (g . (0 + 3)) `1_4 & f . (0 + 3) = F<sub>4</sub>(0 ,(f . 0 ),(f . (0 + 1)),(f . (0 + 2))) )
thus (g . (0 + 1)) `4_4 = F₄(1,F₂(),F₃(),F₄(0 ,F₁(),F₂(),F₃())) by A7, Def7
.= (g . (0 + 2)) `3_4 by A9, Def6 ; :: thesis: ( (g . (0 + 2)) `2_4 = (g . (0 + 3)) `1_4 & f . (0 + 3) = F<sub>4</sub>(0 ,(f . 0 ),(f . (0 + 1)),(f . (0 + 2))) )
thus (g . (0 + 2)) `2_4 = H₁(0 + 2,g . (0 + 2)) `1_4 by Def4
.= (g . (0 + 3)) `1_4 by A10 ; :: thesis: f . (0 + 3) = F₄(0 ,(f . 0 ),(f . (0 + 1)),(f . (0 + 2)))
thus f . (0 + 3) = F₄(0 ,(f . 0 ),(f . (0 + 1)),(f . (0 + 2))) by A9, A17, A18, A19, A21, Def5; :: thesis: verum

end;

A22: 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 A23: S₄[x] ; :: thesis: S₄[x + 1]
A24: (x + 1) + 2 = x + (1 + 2) ;
thus A25: f . ((x + 1) + 3) = (g . ((x + 1) + 3)) `1_4 by A16
.= H<sub>1</sub>((x + 1) + 2,g . ((x + 1) + 2)) `1_4 by A10
.= (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) = F<sub>4</sub>((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 A23; :: 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) = F<sub>4</sub>((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 A23; :: 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) = F<sub>4</sub>((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 A23; :: 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) = F<sub>4</sub>((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )
thus (g . ((x + 1) + 1)) `2_4 = H₁(x + 2,g . (x + 2)) `1_4 by Def4
.= (g . ((x + 1) + 2)) `1_4 by A10, A24 ; :: 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) = F₄((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )
thus (g . ((x + 1) + 1)) `3_4 = H<sub>1</sub>(x + 2,g . (x + 2)) `2_4 by Def5
.= (g . ((x + 1) + 2)) `2_4 by A10, A24 ; :: 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) = F<sub>4</sub>((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )
thus (g . ((x + 1) + 1)) `4_4 = H₁(x + 2,g . (x + 2)) `3_4 by Def6
.= (g . ((x + 1) + 2)) `3_4 by A10, A24 ; :: thesis: ( (g . ((x + 1) + 2)) `2_4 = (g . ((x + 1) + 3)) `1_4 & f . ((x + 1) + 3) = F₄((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) )
thus (g . ((x + 1) + 2)) `2_4 = H<sub>1</sub>((x + 1) + 2,g . ((x + 1) + 2)) `1_4 by Def4
.= (g . ((x + 1) + 3)) `1_4 by A10 ; :: thesis: f . ((x + 1) + 3) = F<sub>4</sub>((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)))
A26: f . ((x + 1) + 1) = (g . x) `3_4 by A16, A23;

per cases ( ( x <= 1 & x <> 1 ) or x = 1 or 1 < x ) ;

suppose ( x <= 1 & x <> 1 ) ; :: thesis: f . ((x + 1) + 3) = F₄((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)))

then A27: x = 0 by NAT_1:26;
hence f . ((x + 1) + 3) = (g . (1 + 3)) `1_4 by A16
.= H<sub>1</sub>(1 + 2,g . (1 + 2)) `1_4 by A10
.= (g . (0 + 3)) `2_4 by Def4
.= H<sub>1</sub>(0 + 2,g . (0 + 2)) `2_4 by A10
.= (g . (0 + 2)) `3_4 by Def5
.= F₄(1,F₂(),F₃(),F₄(0 ,F₁(),F₂(),F₃())) by A9, Def6
.= F₄((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) by A6, A18, A19, A23, A27, Def7 ;
:: thesis: verum

end;

suppose A28: x = 1 ; :: thesis: f . ((x + 1) + 3) = F₄((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)))

then A29: f . ((x + 1) + 1) = F₄(0 ,F₁(),F₂(),F₃()) by A7, A26, Def6;
A30: f . ((x + 1) + 2) = F₄(1,F₂(),F₃(),F₄(0 ,F₁(),F₂(),F₃())) by A7, A23, A28, Def7;
thus f . ((x + 1) + 3) = (g . ((1 + 1) + 3)) `1_4 by A16, A28
.= H<sub>1</sub>(2 + 2,g . (2 + 2)) `1_4 by A10
.= (g . (1 + 3)) `2_4 by Def4
.= H<sub>1</sub>(1 + 2,g . (1 + 2)) `2_4 by A10
.= (g . (0 + 3)) `3_4 by Def5
.= H<sub>1</sub>(0 + 2,g . (0 + 2)) `3_4 by A10
.= (g . (0 + 2)) `4_4 by Def6
.= F₄((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) by A9, A19, A28, A29, A30, Def7 ; :: thesis: verum

end;

suppose A31: 1 < x ; :: thesis: f . ((x + 1) + 3) = F₄((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2)))

then A32: 1 + 1 <= x by NAT_1:13;
then 2 - 2 <= x - 2 by XREAL_1:15;
then A33: x - 2 = x -' 2 by XREAL_0:def 2;
1 - 1 <= x - 1 by A31, XREAL_1:15;
then A34: x - 1 = x -' 1 by XREAL_0:def 2;
A35: (x -' 2) + 2 = x by A32, XREAL_1:237;
A36: x + 1 = (x - 1) + 2 ;
thus f . ((x + 1) + 3) = (g . (x + (1 + 2))) `2_4 by A25
.= H<sub>1</sub>(x + 2,g . (x + 2)) `2_4 by A10
.= (g . ((x -' 1) + 3)) `3_4 by A34, Def5
.= H<sub>1</sub>(x + 1,g . (x + 1)) `3_4 by A10, A34, A36
.= (g . ((x -' 2) + 3)) `4_4 by A33, Def6
.= H<sub>1</sub>((x -' 2) + 2,g . ((x -' 2) + 2)) `4_4 by A10
.= F₄((x + 1),((g . x) `2_4 ),((g . x) `3_4 ),((g . x) `4_4 )) by A35, Def7
.= F₄((x + 1),(f . (x + 1)),(f . ((x + 1) + 1)),(f . ((x + 1) + 2))) by A16, A23, A26 ; :: thesis: verum

end;

end;

end;

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