:: Schemes of Existence of some Types of Functions :: by Jaros{\l}aw Kotowicz :: :: Received September 21, 1990 :: Copyright (c) 1990-2012 Association of Mizar Users begin theorem :: SCHEME1:1 for n being Element of NAT ex m being Element of NAT st ( n = 2 * m or n = (2 * m) + 1 ) proofend; theorem Th2: :: SCHEME1:2 for n being Element of NAT ex m being Element of NAT st ( n = 3 * m or n = (3 * m) + 1 or n = (3 * m) + 2 ) proofend; theorem Th3: :: SCHEME1:3 for n being Element of NAT ex m being Element of NAT st ( n = 4 * m or n = (4 * m) + 1 or n = (4 * m) + 2 or n = (4 * m) + 3 ) proofend; theorem Th4: :: SCHEME1:4 for n being Element of NAT ex m being Element of NAT st ( n = 5 * m or n = (5 * m) + 1 or n = (5 * m) + 2 or n = (5 * m) + 3 or n = (5 * m) + 4 ) proofend; scheme :: SCHEME1:sch 1 ExRealSubseq{ F1() -> Real_Sequence, P1[ set ] } : ex q being Real_Sequence st ( q is subsequence of F1() & ( for n being Element of NAT holds P1[q . n] ) & ( for n being Element of NAT st ( for r being Real st r = F1() . n holds P1[r] ) holds ex m being Element of NAT st F1() . n = q . m ) ) provided A1: for n being Element of NAT ex m being Element of NAT st ( n <= m & P1[F1() . m] ) proofend; scheme :: SCHEME1:sch 2 ExRealSeq2{ F1( set ) -> Real, F2( set ) -> Real } : ex s being Real_Sequence st for n being Element of NAT holds ( s . (2 * n) = F1(n) & s . ((2 * n) + 1) = F2(n) ) proofend; scheme :: SCHEME1:sch 3 ExRealSeq3{ F1( set ) -> Real, F2( set ) -> Real, F3( set ) -> Real } : ex s being Real_Sequence st for n being Element of NAT holds ( s . (3 * n) = F1(n) & s . ((3 * n) + 1) = F2(n) & s . ((3 * n) + 2) = F3(n) ) proofend; scheme :: SCHEME1:sch 4 ExRealSeq4{ F1( set ) -> Real, F2( set ) -> Real, F3( set ) -> Real, F4( set ) -> Real } : ex s being Real_Sequence st for n being Element of NAT holds ( s . (4 * n) = F1(n) & s . ((4 * n) + 1) = F2(n) & s . ((4 * n) + 2) = F3(n) & s . ((4 * n) + 3) = F4(n) ) proofend; scheme :: SCHEME1:sch 5 ExRealSeq5{ F1( set ) -> Real, F2( set ) -> Real, F3( set ) -> Real, F4( set ) -> Real, F5( set ) -> Real } : ex s being Real_Sequence st for n being Element of NAT holds ( s . (5 * n) = F1(n) & s . ((5 * n) + 1) = F2(n) & s . ((5 * n) + 2) = F3(n) & s . ((5 * n) + 3) = F4(n) & s . ((5 * n) + 4) = F5(n) ) proofend; scheme :: SCHEME1:sch 6 PartFuncExD2{ F1() -> non empty set , F2() -> non empty set , P1[ set ], P2[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2() } : ex f being PartFunc of F1(),F2() st ( ( for c being Element of F1() holds ( c in dom f iff ( P1[c] or P2[c] ) ) ) & ( for c being Element of F1() st c in dom f holds ( ( P1[c] implies f . c = F3(c) ) & ( P2[c] implies f . c = F4(c) ) ) ) ) provided A1: for c being Element of F1() st P1[c] holds not P2[c] proofend; scheme :: SCHEME1:sch 7 PartFuncExD29{ F1() -> non empty set , F2() -> non empty set , P1[ set ], P2[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2() } : ex f being PartFunc of F1(),F2() st ( ( for c being Element of F1() holds ( c in dom f iff ( P1[c] or P2[c] ) ) ) & ( for c being Element of F1() st c in dom f holds ( ( P1[c] implies f . c = F3(c) ) & ( P2[c] implies f . c = F4(c) ) ) ) ) provided A1: for c being Element of F1() st P1[c] & P2[c] holds F3(c) = F4(c) proofend; scheme :: SCHEME1:sch 8 PartFuncExD299{ F1() -> non empty set , F2() -> non empty set , P1[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2() } : ex f being PartFunc of F1(),F2() st ( f is total & ( for c being Element of F1() st c in dom f holds ( ( P1[c] implies f . c = F3(c) ) & ( P1[c] implies f . c = F4(c) ) ) ) ) proofend; scheme :: SCHEME1:sch 9 PartFuncExD3{ F1() -> non empty set , F2() -> non empty set , P1[ set ], P2[ set ], P3[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2(), F5( set ) -> Element of F2() } : ex f being PartFunc of F1(),F2() st ( ( for c being Element of F1() holds ( c in dom f iff ( P1[c] or P2[c] or P3[c] ) ) ) & ( for c being Element of F1() st c in dom f holds ( ( P1[c] implies f . c = F3(c) ) & ( P2[c] implies f . c = F4(c) ) & ( P3[c] implies f . c = F5(c) ) ) ) ) provided A1: for c being Element of F1() holds ( ( P1[c] implies not P2[c] ) & ( P1[c] implies not P3[c] ) & ( P2[c] implies not P3[c] ) ) proofend; scheme :: SCHEME1:sch 10 PartFuncExD39{ F1() -> non empty set , F2() -> non empty set , P1[ set ], P2[ set ], P3[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2(), F5( set ) -> Element of F2() } : ex f being PartFunc of F1(),F2() st ( ( for c being Element of F1() holds ( c in dom f iff ( P1[c] or P2[c] or P3[c] ) ) ) & ( for c being Element of F1() st c in dom f holds ( ( P1[c] implies f . c = F3(c) ) & ( P2[c] implies f . c = F4(c) ) & ( P3[c] implies f . c = F5(c) ) ) ) ) provided A1: for c being Element of F1() holds ( ( P1[c] & P2[c] implies F3(c) = F4(c) ) & ( P1[c] & P3[c] implies F3(c) = F5(c) ) & ( P2[c] & P3[c] implies F4(c) = F5(c) ) ) proofend; scheme :: SCHEME1:sch 11 PartFuncExD4{ F1() -> non empty set , F2() -> non empty set , P1[ set ], P2[ set ], P3[ set ], P4[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2(), F5( set ) -> Element of F2(), F6( set ) -> Element of F2() } : ex f being PartFunc of F1(),F2() st ( ( for c being Element of F1() holds ( c in dom f iff ( P1[c] or P2[c] or P3[c] or P4[c] ) ) ) & ( for c being Element of F1() st c in dom f holds ( ( P1[c] implies f . c = F3(c) ) & ( P2[c] implies f . c = F4(c) ) & ( P3[c] implies f . c = F5(c) ) & ( P4[c] implies f . c = F6(c) ) ) ) ) provided A1: for c being Element of F1() holds ( ( P1[c] implies not P2[c] ) & ( P1[c] implies not P3[c] ) & ( P1[c] implies not P4[c] ) & ( P2[c] implies not P3[c] ) & ( P2[c] implies not P4[c] ) & ( P3[c] implies not P4[c] ) ) proofend; scheme :: SCHEME1:sch 12 PartFuncExS2{ F1() -> set , F2() -> set , P1[ set ], P2[ set ], F3( set ) -> set , F4( set ) -> set } : ex f being PartFunc of F1(),F2() st ( ( for x being set holds ( x in dom f iff ( x in F1() & ( P1[x] or P2[x] ) ) ) ) & ( for x being set st x in dom f holds ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) ) ) ) provided A1: for x being set st x in F1() & P1[x] holds not P2[x] and A2: for x being set st x in F1() & P1[x] holds F3(x) in F2() and A3: for x being set st x in F1() & P2[x] holds F4(x) in F2() proofend; scheme :: SCHEME1:sch 13 PartFuncExS3{ F1() -> set , F2() -> set , P1[ set ], P2[ set ], P3[ set ], F3( set ) -> set , F4( set ) -> set , F5( set ) -> set } : ex f being PartFunc of F1(),F2() st ( ( for x being set holds ( x in dom f iff ( x in F1() & ( P1[x] or P2[x] or P3[x] ) ) ) ) & ( for x being set st x in dom f holds ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) & ( P3[x] implies f . x = F5(x) ) ) ) ) provided A1: for x being set st x in F1() holds ( ( P1[x] implies not P2[x] ) & ( P1[x] implies not P3[x] ) & ( P2[x] implies not P3[x] ) ) and A2: for x being set st x in F1() & P1[x] holds F3(x) in F2() and A3: for x being set st x in F1() & P2[x] holds F4(x) in F2() and A4: for x being set st x in F1() & P3[x] holds F5(x) in F2() proofend; scheme :: SCHEME1:sch 14 PartFuncExS4{ F1() -> set , F2() -> set , P1[ set ], P2[ set ], P3[ set ], P4[ set ], F3( set ) -> set , F4( set ) -> set , F5( set ) -> set , F6( set ) -> set } : ex f being PartFunc of F1(),F2() st ( ( for x being set holds ( x in dom f iff ( x in F1() & ( P1[x] or P2[x] or P3[x] or P4[x] ) ) ) ) & ( for x being set st x in dom f holds ( ( P1[x] implies f . x = F3(x) ) & ( P2[x] implies f . x = F4(x) ) & ( P3[x] implies f . x = F5(x) ) & ( P4[x] implies f . x = F6(x) ) ) ) ) provided A1: for x being set st x in F1() holds ( ( P1[x] implies not P2[x] ) & ( P1[x] implies not P3[x] ) & ( P1[x] implies not P4[x] ) & ( P2[x] implies not P3[x] ) & ( P2[x] implies not P4[x] ) & ( P3[x] implies not P4[x] ) ) and A2: for x being set st x in F1() & P1[x] holds F3(x) in F2() and A3: for x being set st x in F1() & P2[x] holds F4(x) in F2() and A4: for x being set st x in F1() & P3[x] holds F5(x) in F2() and A5: for x being set st x in F1() & P4[x] holds F6(x) in F2() proofend; scheme :: SCHEME1:sch 15 PartFuncExCD2{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , P1[ set , set ], P2[ set , set ], F4( set , set ) -> Element of F3(), F5( set , set ) -> Element of F3() } : ex f being PartFunc of [:F1(),F2():],F3() st ( ( for c being Element of F1() for d being Element of F2() holds ( [c,d] in dom f iff ( P1[c,d] or P2[c,d] ) ) ) & ( for c being Element of F1() for d being Element of F2() st [c,d] in dom f holds ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) ) ) ) provided A1: for c being Element of F1() for d being Element of F2() st P1[c,d] holds not P2[c,d] proofend; scheme :: SCHEME1:sch 16 PartFuncExCD3{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , P1[ set , set ], P2[ set , set ], P3[ set , set ], F4( set , set ) -> Element of F3(), F5( set , set ) -> Element of F3(), F6( set , set ) -> Element of F3() } : ex f being PartFunc of [:F1(),F2():],F3() st ( ( for c being Element of F1() for d being Element of F2() holds ( [c,d] in dom f iff ( P1[c,d] or P2[c,d] or P3[c,d] ) ) ) & ( for c being Element of F1() for r being Element of F2() st [c,r] in dom f holds ( ( P1[c,r] implies f . [c,r] = F4(c,r) ) & ( P2[c,r] implies f . [c,r] = F5(c,r) ) & ( P3[c,r] implies f . [c,r] = F6(c,r) ) ) ) ) provided A1: for c being Element of F1() for s being Element of F2() holds ( ( P1[c,s] implies not P2[c,s] ) & ( P1[c,s] implies not P3[c,s] ) & ( P2[c,s] implies not P3[c,s] ) ) proofend; scheme :: SCHEME1:sch 17 PartFuncExCS2{ F1() -> set , F2() -> set , F3() -> set , P1[ set , set ], P2[ set , set ], F4( set , set ) -> set , F5( set , set ) -> set } : ex f being PartFunc of [:F1(),F2():],F3() st ( ( for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] ) ) ) ) & ( for x, y being set st [x,y] in dom f holds ( ( P1[x,y] implies f . [x,y] = F4(x,y) ) & ( P2[x,y] implies f . [x,y] = F5(x,y) ) ) ) ) provided A1: for x, y being set st x in F1() & y in F2() & P1[x,y] holds not P2[x,y] and A2: for x, y being set st x in F1() & y in F2() & P1[x,y] holds F4(x,y) in F3() and A3: for x, y being set st x in F1() & y in F2() & P2[x,y] holds F5(x,y) in F3() proofend; scheme :: SCHEME1:sch 18 PartFuncExCS3{ F1() -> set , F2() -> set , F3() -> set , P1[ set , set ], P2[ set , set ], P3[ set , set ], F4( set , set ) -> set , F5( set , set ) -> set , F6( set , set ) -> set } : ex f being PartFunc of [:F1(),F2():],F3() st ( ( for x, y being set holds ( [x,y] in dom f iff ( x in F1() & y in F2() & ( P1[x,y] or P2[x,y] or P3[x,y] ) ) ) ) & ( for x, y being set st [x,y] in dom f holds ( ( P1[x,y] implies f . [x,y] = F4(x,y) ) & ( P2[x,y] implies f . [x,y] = F5(x,y) ) & ( P3[x,y] implies f . [x,y] = F6(x,y) ) ) ) ) provided A1: for x, y being set st x in F1() & y in F2() holds ( ( P1[x,y] implies not P2[x,y] ) & ( P1[x,y] implies not P3[x,y] ) & ( P2[x,y] implies not P3[x,y] ) ) and A2: for x, y being set st x in F1() & y in F2() & P1[x,y] holds F4(x,y) in F3() and A3: for x, y being set st x in F1() & y in F2() & P2[x,y] holds F5(x,y) in F3() and A4: for x, y being set st x in F1() & y in F2() & P3[x,y] holds F6(x,y) in F3() proofend; scheme :: SCHEME1:sch 19 ExFuncD3{ F1() -> non empty set , F2() -> non empty set , P1[ set ], P2[ set ], P3[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2(), F5( set ) -> Element of F2() } : ex f being Function of F1(),F2() st for c being Element of F1() holds ( ( P1[c] implies f . c = F3(c) ) & ( P2[c] implies f . c = F4(c) ) & ( P3[c] implies f . c = F5(c) ) ) provided A1: for c being Element of F1() holds ( ( P1[c] implies not P2[c] ) & ( P1[c] implies not P3[c] ) & ( P2[c] implies not P3[c] ) ) and A2: for c being Element of F1() holds ( P1[c] or P2[c] or P3[c] ) proofend; scheme :: SCHEME1:sch 20 ExFuncD4{ F1() -> non empty set , F2() -> non empty set , P1[ set ], P2[ set ], P3[ set ], P4[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2(), F5( set ) -> Element of F2(), F6( set ) -> Element of F2() } : ex f being Function of F1(),F2() st for c being Element of F1() holds ( ( P1[c] implies f . c = F3(c) ) & ( P2[c] implies f . c = F4(c) ) & ( P3[c] implies f . c = F5(c) ) & ( P4[c] implies f . c = F6(c) ) ) provided A1: for c being Element of F1() holds ( ( P1[c] implies not P2[c] ) & ( P1[c] implies not P3[c] ) & ( P1[c] implies not P4[c] ) & ( P2[c] implies not P3[c] ) & ( P2[c] implies not P4[c] ) & ( P3[c] implies not P4[c] ) ) and A2: for c being Element of F1() holds ( P1[c] or P2[c] or P3[c] or P4[c] ) proofend; scheme :: SCHEME1:sch 21 FuncExCD2{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , P1[ set , set ], F4( set , set ) -> Element of F3(), F5( set , set ) -> Element of F3() } : ex f being Function of [:F1(),F2():],F3() st for c being Element of F1() for d being Element of F2() st [c,d] in dom f holds ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P1[c,d] implies f . [c,d] = F5(c,d) ) ) proofend; scheme :: SCHEME1:sch 22 FuncExCD3{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , P1[ set , set ], P2[ set , set ], P3[ set , set ], F4( set , set ) -> Element of F3(), F5( set , set ) -> Element of F3(), F6( set , set ) -> Element of F3() } : ex f being Function of [:F1(),F2():],F3() st ( ( for c being Element of F1() for d being Element of F2() holds ( [c,d] in dom f iff ( P1[c,d] or P2[c,d] or P3[c,d] ) ) ) & ( for c being Element of F1() for d being Element of F2() st [c,d] in dom f holds ( ( P1[c,d] implies f . [c,d] = F4(c,d) ) & ( P2[c,d] implies f . [c,d] = F5(c,d) ) & ( P3[c,d] implies f . [c,d] = F6(c,d) ) ) ) ) provided A1: for c being Element of F1() for d being Element of F2() holds ( ( P1[c,d] implies not P2[c,d] ) & ( P1[c,d] implies not P3[c,d] ) & ( P2[c,d] implies not P3[c,d] ) ) and A2: for c being Element of F1() for d being Element of F2() holds ( P1[c,d] or P2[c,d] or P3[c,d] ) proofend;