:: RECDEF_1 semantic presentation

Lemma1: for b1 being Nat
for b2 being non empty set
for b3 being FinSequence of b2 st 1 <= b1 & b1 <= len b3 holds
b3 . b1 is Element of b2
proof end;

definition
let c1 be set ;
let c2 be PartFunc of c1, NAT ;
let c3 be Element of c1;
redefine func . as c2 . c3 -> Nat;
coherence
c2 . c3 is Nat
proof end;
end;

scheme :: RECDEF_1:sch 1
s1{ F1() -> set , P1[ set , set , set ] } :
ex b1 being Function st
( dom b1 = NAT & b1 . 0 = F1() & ( for b2 being Element of NAT holds P1[b2,b1 . b2,b1 . (b2 + 1)] ) )
provided
E2: for b1 being Nat
for b2 being set ex b3 being set st P1[b1,b2,b3] and
E3: for b1 being Nat
for b2, b3, b4 being set st P1[b1,b2,b3] & P1[b1,b2,b4] holds
b3 = b4
proof end;

scheme :: RECDEF_1:sch 2
s2{ F1() -> non empty set , F2() -> Element of F1(), P1[ set , set , set ] } :
ex b1 being Function of NAT ,F1() st
( b1 . 0 = F2() & ( for b2 being Element of NAT holds P1[b2,b1 . b2,b1 . (b2 + 1)] ) )
provided
E2: for b1 being Nat
for b2 being Element of F1() ex b3 being Element of F1() st P1[b1,b2,b3]
proof end;

scheme :: RECDEF_1:sch 3
s3{ F1() -> set , F2( set , set ) -> set } :
ex b1 being Function st
( dom b1 = NAT & b1 . 0 = F1() & ( for b2 being Element of NAT holds b1 . (b2 + 1) = F2(b2,(b1 . b2)) ) )
proof end;

scheme :: RECDEF_1:sch 4
s4{ F1() -> non empty set , F2() -> Element of F1(), F3( set , set ) -> Element of F1() } :
ex b1 being Function of NAT ,F1() st
( b1 . 0 = F2() & ( for b2 being Element of NAT holds b1 . (b2 + 1) = F3(b2,(b1 . b2)) ) )
proof end;

scheme :: RECDEF_1:sch 5
s5{ F1() -> set , F2() -> Nat, P1[ set , set , set ] } :
ex b1 being FinSequence st
( len b1 = F2() & ( b1 . 1 = F1() or F2() = 0 ) & ( for b2 being Nat st 1 <= b2 & b2 < F2() holds
P1[b2,b1 . b2,b1 . (b2 + 1)] ) )
provided
E2: for b1 being Nat st 1 <= b1 & b1 < F2() holds
for b2 being set ex b3 being set st P1[b1,b2,b3] and
E3: for b1 being Nat st 1 <= b1 & b1 < F2() holds
for b2, b3, b4 being set st P1[b1,b2,b3] & P1[b1,b2,b4] holds
b3 = b4
proof end;

scheme :: RECDEF_1:sch 6
s6{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Nat, P1[ set , set , set ] } :
ex b1 being FinSequence of F1() st
( len b1 = F3() & ( b1 . 1 = F2() or F3() = 0 ) & ( for b2 being Nat st 1 <= b2 & b2 < F3() holds
P1[b2,b1 . b2,b1 . (b2 + 1)] ) )
provided
E2: for b1 being Nat st 1 <= b1 & b1 < F3() holds
for b2 being Element of F1() ex b3 being Element of F1() st P1[b1,b2,b3]
proof end;

scheme :: RECDEF_1:sch 7
s7{ F1() -> FinSequence, P1[ set , set , set ] } :
ex b1 being set ex b2 being FinSequence st
( b1 = b2 . (len b2) & len b2 = len F1() & b2 . 1 = F1() . 1 & ( for b3 being Nat st 1 <= b3 & b3 < len F1() holds
P1[F1() . (b3 + 1),b2 . b3,b2 . (b3 + 1)] ) )
provided
E2: for b1 being Nat
for b2 being set st 1 <= b1 & b1 < len F1() holds
ex b3 being set st P1[F1() . (b1 + 1),b2,b3] and
E3: for b1 being Nat
for b2, b3, b4, b5 being set st 1 <= b1 & b1 < len F1() & b5 = F1() . (b1 + 1) & P1[b5,b2,b3] & P1[b5,b2,b4] holds
b3 = b4
proof end;

scheme :: RECDEF_1:sch 8
s8{ F1() -> FinSequence, F2( set , set ) -> set } :
ex b1 being set ex b2 being FinSequence st
( b1 = b2 . (len b2) & len b2 = len F1() & b2 . 1 = F1() . 1 & ( for b3 being Nat st 1 <= b3 & b3 < len F1() holds
b2 . (b3 + 1) = F2((F1() . (b3 + 1)),(b2 . b3)) ) )
proof end;

scheme :: RECDEF_1:sch 9
s9{ F1() -> set , F2() -> Function, F3() -> Function, P1[ set , set , set ] } :
F2() = F3()
provided
E2: ( dom F2() = NAT & F2() . 0 = F1() & ( for b1 being Nat holds P1[b1,F2() . b1,F2() . (b1 + 1)] ) ) and
E3: ( dom F3() = NAT & F3() . 0 = F1() & ( for b1 being Nat holds P1[b1,F3() . b1,F3() . (b1 + 1)] ) ) and
E4: for b1 being Nat
for b2, b3, b4 being set st P1[b1,b2,b3] & P1[b1,b2,b4] holds
b3 = b4
proof end;

scheme :: RECDEF_1:sch 10
s10{ F1() -> non empty set , F2() -> Element of F1(), P1[ set , set , set ], F3() -> Function of NAT ,F1(), F4() -> Function of NAT ,F1() } :
F3() = F4()
provided
E2: ( F3() . 0 = F2() & ( for b1 being Nat holds P1[b1,F3() . b1,F3() . (b1 + 1)] ) ) and
E3: ( F4() . 0 = F2() & ( for b1 being Nat holds P1[b1,F4() . b1,F4() . (b1 + 1)] ) ) and
E4: for b1 being Nat
for b2, b3, b4 being Element of F1() st P1[b1,b2,b3] & P1[b1,b2,b4] holds
b3 = b4
proof end;

scheme :: RECDEF_1:sch 11
s11{ F1() -> set , F2( set , set ) -> set , F3() -> Function, F4() -> Function } :
F3() = F4()
provided
E2: ( dom F3() = NAT & F3() . 0 = F1() & ( for b1 being Nat holds F3() . (b1 + 1) = F2(b1,(F3() . b1)) ) ) and
E3: ( dom F4() = NAT & F4() . 0 = F1() & ( for b1 being Nat holds F4() . (b1 + 1) = F2(b1,(F4() . b1)) ) )
proof end;

scheme :: RECDEF_1:sch 12
s12{ F1() -> non empty set , F2() -> Element of F1(), F3( set , set ) -> Element of F1(), F4() -> Function of NAT ,F1(), F5() -> Function of NAT ,F1() } :
F4() = F5()
provided
E2: ( F4() . 0 = F2() & ( for b1 being Nat holds F4() . (b1 + 1) = F3(b1,(F4() . b1)) ) ) and
E3: ( F5() . 0 = F2() & ( for b1 being Nat holds F5() . (b1 + 1) = F3(b1,(F5() . b1)) ) )
proof end;

scheme :: RECDEF_1:sch 13
s13{ F1() -> Real, F2( set , set ) -> set , F3() -> Function of NAT , REAL , F4() -> Function of NAT , REAL } :
F3() = F4()
provided
E2: ( F3() . 0 = F1() & ( for b1 being Nat holds F3() . (b1 + 1) = F2(b1,(F3() . b1)) ) ) and
E3: ( F4() . 0 = F1() & ( for b1 being Nat holds F4() . (b1 + 1) = F2(b1,(F4() . b1)) ) )
proof end;

scheme :: RECDEF_1:sch 14
s14{ F1() -> set , F2() -> Nat, F3() -> FinSequence, F4() -> FinSequence, P1[ set , set , set ] } :
F3() = F4()
provided
E2: for b1 being Nat st 1 <= b1 & b1 < F2() holds
for b2, b3, b4 being set st P1[b1,b2,b3] & P1[b1,b2,b4] holds
b3 = b4 and
E3: ( len F3() = F2() & ( F3() . 1 = F1() or F2() = 0 ) & ( for b1 being Nat st 1 <= b1 & b1 < F2() holds
P1[b1,F3() . b1,F3() . (b1 + 1)] ) ) and
E4: ( len F4() = F2() & ( F4() . 1 = F1() or F2() = 0 ) & ( for b1 being Nat st 1 <= b1 & b1 < F2() holds
P1[b1,F4() . b1,F4() . (b1 + 1)] ) )
proof end;

scheme :: RECDEF_1:sch 15
s15{ 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
E2: for b1 being Nat st 1 <= b1 & b1 < F3() holds
for b2, b3, b4 being Element of F1() st P1[b1,b2,b3] & P1[b1,b2,b4] holds
b3 = b4 and
E3: ( len F4() = F3() & ( F4() . 1 = F2() or F3() = 0 ) & ( for b1 being Nat st 1 <= b1 & b1 < F3() holds
P1[b1,F4() . b1,F4() . (b1 + 1)] ) ) and
E4: ( len F5() = F3() & ( F5() . 1 = F2() or F3() = 0 ) & ( for b1 being Nat st 1 <= b1 & b1 < F3() holds
P1[b1,F5() . b1,F5() . (b1 + 1)] ) )
proof end;

scheme :: RECDEF_1:sch 16
s16{ F1() -> FinSequence, P1[ set , set , set ], F2() -> set , F3() -> set } :
F2() = F3()
provided
E2: for b1 being Nat
for b2, b3, b4, b5 being set st 1 <= b1 & b1 < len F1() & b5 = F1() . (b1 + 1) & P1[b5,b2,b3] & P1[b5,b2,b4] holds
b3 = b4 and
E3: ex b1 being FinSequence st
( F2() = b1 . (len b1) & len b1 = len F1() & b1 . 1 = F1() . 1 & ( for b2 being Nat st 1 <= b2 & b2 < len F1() holds
P1[F1() . (b2 + 1),b1 . b2,b1 . (b2 + 1)] ) ) and
E4: ex b1 being FinSequence st
( F3() = b1 . (len b1) & len b1 = len F1() & b1 . 1 = F1() . 1 & ( for b2 being Nat st 1 <= b2 & b2 < len F1() holds
P1[F1() . (b2 + 1),b1 . b2,b1 . (b2 + 1)] ) )
proof end;

scheme :: RECDEF_1:sch 17
s17{ F1() -> FinSequence, F2( set , set ) -> set , F3() -> set , F4() -> set } :
F3() = F4()
provided
E2: ex b1 being FinSequence st
( F3() = b1 . (len b1) & len b1 = len F1() & b1 . 1 = F1() . 1 & ( for b2 being Nat st 1 <= b2 & b2 < len F1() holds
b1 . (b2 + 1) = F2((F1() . (b2 + 1)),(b1 . b2)) ) ) and
E3: ex b1 being FinSequence st
( F4() = b1 . (len b1) & len b1 = len F1() & b1 . 1 = F1() . 1 & ( for b2 being Nat st 1 <= b2 & b2 < len F1() holds
b1 . (b2 + 1) = F2((F1() . (b2 + 1)),(b1 . b2)) ) )
proof end;

scheme :: RECDEF_1:sch 18
s18{ F1() -> set , F2() -> Nat, P1[ set , set , set ] } :
( ex b1 being set ex b2 being Function st
( b1 = b2 . F2() & dom b2 = NAT & b2 . 0 = F1() & ( for b3 being Nat holds P1[b3,b2 . b3,b2 . (b3 + 1)] ) ) & ( for b1, b2 being set st ex b3 being Function st
( b1 = b3 . F2() & dom b3 = NAT & b3 . 0 = F1() & ( for b4 being Nat holds P1[b4,b3 . b4,b3 . (b4 + 1)] ) ) & ex b3 being Function st
( b2 = b3 . F2() & dom b3 = NAT & b3 . 0 = F1() & ( for b4 being Nat holds P1[b4,b3 . b4,b3 . (b4 + 1)] ) ) holds
b1 = b2 ) )
provided
E2: for b1 being Nat
for b2 being set ex b3 being set st P1[b1,b2,b3] and
E3: for b1 being Nat
for b2, b3, b4 being set st P1[b1,b2,b3] & P1[b1,b2,b4] holds
b3 = b4
proof end;

scheme :: RECDEF_1:sch 19
s19{ F1() -> set , F2() -> Nat, F3( set , set ) -> set } :
( ex b1 being set ex b2 being Function st
( b1 = b2 . F2() & dom b2 = NAT & b2 . 0 = F1() & ( for b3 being Nat holds b2 . (b3 + 1) = F3(b3,(b2 . b3)) ) ) & ( for b1, b2 being set st ex b3 being Function st
( b1 = b3 . F2() & dom b3 = NAT & b3 . 0 = F1() & ( for b4 being Nat holds b3 . (b4 + 1) = F3(b4,(b3 . b4)) ) ) & ex b3 being Function st
( b2 = b3 . F2() & dom b3 = NAT & b3 . 0 = F1() & ( for b4 being Nat holds b3 . (b4 + 1) = F3(b4,(b3 . b4)) ) ) holds
b1 = b2 ) )
proof end;

scheme :: RECDEF_1:sch 20
s20{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Nat, P1[ set , set , set ] } :
( ex b1 being Element of F1()ex b2 being Function of NAT ,F1() st
( b1 = b2 . F3() & b2 . 0 = F2() & ( for b3 being Nat holds P1[b3,b2 . b3,b2 . (b3 + 1)] ) ) & ( for b1, b2 being Element of F1() st ex b3 being Function of NAT ,F1() st
( b1 = b3 . F3() & b3 . 0 = F2() & ( for b4 being Nat holds P1[b4,b3 . b4,b3 . (b4 + 1)] ) ) & ex b3 being Function of NAT ,F1() st
( b2 = b3 . F3() & b3 . 0 = F2() & ( for b4 being Nat holds P1[b4,b3 . b4,b3 . (b4 + 1)] ) ) holds
b1 = b2 ) )
provided
E2: for b1 being Nat
for b2 being Element of F1() ex b3 being Element of F1() st P1[b1,b2,b3] and
E3: for b1 being Nat
for b2, b3, b4 being Element of F1() st P1[b1,b2,b3] & P1[b1,b2,b4] holds
b3 = b4
proof end;

scheme :: RECDEF_1:sch 21
s21{ F1() -> non empty set , F2() -> Element of F1(), F3() -> Nat, F4( set , set ) -> Element of F1() } :
( ex b1 being Element of F1()ex b2 being Function of NAT ,F1() st
( b1 = b2 . F3() & b2 . 0 = F2() & ( for b3 being Nat holds b2 . (b3 + 1) = F4(b3,(b2 . b3)) ) ) & ( for b1, b2 being Element of F1() st ex b3 being Function of NAT ,F1() st
( b1 = b3 . F3() & b3 . 0 = F2() & ( for b4 being Nat holds b3 . (b4 + 1) = F4(b4,(b3 . b4)) ) ) & ex b3 being Function of NAT ,F1() st
( b2 = b3 . F3() & b3 . 0 = F2() & ( for b4 being Nat holds b3 . (b4 + 1) = F4(b4,(b3 . b4)) ) ) holds
b1 = b2 ) )
proof end;

scheme :: RECDEF_1:sch 22
s22{ F1() -> FinSequence, P1[ set , set , set ] } :
( ex b1 being set ex b2 being FinSequence st
( b1 = b2 . (len b2) & len b2 = len F1() & b2 . 1 = F1() . 1 & ( for b3 being Nat st 1 <= b3 & b3 < len F1() holds
P1[F1() . (b3 + 1),b2 . b3,b2 . (b3 + 1)] ) ) & ( for b1, b2 being set st ex b3 being FinSequence st
( b1 = b3 . (len b3) & len b3 = len F1() & b3 . 1 = F1() . 1 & ( for b4 being Nat st 1 <= b4 & b4 < len F1() holds
P1[F1() . (b4 + 1),b3 . b4,b3 . (b4 + 1)] ) ) & ex b3 being FinSequence st
( b2 = b3 . (len b3) & len b3 = len F1() & b3 . 1 = F1() . 1 & ( for b4 being Nat st 1 <= b4 & b4 < len F1() holds
P1[F1() . (b4 + 1),b3 . b4,b3 . (b4 + 1)] ) ) holds
b1 = b2 ) )
provided
E2: for b1 being Nat
for b2 being set st 1 <= b1 & b1 < len F1() holds
ex b3 being set st P1[F1() . (b1 + 1),b2,b3] and
E3: for b1 being Nat
for b2, b3, b4, b5 being set st 1 <= b1 & b1 < len F1() & b5 = F1() . (b1 + 1) & P1[b5,b2,b3] & P1[b5,b2,b4] holds
b3 = b4
proof end;

scheme :: RECDEF_1:sch 23
s23{ F1() -> FinSequence, F2( set , set ) -> set } :
( ex b1 being set ex b2 being FinSequence st
( b1 = b2 . (len b2) & len b2 = len F1() & b2 . 1 = F1() . 1 & ( for b3 being Nat st 1 <= b3 & b3 < len F1() holds
b2 . (b3 + 1) = F2((F1() . (b3 + 1)),(b2 . b3)) ) ) & ( for b1, b2 being set st ex b3 being FinSequence st
( b1 = b3 . (len b3) & len b3 = len F1() & b3 . 1 = F1() . 1 & ( for b4 being Nat st 1 <= b4 & b4 < len F1() holds
b3 . (b4 + 1) = F2((F1() . (b4 + 1)),(b3 . b4)) ) ) & ex b3 being FinSequence st
( b2 = b3 . (len b3) & len b3 = len F1() & b3 . 1 = F1() . 1 & ( for b4 being Nat st 1 <= b4 & b4 < len F1() holds
b3 . (b4 + 1) = F2((F1() . (b4 + 1)),(b3 . b4)) ) ) holds
b1 = b2 ) )
proof end;