:: SCHEME1 semantic presentation

theorem Th1: :: SCHEME1:1
for b1 being Nat ex b2 being Nat st
( b1 = 2 * b2 or b1 = (2 * b2) + 1 )
proof end;

theorem Th2: :: SCHEME1:2
for b1 being Nat ex b2 being Nat st
( b1 = 3 * b2 or b1 = (3 * b2) + 1 or b1 = (3 * b2) + 2 )
proof end;

theorem Th3: :: SCHEME1:3
for b1 being Nat ex b2 being Nat st
( b1 = 4 * b2 or b1 = (4 * b2) + 1 or b1 = (4 * b2) + 2 or b1 = (4 * b2) + 3 )
proof end;

theorem Th4: :: SCHEME1:4
for b1 being Nat ex b2 being Nat st
( b1 = 5 * b2 or b1 = (5 * b2) + 1 or b1 = (5 * b2) + 2 or b1 = (5 * b2) + 3 or b1 = (5 * b2) + 4 )
proof end;

scheme :: SCHEME1:sch 1
s1{ F1() -> Real_Sequence, P1[ set ] } :
ex b1 being Real_Sequence st
( b1 is subsequence of F1() & ( for b2 being Nat holds P1[b1 . b2] ) & ( for b2 being Nat st ( for b3 being Real st b3 = F1() . b2 holds
P1[b3] ) holds
ex b3 being Nat st F1() . b2 = b1 . b3 ) )
provided
E4: for b1 being Nat ex b2 being Nat st
( b1 <= b2 & P1[F1() . b2] )
proof end;

scheme :: SCHEME1:sch 2
s2{ F1( set ) -> Real, F2( set ) -> Real } :
ex b1 being Real_Sequence st
for b2 being Nat holds
( b1 . (2 * b2) = F1(b2) & b1 . ((2 * b2) + 1) = F2(b2) )
proof end;

scheme :: SCHEME1:sch 3
s3{ F1( set ) -> Real, F2( set ) -> Real, F3( set ) -> Real } :
ex b1 being Real_Sequence st
for b2 being Nat holds
( b1 . (3 * b2) = F1(b2) & b1 . ((3 * b2) + 1) = F2(b2) & b1 . ((3 * b2) + 2) = F3(b2) )
proof end;

scheme :: SCHEME1:sch 4
s4{ F1( set ) -> Real, F2( set ) -> Real, F3( set ) -> Real, F4( set ) -> Real } :
ex b1 being Real_Sequence st
for b2 being Nat holds
( b1 . (4 * b2) = F1(b2) & b1 . ((4 * b2) + 1) = F2(b2) & b1 . ((4 * b2) + 2) = F3(b2) & b1 . ((4 * b2) + 3) = F4(b2) )
proof end;

scheme :: SCHEME1:sch 5
s5{ F1( set ) -> Real, F2( set ) -> Real, F3( set ) -> Real, F4( set ) -> Real, F5( set ) -> Real } :
ex b1 being Real_Sequence st
for b2 being Nat holds
( b1 . (5 * b2) = F1(b2) & b1 . ((5 * b2) + 1) = F2(b2) & b1 . ((5 * b2) + 2) = F3(b2) & b1 . ((5 * b2) + 3) = F4(b2) & b1 . ((5 * b2) + 4) = F5(b2) )
proof end;

scheme :: SCHEME1:sch 6
s6{ F1() -> non empty set , F2() -> non empty set , P1[ set ], P2[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2() } :
ex b1 being PartFunc of F1(),F2() st
( ( for b2 being Element of F1() holds
( b2 in dom b1 iff ( P1[b2] or P2[b2] ) ) ) & ( for b2 being Element of F1() st b2 in dom b1 holds
( ( P1[b2] implies b1 . b2 = F3(b2) ) & ( P2[b2] implies b1 . b2 = F4(b2) ) ) ) )
provided
E4: for b1 being Element of F1() st P1[b1] holds
not P2[b1]
proof end;

scheme :: SCHEME1:sch 7
s7{ F1() -> non empty set , F2() -> non empty set , P1[ set ], P2[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2() } :
ex b1 being PartFunc of F1(),F2() st
( ( for b2 being Element of F1() holds
( b2 in dom b1 iff ( P1[b2] or P2[b2] ) ) ) & ( for b2 being Element of F1() st b2 in dom b1 holds
( ( P1[b2] implies b1 . b2 = F3(b2) ) & ( P2[b2] implies b1 . b2 = F4(b2) ) ) ) )
provided
E4: for b1 being Element of F1() st P1[b1] & P2[b1] holds
F3(b1) = F4(b1)
proof end;

scheme :: SCHEME1:sch 8
s8{ F1() -> non empty set , F2() -> non empty set , P1[ set ], F3( set ) -> Element of F2(), F4( set ) -> Element of F2() } :
ex b1 being PartFunc of F1(),F2() st
( b1 is total & ( for b2 being Element of F1() st b2 in dom b1 holds
( ( P1[b2] implies b1 . b2 = F3(b2) ) & ( P1[b2] implies b1 . b2 = F4(b2) ) ) ) )
proof end;

scheme :: SCHEME1:sch 9
s9{ 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 b1 being PartFunc of F1(),F2() st
( ( for b2 being Element of F1() holds
( b2 in dom b1 iff ( P1[b2] or P2[b2] or P3[b2] ) ) ) & ( for b2 being Element of F1() st b2 in dom b1 holds
( ( P1[b2] implies b1 . b2 = F3(b2) ) & ( P2[b2] implies b1 . b2 = F4(b2) ) & ( P3[b2] implies b1 . b2 = F5(b2) ) ) ) )
provided
E4: for b1 being Element of F1() holds
( ( P1[b1] implies not P2[b1] ) & ( P1[b1] implies not P3[b1] ) & ( P2[b1] implies not P3[b1] ) )
proof end;

scheme :: SCHEME1:sch 10
s10{ 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 b1 being PartFunc of F1(),F2() st
( ( for b2 being Element of F1() holds
( b2 in dom b1 iff ( P1[b2] or P2[b2] or P3[b2] ) ) ) & ( for b2 being Element of F1() st b2 in dom b1 holds
( ( P1[b2] implies b1 . b2 = F3(b2) ) & ( P2[b2] implies b1 . b2 = F4(b2) ) & ( P3[b2] implies b1 . b2 = F5(b2) ) ) ) )
provided
E4: for b1 being Element of F1() holds
( ( P1[b1] & P2[b1] implies F3(b1) = F4(b1) ) & ( P1[b1] & P3[b1] implies F3(b1) = F5(b1) ) & ( P2[b1] & P3[b1] implies F4(b1) = F5(b1) ) )
proof end;

scheme :: SCHEME1:sch 11
s11{ 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 b1 being PartFunc of F1(),F2() st
( ( for b2 being Element of F1() holds
( b2 in dom b1 iff ( P1[b2] or P2[b2] or P3[b2] or P4[b2] ) ) ) & ( for b2 being Element of F1() st b2 in dom b1 holds
( ( P1[b2] implies b1 . b2 = F3(b2) ) & ( P2[b2] implies b1 . b2 = F4(b2) ) & ( P3[b2] implies b1 . b2 = F5(b2) ) & ( P4[b2] implies b1 . b2 = F6(b2) ) ) ) )
provided
E4: for b1 being Element of F1() holds
( ( P1[b1] implies not P2[b1] ) & ( P1[b1] implies not P3[b1] ) & ( P1[b1] implies not P4[b1] ) & ( P2[b1] implies not P3[b1] ) & ( P2[b1] implies not P4[b1] ) & ( P3[b1] implies not P4[b1] ) )
proof end;

scheme :: SCHEME1:sch 12
s12{ F1() -> set , F2() -> set , P1[ set ], P2[ set ], F3( set ) -> set , F4( set ) -> set } :
ex b1 being PartFunc of F1(),F2() st
( ( for b2 being set holds
( b2 in dom b1 iff ( b2 in F1() & ( P1[b2] or P2[b2] ) ) ) ) & ( for b2 being set st b2 in dom b1 holds
( ( P1[b2] implies b1 . b2 = F3(b2) ) & ( P2[b2] implies b1 . b2 = F4(b2) ) ) ) )
provided
E4: for b1 being set st b1 in F1() & P1[b1] holds
not P2[b1] and
E5: for b1 being set st b1 in F1() & P1[b1] holds
F3(b1) in F2() and
E6: for b1 being set st b1 in F1() & P2[b1] holds
F4(b1) in F2()
proof end;

scheme :: SCHEME1:sch 13
s13{ F1() -> set , F2() -> set , P1[ set ], P2[ set ], P3[ set ], F3( set ) -> set , F4( set ) -> set , F5( set ) -> set } :
ex b1 being PartFunc of F1(),F2() st
( ( for b2 being set holds
( b2 in dom b1 iff ( b2 in F1() & ( P1[b2] or P2[b2] or P3[b2] ) ) ) ) & ( for b2 being set st b2 in dom b1 holds
( ( P1[b2] implies b1 . b2 = F3(b2) ) & ( P2[b2] implies b1 . b2 = F4(b2) ) & ( P3[b2] implies b1 . b2 = F5(b2) ) ) ) )
provided
E4: for b1 being set st b1 in F1() holds
( ( P1[b1] implies not P2[b1] ) & ( P1[b1] implies not P3[b1] ) & ( P2[b1] implies not P3[b1] ) ) and
E5: for b1 being set st b1 in F1() & P1[b1] holds
F3(b1) in F2() and
E6: for b1 being set st b1 in F1() & P2[b1] holds
F4(b1) in F2() and
E7: for b1 being set st b1 in F1() & P3[b1] holds
F5(b1) in F2()
proof end;

scheme :: SCHEME1:sch 14
s14{ 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 b1 being PartFunc of F1(),F2() st
( ( for b2 being set holds
( b2 in dom b1 iff ( b2 in F1() & ( P1[b2] or P2[b2] or P3[b2] or P4[b2] ) ) ) ) & ( for b2 being set st b2 in dom b1 holds
( ( P1[b2] implies b1 . b2 = F3(b2) ) & ( P2[b2] implies b1 . b2 = F4(b2) ) & ( P3[b2] implies b1 . b2 = F5(b2) ) & ( P4[b2] implies b1 . b2 = F6(b2) ) ) ) )
provided
E4: for b1 being set st b1 in F1() holds
( ( P1[b1] implies not P2[b1] ) & ( P1[b1] implies not P3[b1] ) & ( P1[b1] implies not P4[b1] ) & ( P2[b1] implies not P3[b1] ) & ( P2[b1] implies not P4[b1] ) & ( P3[b1] implies not P4[b1] ) ) and
E5: for b1 being set st b1 in F1() & P1[b1] holds
F3(b1) in F2() and
E6: for b1 being set st b1 in F1() & P2[b1] holds
F4(b1) in F2() and
E7: for b1 being set st b1 in F1() & P3[b1] holds
F5(b1) in F2() and
E8: for b1 being set st b1 in F1() & P4[b1] holds
F6(b1) in F2()
proof end;

scheme :: SCHEME1:sch 15
s15{ 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 b1 being PartFunc of [:F1(),F2():],F3() st
( ( for b2 being Element of F1()
for b3 being Element of F2() holds
( [b2,b3] in dom b1 iff ( P1[b2,b3] or P2[b2,b3] ) ) ) & ( for b2 being Element of F1()
for b3 being Element of F2() st [b2,b3] in dom b1 holds
( ( P1[b2,b3] implies b1 . [b2,b3] = F4(b2,b3) ) & ( P2[b2,b3] implies b1 . [b2,b3] = F5(b2,b3) ) ) ) )
provided
E4: for b1 being Element of F1()
for b2 being Element of F2() st P1[b1,b2] holds
not P2[b1,b2]
proof end;

scheme :: SCHEME1:sch 16
s16{ 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 b1 being PartFunc of [:F1(),F2():],F3() st
( ( for b2 being Element of F1()
for b3 being Element of F2() holds
( [b2,b3] in dom b1 iff ( P1[b2,b3] or P2[b2,b3] or P3[b2,b3] ) ) ) & ( for b2 being Element of F1()
for b3 being Element of F2() st [b2,b3] in dom b1 holds
( ( P1[b2,b3] implies b1 . [b2,b3] = F4(b2,b3) ) & ( P2[b2,b3] implies b1 . [b2,b3] = F5(b2,b3) ) & ( P3[b2,b3] implies b1 . [b2,b3] = F6(b2,b3) ) ) ) )
provided
E4: for b1 being Element of F1()
for b2 being Element of F2() holds
( ( P1[b1,b2] implies not P2[b1,b2] ) & ( P1[b1,b2] implies not P3[b1,b2] ) & ( P2[b1,b2] implies not P3[b1,b2] ) )
proof end;

scheme :: SCHEME1:sch 17
s17{ F1() -> set , F2() -> set , F3() -> set , P1[ set , set ], P2[ set , set ], F4( set , set ) -> set , F5( set , set ) -> set } :
ex b1 being PartFunc of [:F1(),F2():],F3() st
( ( for b2, b3 being set holds
( [b2,b3] in dom b1 iff ( b2 in F1() & b3 in F2() & ( P1[b2,b3] or P2[b2,b3] ) ) ) ) & ( for b2, b3 being set st [b2,b3] in dom b1 holds
( ( P1[b2,b3] implies b1 . [b2,b3] = F4(b2,b3) ) & ( P2[b2,b3] implies b1 . [b2,b3] = F5(b2,b3) ) ) ) )
provided
E4: for b1, b2 being set st b1 in F1() & b2 in F2() & P1[b1,b2] holds
not P2[b1,b2] and
E5: for b1, b2 being set st b1 in F1() & b2 in F2() & P1[b1,b2] holds
F4(b1,b2) in F3() and
E6: for b1, b2 being set st b1 in F1() & b2 in F2() & P2[b1,b2] holds
F5(b1,b2) in F3()
proof end;

scheme :: SCHEME1:sch 18
s18{ 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 b1 being PartFunc of [:F1(),F2():],F3() st
( ( for b2, b3 being set holds
( [b2,b3] in dom b1 iff ( b2 in F1() & b3 in F2() & ( P1[b2,b3] or P2[b2,b3] or P3[b2,b3] ) ) ) ) & ( for b2, b3 being set st [b2,b3] in dom b1 holds
( ( P1[b2,b3] implies b1 . [b2,b3] = F4(b2,b3) ) & ( P2[b2,b3] implies b1 . [b2,b3] = F5(b2,b3) ) & ( P3[b2,b3] implies b1 . [b2,b3] = F6(b2,b3) ) ) ) )
provided
E4: for b1, b2 being set st b1 in F1() & b2 in F2() holds
( ( P1[b1,b2] implies not P2[b1,b2] ) & ( P1[b1,b2] implies not P3[b1,b2] ) & ( P2[b1,b2] implies not P3[b1,b2] ) ) and
E5: for b1, b2 being set st b1 in F1() & b2 in F2() & P1[b1,b2] holds
F4(b1,b2) in F3() and
E6: for b1, b2 being set st b1 in F1() & b2 in F2() & P2[b1,b2] holds
F5(b1,b2) in F3() and
E7: for b1, b2 being set st b1 in F1() & b2 in F2() & P3[b1,b2] holds
F6(b1,b2) in F3()
proof end;

scheme :: SCHEME1:sch 19
s19{ 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 b1 being Function of F1(),F2() st
for b2 being Element of F1() holds
( ( P1[b2] implies b1 . b2 = F3(b2) ) & ( P2[b2] implies b1 . b2 = F4(b2) ) & ( P3[b2] implies b1 . b2 = F5(b2) ) )
provided
E4: for b1 being Element of F1() holds
( ( P1[b1] implies not P2[b1] ) & ( P1[b1] implies not P3[b1] ) & ( P2[b1] implies not P3[b1] ) ) and
E5: for b1 being Element of F1() holds
( P1[b1] or P2[b1] or P3[b1] )
proof end;

scheme :: SCHEME1:sch 20
s20{ 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 b1 being Function of F1(),F2() st
for b2 being Element of F1() holds
( ( P1[b2] implies b1 . b2 = F3(b2) ) & ( P2[b2] implies b1 . b2 = F4(b2) ) & ( P3[b2] implies b1 . b2 = F5(b2) ) & ( P4[b2] implies b1 . b2 = F6(b2) ) )
provided
E4: for b1 being Element of F1() holds
( ( P1[b1] implies not P2[b1] ) & ( P1[b1] implies not P3[b1] ) & ( P1[b1] implies not P4[b1] ) & ( P2[b1] implies not P3[b1] ) & ( P2[b1] implies not P4[b1] ) & ( P3[b1] implies not P4[b1] ) ) and
E5: for b1 being Element of F1() holds
( P1[b1] or P2[b1] or P3[b1] or P4[b1] )
proof end;

scheme :: SCHEME1:sch 21
s21{ 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 b1 being Function of [:F1(),F2():],F3() st
for b2 being Element of F1()
for b3 being Element of F2() st [b2,b3] in dom b1 holds
( ( P1[b2,b3] implies b1 . [b2,b3] = F4(b2,b3) ) & ( P1[b2,b3] implies b1 . [b2,b3] = F5(b2,b3) ) )
proof end;

scheme :: SCHEME1:sch 22
s22{ 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 b1 being Function of [:F1(),F2():],F3() st
( ( for b2 being Element of F1()
for b3 being Element of F2() holds
( [b2,b3] in dom b1 iff ( P1[b2,b3] or P2[b2,b3] or P3[b2,b3] ) ) ) & ( for b2 being Element of F1()
for b3 being Element of F2() st [b2,b3] in dom b1 holds
( ( P1[b2,b3] implies b1 . [b2,b3] = F4(b2,b3) ) & ( P2[b2,b3] implies b1 . [b2,b3] = F5(b2,b3) ) & ( P3[b2,b3] implies b1 . [b2,b3] = F6(b2,b3) ) ) ) )
provided
E4: for b1 being Element of F1()
for b2 being Element of F2() holds
( ( P1[b1,b2] implies not P2[b1,b2] ) & ( P1[b1,b2] implies not P3[b1,b2] ) & ( P2[b1,b2] implies not P3[b1,b2] ) ) and
E5: for b1 being Element of F1()
for b2 being Element of F2() holds
( P1[b1,b2] or P2[b1,b2] or P3[b1,b2] )
proof end;