### The Mizar article:

### Recursive Definitions

**by****Krzysztof Hryniewiecki**

- Received September 4, 1989
Copyright (c) 1989 Association of Mizar Users

- MML identifier: RECDEF_1
- [ MML identifier index ]

environ vocabulary FINSEQ_1, FUNCT_1, RELAT_1, PARTFUN1, TARSKI, ARYTM_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XREAL_0, REAL_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FUNCT_2, DOMAIN_1; constructors REAL_1, NAT_1, FINSEQ_1, FUNCT_2, DOMAIN_1, XREAL_0, MEMBERED, XBOOLE_0; clusters FUNCT_1, RELSET_1, FINSEQ_1, SUBSET_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI; theorems AXIOMS, TARSKI, REAL_1, NAT_1, FUNCT_1, FINSEQ_1, FUNCT_2, RELAT_1, PARTFUN1, CARD_1, XBOOLE_1, XCMPLX_1; schemes NAT_1, FUNCT_1, FUNCT_2, FINSEQ_1; begin reserve n,m,k for Nat, D for non empty set, Z,x,y,z,y1,y2 for set, p,q for FinSequence; Lm1: for p being FinSequence of D st 1 <= n & n <= len p holds p.n is Element of D proof let p be FinSequence of D; assume 1 <= n & n <= len p; then n in Seg len p by FINSEQ_1:3; then n in dom p by FINSEQ_1:def 3; then A1: p.n in rng p by FUNCT_1:def 5; rng p c= D by FINSEQ_1:def 4; hence p.n is Element of D by A1; end; definition let D be set, p be PartFunc of D,NAT; let n be Element of D; redefine func p.n -> Nat; coherence proof per cases; suppose n in dom p; hence p.n is Nat by PARTFUN1:27; suppose not n in dom p; hence p.n is Nat by CARD_1:51,FUNCT_1:def 4; end; end; :::::::::::::::::::::::::::::::::::::::: :: Schemes of existence :: :::::::::::::::::::::::::::::::::::::::: scheme RecEx{A() -> set,P[set,set,set]}: ex f being Function st dom f = NAT & f.0 = A() & for n being Element of NAT holds P[n,f.n,f.(n+1)] provided A1: for n being Nat for x being set ex y being set st P[n,x,y] and A2: for n being Nat for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1=y2 proof deffunc S(Nat) = {k : k <= $1}; A3: for p,q being Function,k st dom p = S(k) & dom q = S(k) & p.0 = q.0 & for n st n < k holds P[n,p.n,p.(n+1)] & P[n,q.n,q.(n+1)] holds p = q proof let p,q be Function;let k; defpred Z[Nat] means $1 <= k implies p.$1 = q.$1; assume A4: dom p = S(k) & dom q = S(k) & p.0 = q.0 & for n st n < k holds P[n,p.n,p.(n+1)] & P[n,q.n,q.(n+1)]; then A5: Z[0]; A6: for n be Nat st Z[n] holds Z[n+1] proof let n; assume A7: n <= k implies p.n = q.n; assume n+1 <= k; then n < k by NAT_1:38; then P[n,p.n,p.(n+1)] & P[n,p.n,q.(n+1)] by A4,A7; hence p.(n+1) = q.(n+1) by A2; end; A8: for n holds Z[n] from Ind(A5,A6); for x st x in S(k) holds p.x = q.x proof let x; assume x in S(k); then ex m st m=x & m <= k; hence p.x = q.x by A8; end; hence p = q by A4,FUNCT_1:9; end; A9: for n ex p being Function st dom p = S(n) & p.0 = A() & for k st k < n holds P[k,p.k,p.(k+1)] proof defpred Z[Nat] means ex p being Function st dom p = S($1) & p.0 = A() & for k st k < $1 holds P[k,p.k,p.(k+1)]; A10: Z[0] proof deffunc F(set)= A(); consider s being Function such that A11: dom s = S(0) & for x st x in S(0) holds s.x = F(x) from Lambda; take s; thus dom s = S(0) by A11; 0 in S(0); hence s.0 = A() by A11; thus thesis by NAT_1:18; end; A12: for n st Z[n] holds Z[n+1] proof let n; given p being Function such that A13: dom p = S(n) & p.0 = A() & for k st k < n holds P[k,p.k,p.(k+1)]; consider z such that A14: P[n,p.n,z] by A1; defpred ST[set,set] means (for k st k=$1 holds (k <= n implies $2 = p.k) & (k=n+1 implies $2 = z )); A15: for x,y1,y2 being set st x in S(n+1) & ST[x,y1] & ST[x,y2] holds y1 = y2 proof let x,y1,y2 be set; assume A16: x in S(n+1) & (for k st k=x holds (k <= n implies y1 = p.k) & (k=n+1 implies y1 = z )) & (for k st k=x holds (k <= n implies y2 = p.k) & (k=n+1 implies y2 = z )); then A17: ex m st m=x & m <= n+1; then reconsider x as Nat; A18: now assume A19: x = n+1; hence y1 = z by A16 .= y2 by A16,A19; end; now assume A20: x <= n; hence y1 = p.x by A16 .= y2 by A16,A20; end; hence thesis by A17,A18,NAT_1:26; end; A21: for x st x in S(n+1) ex y st ST[x,y] proof let x; assume x in S(n+1); then A22: ex m st m=x & m <= n+1; then reconsider t=x as Nat; A23: t = n+1 implies thesis proof assume A24: t=n+1; take z; let k such that A25: k=x; thus k <= n implies z=p.k proof assume k <= n; then n+1 <= n+0 by A24,A25; hence thesis by REAL_1:53; end; thus thesis; end; t <= n implies thesis proof assume A26: t <= n; take p.x; let k; assume A27: k=x; hence k <= n implies p.x = p.k; assume k=n+1; then n+1 <= n+0 by A26,A27; hence thesis by REAL_1:53; end; hence thesis by A22,A23,NAT_1:26; end; consider q being Function such that A28: dom q = S(n+1) & for x st x in S(n+1) holds ST[x,q.x] from FuncEx(A15,A21); take q; thus dom q = S(n+1) by A28; thus q.0 = A() proof 0 <= n+1 by NAT_1:18; then A29: 0 in S(n+1); 0 <= n by NAT_1:18; hence q.0 = A() by A13,A28,A29; end; let k such that A30: k < n+1; A31: now assume A32: k = n; then k+1 in S(n+1); then A33: P[k,p.k,q.(k+1)] by A14,A28,A32; k <= n+1 by A32,NAT_1:29; then k in S(n+1); hence P[k,q.k,q.(k+1)] by A28,A32,A33; end; now assume k <> n; then A34: k+1 <> n+1 by XCMPLX_1:2; A35: k+1 <= n+1 by A30,NAT_1:38; then A36: k+1 <= n by A34,NAT_1:26; A37: k+1 in S(n+1) by A35; A38: k < n by A36,NAT_1:38; then P[k,p.k,p.(k+1)] by A13; then A39: P[k,p.k,q.(k+1)] by A28,A36,A37; k in S(n+1) by A30; hence P[k,q.k,q.(k+1)] by A28,A38,A39; end; hence thesis by A31; end; thus for n holds Z[n] from Ind(A10,A12); end; A40: for p,q being Function,k st dom p = S(k) & dom q = S(k+1) & p.0 = q.0 & for n st n < k holds P[n,p.n,p.(n+1)] & P[n,q.n,q.(n+1)] holds p.k = q.k proof let p,q be Function;let k; defpred Z[Nat] means $1 <= k implies p.$1 = q.$1; assume A41: dom p = S(k) & dom q = S(k+1) & p.0 = q.0 & for n st n < k holds P[n,p.n,p.(n+1)] & P[n,q.n,q.(n+1)]; then A42: Z[0]; A43: for n st Z[n] holds Z[n+1] proof let n; assume A44: n <= k implies p.n = q.n; assume n+1 <= k; then n < k by NAT_1:38; then P[n,p.n,p.(n+1)] & P[n,p.n,q.(n+1)] by A41,A44; hence p.(n+1) = q.(n+1) by A2; end; for n holds Z[n] from Ind(A42,A43); hence p.k = q.k; end; ex f being Function st dom f = NAT & for n ex p being Function st dom p = S(n) & p.0 = A() & (for k st k < n holds P[k,p.k,p.(k+1)]) & f.n = p.n proof defpred Z[set,set] means for n st n=$1 ex p being Function st dom p = S(n) & p.0 = A() & (for k st k < n holds P[k,p.k,p.(k+1)]) & $2 = p.n; A45: for x,y1,y2 being set st x in NAT & Z[x,y1] & Z[x,y2] holds y1 = y2 proof let x,y1,y2 be set; assume A46: x in NAT & (for n st n=x ex p being Function st dom p = S(n) & p.0 = A() & (for k st k < n holds P[k,p.k,p.(k+1)]) & y1 = p.n) & (for n st n=x ex p being Function st dom p = S(n) & p.0 = A() & (for k st k < n holds P[k,p.k,p.(k+1)]) & y2 = p.n); then reconsider n=x as Nat; consider p1 being Function such that A47: dom p1 = S(n) & p1.0 = A() & (for k st k < n holds P[k,p1.k,p1.(k+1)]) & y1 = p1.n by A46; consider p2 being Function such that A48: dom p2 = S(n) & p2.0 = A() & (for k st k < n holds P[k,p2.k,p2.(k+1)]) & y2 = p2.n by A46; for k st k < n holds P[k,p1.k,p1.(k+1)] & P[k,p2.k,p2.(k+1)] by A47,A48; hence y1 = y2 by A3,A47,A48; end; A49: for x st x in NAT ex y st Z[x,y] proof let x; assume x in NAT; then reconsider n=x as Nat; consider p being Function such that A50: dom p = S(n) & p.0 = A() & for k st k < n holds P[k,p.k,p.(k+1)] by A9; take p.n; let k such that A51: k = x; take p; thus thesis by A50,A51; end; consider f being Function such that A52: dom f = NAT & for x st x in NAT holds Z[x,f.x] from FuncEx(A45,A49); take f; thus dom f = NAT by A52; let n; consider p being Function such that A53: dom p = S(n) & p.0 = A() & (for k st k < n holds P[k,p.k,p.(k+1)]) & f.n = p.n by A52; take p; thus dom p = S(n) & p.0 = A() by A53; thus for k st k < n holds P[k,p.k,p.(k+1)] by A53; thus f.n = p.n by A53; end; then consider f being Function such that A54: dom f = NAT & for n ex p being Function st dom p = S(n) & p.0 = A() & (for k st k < n holds P[k,p.k,p.(k+1)]) & f.n = p.n; take f; thus dom f = NAT by A54; thus f.0 = A() proof ex p being Function st dom p = S(0) & p.0 = A() & (for k st k < 0 holds P[k,p.k,p.(k+1)]) & f.0 = p.0 by A54; hence f.0 = A(); end; let d be Element of NAT; consider p being Function such that A55: dom p = S(d+1) & p.0 = A() & (for k st k < d+1 holds P[k,p.k,p.(k+1)]) & f.(d+1) = p.(d+1) by A54; consider q being Function such that A56: dom q = S(d) & q.0 = A() & (for k st k < d holds P[k,q.k,q.(k+1)]) & f.d = q.d by A54; A57: p.d = q.d proof dom p = S(d+1) & dom q = S(d) & p.0 = q.0 & for k st k < d holds P[k,q.k,q.(k+1)] & P[k,p.k,p.(k+1)] proof thus dom p = S(d+1) by A55; thus dom q = S(d) by A56; thus p.0 = q.0 by A55,A56; let k; assume A58: k < d; hence P[k,q.k,q.(k+1)] by A56; d <= d+1 by NAT_1:29; then k < d+1 by A58,AXIOMS:22; hence thesis by A55; end; hence thesis by A40; end; d < d+1 by REAL_1:69; hence thesis by A55,A56,A57; end; scheme RecExD{D()->non empty set,A() -> Element of D(), P[set,set,set]}: ex f being Function of NAT,D() st f.0 = A() & for n being Element of NAT holds P[n,f.n,f.(n+1)] provided A1: for n being Nat for x being Element of D() ex y being Element of D() st P[n,x,y] proof defpred Q[Element of NAT qua non empty set,set,set] means P[$1,$2,$3]; A2: for x being Element of NAT qua non empty set for y being Element of D() ex z being Element of D() st Q[x,y,z] by A1; consider f being Function of [:(NAT qua non empty set),D():],D() such that A3: for x being Element of NAT qua non empty set for y being Element of D() holds Q[x,y,f.[x qua set,y]] from FuncEx2D(A2); defpred P[FinSequence] means ($1.1=A() & for n st n+2 <= len $1 holds $1.(n+2) = f.[n,$1.(n+1)]); consider X being set such that A4: for x holds x in X iff ex p st p in D()* & P[p] & x=p from SepSeq; A5: x in X implies x in D()* proof assume x in X; then ex p st p in D()* & (p.1=A() & for n st n + 2 <= len p holds p.(n+2) = f.[n,p.(n+1)]) & x=p by A4; hence thesis; end; A6: for p,q st p in X & q in X & len p <= len q holds p c= q proof let p,q; assume A7: p in X & q in X & len p <= len q; A8: (p in D()* & p.1 = A() & for n st n + 2 <= len p holds p.(n+2) = f.[n,p.(n+1)]) & (q in D()* & q.1 = A() & for n st n + 2 <= len q holds q.(n+2) = f.[n,q.(n+1)]) proof A9: ex p' being FinSequence st p' in D()* & (p'.1 = A() & for n st n+2<=len p' holds p'.(n+2) = f.[n,p'.(n+1)]) & p=p' by A4,A7; ex q' being FinSequence st q' in D()* & (q'.1 = A() & for n st n+2<=len q' holds q'.(n+2) = f.[n,q'.(n+1)]) & q=q' by A4,A7; hence thesis by A9; end; A10: for n st 1 <= n & n <= len p holds p.n = q.n proof defpred P[Nat] means 1 <= $1 & $1 <= len p & p.$1 <> q.$1; assume A11: ex n st P[n]; consider k such that A12: P[k] & for n st P[n] holds k <= n from Min(A11); k = 1 proof assume A13: k <> 1; 0 <> k by A12; then consider n such that A14: k = n+1 by NAT_1:22; 1 < n+1 by A12,A13,A14,REAL_1:def 5; then A15: 1 <= n by NAT_1:38; A16: n <> 0 by A13,A14; n+0 <= n+1 by REAL_1:55; then A17: n <= len p by A12,A14,AXIOMS:22; A18: n+0 < n+1 by REAL_1:53; consider m such that A19: n=m+1 by A16,NAT_1:22; A20: m+(1+1) <= len p by A12,A14,A19,XCMPLX_1:1; then A21: m+2 <= len q by A7,AXIOMS:22; p.k = p.(m+(1+1)) by A14,A19,XCMPLX_1:1 .=f.[m,p.n] by A8,A19,A20 .=f.[m,q.(m+1)] by A12,A14,A15,A17,A18,A19 .=q.(m+(1+1)) by A8,A21 .=q.k by A14,A19,XCMPLX_1:1; hence thesis by A12; end; hence contradiction by A8,A12; end; now let x; assume x in p; then consider n such that A22: n in dom p & x = [n,p.n] by FINSEQ_1 :16; n in Seg len p by A22,FINSEQ_1:def 3; then A23: 1 <= n & n <= len p by FINSEQ_1:3; then A24: x = [n,q.n] by A10,A22; 1 <= n & n <= len q by A7,A23,AXIOMS:22; then n in Seg len q by FINSEQ_1:3; then n in dom q by FINSEQ_1:def 3; hence x in q by A24,FUNCT_1:8; end; hence thesis by TARSKI:def 3; end; set Y = union X; ex f being Function st f = Y proof defpred Z[set,set] means [$1,$2] in Y; A25: for x,y,z st Z[x,y] & Z[x,z] holds y=z proof let x,y,z; assume A26: [x,y] in Y & [x,z] in Y; then consider Z1 being set such that A27: [x,y] in Z1 & Z1 in X by TARSKI:def 4; Z1 in D()* by A5,A27; then reconsider p=Z1 as FinSequence of D() by FINSEQ_1:def 11; consider Z2 being set such that A28: [x,z] in Z2 & Z2 in X by A26,TARSKI:def 4; Z2 in D()* by A5,A28; then reconsider q=Z2 as FinSequence of D() by FINSEQ_1:def 11; A29: now assume len p <= len q; then p c= Z2 by A6,A27,A28; then [x,y] in q & [x,z] in q by A27,A28; hence y=z by FUNCT_1:def 1; end; now assume len q <= len p; then q c= Z1 by A6,A27,A28; then [x,y] in p & [x,z] in p by A27,A28; hence y=z by FUNCT_1:def 1; end; hence thesis by A29; end; consider h being Function such that A30: for x,y holds [x,y] in h iff x in NAT & Z[x,y] from GraphFunc(A25); take h; A31: for x,y holds [x,y] in h iff [x,y] in Y proof let x,y; thus [x,y] in h implies [x,y] in Y by A30; thus [x,y] in Y implies [x,y] in h proof assume A32: [x,y] in Y; then consider Z such that A33: [x,y] in Z & Z in X by TARSKI:def 4; Z in D()* by A5,A33; then reconsider p=Z as FinSequence of D() by FINSEQ_1:def 11; x in dom p by A33,RELAT_1:def 4; hence thesis by A30,A32; end; end; for x holds x in h iff x in Y proof let x; thus x in h implies x in Y proof assume A34: x in h; then ex y,z st [y,z] = x by RELAT_1:def 1; hence thesis by A31,A34; end; assume A35: x in Y; then consider Z such that A36: x in Z & Z in X by TARSKI:def 4; Z in D()* by A5,A36; then reconsider p=Z as FinSequence of D() by FINSEQ_1:def 11; x in p by A36; then ex y,z st [y,z] = x by RELAT_1:def 1; hence thesis by A31,A35; end; hence h = Y by TARSKI:2; end; then consider g being Function such that A37: g = Y; A38: rng g c= D() proof for x st x in rng g holds x in D() proof let x; assume x in rng g; then consider y such that A39: y in dom g & x = g.y by FUNCT_1:def 5; [y,x] in Y by A37,A39,FUNCT_1:8; then consider Z such that A40: [y,x] in Z & Z in X by TARSKI:def 4; Z in D()* by A5,A40; then reconsider p=Z as FinSequence of D() by FINSEQ_1:def 11; A41: y in dom p by A40,FUNCT_1:8; x = p.y by A40,FUNCT_1:8; then A42: x in rng p by A41,FUNCT_1:def 5; rng p c= D() by FINSEQ_1:def 4; hence x in D() by A42; end; hence thesis by TARSKI:def 3; end; then reconsider h = g as Function of dom g,D() by FUNCT_2:4; A43: for n holds (n+1) in dom h proof defpred P[Nat] means $1+1 in dom h; A44: P[0] proof A45: <*A()*>.1 = A() by FINSEQ_1:def 8; A46: <*A()*> in D()* by FINSEQ_1:def 11; for n st n+2 <= len <*A()*> holds <*A()*>.(n+2) = f.[n,<*A()*>.(n+1)] proof let n; assume n+2 <= len <*A()*>; then n+2 <= 1 by FINSEQ_1:56; then n+(1+1) <= n+1 by NAT_1:37; hence thesis by REAL_1:53; end; then <*A()*> in X by A4,A45,A46; then A47: {[1,A()]} in X by FINSEQ_1:52; [1,A()] in {[1,A()]} by TARSKI:def 1; then [1,A()] in h by A37,A47,TARSKI:def 4; hence 0+1 in dom h by FUNCT_1:8; end; A48: for k st P[k] holds P[k+1] proof let k; assume k+1 in dom h; then [k+1,h.(k+1)] in Y by A37,FUNCT_1:8; then consider Z such that A49: [k+1,h.(k+1)] in Z & Z in X by TARSKI:def 4; Z in D()* by A5,A49; then reconsider Z as FinSequence of D() by FINSEQ_1:def 11; A50: k+1 = len Z implies thesis proof assume A51: k+1 = len Z; set p=Z^<*f.[k,Z.(k+1)]*>; len p = len Z + len <*f.[k,Z.(k+1)]*> by FINSEQ_1:35 .=k+1+1 by A51,FINSEQ_1:56; then 1 <= k+1+1 & k+1+1 <= len p by NAT_1:37; then k+1+1 in Seg len p by FINSEQ_1:3; then k+1+1 in dom p by FINSEQ_1:def 3; then A52: [k+1+1,p.(k+1+1)] in p by FUNCT_1:8; p in X proof 1 <= 1 & 1 <= len Z by A51,NAT_1:37; then 1 in Seg len Z by FINSEQ_1:3; then A53: 1 in dom Z by FINSEQ_1:def 3; Z.1 = A() proof ex p being FinSequence st p in D()* & p.1 = A() & (for n st n+2 <= len p holds p.(n+2) = f.[n,p.(n+1)]) & Z=p by A4,A49; hence thesis; end; then A54: p.1 = A() by A53,FINSEQ_1:def 7; A55: p in D()* proof reconsider n=k as Element of (NAT qua non empty set); Z.(k+1) is Element of D() proof 1 <= k + 1 by NAT_1:37; then k+1 in Seg len Z by A51,FINSEQ_1:3; then k+1 in dom Z by FINSEQ_1:def 3; then A56: Z.(k+1) in rng Z by FUNCT_1:def 5; rng Z c= D() by FINSEQ_1:def 4; hence Z.(k+1) is Element of D() by A56; end; then reconsider z=Z.(k+1) as Element of D(); p= Z^<*f.[n,z]*>; hence thesis by FINSEQ_1:def 11; end; for n st n+2 <= len p holds p.(n+2) = f.[n,p.(n+1)] proof let n;assume n+2 <= len p; then A57: n+2 <= len Z + len <*f.[k,Z.(k+1)]*> by FINSEQ_1:35; then A58: n+2 <= len Z + 1 by FINSEQ_1:57; A59: n+2 = len Z + 1 implies thesis proof assume A60: n+2 = len Z + 1; then n+2 = k+(1+1) by A51,XCMPLX_1:1; then A61: n=k by XCMPLX_1:2; A62: p.(n+2) = <*f.[k,Z.(k+1)]*>.(n+2-len Z) by A57,A60, FINSEQ_1:36 .=<*f.[k,Z.(k+1)]*>.(n+2-(n+2-1)) by A60, XCMPLX_1:26 .=<*f.[k,Z.(k+1)]*>.(n+2-(n+2)+1) by XCMPLX_1: 37 .=<*f.[k,Z.(k+1)]*>.(0+1) by XCMPLX_1:14 .=f.[n,Z.(n+1)] by A61,FINSEQ_1:57; A63: 1 <= n + 1 by NAT_1:37; n+(1+1) <= len Z + 1 by A57,FINSEQ_1:57; then n+1+1 <= len Z + 1 by XCMPLX_1:1; then n+1 <= len Z by REAL_1:53; then n+1 in Seg len Z by A63,FINSEQ_1:3; then n+1 in dom Z by FINSEQ_1:def 3; hence thesis by A62,FINSEQ_1:def 7; end; n+2 <> len Z + 1 implies thesis proof assume A64: n+2 <> len Z + 1; then A65: n+2 <= len Z by A58,NAT_1:26; 1 <= n+(1+1) by NAT_1:37; then n+2 in Seg len Z by A65,FINSEQ_1:3; then A66: n+2 in dom Z by FINSEQ_1:def 3; ex q st q in D()* & q.1 = A() & (for n st n+2 <= len q holds q.(n+2) = f.[n,q.(n+1)]) & Z = q by A4,A49; then Z.(n+2) = f.[n,Z.(n+1)] by A65; then A67: p.(n+2) = f.[n,Z.(n+1)] by A66, FINSEQ_1:def 7; A68: 1 <= n + 1 by NAT_1:37; n+(1+1) <= len Z by A58,A64,NAT_1:26; then n+1+1 <= len Z by XCMPLX_1:1; then n+1+1 <= len Z + 1 by NAT_1:37; then n+1 <= len Z by REAL_1:53; then n+1 in Seg len Z by A68,FINSEQ_1:3; then n+1 in dom Z by FINSEQ_1:def 3; hence thesis by A67,FINSEQ_1:def 7; end; hence thesis by A59; end; hence thesis by A4,A54,A55; end; then [k+1+1,p.(k+1+1)] in h by A37,A52,TARSKI:def 4; hence k+1+1 in dom h by FUNCT_1:8; end; k+1 <> len Z implies thesis proof assume A69: k+1 <> len Z; k+1 in dom Z by A49,FUNCT_1:8; then k+1 in Seg len Z by FINSEQ_1:def 3; then 1 <= k+1 & k+1 <= len Z by FINSEQ_1:3; then k+1 < len Z by A69,REAL_1:def 5; then A70: k+1+1 <= len Z by NAT_1:38; 1 <= k+1+1 by NAT_1:37; then k+1+1 in Seg len Z by A70,FINSEQ_1:3; then k+1+1 in dom Z by FINSEQ_1:def 3; then [k+1+1,Z.(k+1+1)] in Z by FUNCT_1:8; then [k+1+1,Z.(k+1+1)] in h by A37,A49,TARSKI:def 4; hence k+1+1 in dom h by FUNCT_1:8; end; hence thesis by A50; end; thus for k holds P[k] from Ind(A44,A48); end; ex g being Function of NAT,D() st for n holds g.n = h.(n+1) proof ex g being Function st dom g = NAT & for n holds g.n = h.(n+1) proof defpred P[set,set] means ex n st n = $1 & $2=h.(n+1); A71: for x,y1,y2 st x in NAT & P[x,y1] & P[x,y2] holds y1=y2; A72: for x st x in NAT ex y st P[x,y] proof let x; assume x in NAT; then reconsider n=x as Nat; take h.(n+1);take n;thus thesis; end; consider g being Function such that A73: dom g = NAT & for x st x in NAT holds P[x,g.x] from FuncEx(A71,A72); take g; thus dom g = NAT by A73; thus for n holds g.n = h.(n+1) proof let n; ex m st m=n & g.n = h.(m+1) by A73; hence thesis; end; end; then consider g being Function such that A74: dom g = NAT & for n holds g.n = h.(n+1); rng g c= D() proof let x; assume x in rng g; then consider y such that A75: y in dom g & x = g.y by FUNCT_1:def 5; reconsider k=y as Nat by A74,A75; k+1 in dom h by A43; then A76: h.(k+1) in rng h by FUNCT_1:def 5; x=h.(k+1) by A74,A75; hence x in D() by A38,A76; end; then reconsider g as Function of NAT,D() by A74,FUNCT_2:4; take g; thus thesis by A74; end; then consider g being Function of NAT,D() such that A77: for n holds g.n = h.(n+1); take g; A78: for n holds h.(n+2) = f.[n,h.(n+1)] proof let n; (n+1)+1 in dom h by A43; then n+(1+1) in dom h by XCMPLX_1:1; then [n+2,h.(n+2)] in h by FUNCT_1:def 4; then consider Z being set such that A79: [n+2,h.(n+2)] in Z & Z in X by A37,TARSKI:def 4; A80: ex p st p in D()* & (p.1=A() & for n st n+2 <= len p holds p.(n+2) = f.[n,p.(n+1)]) & Z=p by A4,A79; Z in D()* by A5,A79; then reconsider Z as FinSequence of D() by FINSEQ_1:def 11; n+2 in dom Z & h.(n+2) = Z.(n+2) by A79,FUNCT_1:8; then n+2 in Seg len Z by FINSEQ_1:def 3; then A81: n+2 <= len Z by FINSEQ_1:3; A82: 1 <= n+1 by NAT_1:37; n+1 <= n+2 by REAL_1:55; then n+1 <= len Z by A81,AXIOMS:22; then n+1 in Seg len Z by A82,FINSEQ_1:3; then n+1 in dom Z by FINSEQ_1:def 3; then [n+1,Z.(n+1)] in Z by FUNCT_1:8; then A83: [n+1,Z.(n+1)] in h by A37,A79,TARSKI:def 4; thus h.(n+2) = Z.(n+2) by A79,FUNCT_1:8 .= f.[n,Z.(n+1)] by A80,A81 .= f.[n,h.(n+1)] by A83,FUNCT_1:8; end; thus g.0 = A() proof A84: <*A()*> in D()* by FINSEQ_1:def 11; A85: <*A()*>.1 = A() by FINSEQ_1:def 8; for n st n + 2 <= len <*A()*> holds <*A()*>.(n+2) = f.[n,<*A()*>.(n+1)] proof let n; assume n + 2 <= len <*A()*>; then n +(1+1) <= 0 + 1 by FINSEQ_1:56; then n +1+1 <= 0 + 1 by XCMPLX_1:1; then n + 1 <= 0 by REAL_1:53; then n + 1 <= 0 + n by NAT_1:37; hence thesis by REAL_1:53; end; then <*A()*> in X by A4,A84,A85; then A86: {[1,A()]} in X by FINSEQ_1:52; [1,A()] in {[1,A()]} by TARSKI:def 1; then [1,A()] in h by A37,A86,TARSKI:def 4; then A() = h.(0+1) by FUNCT_1:8 .= g.0 by A77; hence thesis; end; let n be Element of NAT; P[n,g.n,f.[n,g.n]] by A3; then A87: P[n,g.n,f.[n,h.(n+1)]] by A77; h.(n+(1+1)) =f.[n,h.(n+1)] by A78; then P[n,g.n,h.(n+1+1)] by A87,XCMPLX_1:1; hence P[n,g.n,g.(n+1)] by A77; end; scheme LambdaRecEx{A() -> set,G(set,set) -> set}: ex f being Function st dom f = NAT & f.0 = A() & for n being Element of NAT holds f.(n+1) = G(n,f.n) proof defpred P[set,set,set] means $3 = G($1,$2); A1: for n being Nat for x being set ex y being set st P[n,x,y]; A2: for n being Nat for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1=y2; consider f being Function such that A3: dom f = NAT & f.0 = A() & for n being Element of NAT holds P[n,f.n,f.(n+1)] from RecEx(A1,A2); take f; thus dom f = NAT & f.0 = A() by A3; thus thesis by A3; end; scheme LambdaRecExD{D() -> non empty set, A() -> Element of D(), G(set,set) -> Element of D()}: ex f being Function of NAT,D() st f.0 = A() & for n being Element of NAT holds f.(n+1) = G(n,f.n) proof defpred P[set,set,set] means $3=G($1,$2); A1: for n being Nat for x being Element of D() ex y being Element of D() st P[n,x,y]; consider f being Function of NAT,D() such that A2: f.0 = A() & for n being Element of NAT holds P[n,f.n,f.(n+1)] from RecExD(A1); take f; thus f.0 = A() by A2; thus for n being (Element of NAT) holds f.(n+1) = G(n,f.n) by A2; end; scheme FinRecEx{A() -> set,N() -> Nat,P[set,set,set]}: ex p being FinSequence st len p = N() & (p.1 = A() or N() = 0) & for n st 1 <= n & n < N() holds P[n,p.n,p.(n+1)] provided A1: for n being Nat st 1 <= n & n < N() for x being set ex y being set st P[n,x,y] and A2: for n being Nat st 1 <= n & n < N() for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2 proof defpred Q[Nat,set,set] means ($1 < N()-1 implies P[$1+1,$2,$3]) & (not $1 < N()-1 implies $3=0); A3: for n being Nat for x being set ex y being set st Q[n,x,y] proof let n be Nat,x be set; n < N()-1 implies thesis proof assume A4: n < N()-1; then A5: n+1 < N() by REAL_1:86; 1 <= n+1 by NAT_1:29; then consider y such that A6: P[n+1,x,y] by A1,A5; take y; thus n < N()-1 implies P[n+1,x,y] by A6; thus thesis by A4; end; hence thesis; end; A7: for n being Nat for x,y1,y2 being set st Q[n,x,y1] & Q[n,x,y2] holds y1 = y2 proof let n be Nat,x,y1,y2 be set; assume A8: (n < N()-1 implies P[n+1,x,y1]) & (not n < N()-1 implies y1=0) & (n < N()-1 implies P[n+1,x,y2]) & (not n < N()-1 implies y2=0); n < N()-1 implies thesis proof assume n < N()-1; then A9: n+1 < N() by REAL_1:86; 1 <= n+1 by NAT_1:29; hence y1 = y2 by A2,A8,A9; end; hence thesis by A8; end; consider f being Function such that A10: dom f = NAT & f.0 = A() & for n being Element of NAT holds Q[n,f.n,f.(n+1)] from RecEx(A3,A7); defpred Q[set,set] means for r being Real st r=$1 holds $2=f.(r-1); A11: for x st x in REAL ex y st Q[x,y] proof let x; assume x in REAL; then reconsider r=x as Real; take f.(r-1); thus thesis; end; A12: for x,y1,y2 st x in REAL & Q[x,y1] & Q[x,y2] holds y1 = y2 proof let x,y1,y2; assume A13: x in REAL & (for r being Real st r=x holds y1=f.(r-1)) & (for r being Real st r=x holds y2=f.(r-1)); then reconsider r = x as Real; thus y1 = f.(r-1) by A13 .= y2 by A13; end; consider g being Function such that A14: dom g = REAL & for x st x in REAL holds Q[x,g.x] from FuncEx(A12,A11); Seg N() c= REAL by XBOOLE_1:1; then A15: dom (g|Seg N()) = Seg N() by A14,RELAT_1:91; then reconsider p = g|Seg N() as FinSequence by FINSEQ_1:def 2; take p; A16: for n being Nat st n < N() holds p.(n+1) = f.n proof let n be Nat such that A17: n < N(); A18: 1 <= n+1 by NAT_1:29; n+1 <= N() by A17,NAT_1:38; then A19: n+1 in Seg N() by A18,FINSEQ_1:3; g.(n+1) = f.(n+1-1) by A14 .= f.(n+(1-1)) by XCMPLX_1:29 .= f.n; hence thesis by A19,FUNCT_1:72; end; thus len p = N() by A15,FINSEQ_1:def 3; thus p.1 = A() or N() = 0 proof N() <> 0 implies thesis proof assume N() <> 0; then consider k such that A20: N() = k+1 by NAT_1:22; 0 <= k by NAT_1:18; then 0 + 1 <= k +1 by REAL_1:55; then 1 in Seg N() by A20,FINSEQ_1:3; then p.1 = g.1 by FUNCT_1:72 .= f.(1-1) by A14 .= A() by A10; hence thesis; end; hence thesis; end; let n; assume A21: 1 <= n & n < N(); then 0 <> n; then consider k such that A22: n = k+1 by NAT_1:22; k < N()-1 by A21,A22,REAL_1:86; then P[k+1,f.k,f.(k+1)] by A10; then A23: P[k+1,f.k,p.(k+1+1)] by A16,A21,A22; k <= k+1 by NAT_1:29; then k < N() by A21,A22,AXIOMS:22; hence P[n,p.n,p.(n+1)] by A16,A22,A23; end; scheme FinRecExD{D() -> non empty set,A() -> Element of D(), N() -> Nat, P[set,set,set]}: ex p being FinSequence of D() st len p = N() & (p.1 = A() or N() = 0) & for n st 1 <= n & n < N() holds P[n,p.n,p.(n+1)] provided A1: for n being Nat st 1 <= n & n < N() holds for x being Element of D() ex y being Element of D() st P[n,x,y] proof consider 00 being Element of D(); defpred Z[Nat,set,set] means ($1 < N()-1 implies P[$1+1,$2,$3]) & (not $1 < N()-1 implies $3=00); A2: for n being Nat for x being Element of D() ex y being Element of D() st Z[n,x,y] proof let n be Nat,x be Element of D(); n < N()-1 implies thesis proof assume A3: n < N()-1; then 1 <= n+1 & n+1 < N() by NAT_1:29,REAL_1:86; then consider y being Element of D() such that A4: P[n+1,x,y] by A1; take y; thus n < N()-1 implies P[n+1,x,y] by A4; thus thesis by A3; end; hence thesis; end; consider f being Function of NAT,D() such that A5: f.0 = A() & for n being Element of NAT holds Z[n,f.n,f.(n+1)] from RecExD(A2); defpred P[set,set] means for r being Real st r = $1 holds $2 = f.(r-1); A6: for x st x in REAL ex y st P[x,y] proof let x; assume x in REAL; then reconsider r=x as Real; take f.(r-1); thus thesis; end; A7: for x,y1,y2 st x in REAL & P[x,y1] & P[x,y2] holds y1 = y2 proof let x,y1,y2; assume A8: x in REAL & (for r being Real st r=x holds y1=f.(r-1)) & (for r being Real st r=x holds y2=f.(r-1)); then reconsider r = x as Real; thus y1 = f.(r-1) by A8 .= y2 by A8; end; consider g being Function such that A9: dom g = REAL & for x st x in REAL holds P[x,g.x] from FuncEx(A7,A6); Seg N() c= REAL by XBOOLE_1:1; then A10: dom (g|Seg N()) = Seg N() by A9,RELAT_1:91; then reconsider p = g|Seg N() as FinSequence by FINSEQ_1:def 2; rng p c= D() proof let x; assume x in rng p; then consider y such that A11: y in dom p & x = p.y by FUNCT_1:def 5; reconsider y as Nat by A11; A12: f.(y-1) in D() proof y <> 0 by A10,A11,FINSEQ_1:3; then consider k such that A13: y = k+1 by NAT_1:22; f.k in D(); hence f.(y-1) in D() by A13,XCMPLX_1:26; end; p.y = g.y by A11,FUNCT_1:70; hence thesis by A9,A11,A12; end; then reconsider p as FinSequence of D() by FINSEQ_1:def 4; take p; A14: for n being Nat st n < N() holds p.(n+1) = f.n proof let n be Nat such that A15: n < N(); A16: 1 <= n+1 by NAT_1:29; n+1 <= N() by A15,NAT_1:38; then A17: n+1 in Seg N() by A16,FINSEQ_1:3; g.(n+1) = f.(n+1-1) by A9 .= f.(n+(1-1)) by XCMPLX_1:29 .= f.n; hence thesis by A17,FUNCT_1:72; end; thus len p = N() by A10,FINSEQ_1:def 3; thus p.1 = A() or N() = 0 proof N() <> 0 implies thesis proof assume N() <> 0; then consider k such that A18: N() = k+1 by NAT_1:22; 0 <= k by NAT_1:18; then 0 + 1 <= k +1 by REAL_1:55; then 1 in Seg N() by A18,FINSEQ_1:3; then p.1 = g.1 by FUNCT_1:72 .= f.(1-1) by A9 .= A() by A5; hence thesis; end; hence thesis; end; let n; assume A19: 1 <= n & n < N(); then 0 <> n; then consider k such that A20: n = k+1 by NAT_1:22; k < N() - 1 by A19,A20,REAL_1:86; then P[k+1,f.k,f.(k+1)] by A5; then A21: P[k+1,f.k,p.(k+1+1)] by A14,A19,A20; k <= k+1 by NAT_1:29; then k < N() by A19,A20,AXIOMS:22; hence P[n,p.n,p.(n+1)] by A14,A20,A21; end; scheme SeqBinOpEx{S() -> FinSequence,P[set,set,set]}: ex x st ex p being FinSequence st x = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds P[S().(k+1),p.k,p.(k+1)] provided A1: for k,x st 1 <= k & k < len S() ex y st P[S().(k+1),x,y] and A2: for k,x,y1,y2,z st 1 <= k & k < len S() & z = S().(k+1) & P[z,x,y1] & P[z,x,y2] holds y1 = y2 proof defpred Q[Nat,set,set] means P[S().($1+1),$2,$3]; A3: for k st 1 <= k & k < len S() for x ex y st Q[k,x,y] by A1; A4: for k st 1 <= k & k < len S() for x,y1,y2 st Q[k,x,y1] & Q[k,x,y2] holds y1 = y2 by A2; consider p such that A5: len p = len S() & (p.1 = S().1 or len S() = 0) & for k st 1 <= k & k < len S() holds Q[k,p.k,p.(k+1)] from FinRecEx(A3,A4); A6: len S() <> 0 implies thesis proof assume A7: len S() <> 0; take p.(len p),p; thus p.(len p) = p.(len p) & len p = len S() & p.1 = S().1 by A5,A7; let k; assume 1 <= k & k < len S(); hence thesis by A5; end; len S() = 0 implies thesis proof assume A8: len S() = 0; take S().0,S(); thus S().0 = S().(len S()) & len S() = len S() & S().1 = S(). 1 by A8; thus thesis by A8,AXIOMS:22; end; hence thesis by A6; end; scheme LambdaSeqBinOpEx{S() -> FinSequence,F(set,set) -> set}: ex x st ex p being FinSequence st x = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds p.(k+1) = F(S().(k+1),p.k) proof defpred P[set,set,set] means $3 = F($1,$2); A1: for k,x st 1 <= k & k < len S() ex y st P[S().(k+1),x,y]; A2: for k,x,y1,y2,z st 1 <= k & k < len S() & z = S().(k+1) & P[z,x,y1] & P[z,x,y2] holds y1 = y2; consider x such that A3: ex p st x = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds P[S().(k+1),p.k,p.(k+1)] from SeqBinOpEx(A1,A2); take x; consider p such that A4: x = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds p.(k+1) = F(S().(k+1),p.k) by A3; take p; thus x = p.(len p) & len p = len S() & p.1 = S().1 by A4; let k; assume 1 <= k & k < len S(); hence p.(k+1) = F(S().(k+1),p.k) by A4; end; :::::::::::::::::::::::::::::::::::::: :: Schemes of uniqueness :: :::::::::::::::::::::::::::::::::::::: scheme RecUn{A() -> set, F, G() -> Function, P[set,set,set]}: F() = G() provided A1: dom F() = NAT & F().0 = A() & for n holds P[n,F().n,F().(n+1)] and A2: dom G() = NAT & G().0 = A() & for n holds P[n,G().n,G().(n+1)] and A3: for n for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2 proof defpred P[Nat] means F().$1 = G().$1; A4: P[0] by A1,A2; A5: for n st P[n] holds P[n+1] proof let n; assume F().n = G().n; then P[n,F().n,F().(n+1)] & P[n,F().n,G().(n+1)] by A1,A2; hence F().(n+1) = G().(n+1) by A3; end; for n holds P[n] from Ind(A4,A5); then for x st x in NAT holds F().x = G().x; hence F() = G() by A1,A2,FUNCT_1:9; end; scheme RecUnD{D() -> non empty set,A() -> Element of D(), P[set,set,set], F, G() -> Function of NAT,D()} : F() = G() provided A1: F().0 = A() & (for n holds P[n,F().n,F().(n+1)]) and A2: G().0 = A() & (for n holds P[n,G().n,G().(n+1)]) and A3: for n being Nat,x,y1,y2 being Element of D() st P[n,x,y1] & P[n,x,y2] holds y1=y2 proof assume A4: F() <> G(); A5: dom F() = NAT by FUNCT_2:def 1; dom G() = NAT by FUNCT_2:def 1; then consider x such that A6: x in NAT & F().x <> G().x by A4,A5,FUNCT_1:9; defpred Q[Nat] means F().$1 <> G().$1; A7: ex k st Q[k] by A6; consider m such that A8: Q[m] & for n st Q[n] holds m <= n from Min(A7); now assume m<>0; then consider k such that A9: m=k+1 by NAT_1:22; k < m by A9,NAT_1:38; then A10: F().k = G().k by A8; P[k,F().k,F().(k+1)] & P[k,G().k,G().(k+1)] by A1,A2; hence contradiction by A3,A8,A9,A10; end; hence contradiction by A1,A2,A8; end; scheme LambdaRecUn{A() -> set, RecFun(set,set) -> set, F, G() -> Function}: F() = G() provided A1: dom F() = NAT & F().0 = A() & for n holds F().(n+1) = RecFun(n,F().n) and A2: dom G() = NAT & G().0 = A() & for n holds G().(n+1) = RecFun(n,G().n) proof defpred P[Nat,set,set] means $3=RecFun($1,$2); A3: dom F() = NAT & F().0 = A() & for n holds P[n,F().n,F().(n+1)] by A1; A4: dom G() = NAT & G().0 = A() & for n holds P[n,G().n,G().(n+1)] by A2; A5: for n being Nat,x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1=y2; thus F() = G() from RecUn(A3,A4,A5); end; scheme LambdaRecUnD{D() -> non empty set,A() -> Element of D(), RecFun(set,set) -> Element of D(), F, G() -> Function of NAT,D()}: F() = G() provided A1: F().0 = A() & for n holds F().(n+1) = RecFun(n,F().n) and A2: G().0 = A() & for n holds G().(n+1) = RecFun(n,G().n) proof defpred P[Nat,set,set] means $3=RecFun($1,$2); A3: F().0 = A() & for n holds P[n,F().n,F().(n+1)] by A1; A4: G().0 = A() & for n holds P[n,G().n,G().(n+1)] by A2; A5: for n being Nat,x,y1,y2 being Element of D() st P[n,x,y1] & P[n,x,y2] holds y1=y2; thus F() = G() from RecUnD(A3,A4,A5); end; scheme LambdaRecUnR{A() -> Real, RecFun(set,set) -> set, F, G() -> Function of NAT,REAL}: F() = G() provided A1: F().0 = A() & for n holds F().(n+1) = RecFun(n,F().n) and A2: G().0 = A() & for n holds G().(n+1) = RecFun(n,G().n) proof defpred P[Nat,set,set] means $3=RecFun($1,$2); A3: F().0 = A() & for n holds P[n,F().n,F().(n+1)] by A1; A4: G().0 = A() & for n holds P[n,G().n,G().(n+1)] by A2; A5: for n being Nat,x,y1,y2 being Element of REAL st P[n,x,y1] & P[n,x,y2] holds y1=y2; thus F() = G() from RecUnD(A3,A4,A5); end; scheme FinRecUn{A() -> set,N() -> Nat, F, G() -> FinSequence, P[set,set,set]}: F() = G() provided A1: for n st 1 <= n & n < N() for x,y1,y2 being set st P[n,x,y1] & P[n,x,y2] holds y1 = y2 and A2: len F() = N() & (F().1 = A() or N() = 0) & for n st 1 <= n & n < N() holds P[n,F().n,F().(n+1)] and A3: len G() = N() & (G().1 = A() or N() = 0) & for n st 1 <= n & n < N() holds P[n,G().n,G().(n+1)] proof A4: dom F() = Seg len G() by A2,A3,FINSEQ_1:def 3 .= dom G() by FINSEQ_1:def 3; assume F() <> G(); then consider x such that A5: x in dom F() & F().x <> G().x by A4,FUNCT_1:9; A6: x in Seg len F() by A5,FINSEQ_1:def 3; reconsider x as Nat by A5; defpred P[Nat] means 1 <= $1 & $1 <= N() & F().$1 <> G().$1; 1 <= x & x <= N() by A2,A6,FINSEQ_1:3; then A7: ex n st P[n] by A5; consider n such that A8: P[n]& for k st P[k] holds n <= k from Min(A7); n <> 1 by A2,A3,A8; then A9: 1 < n by A8,REAL_1:def 5; 0 <> n by A8; then consider k such that A10: n = k+1 by NAT_1:22; A11: 1 <= k by A9,A10,NAT_1:38; k < n by A10,REAL_1:69; then A12: k < N() by A8,AXIOMS:22; n > k by A10,NAT_1:38; then F().k = G().k by A8,A11,A12; then P[k,F().k,F().(k+1)] & P[k,F().k,G().(k+1)] by A2,A3,A11,A12; hence contradiction by A1,A8,A10,A11,A12; end; scheme FinRecUnD{D() -> non empty set, A() -> Element of D(), N() -> Nat, F, G() -> FinSequence of D(), P[set,set,set]}: F() = G() provided A1: for n st 1 <= n & n < N() for x,y1,y2 being Element of D() st P[n,x,y1] & P[n,x,y2] holds y1 = y2 and A2: len F() = N() & (F().1 = A() or N() = 0) & for n st 1 <= n & n < N() holds P[n,F().n,F().(n+1)] and A3: len G() = N() & (G().1 = A() or N() = 0) & for n st 1 <= n & n < N() holds P[n,G().n,G().(n+1)] proof A4: dom F() = Seg len G() by A2,A3,FINSEQ_1:def 3 .= dom G() by FINSEQ_1:def 3; assume F() <> G(); then consider x such that A5: x in dom F() & F().x <> G().x by A4,FUNCT_1:9; A6: x in Seg len F() by A5,FINSEQ_1:def 3; reconsider x as Nat by A5; defpred P[Nat] means 1 <= $1 & $1 <= N() & F().$1 <> G().$1; 1 <= x & x <= N() by A2,A6,FINSEQ_1:3; then A7: ex n st P[n] by A5; consider n such that A8: P[n] & for k st P[k] holds n <= k from Min(A7); n <> 1 by A2,A3,A8; then A9: 1 < n by A8,REAL_1:def 5; 0 <> n by A8; then consider k such that A10: n = k+1 by NAT_1:22; A11: 1 <= k by A9,A10,NAT_1:38; k < n by A10,REAL_1:69; then A12: k < N() by A8,AXIOMS:22; n > k by A10,NAT_1:38; then A13: F().k = G().k by A8,A11,A12; reconsider Fk = F().k as Element of D() by A2,A11,A12,Lm1; reconsider Fk1 = F().(k+1) as Element of D() by A2,A8,A10,Lm1; reconsider Gk1 = G().(k+1) as Element of D() by A3,A8,A10,Lm1; P[k,Fk,Fk1] & P[k,Fk,Gk1] by A2,A3,A11,A12,A13; hence contradiction by A1,A8,A10,A11,A12; end; scheme SeqBinOpUn{S() -> FinSequence,P[set,set,set],x, y() -> set}: x() = y() provided A1: for k,x,y1,y2,z st 1 <= k & k < len S() & z = S().(k+1) & P[z,x,y1] & P[z,x,y2] holds y1 = y2 and A2: ex p being FinSequence st x() = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds P[S().(k+1),p.k,p.(k+1)] and A3: ex p being FinSequence st y() = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds P[S().(k+1),p.k,p.(k+1)] proof defpred Q[Nat,set,set] means P[S().($1+1),$2,$3]; A4: for k st 1 <= k & k < len S() for x,y1,y2 st Q[k,x,y1] & Q[k,x,y2] holds y1 = y2 by A1; consider p such that A5: x() = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds Q[k,p.k,p.(k+1)] by A2; consider q such that A6: y() = q.(len q) & len q = len S() & q.1 = S().1 & for k st 1 <= k & k < len S() holds Q[k,q.k,q.(k+1)] by A3; A7: len p = len S() & (p.1 = S().1 or len S() = 0) & for k st 1 <= k & k < len S() holds Q[k,p.k,p.(k+1)] by A5; A8: len q = len S() & (q.1 = S().1 or len S() = 0) & for k st 1 <= k & k < len S() holds Q[k,q.k,q.(k+1)] by A6; p = q from FinRecUn(A4,A7,A8); hence x() = y() by A5,A6; end; scheme LambdaSeqBinOpUn{S() -> FinSequence, F(set,set) -> set, x, y() -> set}: x() = y() provided A1: ex p being FinSequence st x() = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds p.(k+1) = F(S().(k+1),p.k) and A2: ex p being FinSequence st y() = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds p.(k+1) = F(S().(k+1),p.k) proof defpred P[set,set,set] means $3 = F($1,$2); A3: for k,x,y1,y2,z st 1 <= k & k < len S() & z = S().(k+1) & P[z,x,y1] & P[z,x,y2] holds y1 = y2; A4: ex p st x() = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds P[S().(k+1),p.k,p.(k+1)] by A1; A6: ex p st y() = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds P[S().(k+1),p.k,p.(k+1)] by A2; thus x() = y() from SeqBinOpUn(A3,A4,A6); end; ::::::::::::::::::::::::::::::: :: Schemes of definitness :: ::::::::::::::::::::::::::::::: scheme DefRec{A() -> set,n() -> Nat,P[set,set,set]}: (ex y being set st ex f being Function st y = f.n() & dom f = NAT & f.0 = A() & for n holds P[n,f.n,f.(n+1)]) & for y1,y2 being set st (ex f being Function st y1 = f.n() & dom f = NAT & f.0 = A() & for n holds P[n,f.n,f.(n+1)]) & (ex f being Function st y2 = f.n() & dom f = NAT & f.0 = A() & for n holds P[n,f.n,f.(n+1)]) holds y1 = y2 provided A1: for n,x ex y st P[n,x,y] and A2: for n,x,y1,y2 st P[n,x,y1] & P[n,x,y2] holds y1 = y2 proof defpred Q[set,set,set] means P[$1,$2,$3]; A3: for n,x ex y st Q[n,x,y] by A1; A4: for n,x,y1,y2 st Q[n,x,y1] & Q[n,x,y2] holds y1 = y2 by A2; consider f being Function such that A5: dom f = NAT & f.0 = A() & for n being Element of NAT holds Q[n,f.n,f.(n+1)] from RecEx(A3,A4); thus (ex y being set st ex f being Function st y = f.n() & dom f = NAT & f.0 = A() & for n holds P[n,f.n,f.(n+1)]) proof take f.n(),f; thus f.n() = f.n() & dom f = NAT & f.0 = A() & for n holds P[n,f.n,f.(n+1)] by A5; end; let y1,y2 be set; given f1 being Function such that A6: y1 = f1.n() & dom f1 = NAT & f1.0 = A() & for n holds Q[n,f1.n,f1.(n+1)]; given f2 being Function such that A7: y2 = f2.n() & dom f2 = NAT & f2.0 = A() & for n holds Q[n,f2.n,f2.(n+1)]; A8: dom f1 = NAT & f1.0 = A() & for n holds Q[n,f1.n,f1.(n+1)] by A6; A9: dom f2 = NAT & f2.0 = A() & for n holds Q[n,f2.n,f2.(n+1)] by A7; f1 = f2 from RecUn(A8,A9,A4); hence y1 = y2 by A6,A7; end; scheme LambdaDefRec{A() -> set,n() -> Nat,RecFun(set,set) -> set}: (ex y being set st ex f being Function st y = f.n() & dom f = NAT & f.0 = A() & for n holds f.(n+1) = RecFun(n,f.n)) & for y1,y2 being set st (ex f being Function st y1 = f.n() & dom f = NAT & f.0 = A() & for n holds f.(n+1) = RecFun(n,f.n)) & (ex f being Function st y2 = f.n() & dom f = NAT & f.0 = A() & for n holds f.(n+1) = RecFun(n,f.n)) holds y1 = y2 proof defpred P[set,set,set] means for z st z = $2 holds $3 = RecFun($1,z); A1: for n,x ex y st P[n,x,y] proof let n,x; take RecFun(n,x);let z; assume z = x; hence thesis; end; A2: for n,x,y1,y2 st P[n,x,y1] & P[n,x,y2] holds y1 = y2 proof let n,x,y1,y2; assume A3: (for z st z = x holds y1 = RecFun(n,z)) & for z st z = x holds y2 = RecFun(n,z); hence y1 = RecFun(n,x) .= y2 by A3; end; X: (ex y being set st ex f being Function st y = f.n() & dom f = NAT & f.0 = A() & for n holds P[n,f.n,f.(n+1)] ) & for y1,y2 being set st (ex f being Function st y1 = f.n() & dom f = NAT & f.0 = A() & for n holds P[n,f.n,f.(n+1)] ) & (ex f being Function st y2 = f.n() & dom f = NAT & f.0 = A() & for n holds P[n,f.n,f.(n+1)] ) holds y1 = y2 from DefRec(A1,A2); then consider y being set, f being Function such that W1: y = f.n() & dom f = NAT & f.0 = A() and W2: for n holds P[n,f.n,f.(n+1)]; thus ex y being set st ex f being Function st y = f.n() & dom f = NAT & f.0 = A() & for n holds f.(n+1) = RecFun(n,f.n) proof take y,f; thus thesis by W1,W2; end; let y1,y2 being set; given f1 being Function such that G1: y1 = f1.n() & dom f1 = NAT & f1.0 = A() & for n holds f1.(n+1) = RecFun(n,f1.n); given f2 being Function such that G2: y2 = f2.n() & dom f2 = NAT & f2.0 = A() & for n holds f2.(n+1) = RecFun(n,f2.n); A: for n holds P[n,f1.n,f1.(n+1)] by G1; for n holds P[n,f2.n,f2.(n+1)] by G2; hence y1 = y2 by X,G1,G2,A; end; scheme DefRecD{D() -> non empty set,A() -> (Element of D()), n() -> Nat,P[set,set,set]}: (ex y being Element of D() st ex f being Function of NAT,D() st y = f.n() & f.0 = A() & for n holds P[n,f.n,f.(n+1)]) & for y1,y2 being Element of D() st (ex f being Function of NAT,D() st y1 = f.n() & f.0 = A() & for n holds P[n,f.n,f.(n+1)]) & (ex f being Function of NAT,D() st y2 = f.n() & f.0 = A() & for n holds P[n,f.n,f.(n+1)]) holds y1 = y2 provided A1: for n being Nat,x being Element of D() ex y being Element of D() st P[n,x,y] and A2: for n being Nat, x,y1,y2 being Element of D() st P[n,x,y1] & P[n,x,y2] holds y1 = y2 proof defpred Q[set,set,set] means P[$1,$2,$3]; A3: for n being Nat,x being Element of D() ex y being Element of D() st Q[n,x,y] by A1; consider f being Function of NAT,D() such that A4: f.0 = A() & for n being Element of NAT holds Q[n,f.n,f.(n+1)] from RecExD(A3); thus (ex y being Element of D() st ex f being Function of NAT,D() st y = f.n() & f.0 = A() & for n holds P[n,f.n,f.(n+1)]) proof take f.n(),f; thus f.n() = f.n() & f.0 = A() & for n holds P[n,f.n,f.(n+1)] by A4; end; A5: for n being Nat, x,y1,y2 being Element of D() st Q[n,x,y1] & Q[n,x,y2] holds y1 = y2 by A2; let y1,y2 be Element of D(); given f1 being Function of NAT,D() such that A6: y1 = f1.n() & f1.0 = A() & for n holds Q[n,f1.n,f1.(n+1)]; given f2 being Function of NAT,D() such that A7: y2 = f2.n() & f2.0 = A() & for n holds Q[n,f2.n,f2.(n+1)]; A8: f1.0 = A() & for n holds Q[n,f1.n,f1.(n+1)] by A6; A9: f2.0 = A() & for n holds Q[n,f2.n,f2.(n+1)] by A7; f1 = f2 from RecUnD(A8,A9,A5); hence y1 = y2 by A6,A7; end; scheme LambdaDefRecD{D() -> non empty set, A() -> Element of D(), n() -> Nat, RecFun(set,set) -> Element of D()}: (ex y being Element of D() st ex f being Function of NAT,D() st y = f.n() & f.0 = A() & for n being Nat holds f.(n+1) = RecFun(n,f.n)) & for y1,y2 being Element of D() st (ex f being Function of NAT,D() st y1 = f.n() & f.0 = A() & for n being Nat holds f.(n+1) = RecFun(n,f.n)) & (ex f being Function of NAT,D() st y2 = f.n() & f.0 = A() & for n being Nat holds f.(n+1) = RecFun(n,f.n)) holds y1 = y2 proof defpred Q[set,set,set] means for z being Element of D() st z=$2 holds $3 = RecFun($1,z); A1: for n being Nat,x being Element of D() ex y being Element of D() st Q[n,x,y] proof let n be Nat,x be Element of D();take RecFun(n,x); let z be Element of D(); assume z = x; hence thesis; end; A2: for n being Nat,x,y1,y2 being Element of D() st Q[n,x,y1] & Q[n,x,y2] holds y1 = y2 proof let n be Nat,x,y1,y2 be Element of D();assume A3: (for z being Element of D() st z = x holds y1 = RecFun(n,z)) & for z being Element of D() st z = x holds y2 = RecFun(n,z); hence y1 = RecFun(n,x) .= y2 by A3; end; X: (ex y being Element of D() st ex f being Function of NAT,D() st y = f.n() & f.0 = A() & for n being Nat holds Q[n,f.n,f.(n+1)]) & for y1,y2 being Element of D() st (ex f being Function of NAT,D() st y1 = f.n() & f.0 = A() & for n being Nat holds Q[n,f.n,f.(n+1)]) & (ex f being Function of NAT,D() st y2 = f.n() & f.0 = A() & for n being Nat holds Q[n,f.n,f.(n+1)]) holds y1 = y2 from DefRecD(A1,A2); then consider y being Element of D(), f being Function of NAT,D() such that W1: y = f.n() & f.0 = A() and W2: for n being Nat holds Q[n,f.n,f.(n+1)]; thus ex y being Element of D() st ex f being Function of NAT,D() st y = f.n() & f.0 = A() & for n being Nat holds f.(n+1) = RecFun(n,f.n) proof take y,f; thus thesis by W1,W2; end; let y1,y2 being Element of D(); given f being Function of NAT,D() such that G1: y1 = f.n() & f.0 = A() & for n being Nat holds f.(n+1) = RecFun(n,f.n); given f2 being Function of NAT,D() such that G2: y2 = f2.n() & f2.0 = A() & for n being Nat holds f2.(n+1) = RecFun(n,f2.n); A: for n being Nat holds Q[n,f.n,f.(n+1)] by G1; for n being Nat holds Q[n,f2.n,f2.(n+1)] by G2; hence y1 = y2 by X,A,G1,G2; end; scheme SeqBinOpDef{S() -> FinSequence,P[set,set,set]}: (ex x st ex p being FinSequence st x = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds P[S().(k+1),p.k,p.(k+1)]) & for x,y st (ex p being FinSequence st x = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds P[S().(k+1),p.k,p.(k+1)]) & (ex p being FinSequence st y = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds P[S().(k+1),p.k,p.(k+1)]) holds x = y provided A1: for k,y st 1 <= k & k < len S() ex z st P[S().(k+1),y,z] and A2: for k,x,y1,y2,z st 1 <= k & k < len S() & z = S().(k+1) & P[z,x,y1] & P[z,x,y2] holds y1 = y2 proof defpred Q[set,set,set] means P[$1,$2,$3]; A3: for k,y st 1 <= k & k < len S() ex z st Q[S().(k+1),y,z] by A1; A4: for k,x,y1,y2,z st 1 <= k & k < len S() & z = S().(k+1) & Q[z,x,y1] & Q[z,x,y2] holds y1 = y2 by A2; thus (ex x st ex p being FinSequence st x = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds Q[S().(k+1),p.k,p.(k+1)]) from SeqBinOpEx(A3,A4); let x,y; assume A5: ex p being FinSequence st x = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds Q[S().(k+1),p.k,p.(k+1)]; assume A6: ex p being FinSequence st y = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds Q[S().(k+1),p.k,p.(k+1)]; thus x = y from SeqBinOpUn(A4,A5,A6); end; scheme LambdaSeqBinOpDef{S() -> FinSequence,F(set,set) -> set}: (ex x st ex p being FinSequence st x = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds p.(k+1) = F(S().(k+1),p.k)) & for x,y st (ex p being FinSequence st x = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds p.(k+1) = F(S().(k+1),p.k)) & (ex p being FinSequence st y = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds p.(k+1) = F(S().(k+1),p.k)) holds x = y proof deffunc G(set,set)= F($1,$2); thus (ex x st ex p being FinSequence st x = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds p.(k+1) = G(S().(k+1),p.k)) from LambdaSeqBinOpEx; let x,y; assume A1: ex p being FinSequence st x = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds p.(k+1) = G(S().(k+1),p.k); assume A2: ex p being FinSequence st y = p.(len p) & len p = len S() & p.1 = S().1 & for k st 1 <= k & k < len S() holds p.(k+1) = G(S().(k+1),p.k); thus x = y from LambdaSeqBinOpUn(A1,A2); end;

Back to top