begin
defpred S1[ Nat] means for R being finite Subset of st R <> {} & card R = $1 holds
( R is bounded_above & upper_bound R in R & R is bounded_below & lower_bound R in R );
Lm1:
S1[ 0 ]
;
Lm2:
for n being Element of NAT st S1[n] holds
S1[n + 1]
Lm3:
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(Lm1, Lm2);
theorem Th1:
begin
theorem
canceled;
theorem Th3:
theorem
theorem Th5:
theorem
theorem
theorem Th8:
theorem
theorem
theorem Th11:
theorem
theorem
theorem Th14:
theorem Th15:
theorem Th16:
theorem
theorem
theorem Th19:
theorem Th20:
defpred S2[ Element of NAT ] means for v being FinSequence of REAL st card (rng v) = $1 holds
ex v1 being FinSequence of REAL st
( rng v1 = rng v & len v1 = card (rng v) & v1 is increasing );
Lm4:
S2[ 0 ]
Lm5:
for n being Element of NAT st S2[n] holds
S2[n + 1]
Lm6:
for n being Element of NAT holds S2[n]
from NAT_1:sch 1(Lm4, Lm5);
theorem
defpred S3[ Element of NAT ] means for v1, v2 being FinSequence of REAL st len v1 = $1 & len v2 = $1 & rng v1 = rng v2 & v1 is increasing & v2 is increasing holds
v1 = v2;
Lm7:
S3[ 0 ]
Lm8:
for n being Element of NAT st S3[n] holds
S3[n + 1]
Lm9:
for n being Element of NAT holds S3[n]
from NAT_1:sch 1(Lm7, Lm8);
theorem
begin
definition
let v1,
v2 be
FinSequence of
REAL ;
assume A1:
v1 <> {}
;
func GoB v1,
v2 -> Matrix of
means :
Def1:
(
len it = len v1 &
width it = len v2 & ( for
n,
m being
Element of
NAT st
[n,m] in Indices it holds
it * n,
m = |[(v1 . n),(v2 . m)]| ) );
existence
ex b1 being Matrix of st
( len b1 = len v1 & width b1 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b1 holds
b1 * n,m = |[(v1 . n),(v2 . m)]| ) )
uniqueness
for b1, b2 being Matrix of st len b1 = len v1 & width b1 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b1 holds
b1 * n,m = |[(v1 . n),(v2 . m)]| ) & len b2 = len v1 & width b2 = len v2 & ( for n, m being Element of NAT st [n,m] in Indices b2 holds
b2 * n,m = |[(v1 . n),(v2 . m)]| ) holds
b1 = b2
end;
:: deftheorem Def1 defines GoB GOBOARD2:def 1 :
:: deftheorem Def2 defines Incr GOBOARD2:def 2 :
:: deftheorem defines GoB GOBOARD2:def 3 :
theorem Th23:
theorem Th24:
theorem
theorem
theorem
theorem
theorem