:: Mizar Analysis of Algorithms: Algorithms over Integers
:: by Grzegorz Bancerek
::
:: Received March 18, 2008
:: Copyright (c) 2008 Association of Mizar Users

:: AOFA_I00 semantic presentation

theorem Lem3: :: AOFA_I00:1
for x, y, z, a, b, c being set st a <> b & b <> c & c <> a holds
ex f being Function st
( f . a = x & f . b = y & f . c = z )
proof end;

definition
let F be non empty functional set ;
let x, f be set ;
func F \ x,f -> Subset of F equals :: AOFA_I00:def 1
{ g where g is Element of F : g . x <> f } ;
coherence
{ g where g is Element of F : g . x <> f } is Subset of F
proof end;
end;

:: deftheorem defines \ AOFA_I00:def 1 :
for F being non empty functional set
for x, f being set holds F \ x,f = { g where g is Element of F : g . x <> f } ;

theorem LemTS: :: AOFA_I00:2
for F being non empty functional set
for x, y being set
for g being Element of F holds
( g in F \ x,y iff g . x <> y )
proof end;

definition
let X be set ;
let Y, Z be set ;
let f be Function of [:(Funcs X,INT ),Y:],Z;
mode Variable of f -> Element of X means :ELEM: :: AOFA_I00:def 2
verum;
existence
ex b1 being Element of X st verum ;
end;

:: deftheorem ELEM defines Variable AOFA_I00:def 2 :
for X, Y, Z being set
for f being Function of [:(Funcs X,INT ),Y:],Z
for b5 being Element of X holds
( b5 is Variable of f iff verum );

notation
let f be real-yielding Function;
let x be real number ;
synonym f * x for x (#) f;
end;

definition
let t1, t2 be integer-yielding Function;
func t1 div t2 -> integer-yielding Function means :DEFdiv: :: AOFA_I00:def 3
( dom it = (dom t1) /\ (dom t2) & ( for s being set st s in dom it holds
it . s = (t1 . s) div (t2 . s) ) );
correctness
existence
ex b1 being integer-yielding Function st
( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = (t1 . s) div (t2 . s) ) );
uniqueness
for b1, b2 being integer-yielding Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = (t1 . s) div (t2 . s) ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds
b2 . s = (t1 . s) div (t2 . s) ) holds
b1 = b2;
proof end;
func t1 mod t2 -> integer-yielding Function means :DEFmod: :: AOFA_I00:def 4
( dom it = (dom t1) /\ (dom t2) & ( for s being set st s in dom it holds
it . s = (t1 . s) mod (t2 . s) ) );
correctness
existence
ex b1 being integer-yielding Function st
( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = (t1 . s) mod (t2 . s) ) );
uniqueness
for b1, b2 being integer-yielding Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = (t1 . s) mod (t2 . s) ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds
b2 . s = (t1 . s) mod (t2 . s) ) holds
b1 = b2;
proof end;
func leq t1,t2 -> integer-yielding Function means :DEFleq: :: AOFA_I00:def 5
( dom it = (dom t1) /\ (dom t2) & ( for s being set st s in dom it holds
it . s = IFGT (t1 . s),(t2 . s),0 ,1 ) );
correctness
existence
ex b1 being integer-yielding Function st
( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = IFGT (t1 . s),(t2 . s),0 ,1 ) );
uniqueness
for b1, b2 being integer-yielding Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = IFGT (t1 . s),(t2 . s),0 ,1 ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds
b2 . s = IFGT (t1 . s),(t2 . s),0 ,1 ) holds
b1 = b2;
proof end;
func gt t1,t2 -> integer-yielding Function means :DEFgt: :: AOFA_I00:def 6
( dom it = (dom t1) /\ (dom t2) & ( for s being set st s in dom it holds
it . s = IFGT (t1 . s),(t2 . s),1,0 ) );
correctness
existence
ex b1 being integer-yielding Function st
( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = IFGT (t1 . s),(t2 . s),1,0 ) );
uniqueness
for b1, b2 being integer-yielding Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = IFGT (t1 . s),(t2 . s),1,0 ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds
b2 . s = IFGT (t1 . s),(t2 . s),1,0 ) holds
b1 = b2;
proof end;
func eq t1,t2 -> integer-yielding Function means :DEFeq: :: AOFA_I00:def 7
( dom it = (dom t1) /\ (dom t2) & ( for s being set st s in dom it holds
it . s = IFEQ (t1 . s),(t2 . s),1,0 ) );
correctness
existence
ex b1 being integer-yielding Function st
( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = IFEQ (t1 . s),(t2 . s),1,0 ) );
uniqueness
for b1, b2 being integer-yielding Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = IFEQ (t1 . s),(t2 . s),1,0 ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds
b2 . s = IFEQ (t1 . s),(t2 . s),1,0 ) holds
b1 = b2;
proof end;
end;

:: deftheorem DEFdiv defines div AOFA_I00:def 3 :
for t1, t2, b3 being integer-yielding Function holds
( b3 = t1 div t2 iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds
b3 . s = (t1 . s) div (t2 . s) ) ) );

:: deftheorem DEFmod defines mod AOFA_I00:def 4 :
for t1, t2, b3 being integer-yielding Function holds
( b3 = t1 mod t2 iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds
b3 . s = (t1 . s) mod (t2 . s) ) ) );

:: deftheorem DEFleq defines leq AOFA_I00:def 5 :
for t1, t2, b3 being integer-yielding Function holds
( b3 = leq t1,t2 iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds
b3 . s = IFGT (t1 . s),(t2 . s),0 ,1 ) ) );

:: deftheorem DEFgt defines gt AOFA_I00:def 6 :
for t1, t2, b3 being integer-yielding Function holds
( b3 = gt t1,t2 iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds
b3 . s = IFGT (t1 . s),(t2 . s),1,0 ) ) );

:: deftheorem DEFeq defines eq AOFA_I00:def 7 :
for t1, t2, b3 being integer-yielding Function holds
( b3 = eq t1,t2 iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds
b3 . s = IFEQ (t1 . s),(t2 . s),1,0 ) ) );

definition
let X be non empty set ;
let f be Function of X, INT ;
let x be integer number ;
:: original: +
redefine func f + x -> Function of X, INT means :DEFplus2: :: AOFA_I00:def 8
for s being Element of X holds it . s = (f . s) + x;
compatibility
for b1 being Function of X, INT holds
( b1 = x + f iff for s being Element of X holds b1 . s = (f . s) + x )
proof end;
coherence
x + f is Function of X, INT
proof end;
:: original: -
redefine func f - x -> Function of X, INT means :: AOFA_I00:def 9
for s being Element of X holds it . s = (f . s) - x;
compatibility
for b1 being Function of X, INT holds
( b1 = f - x iff for s being Element of X holds b1 . s = (f . s) - x )
proof end;
coherence
f - x is Function of X, INT
proof end;
:: original: *
redefine func f * x -> Function of X, INT means :DEFmult2: :: AOFA_I00:def 10
for s being Element of X holds it . s = (f . s) * x;
compatibility
for b1 being Function of X, INT holds
( b1 = f * x iff for s being Element of X holds b1 . s = (f . s) * x )
proof end;
coherence
f * x is Function of X, INT
proof end;
end;

:: deftheorem DEFplus2 defines + AOFA_I00:def 8 :
for X being non empty set
for f being Function of X, INT
for x being integer number
for b4 being Function of X, INT holds
( b4 = f + x iff for s being Element of X holds b4 . s = (f . s) + x );

:: deftheorem defines - AOFA_I00:def 9 :
for X being non empty set
for f being Function of X, INT
for x being integer number
for b4 being Function of X, INT holds
( b4 = f - x iff for s being Element of X holds b4 . s = (f . s) - x );

:: deftheorem DEFmult2 defines * AOFA_I00:def 10 :
for X being non empty set
for f being Function of X, INT
for x being integer number
for b4 being Function of X, INT holds
( b4 = f * x iff for s being Element of X holds b4 . s = (f . s) * x );

definition
let X be set ;
let f, g be Function of X, INT ;
:: original: div
redefine func f div g -> Function of X, INT ;
coherence
f div g is Function of X, INT
proof end;
:: original: mod
redefine func f mod g -> Function of X, INT ;
coherence
f mod g is Function of X, INT
proof end;
:: original: leq
redefine func leq f,g -> Function of X, INT ;
coherence
leq f,g is Function of X, INT
proof end;
:: original: gt
redefine func gt f,g -> Function of X, INT ;
coherence
gt f,g is Function of X, INT
proof end;
:: original: eq
redefine func eq f,g -> Function of X, INT ;
coherence
eq f,g is Function of X, INT
proof end;
end;

definition
let X be non empty set ;
let t1, t2 be Function of X, INT ;
:: original: -
redefine func t1 - t2 -> Function of X, INT means :DEFminus3: :: AOFA_I00:def 11
for s being Element of X holds it . s = (t1 . s) - (t2 . s);
compatibility
for b1 being Function of X, INT holds
( b1 = t1 - t2 iff for s being Element of X holds b1 . s = (t1 . s) - (t2 . s) )
proof end;
coherence
t1 - t2 is Function of X, INT
proof end;
:: original: +
redefine func t1 + t2 -> Function of X, INT means :: AOFA_I00:def 12
for s being Element of X holds it . s = (t1 . s) + (t2 . s);
compatibility
for b1 being Function of X, INT holds
( b1 = t1 + t2 iff for s being Element of X holds b1 . s = (t1 . s) + (t2 . s) )
proof end;
coherence
t1 + t2 is Function of X, INT
proof end;
end;

:: deftheorem DEFminus3 defines - AOFA_I00:def 11 :
for X being non empty set
for t1, t2, b4 being Function of X, INT holds
( b4 = t1 - t2 iff for s being Element of X holds b4 . s = (t1 . s) - (t2 . s) );

:: deftheorem defines + AOFA_I00:def 12 :
for X being non empty set
for t1, t2, b4 being Function of X, INT holds
( b4 = t1 + t2 iff for s being Element of X holds b4 . s = (t1 . s) + (t2 . s) );

registration
let A be non empty set ;
let B be infinite set ;
cluster Funcs A,B -> infinite ;
coherence
not Funcs A,B is finite
proof end;
end;

definition
let N be set ;
let v, f be Function;
func v ** f,N -> Function means :DSTAR: :: AOFA_I00:def 13
( ex Y being set st
( ( for y being set holds
( y in Y iff ex h being Function st
( h in dom v & y in rng h ) ) ) & ( for a being set holds
( a in dom it iff ( a in Funcs N,Y & ex g being Function st
( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom it holds
it . g = v . (g * f) ) );
uniqueness
for b1, b2 being Function st ex Y being set st
( ( for y being set holds
( y in Y iff ex h being Function st
( h in dom v & y in rng h ) ) ) & ( for a being set holds
( a in dom b1 iff ( a in Funcs N,Y & ex g being Function st
( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom b1 holds
b1 . g = v . (g * f) ) & ex Y being set st
( ( for y being set holds
( y in Y iff ex h being Function st
( h in dom v & y in rng h ) ) ) & ( for a being set holds
( a in dom b2 iff ( a in Funcs N,Y & ex g being Function st
( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom b2 holds
b2 . g = v . (g * f) ) holds
b1 = b2
proof end;
existence
ex b1 being Function st
( ex Y being set st
( ( for y being set holds
( y in Y iff ex h being Function st
( h in dom v & y in rng h ) ) ) & ( for a being set holds
( a in dom b1 iff ( a in Funcs N,Y & ex g being Function st
( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom b1 holds
b1 . g = v . (g * f) ) )
proof end;
end;

:: deftheorem DSTAR defines ** AOFA_I00:def 13 :
for N being set
for v, f, b4 being Function holds
( b4 = v ** f,N iff ( ex Y being set st
( ( for y being set holds
( y in Y iff ex h being Function st
( h in dom v & y in rng h ) ) ) & ( for a being set holds
( a in dom b4 iff ( a in Funcs N,Y & ex g being Function st
( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom b4 holds
b4 . g = v . (g * f) ) ) );

definition
let X, Y, Z, N be non empty set ;
let v be Element of Funcs (Funcs X,Y),Z;
let f be Function of X,N;
:: original: **
redefine func v ** f,N -> Element of Funcs (Funcs N,Y),Z;
coherence
v ** f,N is Element of Funcs (Funcs N,Y),Z
proof end;
end;

theorem LemR: :: AOFA_I00:3
for f1, f2, g being Function st rng g c= dom f2 holds
(f1 +* f2) * g = f2 * g
proof end;

theorem LemQ: :: AOFA_I00:4
for X, N, I being non empty set
for s being Function of X,I
for c being Function of X,N st c is one-to-one holds
for n being Element of I holds (N --> n) +* (s * (c " )) is Function of N,I
proof end;

theorem ThDS1: :: AOFA_I00:5
for N, X, I being non empty set
for v1, v2 being Function st dom v1 = dom v2 & dom v1 = Funcs X,I holds
for f being Function of X,N st f is one-to-one & v1 ** f,N = v2 ** f,N holds
v1 = v2
proof end;

registration
let X be set ;
cluster one-to-one onto Relation of X, Card X;
existence
ex b1 being Function of X, Card X st
( b1 is one-to-one & b1 is onto )
proof end;
cluster one-to-one onto Relation of Card X,X;
existence
ex b1 being Function of Card X,X st
( b1 is one-to-one & b1 is onto )
proof end;
end;

definition
let X be set ;
mode Enumeration of X is one-to-one onto Function of X, Card X;
mode Denumeration of X is one-to-one onto Function of Card X,X;
end;

theorem ThNum1: :: AOFA_I00:6
for X being set
for f being Function holds
( f is Enumeration of X iff ( dom f = X & rng f = Card X & f is one-to-one ) )
proof end;

theorem ThNum2: :: AOFA_I00:7
for X being set
for f being Function holds
( f is Denumeration of X iff ( dom f = Card X & rng f = X & f is one-to-one ) )
proof end;

theorem ThNum6: :: AOFA_I00:8
for X being non empty set
for x, y being Element of X
for f being Enumeration of X holds (f +* x,(f . y)) +* y,(f . x) is Enumeration of X
proof end;

theorem :: AOFA_I00:9
for X being non empty set
for x being Element of X ex f being Enumeration of X st f . x = <