:: Recursive Definitions. {P}art {II}
:: by Artur Korni{\l}owicz
::
:: Received February 10, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ZFMISC_1, XBOOLE_0, SUBSET_1, FUNCT_1, RELAT_1, FUNCT_4,
TARSKI, CARD_1, ARYTM_3, MCART_1, NAT_1, ARYTM_1, XXREAL_0, FUNCT_7,
RECDEF_2, XTUPLE_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, MCART_1, DOMAIN_1,
ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, NAT_D, RELAT_1, FUNCT_1, FUNCT_2,
FUNCT_4, FUNCT_7, XXREAL_0;
constructors DOMAIN_1, FUNCT_4, XXREAL_0, NAT_1, INT_1, BINARITH, FUNCT_7,
NAT_D, RELSET_1, XTUPLE_0;
registrations SUBSET_1, ORDINAL1, RELSET_1, XREAL_0, NAT_1, INT_1, XTUPLE_0;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0;
expansions TARSKI;
theorems MCART_1, NAT_1, FUNCT_1, FUNCT_2, RELSET_1, INT_1, FUNCT_4, XBOOLE_0,
XBOOLE_1, DOMAIN_1, XREAL_1, XREAL_0, NAT_D, XTUPLE_0, SUBSET_1,
ORDINAL1;
schemes NAT_1, RECDEF_1, FUNCT_1, XBOOLE_0, PARTFUN1;
begin
reserve a,b,c,d,e,z for object, A,B,C,D,E for set;
:: Projections
definition
let x be triple object;
consider x1,x2,x3 being object such that
A1: x = [x1,x2,x3] by XTUPLE_0:def 5;
redefine func x`1_3 means :: redefines `1_3 (XTUPLE_0, definition)
for y1,y2,y3 being object holds x = [y1,y2,y3] implies
it = y1;
compatibility by A1;
redefine func x`2_3 means :: redefines `2_3 (XTUPLE_0, definition)
for y1,y2,y3 being object holds x = [y1,y2,y3] implies
it = y2;
compatibility by A1;
redefine func x`3_3 means :: redefines `3_3 (XTUPLE_0, synonym) → `2 (XTUPLE_0, definition)
for y1,y2,y3 being object holds x = [y1,y2,y3] implies
it = y3;
compatibility by A1;
end;
::$CT
theorem
z in [:A,B,C:] implies z`1_3 in A & z`2_3 in B & z`3_3 in C
proof
assume
A1: z in [:A,B,C:];
then
A2: C is non empty by MCART_1:31;
A3: A is non empty & B is non empty by A1,MCART_1:31;
then consider
a being Element of A, b being Element of B, c being Element of C
such that
A4: z = [a,b,c] by A1,A2,DOMAIN_1:3;
A5: z`3_3 = c by A4;
z`1_3 = a & z`2_3 = b by A4;
hence thesis by A3,A2,A5;
end;
theorem Th3:
z in [:A,B,C:] implies z = [ z`1_3, z`2_3, z`3_3 ]
proof
assume
A1: z in [:A,B,C:];
then
A2: C is non empty by MCART_1:31;
A is non empty & B is non empty by A1,MCART_1:31;
then
ex a being Element of A, b being Element of B, c being Element of C st z
= [a,b,c] by A1,A2,DOMAIN_1:3;
hence thesis;
end;
definition
let x be quadruple object;
consider x1,x2,x3,x4 being object such that
A1: x = [x1,x2,x3,x4] by XTUPLE_0:def 9;
redefine func x`1_4 means :: redefines `1_4 (XTUPLE_0, definition)
for y1,y2,y3,y4 being object holds x = [y1,y2,y3,y4]
implies it = y1;
compatibility by A1;
redefine func x`2_4 means :: redefines `2_4 (XTUPLE_0, definition)
for y1,y2,y3,y4 being object holds x = [y1,y2,y3,y4]
implies it = y2;
compatibility by A1;
redefine func x`3_4 means :: redefines `3_4 (XTUPLE_0, synonym) → `2_3 (XTUPLE_0, definition)
for y1,y2,y3,y4 being object holds x = [y1,y2,y3,y4]
implies it = y3;
compatibility by A1;
redefine func x`4_4 means :: redefines `4_4 (XTUPLE_0, synonym) → `2 (XTUPLE_0, definition)
for y1,y2,y3,y4 being object holds x = [y1,y2,y3,y4]
implies it = y4;
compatibility by A1;
end;
::$CT
theorem
z in [:A,B,C,D:] implies z`1_4 in A & z`2_4 in B & z`3_4 in C & z`4_4 in D
proof
assume
A1: z in [:A,B,C,D:];
then
A2: C is non empty & D is non empty by MCART_1:51;
A3: A is non empty & B is non empty by A1,MCART_1:51;
then consider
a being Element of A, b being Element of B, c being Element of C, d
being Element of D such that
A4: z = [a,b,c,d] by A1,A2,DOMAIN_1:10;
A5: z`3_4 = c & z`4_4 = d by A4;
z`1_4 = a & z`2_4 = b by A4;
hence thesis by A3,A2,A5;
end;
theorem
z in [:A,B,C,D:] implies z = [ z`1_4, z`2_4, z`3_4, z`4_4 ]
proof
assume
A1: z in [:A,B,C,D:];
then
A2: C is non empty & D is non empty by MCART_1:51;
A is non empty & B is non empty by A1,MCART_1:51;
then ex a being Element of A, b being Element of B, c being Element of C, d
being Element of D st z = [a,b,c,d] by A1,A2,DOMAIN_1:10;
hence thesis;
end;
definition
::$CD 5
end;
::$CT 3
:: Conditional schemes
scheme
ExFunc3Cond { C() -> set, P,Q,R[object], F,G,H(object) -> object }:
ex f being
Function st dom f = C() & for c being set st c in C() holds (P[c] implies f.c =
F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c))
provided
A1: for c being set st c in C() holds (P[c] implies not Q[c]) & (P[c]
implies not R[c]) & (Q[c] implies not R[c]) and
A2: for c being set st c in C() holds P[c] or Q[c] or R[c]
proof
consider D1 being set such that
A3: for x being object holds x in D1 iff x in C() & P[x] from XBOOLE_0:sch
1;
consider D3 being set such that
A4: for x being object holds x in D3 iff x in C() & R[x] from XBOOLE_0:sch
1;
consider f1 being Function such that
A5: dom f1 = D1 and
A6: for x being object st x in D1 holds f1.x = F(x) from FUNCT_1:sch 3;
consider D2 being set such that
A7: for x being object holds x in D2 iff x in C() & Q[x] from XBOOLE_0:sch
1;
consider f3 being Function such that
A8: dom f3 = D3 and
A9: for x being object st x in D3 holds f3.x = H(x) from FUNCT_1:sch 3;
consider f2 being Function such that
A10: dom f2 = D2 and
A11: for x being object st x in D2 holds f2.x = G(x) from FUNCT_1:sch 3;
set f = f1 +* f2 +* f3;
take f;
A12: dom f = dom (f1 +* f2) \/ dom f3 by FUNCT_4:def 1
.= dom f1 \/ dom f2 \/ dom f3 by FUNCT_4:def 1;
thus dom f = C()
proof
A13: D3 c= C()
by A4;
A14: D2 c= C()
by A7;
D1 c= C()
by A3;
then D1 \/ D2 c= C() by A14,XBOOLE_1:8;
hence dom f c= C() by A5,A10,A8,A12,A13,XBOOLE_1:8;
let x be object;
assume
A15: x in C();
then P[x] or Q[x] or R[x] by A2;
then x in D1 or x in D2 or x in D3 by A3,A7,A4,A15;
then x in D1 \/ D2 or x in D3 by XBOOLE_0:def 3;
hence thesis by A5,A10,A8,A12,XBOOLE_0:def 3;
end;
let c be set such that
A16: c in C();
hereby
assume
A17: P[c];
not Q[c] by A1,A16,A17;
then
A18: not c in D2 by A7;
not R[c] by A1,A16,A17;
then not c in D3 by A4;
hence f.c = (f1 +* f2).c by A8,FUNCT_4:11
.= f1.c by A10,A18,FUNCT_4:11
.= F(c) by A6,A17,A3,A16;
end;
hereby
assume
A19: Q[c];
not R[c] by A1,A16,A19;
then not c in D3 by A4;
hence f.c = (f1 +* f2).c by A8,FUNCT_4:11
.= f2.c by A10,A19,A7,A16,FUNCT_4:13
.= G(c) by A11,A19,A7,A16;
end;
assume
A20: R[c];
hence f.c = f3.c by A8,A4,A16,FUNCT_4:13
.= H(c) by A9,A20,A4,A16;
end;
scheme
ExFunc4Cond { C() -> set, P,Q,R,S[object], F,G,H,I(object) -> object }:
ex f being
Function st dom f = C() & for c being set st c in C() holds (P[c] implies f.c =
F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c)) & (S[c] implies f
.c = I(c))
provided
A1: for c being set st c in C() holds (P[c] implies not Q[c]) & (P[c]
implies not R[c]) & (P[c] implies not S[c]) & (Q[c] implies not R[c]) & (Q[c]
implies not S[c]) & (R[c] implies not S[c]) and
A2: for c being set st c in C() holds P[c] or Q[c] or R[c] or S[c]
proof
consider D1 being set such that
A3: for x being object holds x in D1 iff x in C() & P[x] from XBOOLE_0:sch
1;
consider D4 being set such that
A4: for x being object holds x in D4 iff x in C() & S[x] from XBOOLE_0:sch
1;
consider f1 being Function such that
A5: dom f1 = D1 and
A6: for x being object st x in D1 holds f1.x = F(x) from FUNCT_1:sch 3;
consider D2 being set such that
A7: for x being object holds x in D2 iff x in C() & Q[x] from XBOOLE_0:sch
1;
consider f2 being Function such that
A8: dom f2 = D2 and
A9: for x being object st x in D2 holds f2.x = G(x) from FUNCT_1:sch 3;
consider D3 being set such that
A10: for x being object holds x in D3 iff x in C() & R[x] from XBOOLE_0:sch
1;
consider f4 being Function such that
A11: dom f4 = D4 and
A12: for x being object st x in D4 holds f4.x = I(x) from FUNCT_1:sch 3;
consider f3 being Function such that
A13: dom f3 = D3 and
A14: for x being object st x in D3 holds f3.x = H(x) from FUNCT_1:sch 3;
set f = f1 +* f2 +* f3 +* f4;
take f;
A15: dom f = dom (f1 +* f2 +* f3) \/ dom f4 by FUNCT_4:def 1
.= dom (f1 +* f2) \/ dom f3 \/ dom f4 by FUNCT_4:def 1
.= dom f1 \/ dom f2 \/ dom f3 \/ dom f4 by FUNCT_4:def 1;
thus dom f = C()
proof
A16: D4 c= C()
by A4;
A17: D3 c= C()
by A10;
A18: D2 c= C()
by A7;
D1 c= C()
by A3;
then D1 \/ D2 c= C() by A18,XBOOLE_1:8;
then D1 \/ D2 \/ D3 c= C() by A17,XBOOLE_1:8;
hence dom f c= C() by A5,A8,A13,A11,A15,A16,XBOOLE_1:8;
let x be object;
assume
A19: x in C();
then P[x] or Q[x] or R[x] or S[x] by A2;
then x in D1 or x in D2 or x in D3 or x in D4 by A3,A7,A10,A4,A19;
then x in D1 \/ D2 or x in D3 or x in D4 by XBOOLE_0:def 3;
then x in D1 \/ D2 \/ D3 or x in D4 by XBOOLE_0:def 3;
hence thesis by A5,A8,A13,A11,A15,XBOOLE_0:def 3;
end;
let c be set such that
A20: c in C();
hereby
assume
A21: P[c];
not R[c] by A1,A20,A21;
then
A22: not c in D3 by A10;
not Q[c] by A1,A20,A21;
then
A23: not c in D2 by A7;
not S[c] by A1,A20,A21;
then not c in D4 by A4;
hence f.c = (f1 +* f2 +* f3).c by A11,FUNCT_4:11
.= (f1 +* f2).c by A13,A22,FUNCT_4:11
.= f1.c by A8,A23,FUNCT_4:11
.= F(c) by A6,A21,A3,A20;
end;
hereby
assume
A24: Q[c];
not R[c] by A1,A20,A24;
then
A25: not c in D3 by A10;
not S[c] by A1,A20,A24;
then not c in D4 by A4;
hence f.c = (f1 +* f2 +* f3).c by A11,FUNCT_4:11
.= (f1 +* f2).c by A13,A25,FUNCT_4:11
.= f2.c by A8,A24,A7,A20,FUNCT_4:13
.= G(c) by A9,A24,A7,A20;
end;
hereby
assume
A26: R[c];
not S[c] by A1,A20,A26;
then not c in D4 by A4;
hence f.c = (f1 +* f2 +* f3).c by A11,FUNCT_4:11
.= f3.c by A13,A26,A10,A20,FUNCT_4:13
.= H(c) by A14,A26,A10,A20;
end;
assume
A27: S[c];
hence f.c = f4.c by A11,A4,A20,FUNCT_4:13
.= I(c) by A12,A27,A4,A20;
end;
:: 1 step
scheme DoubleChoiceRec { A, B() -> non empty set, A0() -> Element of
A(), B0() -> Element of B(), P[object,object,object,object,object] }:
ex f
being sequence of A(), g being sequence of B() st f.0 = A0() & g.0 =
B0() & for n being Nat holds P[n,f.n,g.n,f.(n+1),g.(n+1)] provided
A1: for n being Nat, x being Element of A(), y being Element of B()
ex x1 being Element of A(), y1 being Element of B() st
P[n,x,y,x1,y1] proof defpred P1[set,set,set] means
P[$1,($2)`1,($2)`2,($3)`1,($3)`2];
A2: for n being Nat, x being Element of [:A(),B():] ex y being
Element of [:A(),B():] st P1[n,x,y]
proof
let n be Nat, x be Element of [:A(),B():];
consider ai being Element of A(), bi being Element of B() such that
A3: P[n,x`1,x`2,ai,bi] by A1;
take [ai,bi];
thus thesis by A3;
end;
consider f being sequence of [:A(),B():] such that
A4: f.0 = [A0(),B0()] and
A5: for e being Nat holds P1[e,f.e,f.(e+1)] from RECDEF_1:sch
2( A2);
take pr1 f, pr2 f;
[A0(),B0()]`1 = A0() & [A0(),B0()]`2 = B0();
hence (pr1 f).0 = A0() & (pr2 f).0 = B0() by A4,FUNCT_2:def 5,def 6;
let i be Nat;
A6: (f.(i+1))`1 = (pr1 f).(i+1) & (f.(i+1))`2 = (pr2 f).(i+1) by FUNCT_2:def 5
,def 6;
i in NAT by ORDINAL1:def 12;
then (f.i)`1 = (pr1 f).i & (f.i)`2 = (pr2 f).i by FUNCT_2:def 5,def 6;
hence thesis by A5,A6;
end;
:: 2 steps
scheme
LambdaRec2Ex { A,B() -> set, F(object,object,object) -> object }:
ex f being Function st
dom f = NAT & f.0 = A() & f.1 = B() & for n being Nat holds f.(n+2)
= F(n,f.n,f.(n+1)) proof
defpred C[set] means $1 = 0;
deffunc G(Nat,set) = [$2`2_3, $2`3_3, F($1+1,$2`2_3,$2`3_3)];
set r03 = F(0,A(),B());
set r13 = F(1,B(),r03);
deffunc H(Nat,set) = G($1+1,$2);
consider h being Function such that
dom h = NAT and
A1: h.0 = [ B(), r03, r13 ] and
A2: for n being Nat holds h.(n+1) = H(n,h.n) from NAT_1:sch 11;
deffunc Y(Nat) = h.($1-'1);
deffunc X(set) = [ A(), B(), r03 ];
consider g being Function such that
dom g = NAT and
A3: for x being Element of NAT holds
(C[x] implies g.x = X(x)) & (not C[x] implies g.x = Y(x))
from PARTFUN1:sch 4;
deffunc M(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 = M(x) from FUNCT_1:sch 3;
defpred P[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) = F($1,f.$1,f.($1+1));
A6: g.0 = [ A(), B(), r03 ] by A3;
A7: for n being Nat holds g.(n+2) = G(n+1,g.(n+1))
proof
let n be Nat;
A8: n+2-1 = n+(2-1) & 0 <= n+1;
A9: g.(n+1) = Y(n+1) by A3
.= h.n by NAT_D:34;
thus g.(n+2) = Y(n+2) by A3
.= h.(n+1) by A8,XREAL_0:def 2
.= G(n+1,g.(n+1)) by A2,A9;
end;
then
A10: (g.(0+2))`2_3 = G(0+1,g.(0+1))`2_3
.= (g.(0+1))`3_3;
take f;
thus dom f = NAT by A4;
thus
A11: f.0 = (g.0)`1_3 by A5
.= A() by A6;
A12: g.1 = Y(1) by A3
.= [ B(), r03, r13 ] by A1,XREAL_1:232;
then
A13: (g.(0+1))`1_3 = B()
.= (g.0)`2_3 by A6;
A14: for x being Nat st P[x] holds P[x+1]
proof
let x be Nat;
assume
A15: P[x];
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
.= G(x+1+1,g.(x+1+1))`1_3 by A7
.= (g.(x+1+1))`2_3;
thus (g.(x+1+1))`1_3 = (g.(x+1))`2_3 by A15;
thus (g.(x+1+2))`1_3 = G(x+1+1,g.(x+1+1))`1_3 by A7
.= (g.(x+1))`3_3 by A15;
hence (g.(x+1+2))`1_3 = (g.(x+1+1))`2_3 by A15;
thus (g.(x+1+2))`2_3 = G(x+1+1,g.(x+1+1))`2_3 by A7
.= (g.(x+1+1))`3_3;
per cases;
suppose
A18: x = 0;
hence f.(x+1+2) = (g.(1+2))`1_3 by A5
.= G(1+1,g.(1+1))`1_3 by A7
.= (g.(0+1))`3_3 by A15,A18
.= r13 by A12
.= F(0+1,B(),(g.0)`3_3) by A6
.= F(x+1,f.(x+1),f.(x+1+1)) by A6,A15,A16,A18;
end;
suppose
x <> 0;
then 0 < x;
then
A19: 0+1 <= x by NAT_1:13;
then
A20: x-'1+1 = x by XREAL_1:235;
1-1 <= x-1 by A19,XREAL_1:13;
then
A21: x-1 = x-'1 by XREAL_0:def 2;
x+1 = x-1+2;
hence f.(x+1+2) = G(x-'1+1,g.(x-'1+1))`3_3 by A7,A15,A17,A21
.= F(x+1,f.(x+1),f.(x+1+1)) by A15,A16,A20;
end;
end;
A22: f.(0+2) = (g.(0+2))`1_3 by A5
.= G(0+1,g.(0+1))`1_3 by A7
.= (g.(0+1))`2_3;
thus
A23: f.1 = (g.1)`1_3 by A5
.= B() by A12;
A24: (g.(0+2))`1_3 = G(0+1,g.(0+1))`1_3 by A7
.= (g.1)`2_3
.= r03 by A12
.= (g.0)`3_3 by A6;
then (g.(0+2))`1_3 = r03 by A6
.= (g.(0+1))`2_3 by A12;
then
A25: P[0] by A12,A11,A23,A22,A13,A24,A10;
for x being Nat holds P[x] from NAT_1:sch 2(A25,A14);
hence thesis;
end;
scheme
LambdaRec2ExD { X() -> non empty set, A,B() -> Element of X(),
F(object,object,object) -> Element of X() }:
ex f being sequence of X() st f.0 = A() & f.1 = B()
& for n being Nat holds f.(n+2) = F(n,f.n,f.(n+1)) proof
consider f being Function such that
A1: dom f = NAT and
A2: f.0 = A() & f.1 = B() and
A3: for n being Nat holds f.(n+2) = F(n,f.n,f.(n+1)) from
LambdaRec2Ex;
rng f c= X()
proof
let y be object;
assume y in rng f;
then consider n being object such that
A4: n in dom f and
A5: f.n = y by FUNCT_1:def 3;
reconsider n as Nat by A1,A4;
per cases;
suppose
n <= 1;
then n = 0 or n = 1 by NAT_1:25;
hence thesis by A2,A5;
end;
suppose
n > 1;
then 1+1 <= n by NAT_1:13;
then n-2 in NAT by INT_1:5;
then f.(n-2+2) = F(n-2,f.(n-2),f.(n-2+1)) by A3;
hence thesis by A5;
end;
end;
then f is sequence of X() by A1,FUNCT_2:def 1,RELSET_1:4;
hence thesis by A2,A3;
end;
scheme
LambdaRec2Un { A,B() -> object, F,G() -> Function,
F(object,object,object) -> object }:
F() = G()
provided
A1: dom F() = NAT and
A2: F().0 = A() & F().1 = B() and
A3: for n being Nat holds F().(n+2) = F(n,F().n,F().(n+1)) and
A4: dom G() = NAT and
A5: G().0 = A() & G().1 = B() and
A6: for n being Nat holds G().(n+2) = F(n,G().n,G().(n+1))
proof
defpred Q[Nat] means F().$1 <> G().$1;
assume F() <> G();
then ex x being object st x in NAT & F().x <> G().x by A1,A4,FUNCT_1:2;
then
A7: ex k being Nat st Q[k];
consider m being Nat such that
A8: Q[m] and
A9: for n being Nat st Q[n] holds m <= n from NAT_1:sch 5(A7);
now
set k = m-'2;
A10: F().(k+2) = F(k,F().k,F().(k+1)) & G().(k+2) = F(k,G().k,G().(k+1))
by A3,A6;
assume m <> 0 & m <> 1;
then 1 < m by NAT_1:25;
then 1+1 <= m by NAT_1:13;
then
A11: m = k+2 by XREAL_1:235;
then
A12: F().(k+1) = G().(k+1) by A9,XREAL_1:6;
k+0 < m by A11,XREAL_1:6;
hence contradiction by A8,A9,A11,A12,A10;
end;
hence contradiction by A2,A5,A8;
end;
scheme
LambdaRec2UnD { X() -> non empty set, A,B() -> Element of X(), F,G() ->
sequence of X(), F(object,object,object) -> Element of X() }: F() = G()
provided
A1: F().0 = A() & F().1 = B() and
A2: for n being Nat holds F().(n+2) = F(n,F().n,F().(n+1)) and
A3: G().0 = A() & G().1 = B() and
A4: for n being Nat holds G().(n+2) = F(n,G().n,G().(n+1))
proof
A5: dom G() = NAT by FUNCT_2:def 1;
A6: dom F() = NAT by FUNCT_2:def 1;
thus F() = G() from LambdaRec2Un(A6,A1,A2,A5,A3,A4);
end;
:: 3 steps
scheme
LambdaRec3Ex { A,B,C() -> set, F(object,object,object,object) -> object }:
ex f being
Function st dom f = NAT & f.0 = A() & f.1 = B() & f.2 = C() & for n being
Nat holds f.(n+3) = F(n,f.n,f.(n+1),f.(n+2)) proof
defpred C3[object] means In($1,NAT) > 1;
defpred C2[object] means $1 = 1;
defpred C1[object] means $1 = 0;
deffunc G(Nat,set) = [$2`2_4, $2`3_4, $2`4_4, F($1+1,$2`2_4,$2`3_4,$2`4_4)];
set r04 = F(0,A(),B(),C());
set r14 = F(1,B(),C(),r04);
set r24 = F(2,C(),r04,r14);
deffunc H(Nat,set) = G($1+2,$2);
consider h being Function such that
dom h = NAT and
A1: h.0 = [ C(), r04, r14, r24 ] and
A2: for n being Nat holds h.(n+1) = H(n,h.n) from NAT_1:sch 11;
deffunc X3(object) = h.(In($1,NAT)-'2);
deffunc X2(object) = [ B(), C(), r04, r14 ];
deffunc X1(object) = [ A(), B(), C(), r04 ];
A3: for c being set st c in NAT holds C1[c] or C2[c] or C3[c]
proof
let c be set;
assume c in NAT;
then In(c,NAT) = c by SUBSET_1:def 8;
hence thesis by NAT_1:25;
end;
A4: for c being set st c in NAT holds (C1[c] implies not C2[c]) & (C1[c]
implies not C3[c]) & (C2[c] implies not C3[c]);
consider g being Function such that
dom g = NAT and
A5: for x being set st x in NAT holds (C1[x] implies g.x = X1(x)) & (C2[
x] implies g.x = X2(x)) & (C3[x] implies g.x = X3(x))
from ExFunc3Cond(A4,A3);
A6: g.2 = X3(2) by A5
.= [ C(), r04, r14, r24 ] by A1,XREAL_1:232;
A7: for n being Nat holds g.(n+3) = G(n+2,g.(n+2))
proof
let n be Nat;
0+1 < n+2 by XREAL_1:8;
then
A8: g.(n+2) = X3(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) = X3(n+3) by A5
.= h.(n+1) by A9,XREAL_0:def 2
.= G(n+2,g.(n+2)) by A2,A8;
end;
A10: g.1 = [ B(), C(), r04, r14 ] by A5;
then
A11: (g.(0+1))`3_4 = r04
.= (g.(0+2))`2_4 by A6;
A12: g.0 = [ A(), B(), C(), r04 ] by A5;
then
A13: (g.0)`3_4 = C()
.= (g.(0+1))`2_4 by A10;
A14: (g.(0+1))`4_4 = r14 by A10
.= (g.(0+2))`3_4 by A6;
A15: (g.0)`4_4 = r04 by A12
.= (g.(0+1))`3_4 by A10;
A16: (g.(0+1))`1_4 = B() by A10
.= (g.0)`2_4 by A12;
deffunc M(Nat) = (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 = M(x) from FUNCT_1:sch 4;
A19: f.(0+3) = (g.(0+3))`1_4 by A18
.= G(0+2,g.(0+2))`1_4 by A7
.= (g.(0+2))`2_4;
take f;
thus dom f = NAT by A17;
defpred P[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: (g.(0+2))`2_4 = G(0+2,g.(0+2))`1_4
.= (g.(0+3))`1_4 by A7;
thus
A21: f.0 = (g.0)`1_4 by A18
.= A() by A12;
thus
A22: f.1 = (g.1)`1_4 by A18
.= B() by A10;
thus
A23: f.2 = (g.2)`1_4 by A18
.= C() by A6;
A24: for x being Nat st P[x] holds P[x+1]
proof
let x be Nat;
A25: x+1+2 = x+(1+2);
assume
A26: P[x];
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
.= G(x+1+2,g.(x+1+2))`1_4 by A7
.= (g.(x+1+2))`2_4;
thus (g.(x+1+1))`1_4 = (g.(x+1))`2_4 by A26;
thus (g.(x+1))`3_4 = (g.(x+1+1))`2_4 by A26;
thus (g.(x+1))`4_4 = (g.(x+1+1))`3_4 by A26;
thus (g.(x+1+1))`2_4 = G(x+2,g.(x+2))`1_4
.= (g.(x+1+2))`1_4 by A7,A25;
thus (g.(x+1+1))`3_4 = G(x+2,g.(x+2))`2_4
.= (g.(x+1+2))`2_4 by A7,A25;
thus (g.(x+1+1))`4_4 = G(x+2,g.(x+2))`3_4
.= (g.(x+1+2))`3_4 by A7,A25;
thus (g.(x+1+2))`2_4 = G(x+1+2,g.(x+1+2))`1_4
.= (g.(x+1+3))`1_4 by A7;
per cases;
suppose
x <= 1 & x <> 1;
then
A29: x = 0 by NAT_1:25;
hence f.(x+1+3) = (g.(1+3))`1_4 by A18
.= G(1+2,g.(1+2))`1_4 by A7
.= (g.(0+3))`2_4
.= G(0+2,g.(0+2))`2_4 by A7
.= (g.(0+2))`3_4
.= r14 by A6
.= F(x+1,f.(x+1),f.(x+1+1),f.(x+1+2)) by A12,A22,A23,A26,A29;
end;
suppose
A30: x = 1;
then
A31: f.(x+1+1) = r04 & f.(x+1+2) = r14 by A10,A26,A27;
thus f.(x+1+3) = (g.(1+1+3))`1_4 by A18,A30
.= G(2+2,g.(2+2))`1_4 by A7
.= (g.(1+3))`2_4
.= G(1+2,g.(1+2))`2_4 by A7
.= (g.(0+3))`3_4
.= G(0+2,g.(0+2))`3_4 by A7
.= (g.(0+2))`4_4
.= F(x+1,f.(x+1),f.(x+1+1),f.(x+1+2)) by A6,A23,A30,A31;
end;
suppose
A32: 1 < x;
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
.= G(x+2,g.(x+2))`2_4 by A7
.= (g.(x-'1+3))`3_4 by A33
.= G(x+1,g.(x+1))`3_4 by A7,A33,A37
.= (g.(x-'2+3))`4_4 by A36
.= G(x-'2+2,g.(x-'2+2))`4_4 by A7
.= F(x+1,(g.x)`2_4,(g.x)`3_4,(g.x)`4_4) by A35
.= F(x+1,f.(x+1),f.(x+1+1),f.(x+1+2)) by A18,A26,A27;
end;
end;
(g.(0+1))`2_4 = C() by A10
.= (g.(0+2))`1_4 by A6;
then
A38: P[0] by A6,A21,A22,A23,A19,A16,A13,A15,A11,A14,A20;
for x being Nat holds P[x] from NAT_1:sch 2(A38,A24);
hence thesis;
end;
scheme
LambdaRec3ExD { X() -> non empty set, A,B,C() -> Element of X(),
F(object,object,object,object) -> Element of X() }:
ex f being sequence of X() st f.0 = A() & f.1 = B() & f.2 = C() &
for n being Nat holds f.(n+3) = F(n,f.n,f.(n+1),f.(n+2)) proof
consider f being Function such that
A1: dom f = NAT and
A2: f.0 = A() & f.1 = B() & f.2 = C() and
A3: for n being Nat holds f.(n+3) = F(n,f.n,f.(n+1),f.(n+2))
from LambdaRec3Ex;
rng f c= X()
proof
let y be object;
assume y in rng f;
then consider n being object such that
A4: n in dom f and
A5: f.n = y by FUNCT_1:def 3;
reconsider n as Nat by A1,A4;
per cases;
suppose
n <= 2;
then n = 0 or ... or n = 2;
hence thesis by A2,A5;
end;
suppose
n > 2;
then 2+1 <= n by NAT_1:13;
then n-3 in NAT by INT_1:5;
then f.(n-3+3) = F(n-3,f.(n-3),f.(n-3+1),f.(n-3+2)) by A3;
hence thesis by A5;
end;
end;
then f is sequence of X() by A1,FUNCT_2:def 1,RELSET_1:4;
hence thesis by A2,A3;
end;
scheme
LambdaRec3Un { A,B,C() -> object, F,G() -> Function,
F(object,object,object,object) -> object }: F() = G()
provided
A1: dom F() = NAT and
A2: F().0 = A() & F().1 = B() & F().2 = C() and
A3: for n being Nat holds F().(n+3) = F(n,F().n,F().(n+1),F()
.(n+2)) and
A4: dom G() = NAT and
A5: G().0 = A() & G().1 = B() & G().2 = C() and
A6: for n being Nat holds G().(n+3) = F(n,G().n,G().(n+1),G()
.(n+2))
proof
defpred Q[Nat] means F().$1 <> G().$1;
assume F() <> G();
then ex x being object st x in NAT & F().x <> G().x by A1,A4,FUNCT_1:2;
then
A7: ex k being Nat st Q[k];
consider m being Nat such that
A8: Q[m] and
A9: for n being Nat st Q[n] holds m <= n from NAT_1:sch 5(A7);
now
set k = m-'3;
A10: F().(k+3) = F(k,F().k,F().(k+1),F().(k+2)) & G().(k+3) = F(k,G().k,G(
).(k+1) ,G().(k+2)) by A3,A6;
assume m <> 0 & ... & m <> 2;
then 2 < m;
then 2+1 <= m by NAT_1:13;
then
A11: m = k+3 by XREAL_1:235;
then
A12: F().(k+1) = G().(k+1) by A9,XREAL_1:6;
A13: F().(k+2) = G().(k+2) by A9,A11,XREAL_1:6;
k+0 < m by A11,XREAL_1:6;
hence contradiction by A8,A9,A11,A12,A13,A10;
end;
hence contradiction by A2,A5,A8;
end;
scheme
LambdaRec3UnD { X() -> non empty set, A,B,C() -> Element of X(), F,G() ->
sequence of X(), F(object,object,object,object) -> Element of X() }:
F() = G()
provided
A1: F().0 = A() & F().1 = B() & F().2 = C() and
A2: for n being Nat holds F().(n+3) = F(n,F().n,F().(n+1),F()
.(n+2)) and
A3: G().0 = A() & G().1 = B() & G().2 = C() and
A4: for n being Nat holds G().(n+3) = F(n,G().n,G().(n+1),G()
.(n+2))
proof
A5: dom G() = NAT by FUNCT_2:def 1;
A6: dom F() = NAT by FUNCT_2:def 1;
thus F() = G() from LambdaRec3Un(A6,A1,A2,A5,A3,A4);
end;
:: 4 steps
scheme
LambdaRec4Un { A,B,C,D() -> object, F,G() -> Function,
F(object,object,object,object,object) -> object }: F() = G()
provided
A1: dom F() = NAT and
A2: F().0 = A() & F().1 = B() & F().2 = C() & F().3 = D() and
A3: for n being Nat holds F().(n+4) = F(n,F().n,F().(n+1),F()
.(n+2),F().(n+3)) and
A4: dom G() = NAT and
A5: G().0 = A() & G().1 = B() & G().2 = C() & G().3 = D() and
A6: for n being Nat holds G().(n+4) = F(n,G().n,G().(n+1),G()
.(n+2),G().(n+3))
proof
defpred Q[Nat] means F().$1 <> G().$1;
assume F() <> G();
then ex x being object st x in NAT & F().x <> G().x by A1,A4,FUNCT_1:2;
then
A7: ex k being Nat st Q[k];
consider m being Nat such that
A8: Q[m] and
A9: for n being Nat st Q[n] holds m <= n from NAT_1:sch 5(A7);
now
set k = m-'4;
A10: F().(k+4) = F(k,F().k,F().(k+1),F().(k+2),F().(k+3)) & G().(k+4) = F(
k,G().k,G().(k+1),G().(k+2),G().(k+3)) by A3,A6;
assume m <> 0 & ... & m <> 3;
then 3 < m;
then 3+1 <= m by NAT_1:13;
then
A11: m = k+4 by XREAL_1:235;
then
A12: F().(k+1) = G().(k+1) by A9,XREAL_1:6;
k+3 < m by A11,XREAL_1:6;
then
A13: F().(k+3) = G().(k+3) by A9;
k+2 < m by A11,XREAL_1:6;
then
A14: F().(k+2) = G().(k+2) by A9;
k+0 < m by A11,XREAL_1:6;
hence contradiction by A8,A9,A11,A12,A14,A13,A10;
end;
hence contradiction by A2,A5,A8;
end;
scheme
LambdaRec4UnD { X() -> non empty set, A,B,C,D() -> Element of X(), F,G() ->
sequence of X(), F(object,object,object,object,object) -> Element of X() }:
F() = G()
provided
A1: F().0 = A() & F().1 = B() & F().2 = C() & F().3 = D() and
A2: for n being Nat holds F().(n+4) = F(n,F().n,F().(n+1),F()
.(n+2),F().(n+3)) and
A3: G().0 = A() & G().1 = B() & G().2 = C() & G().3 = D() and
A4: for n being Nat holds G().(n+4) = F(n,G().n,G().(n+1),G()
.(n+2),G().(n+3))
proof
A5: dom G() = NAT by FUNCT_2:def 1;
A6: dom F() = NAT by FUNCT_2:def 1;
thus F() = G() from LambdaRec4Un(A6,A1,A2,A5,A3,A4);
end;
begin :: Addenda
:: 2010.05.120, A.T.
theorem
for x,y,X,Y,Z being set
st x`1_3 = y`1_3 & x`2_3 = y`2_3 & x`3_3 = y`3_3 &
y in [:X,Y,Z:] & x in [:X,Y,Z:]
holds x = y
proof
let x,y,X,Y,Z be set;
assume
A1: x`1_3 = y`1_3 & x`2_3 = y`2_3 & x`3_3 = y`3_3 & y in [:X,Y,Z:];
assume x in [:X,Y,Z:];
hence x = [ x`1_3, x`2_3, x`3_3 ] by Th3
.= y by A1,Th3;
end;