:: RECDEF_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for n being 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
proof end;

definition
let D be set ;
let p be PartFunc of D, NAT ;
let n be Element of D;
:: original: .
redefine func p . n -> Nat;
coherence
p . n is Nat
proof end;
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 Nat
for x being set ex y being set st P1[n,x,y] and
A2: for n being Nat
for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2
proof end;

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 Nat
for x being Element of F1() ex y being Element of F1() st P1[n,x,y]
proof end;

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

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

scheme :: RECDEF_1:sch 5
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 Nat st 1 <= n & n < F2() holds
P1[n,p . n,p . (n + 1)] ) )
provided
A1: for n being Nat st 1 <= n & n < F2() holds
for x being set ex y being set st P1[n,x,y] and
A2: for n being 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
proof end;

scheme :: RECDEF_1:sch 6
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 Nat st 1 <= n & n < F3() holds
P1[n,p . n,p . (n + 1)] ) )
provided
A1: for n being Nat st 1 <= n & n < F3() holds
for x being Element of F1() ex y being Element of F1() st P1[n,x,y]
proof end;

scheme :: RECDEF_1:sch 7
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 Nat st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) )
provided
A1: for k being Nat
for x being set st 1 <= k & k < len F1() holds
ex y being set st P1[F1() . (k + 1),x,y] and
A2: for k being 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
proof end;

scheme :: RECDEF_1:sch 8
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 Nat st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) )
proof end;

scheme :: RECDEF_1:sch 9
RecUn{ F1() -> set , F2() -> Function, F3() -> Function, P1[ set , set , set ] } :
F2() = F3()
provided
A1: ( dom F2() = NAT & F2() . 0 = F1() & ( for n being Nat holds P1[n,F2() . n,F2() . (n + 1)] ) ) and
A2: ( dom F3() = NAT & F3() . 0 = F1() & ( for n being Nat holds P1[n,F3() . n,F3() . (n + 1)] ) ) and
A3: for n being Nat
for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2
proof end;

scheme :: RECDEF_1:sch 10
RecUnD{ 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
A1: ( F3() . 0 = F2() & ( for n being Nat holds P1[n,F3() . n,F3() . (n + 1)] ) ) and
A2: ( F4() . 0 = F2() & ( for n being Nat holds P1[n,F4() . n,F4() . (n + 1)] ) ) and
A3: for n being Nat
for x, y1, y2 being Element of F1() st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2
proof end;

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

scheme :: RECDEF_1:sch 12
LambdaRecUnD{ 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
A1: ( F4() . 0 = F2() & ( for n being Nat holds F4() . (n + 1) = F3(n,(F4() . n)) ) ) and
A2: ( F5() . 0 = F2() & ( for n being Nat holds F5() . (n + 1) = F3(n,(F5() . n)) ) )
proof end;

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

scheme :: RECDEF_1:sch 14
FinRecUn{ F1() -> set , F2() -> Nat, F3() -> FinSequence, F4() -> FinSequence, P1[ set , set , set ] } :
F3() = F4()
provided
A1: for n being 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 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 Nat st 1 <= n & n < F2() holds
P1[n,F4() . n,F4() . (n + 1)] ) )
proof end;

scheme :: RECDEF_1:sch 15
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 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 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 Nat st 1 <= n & n < F3() holds
P1[n,F5() . n,F5() . (n + 1)] ) )
proof end;

scheme :: RECDEF_1:sch 16
SeqBinOpUn{ F1() -> FinSequence, P1[ set , set , set ], F2() -> set , F3() -> set } :
F2() = F3()
provided
A1: for k being 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 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 Nat st 1 <= k & k < len F1() holds
P1[F1() . (k + 1),p . k,p . (k + 1)] ) )
proof end;

scheme :: RECDEF_1:sch 17
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 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 Nat st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) )
proof end;

scheme :: RECDEF_1:sch 18
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 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 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 Nat holds P1[n,f . n,f . (n + 1)] ) ) holds
y1 = y2 ) )
provided
A1: for n being Nat
for x being set ex y being set st P1[n,x,y] and
A2: for n being Nat
for x, y1, y2 being set st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2
proof end;

scheme :: RECDEF_1:sch 19
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 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 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 Nat holds f . (n + 1) = F3(n,(f . n)) ) ) holds
y1 = y2 ) )
proof end;

scheme :: RECDEF_1:sch 20
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 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 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 Nat holds P1[n,f . n,f . (n + 1)] ) ) holds
y1 = y2 ) )
provided
A1: for n being Nat
for x being Element of F1() ex y being Element of F1() st P1[n,x,y] and
A2: for n being Nat
for x, y1, y2 being Element of F1() st P1[n,x,y1] & P1[n,x,y2] holds
y1 = y2
proof end;

scheme :: RECDEF_1:sch 21
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 ) )
proof end;

scheme :: RECDEF_1:sch 22
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 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 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 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 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 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
proof end;

scheme :: RECDEF_1:sch 23
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 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 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 Nat st 1 <= k & k < len F1() holds
p . (k + 1) = F2((F1() . (k + 1)),(p . k)) ) ) holds
x = y ) )
proof end;