:: Recursive Definitions :: by Krzysztof Hryniewiecki :: :: Received September 4, 1989 :: Copyright (c) 1990-2012 Association of Mizar Users begin Lm1: for n being Element of NAT for D being non empty set for p being FinSequence of D st 1 <= n & n <= len p holds p . n is Element of D proofend; definition let p be natural-valued Function; let n be set ; :: original:. redefine funcp . n -> Element of NAT ; coherence p . n is Element of NAT by ORDINAL1:def_12; end; scheme :: RECDEF_1:sch 1 RecEx{ F1() -> set , P1[ set , set , set ] } : ex f being Function st ( dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) provided A1: for n being Element of NAT for x being set ex y being set st P1[n,x,y] proofend; scheme :: RECDEF_1:sch 2 RecExD{ F1() -> non empty set , F2() -> Element of F1(), P1[ set , set , set ] } : ex f being Function of NAT,F1() st ( f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) provided A1: for n being Element of NAT for x being Element of F1() ex y being Element of F1() st P1[n,x,y] proofend; scheme :: RECDEF_1:sch 3 FinRecEx{ F1() -> set , F2() -> Nat, P1[ set , set , set ] } : ex p being FinSequence st ( len p = F2() & ( p . 1 = F1() or F2() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F2() holds P1[n,p . n,p . (n + 1)] ) ) provided A1: for n being Element of NAT st 1 <= n & n < F2() holds for x being set ex y being set st P1[n,x,y] proofend; scheme :: RECDEF_1:sch 4 FinRecExD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Nat, P1[ set , set , set ] } : ex p being FinSequence of F1() st ( len p = F3() & ( p . 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F3() holds P1[n,p . n,p . (n + 1)] ) ) provided A1: for n being Element of NAT st 1 <= n & n < F3() holds for x being Element of F1() ex y being Element of F1() st P1[n,x,y] proofend; scheme :: RECDEF_1:sch 5 SeqBinOpEx{ F1() -> FinSequence, P1[ set , set , set ] } : ex x being set ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) provided A1: for k being Element of NAT for x being set st 1 <= k & k < len F1() holds ex y being set st P1[F1() . (k + 1),x,y] proofend; scheme :: RECDEF_1:sch 6 LambdaSeqBinOpEx{ F1() -> FinSequence, F2( set , set ) -> set } : ex x being set ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) proofend; scheme :: RECDEF_1:sch 7 FinRecUn{ F1() -> set , F2() -> Nat, F3() -> FinSequence, F4() -> FinSequence, P1[ set , set , set ] } : F3() = F4() provided A1: for n being Element of NAT st 1 <= n & n < F2() holds for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds y1 = y2 and A2: ( len F3() = F2() & ( F3() . 1 = F1() or F2() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F2() holds P1[n,F3() . n,F3() . (n + 1)] ) ) and A3: ( len F4() = F2() & ( F4() . 1 = F1() or F2() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F2() holds P1[n,F4() . n,F4() . (n + 1)] ) ) proofend; scheme :: RECDEF_1:sch 8 FinRecUnD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Nat, F4() -> FinSequence of F1(), F5() -> FinSequence of F1(), P1[ set , set , set ] } : F4() = F5() provided A1: for n being Element of NAT st 1 <= n & n < F3() holds for x, y1, y2 being Element of F1() st P1[n,x,y1] & P1[n,x,y2] holds y1 = y2 and A2: ( len F4() = F3() & ( F4() . 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F3() holds P1[n,F4() . n,F4() . (n + 1)] ) ) and A3: ( len F5() = F3() & ( F5() . 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n < F3() holds P1[n,F5() . n,F5() . (n + 1)] ) ) proofend; scheme :: RECDEF_1:sch 9 SeqBinOpUn{ F1() -> FinSequence, P1[ set , set , set ], F2() -> set , F3() -> set } : F2() = F3() provided A1: for k being Element of NAT for x, y1, y2, z being set st 1 <= k & k < len F1() & z = F1() . (k + 1) & P1[z,x,y1] & P1[z,x,y2] holds y1 = y2 and A2: ex p being FinSequence st ( F2() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) and A3: ex p being FinSequence st ( F3() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) proofend; scheme :: RECDEF_1:sch 10 LambdaSeqBinOpUn{ F1() -> FinSequence, F2( set , set ) -> set , F3() -> set , F4() -> set } : F3() = F4() provided A1: ex p being FinSequence st ( F3() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) and A2: ex p being FinSequence st ( F4() = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) proofend; scheme :: RECDEF_1:sch 11 DefRec{ F1() -> set , F2() -> Nat, P1[ set , set , set ] } : ( ex y being set ex f being Function st ( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being set st ex f being Function st ( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ex f being Function st ( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) holds y1 = y2 ) ) provided A1: for n being Element of NAT for x being set ex y being set st P1[n,x,y] and A2: for n being Element of NAT for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds y1 = y2 proofend; scheme :: RECDEF_1:sch 12 LambdaDefRec{ F1() -> set , F2() -> Nat, F3( set , set ) -> set } : ( ex y being set ex f being Function st ( y = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) & ( for y1, y2 being set st ex f being Function st ( y1 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) & ex f being Function st ( y2 = f . F2() & dom f = NAT & f . 0 = F1() & ( for n being Element of NAT holds f . (n + 1) = F3(n,(f . n)) ) ) holds y1 = y2 ) ) proofend; scheme :: RECDEF_1:sch 13 DefRecD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Nat, P1[ set , set , set ] } : ( ex y being Element of F1() ex f being Function of NAT,F1() st ( y = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ( for y1, y2 being Element of F1() st ex f being Function of NAT,F1() st ( y1 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) & ex f being Function of NAT,F1() st ( y2 = f . F3() & f . 0 = F2() & ( for n being Element of NAT holds P1[n,f . n,f . (n + 1)] ) ) holds y1 = y2 ) ) provided A1: for n being Element of NAT for x being Element of F1() ex y being Element of F1() st P1[n,x,y] and A2: for n being Element of NAT for x, y1, y2 being Element of F1() st P1[n,x,y1] & P1[n,x,y2] holds y1 = y2 proofend; scheme :: RECDEF_1:sch 14 LambdaDefRecD{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Nat, F4( set , set ) -> Element of F1() } : ( ex y being Element of F1() ex f being Function of NAT,F1() st ( y = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) & ( for y1, y2 being Element of F1() st ex f being Function of NAT,F1() st ( y1 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) & ex f being Function of NAT,F1() st ( y2 = f . F3() & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = F4(n,(f . n)) ) ) holds y1 = y2 ) ) proofend; scheme :: RECDEF_1:sch 15 SeqBinOpDef{ F1() -> FinSequence, P1[ set , set , set ] } : ( ex x being set ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) & ( for x, y being set st ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) & ex p being FinSequence st ( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds P1[F1() . (k + 1),p . k,p . (k + 1)] ) ) holds x = y ) ) provided A1: for k being Element of NAT for y being set st 1 <= k & k < len F1() holds ex z being set st P1[F1() . (k + 1),y,z] and A2: for k being Element of NAT for x, y1, y2, z being set st 1 <= k & k < len F1() & z = F1() . (k + 1) & P1[z,x,y1] & P1[z,x,y2] holds y1 = y2 proofend; scheme :: RECDEF_1:sch 16 LambdaSeqBinOpDef{ F1() -> FinSequence, F2( set , set ) -> set } : ( ex x being set ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) & ( for x, y being set st ex p being FinSequence st ( x = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) & ex p being FinSequence st ( y = p . (len p) & len p = len F1() & p . 1 = F1() . 1 & ( for k being Element of NAT st 1 <= k & k < len F1() holds p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) holds x = y ) ) proofend; scheme :: RECDEF_1:sch 17 SeqExD{ F1() -> non empty set , F2() -> Element of NAT , P1[ set , set ] } : ex p being FinSequence of F1() st ( dom p = Seg F2() & ( for k being Element of NAT st k in Seg F2() holds P1[k,p /. k] ) ) provided A1: for k being Element of NAT st k in Seg F2() holds ex x being Element of F1() st P1[k,x] proofend; scheme :: RECDEF_1:sch 18 FinRecExD2{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Element of NAT , P1[ set , set , set ] } : ex p being FinSequence of F1() st ( len p = F3() & ( p /. 1 = F2() or F3() = 0 ) & ( for n being Element of NAT st 1 <= n & n <= F3() - 1 holds P1[n,p /. n,p /. (n + 1)] ) ) provided A1: for n being Element of NAT st 1 <= n & n <= F3() - 1 holds for x being Element of F1() ex y being Element of F1() st P1[n,x,y] proofend;