:: by Grzegorz Bancerek

::

:: Received July 9, 2007

:: Copyright (c) 2007-2012 Association of Mizar Users

begin

theorem Th1: :: AOFA_000:1

for f, g, h being Function

for A being set st A c= dom f & A c= dom g & rng h c= A & ( for x being set st x in A holds

f . x = g . x ) holds

f * h = g * h

for A being set st A c= dom f & A c= dom g & rng h c= A & ( for x being set st x in A holds

f . x = g . x ) holds

f * h = g * h

proof end;

:: deftheorem Def1 defines is_a_unity_wrt AOFA_000:def 1 :

for f being homogeneous Function

for x being set holds

( x is_a_unity_wrt f iff for y, z being set st ( <*y,z*> in dom f or <*z,y*> in dom f ) holds

( <*x,y*> in dom f & f . <*x,y*> = y & <*y,x*> in dom f & f . <*y,x*> = y ) );

for f being homogeneous Function

for x being set holds

( x is_a_unity_wrt f iff for y, z being set st ( <*y,z*> in dom f or <*z,y*> in dom f ) holds

( <*x,y*> in dom f & f . <*x,y*> = y & <*y,x*> in dom f & f . <*y,x*> = y ) );

definition

let f be homogeneous Function;

end;
attr f is associative means :Def2: :: AOFA_000:def 2

for x, y, z being set st <*x,y*> in dom f & <*y,z*> in dom f & <*(f . <*x,y*>),z*> in dom f & <*x,(f . <*y,z*>)*> in dom f holds

f . <*(f . <*x,y*>),z*> = f . <*x,(f . <*y,z*>)*>;

for x, y, z being set st <*x,y*> in dom f & <*y,z*> in dom f & <*(f . <*x,y*>),z*> in dom f & <*x,(f . <*y,z*>)*> in dom f holds

f . <*(f . <*x,y*>),z*> = f . <*x,(f . <*y,z*>)*>;

:: deftheorem Def2 defines associative AOFA_000:def 2 :

for f being homogeneous Function holds

( f is associative iff for x, y, z being set st <*x,y*> in dom f & <*y,z*> in dom f & <*(f . <*x,y*>),z*> in dom f & <*x,(f . <*y,z*>)*> in dom f holds

f . <*(f . <*x,y*>),z*> = f . <*x,(f . <*y,z*>)*> );

for f being homogeneous Function holds

( f is associative iff for x, y, z being set st <*x,y*> in dom f & <*y,z*> in dom f & <*(f . <*x,y*>),z*> in dom f & <*x,(f . <*y,z*>)*> in dom f holds

f . <*(f . <*x,y*>),z*> = f . <*x,(f . <*y,z*>)*> );

:: deftheorem Def3 defines unital AOFA_000:def 3 :

for f being homogeneous Function holds

( f is unital iff ex x being set st x is_a_unity_wrt f );

for f being homogeneous Function holds

( f is unital iff ex x being set st x is_a_unity_wrt f );

definition

let X be set ;

let Y be non empty set ;

let Z be FinSequenceSet of X;

let y be Element of Y;

:: original: -->

redefine func Z --> y -> PartFunc of (X *),Y;

coherence

Z --> y is PartFunc of (X *),Y

end;
let Y be non empty set ;

let Z be FinSequenceSet of X;

let y be Element of Y;

:: original: -->

redefine func Z --> y -> PartFunc of (X *),Y;

coherence

Z --> y is PartFunc of (X *),Y

proof end;

registration

let X be non empty set ;

let x be Element of X;

let n be Nat;

coherence

for b_{1} being PartFunc of (X *),X st b_{1} = (n -tuples_on X) --> x holds

( not b_{1} is empty & b_{1} is quasi_total & b_{1} is homogeneous )

end;
let x be Element of X;

let n be Nat;

coherence

for b

( not b

proof end;

theorem Th2: :: AOFA_000:2

for X being non empty set

for x being Element of X

for n being Nat holds arity ((n -tuples_on X) --> x) = n

for x being Element of X

for n being Nat holds arity ((n -tuples_on X) --> x) = n

proof end;

Lm1: now :: thesis: for X being non empty set

for x being Element of X

for n being Nat holds (n -tuples_on X) --> x is n -ary

for x being Element of X

for n being Nat holds (n -tuples_on X) --> x is n -ary

let X be non empty set ; :: thesis: for x being Element of X

for n being Nat holds (n -tuples_on X) --> x is n -ary

let x be Element of X; :: thesis: for n being Nat holds (n -tuples_on X) --> x is n -ary

let n be Nat; :: thesis: (n -tuples_on X) --> x is n -ary

arity ((n -tuples_on X) --> x) = n by Th2;

hence (n -tuples_on X) --> x is n -ary by COMPUT_1:def 21; :: thesis: verum

end;
for n being Nat holds (n -tuples_on X) --> x is n -ary

let x be Element of X; :: thesis: for n being Nat holds (n -tuples_on X) --> x is n -ary

let n be Nat; :: thesis: (n -tuples_on X) --> x is n -ary

arity ((n -tuples_on X) --> x) = n by Th2;

hence (n -tuples_on X) --> x is n -ary by COMPUT_1:def 21; :: thesis: verum

registration

let X be non empty set ;

let x be Element of X;

let n be Nat;

coherence

for b_{1} being homogeneous PartFunc of (X *),X st b_{1} = (n -tuples_on X) --> x holds

b_{1} is n -ary
by Lm1;

end;
let x be Element of X;

let n be Nat;

coherence

for b

b

registration

let X be non empty set ;

ex b_{1} being non empty homogeneous quasi_total PartFunc of (X *),X st

( b_{1} is 2 -ary & b_{1} is associative & b_{1} is unital )

ex b_{1} being non empty homogeneous quasi_total PartFunc of (X *),X st b_{1} is 0 -ary

ex b_{1} being non empty homogeneous quasi_total PartFunc of (X *),X st b_{1} is 3 -ary

end;
cluster non empty Relation-like X * -defined X -valued Function-like homogeneous quasi_total 2 -ary associative unital for Element of bool [:(X *),X:];

existence ex b

( b

proof end;

cluster non empty Relation-like X * -defined X -valued Function-like homogeneous quasi_total 0 -ary for Element of bool [:(X *),X:];

existence ex b

proof end;

cluster non empty Relation-like X * -defined X -valued Function-like homogeneous quasi_total 3 -ary for Element of bool [:(X *),X:];

existence ex b

proof end;

theorem Th3: :: AOFA_000:3

for X being non empty set

for p being FinSequence of FinTrees X

for x, t being set st t in rng p holds

t <> x -tree p

for p being FinSequence of FinTrees X

for x, t being set st t in rng p holds

t <> x -tree p

proof end;

:: deftheorem defines +* AOFA_000:def 4 :

for f, g being Function

for X being set holds (f,X) +* g = g +* (f | X);

for f, g being Function

for X being set holds (f,X) +* g = g +* (f | X);

definition

let X, Y be non empty set ;

let f, g be Element of Funcs (X,Y);

let A be set ;

:: original: +*

redefine func (f,A) +* g -> Element of Funcs (X,Y);

coherence

(f,A) +* g is Element of Funcs (X,Y)

end;
let f, g be Element of Funcs (X,Y);

let A be set ;

:: original: +*

redefine func (f,A) +* g -> Element of Funcs (X,Y);

coherence

(f,A) +* g is Element of Funcs (X,Y)

proof end;

definition

let X, Y, Z be non empty set ;

let f be Element of Funcs (X,Y);

let g be Element of Funcs (Y,Z);

:: original: *

redefine func g * f -> Element of Funcs (X,Z);

coherence

f * g is Element of Funcs (X,Z)

end;
let f be Element of Funcs (X,Y);

let g be Element of Funcs (Y,Z);

:: original: *

redefine func g * f -> Element of Funcs (X,Z);

coherence

f * g is Element of Funcs (X,Z)

proof end;

definition

let f be Function;

let x be set ;

{ ((iter (f,n)) . x) where n is Element of NAT : x in dom (iter (f,n)) } is set ;

end;
let x be set ;

func f orbit x -> set equals :: AOFA_000:def 5

{ ((iter (f,n)) . x) where n is Element of NAT : x in dom (iter (f,n)) } ;

coherence { ((iter (f,n)) . x) where n is Element of NAT : x in dom (iter (f,n)) } ;

{ ((iter (f,n)) . x) where n is Element of NAT : x in dom (iter (f,n)) } is set ;

:: deftheorem defines orbit AOFA_000:def 5 :

for f being Function

for x being set holds f orbit x = { ((iter (f,n)) . x) where n is Element of NAT : x in dom (iter (f,n)) } ;

for f being Function

for x being set holds f orbit x = { ((iter (f,n)) . x) where n is Element of NAT : x in dom (iter (f,n)) } ;

definition

let f be Function;

assume B1: rng f c= dom f ;

let A, x be set ;

defpred S_{1}[ Nat] means for a being set st a in dom f holds

a in dom (iter (f,$1));

A1: field f = dom f by B1, XBOOLE_1:12;

then iter (f,0) = id (dom f) by FUNCT_7:68;

then A2: S_{1}[ 0 ]
by FUNCT_1:17;

_{1}[i]
from NAT_1:sch 1(A2, A3);

ex b_{1} being Function st

( dom b_{1} = dom f & ( for a being set st a in dom f holds

( ( f orbit a c= A implies b_{1} . a = x ) & ( for n being Nat st (iter (f,n)) . a nin A & ( for i being Nat st i < n holds

(iter (f,i)) . a in A ) holds

b_{1} . a = (iter (f,n)) . a ) ) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for a being set st a in dom f holds

( ( f orbit a c= A implies b_{1} . a = x ) & ( for n being Nat st (iter (f,n)) . a nin A & ( for i being Nat st i < n holds

(iter (f,i)) . a in A ) holds

b_{1} . a = (iter (f,n)) . a ) ) ) & dom b_{2} = dom f & ( for a being set st a in dom f holds

( ( f orbit a c= A implies b_{2} . a = x ) & ( for n being Nat st (iter (f,n)) . a nin A & ( for i being Nat st i < n holds

(iter (f,i)) . a in A ) holds

b_{2} . a = (iter (f,n)) . a ) ) ) holds

b_{1} = b_{2}

end;
assume B1: rng f c= dom f ;

let A, x be set ;

defpred S

a in dom (iter (f,$1));

A1: field f = dom f by B1, XBOOLE_1:12;

then iter (f,0) = id (dom f) by FUNCT_7:68;

then A2: S

A3: now :: thesis: for i being Element of NAT st S_{1}[i] holds

S_{1}[i + 1]

A8:
for i being Element of NAT holds SS

let i be Element of NAT ; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A4: S_{1}[i]
; :: thesis: S_{1}[i + 1]

thus S_{1}[i + 1]
:: thesis: verum

end;
assume A4: S

thus S

proof

let a be set ; :: thesis: ( a in dom f implies a in dom (iter (f,(i + 1))) )

assume a in dom f ; :: thesis: a in dom (iter (f,(i + 1)))

then A5: a in dom (iter (f,i)) by A4;

then A6: (iter (f,i)) . a in rng (iter (f,i)) by FUNCT_1:def 3;

A7: rng (iter (f,i)) c= dom f by A1, FUNCT_7:72;

iter (f,(i + 1)) = f * (iter (f,i)) by FUNCT_7:71;

hence a in dom (iter (f,(i + 1))) by A5, A6, A7, FUNCT_1:11; :: thesis: verum

end;
assume a in dom f ; :: thesis: a in dom (iter (f,(i + 1)))

then A5: a in dom (iter (f,i)) by A4;

then A6: (iter (f,i)) . a in rng (iter (f,i)) by FUNCT_1:def 3;

A7: rng (iter (f,i)) c= dom f by A1, FUNCT_7:72;

iter (f,(i + 1)) = f * (iter (f,i)) by FUNCT_7:71;

hence a in dom (iter (f,(i + 1))) by A5, A6, A7, FUNCT_1:11; :: thesis: verum

func (A,x) iter f -> Function means :: AOFA_000:def 6

( dom it = dom f & ( for a being set st a in dom f holds

( ( f orbit a c= A implies it . a = x ) & ( for n being Nat st (iter (f,n)) . a nin A & ( for i being Nat st i < n holds

(iter (f,i)) . a in A ) holds

it . a = (iter (f,n)) . a ) ) ) );

existence ( dom it = dom f & ( for a being set st a in dom f holds

( ( f orbit a c= A implies it . a = x ) & ( for n being Nat st (iter (f,n)) . a nin A & ( for i being Nat st i < n holds

(iter (f,i)) . a in A ) holds

it . a = (iter (f,n)) . a ) ) ) );

ex b

( dom b

( ( f orbit a c= A implies b

(iter (f,i)) . a in A ) holds

b

proof end;

uniqueness for b

( ( f orbit a c= A implies b

(iter (f,i)) . a in A ) holds

b

( ( f orbit a c= A implies b

(iter (f,i)) . a in A ) holds

b

b

proof end;

:: deftheorem defines iter AOFA_000:def 6 :

for f being Function st rng f c= dom f holds

for A, x being set

for b_{4} being Function holds

( b_{4} = (A,x) iter f iff ( dom b_{4} = dom f & ( for a being set st a in dom f holds

( ( f orbit a c= A implies b_{4} . a = x ) & ( for n being Nat st (iter (f,n)) . a nin A & ( for i being Nat st i < n holds

(iter (f,i)) . a in A ) holds

b_{4} . a = (iter (f,n)) . a ) ) ) ) );

for f being Function st rng f c= dom f holds

for A, x being set

for b

( b

( ( f orbit a c= A implies b

(iter (f,i)) . a in A ) holds

b

definition

let f be Function;

assume B1: rng f c= dom f ;

let A be set ;

let g be Function;

defpred S_{1}[ Nat] means for a being set st a in dom f holds

a in dom (iter (f,$1));

A1: field f = dom f by B1, XBOOLE_1:12;

then iter (f,0) = id (dom f) by FUNCT_7:68;

then A2: S_{1}[ 0 ]
by FUNCT_1:17;

_{1}[i]
from NAT_1:sch 1(A2, A3);

ex b_{1} being Function st

( dom b_{1} = dom f & ( for a being set st a in dom f holds

( ( f orbit a c= A implies b_{1} . a = g . a ) & ( for n being Nat st (iter (f,n)) . a nin A & ( for i being Nat st i < n holds

(iter (f,i)) . a in A ) holds

b_{1} . a = (iter (f,n)) . a ) ) ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for a being set st a in dom f holds

( ( f orbit a c= A implies b_{1} . a = g . a ) & ( for n being Nat st (iter (f,n)) . a nin A & ( for i being Nat st i < n holds

(iter (f,i)) . a in A ) holds

b_{1} . a = (iter (f,n)) . a ) ) ) & dom b_{2} = dom f & ( for a being set st a in dom f holds

( ( f orbit a c= A implies b_{2} . a = g . a ) & ( for n being Nat st (iter (f,n)) . a nin A & ( for i being Nat st i < n holds

(iter (f,i)) . a in A ) holds

b_{2} . a = (iter (f,n)) . a ) ) ) holds

b_{1} = b_{2}

end;
assume B1: rng f c= dom f ;

let A be set ;

let g be Function;

defpred S

a in dom (iter (f,$1));

A1: field f = dom f by B1, XBOOLE_1:12;

then iter (f,0) = id (dom f) by FUNCT_7:68;

then A2: S

A3: now :: thesis: for i being Element of NAT st S_{1}[i] holds

S_{1}[i + 1]

A8:
for i being Element of NAT holds SS

let i be Element of NAT ; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A4: S_{1}[i]
; :: thesis: S_{1}[i + 1]

thus S_{1}[i + 1]
:: thesis: verum

end;
assume A4: S

thus S

proof

let a be set ; :: thesis: ( a in dom f implies a in dom (iter (f,(i + 1))) )

assume a in dom f ; :: thesis: a in dom (iter (f,(i + 1)))

then A5: a in dom (iter (f,i)) by A4;

then A6: (iter (f,i)) . a in rng (iter (f,i)) by FUNCT_1:def 3;

A7: rng (iter (f,i)) c= dom f by A1, FUNCT_7:72;

iter (f,(i + 1)) = f * (iter (f,i)) by FUNCT_7:71;

hence a in dom (iter (f,(i + 1))) by A5, A6, A7, FUNCT_1:11; :: thesis: verum

end;
assume a in dom f ; :: thesis: a in dom (iter (f,(i + 1)))

then A5: a in dom (iter (f,i)) by A4;

then A6: (iter (f,i)) . a in rng (iter (f,i)) by FUNCT_1:def 3;

A7: rng (iter (f,i)) c= dom f by A1, FUNCT_7:72;

iter (f,(i + 1)) = f * (iter (f,i)) by FUNCT_7:71;

hence a in dom (iter (f,(i + 1))) by A5, A6, A7, FUNCT_1:11; :: thesis: verum

func (A,g) iter f -> Function means :Def7: :: AOFA_000:def 7

( dom it = dom f & ( for a being set st a in dom f holds

( ( f orbit a c= A implies it . a = g . a ) & ( for n being Nat st (iter (f,n)) . a nin A & ( for i being Nat st i < n holds

(iter (f,i)) . a in A ) holds

it . a = (iter (f,n)) . a ) ) ) );

existence ( dom it = dom f & ( for a being set st a in dom f holds

( ( f orbit a c= A implies it . a = g . a ) & ( for n being Nat st (iter (f,n)) . a nin A & ( for i being Nat st i < n holds

(iter (f,i)) . a in A ) holds

it . a = (iter (f,n)) . a ) ) ) );

ex b

( dom b

( ( f orbit a c= A implies b

(iter (f,i)) . a in A ) holds

b

proof end;

uniqueness for b

( ( f orbit a c= A implies b

(iter (f,i)) . a in A ) holds

b

( ( f orbit a c= A implies b

(iter (f,i)) . a in A ) holds

b

b

proof end;

:: deftheorem Def7 defines iter AOFA_000:def 7 :

for f being Function st rng f c= dom f holds

for A being set

for g, b_{4} being Function holds

( b_{4} = (A,g) iter f iff ( dom b_{4} = dom f & ( for a being set st a in dom f holds

( ( f orbit a c= A implies b_{4} . a = g . a ) & ( for n being Nat st (iter (f,n)) . a nin A & ( for i being Nat st i < n holds

(iter (f,i)) . a in A ) holds

b_{4} . a = (iter (f,n)) . a ) ) ) ) );

for f being Function st rng f c= dom f holds

for A being set

for g, b

( b

( ( f orbit a c= A implies b

(iter (f,i)) . a in A ) holds

b

theorem Th10: :: AOFA_000:10

for f, g being Function

for a, A being set st rng f c= dom f & a in dom f & not f orbit a c= A holds

ex n being Nat st

( ((A,g) iter f) . a = (iter (f,n)) . a & (iter (f,n)) . a nin A & ( for i being Nat st i < n holds

(iter (f,i)) . a in A ) )

for a, A being set st rng f c= dom f & a in dom f & not f orbit a c= A holds

ex n being Nat st

( ((A,g) iter f) . a = (iter (f,n)) . a & (iter (f,n)) . a nin A & ( for i being Nat st i < n holds

(iter (f,i)) . a in A ) )

proof end;

theorem Th11: :: AOFA_000:11

for f, g being Function

for a, A being set st rng f c= dom f & a in dom f & g * f = g & a in A holds

((A,g) iter f) . a = ((A,g) iter f) . (f . a)

for a, A being set st rng f c= dom f & a in dom f & g * f = g & a in A holds

((A,g) iter f) . a = ((A,g) iter f) . (f . a)

proof end;

theorem Th12: :: AOFA_000:12

for f, g being Function

for a, A being set st rng f c= dom f & a in dom f & a nin A holds

((A,g) iter f) . a = a

for a, A being set st rng f c= dom f & a in dom f & a nin A holds

((A,g) iter f) . a = a

proof end;

definition

let X be non empty set ;

let f be Element of Funcs (X,X);

let A be set ;

let g be Element of Funcs (X,X);

:: original: iter

redefine func (A,g) iter f -> Element of Funcs (X,X);

coherence

(A,g) iter f is Element of Funcs (X,X)

end;
let f be Element of Funcs (X,X);

let A be set ;

let g be Element of Funcs (X,X);

:: original: iter

redefine func (A,g) iter f -> Element of Funcs (X,X);

coherence

(A,g) iter f is Element of Funcs (X,X)

proof end;

begin

theorem Th13: :: AOFA_000:13

for X being non empty set

for S being non empty FinSequence of NAT ex A being Universal_Algebra st

( the carrier of A = X & signature A = S )

for S being non empty FinSequence of NAT ex A being Universal_Algebra st

( the carrier of A = X & signature A = S )

proof end;

theorem Th14: :: AOFA_000:14

for S being non empty FinSequence of NAT ex A being Universal_Algebra st

( the carrier of A = NAT & signature A = S & ( for i, j being Nat st i in dom S & j = S . i holds

the charact of A . i = (j -tuples_on NAT) --> i ) )

( the carrier of A = NAT & signature A = S & ( for i, j being Nat st i in dom S & j = S . i holds

the charact of A . i = (j -tuples_on NAT) --> i ) )

proof end;

theorem :: AOFA_000:15

for S being non empty FinSequence of NAT

for i, j being Nat st i in dom S & j = S . i holds

for X being non empty set

for f being Function of (j -tuples_on X),X ex A being Universal_Algebra st

( the carrier of A = X & signature A = S & the charact of A . i = f )

for i, j being Nat st i in dom S & j = S . i holds

for X being non empty set

for f being Function of (j -tuples_on X),X ex A being Universal_Algebra st

( the carrier of A = X & signature A = S & the charact of A . i = f )

proof end;

registration

let f be non empty FinSequence of NAT ;

let D be non empty disjoint_with_NAT set ;

coherence

for b_{1} being Element of (FreeUnivAlgNSG (f,D)) holds

( b_{1} is Relation-like & b_{1} is Function-like )
;

end;
let D be non empty disjoint_with_NAT set ;

coherence

for b

( b

registration

let f be non empty FinSequence of NAT ;

let D be non empty disjoint_with_NAT set ;

coherence

for b_{1} being Element of (FreeUnivAlgNSG (f,D)) holds b_{1} is DecoratedTree-like
;

coherence

for b_{1} being FinSequence of (FreeUnivAlgNSG (f,D)) holds b_{1} is DTree-yielding
;

end;
let D be non empty disjoint_with_NAT set ;

coherence

for b

coherence

for b

theorem Th16: :: AOFA_000:16

for G being non empty DTConstrStr

for t being set holds

( not t in TS G or ex d being Symbol of G st

( d in Terminals G & t = root-tree d ) or ex o being Symbol of G ex p being FinSequence of TS G st

( o ==> roots p & t = o -tree p ) )

for t being set holds

( not t in TS G or ex d being Symbol of G st

( d in Terminals G & t = root-tree d ) or ex o being Symbol of G ex p being FinSequence of TS G st

( o ==> roots p & t = o -tree p ) )

proof end;

theorem Th17: :: AOFA_000:17

for X being non empty disjoint_with_NAT set

for S being non empty FinSequence of NAT

for i being Nat st i in dom S holds

for p being FinSequence of (FreeUnivAlgNSG (S,X)) st len p = S . i holds

(Den ((In (i,(dom the charact of (FreeUnivAlgNSG (S,X))))),(FreeUnivAlgNSG (S,X)))) . p = i -tree p

for S being non empty FinSequence of NAT

for i being Nat st i in dom S holds

for p being FinSequence of (FreeUnivAlgNSG (S,X)) st len p = S . i holds

(Den ((In (i,(dom the charact of (FreeUnivAlgNSG (S,X))))),(FreeUnivAlgNSG (S,X)))) . p = i -tree p

proof end;

definition

let A be non-empty UAStr ;

let B be Subset of A;

let n be Nat;

ex b_{1} being Subset of A ex F being Function of NAT,(bool the carrier of A) st

( b_{1} = F . n & F . 0 = B & ( for n being Nat holds F . (n + 1) = (F . n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= F . n ) } ) )

for b_{1}, b_{2} being Subset of A st ex F being Function of NAT,(bool the carrier of A) st

( b_{1} = F . n & F . 0 = B & ( for n being Nat holds F . (n + 1) = (F . n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= F . n ) } ) ) & ex F being Function of NAT,(bool the carrier of A) st

( b_{2} = F . n & F . 0 = B & ( for n being Nat holds F . (n + 1) = (F . n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= F . n ) } ) ) holds

b_{1} = b_{2}

end;
let B be Subset of A;

let n be Nat;

func B |^ n -> Subset of A means :Def8: :: AOFA_000:def 8

ex F being Function of NAT,(bool the carrier of A) st

( it = F . n & F . 0 = B & ( for n being Nat holds F . (n + 1) = (F . n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= F . n ) } ) );

existence ex F being Function of NAT,(bool the carrier of A) st

( it = F . n & F . 0 = B & ( for n being Nat holds F . (n + 1) = (F . n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= F . n ) } ) );

ex b

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def8 defines |^ AOFA_000:def 8 :

for A being non-empty UAStr

for B being Subset of A

for n being Nat

for b_{4} being Subset of A holds

( b_{4} = B |^ n iff ex F being Function of NAT,(bool the carrier of A) st

( b_{4} = F . n & F . 0 = B & ( for n being Nat holds F . (n + 1) = (F . n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= F . n ) } ) ) );

for A being non-empty UAStr

for B being Subset of A

for n being Nat

for b

( b

( b

theorem Th19: :: AOFA_000:19

for A being Universal_Algebra

for B being Subset of A

for n being Nat holds B |^ (n + 1) = (B |^ n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= B |^ n ) }

for B being Subset of A

for n being Nat holds B |^ (n + 1) = (B |^ n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= B |^ n ) }

proof end;

theorem Th20: :: AOFA_000:20

for A being Universal_Algebra

for B being Subset of A

for n being Nat

for x being set holds

( x in B |^ (n + 1) iff ( x in B |^ n or ex o being Element of dom the charact of A ex p being Element of the carrier of A * st

( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ n ) ) )

for B being Subset of A

for n being Nat

for x being set holds

( x in B |^ (n + 1) iff ( x in B |^ n or ex o being Element of dom the charact of A ex p being Element of the carrier of A * st

( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ n ) ) )

proof end;

theorem Th21: :: AOFA_000:21

for A being Universal_Algebra

for B being Subset of A

for n, m being Nat st n <= m holds

B |^ n c= B |^ m

for B being Subset of A

for n, m being Nat st n <= m holds

B |^ n c= B |^ m

proof end;

theorem Th22: :: AOFA_000:22

for A being Universal_Algebra

for B1, B2 being Subset of A st B1 c= B2 holds

for n being Nat holds B1 |^ n c= B2 |^ n

for B1, B2 being Subset of A st B1 c= B2 holds

for n being Nat holds B1 |^ n c= B2 |^ n

proof end;

theorem Th23: :: AOFA_000:23

for A being Universal_Algebra

for B being Subset of A

for n being Nat

for x being set holds

( x in B |^ (n + 1) iff ( x in B or ex o being Element of dom the charact of A ex p being Element of the carrier of A * st

( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ n ) ) )

for B being Subset of A

for n being Nat

for x being set holds

( x in B |^ (n + 1) iff ( x in B or ex o being Element of dom the charact of A ex p being Element of the carrier of A * st

( x = (Den (o,A)) . p & p in dom (Den (o,A)) & rng p c= B |^ n ) ) )

proof end;

scheme :: AOFA_000:sch 1

MaxVal{ F_{1}() -> non empty set , F_{2}() -> set , P_{1}[ set , set ] } :

provided

MaxVal{ F

provided

A1:
F_{2}() is finite
and

A2: for x being Element of F_{1}() st x in F_{2}() holds

ex n being Nat st P_{1}[x,n]
and

A3: for x being Element of F_{1}()

for n, m being Nat st P_{1}[x,n] & n <= m holds

P_{1}[x,m]

A2: for x being Element of F

ex n being Nat st P

A3: for x being Element of F

for n, m being Nat st P

P

proof end;

theorem Th24: :: AOFA_000:24

for A being Universal_Algebra

for B being Subset of A ex C being Subset of A st

( C = union { (B |^ n) where n is Element of NAT : verum } & C is opers_closed )

for B being Subset of A ex C being Subset of A st

( C = union { (B |^ n) where n is Element of NAT : verum } & C is opers_closed )

proof end;

theorem Th25: :: AOFA_000:25

for A being Universal_Algebra

for B, C being Subset of A st C is opers_closed & B c= C holds

union { (B |^ n) where n is Element of NAT : verum } c= C

for B, C being Subset of A st C is opers_closed & B c= C holds

union { (B |^ n) where n is Element of NAT : verum } c= C

proof end;

definition

let A be Universal_Algebra;

the carrier of A \ (union { (rng o) where o is Element of Operations A : verum } ) is Subset of A ;

end;
func Generators A -> Subset of A equals :: AOFA_000:def 9

the carrier of A \ (union { (rng o) where o is Element of Operations A : verum } );

coherence the carrier of A \ (union { (rng o) where o is Element of Operations A : verum } );

the carrier of A \ (union { (rng o) where o is Element of Operations A : verum } ) is Subset of A ;

:: deftheorem defines Generators AOFA_000:def 9 :

for A being Universal_Algebra holds Generators A = the carrier of A \ (union { (rng o) where o is Element of Operations A : verum } );

for A being Universal_Algebra holds Generators A = the carrier of A \ (union { (rng o) where o is Element of Operations A : verum } );

theorem Th26: :: AOFA_000:26

for A being Universal_Algebra

for a being Element of A holds

( a in Generators A iff for o being Element of Operations A holds not a in rng o )

for a being Element of A holds

( a in Generators A iff for o being Element of Operations A holds not a in rng o )

proof end;

theorem Th30: :: AOFA_000:30

for A being Universal_Algebra

for G being Subset of A holds

( G is GeneratorSet of A iff for I being Element of A ex n being Nat st I in G |^ n )

for G being Subset of A holds

( G is GeneratorSet of A iff for I being Element of A ex n being Nat st I in G |^ n )

proof end;

theorem Th31: :: AOFA_000:31

for A being Universal_Algebra

for B being Subset of A

for G being GeneratorSet of A st G c= B holds

B is GeneratorSet of A

for B being Subset of A

for G being GeneratorSet of A st G c= B holds

B is GeneratorSet of A

proof end;

theorem Th32: :: AOFA_000:32

for A being Universal_Algebra

for G being GeneratorSet of A

for a being Element of A st ( for o being Element of Operations A holds not a in rng o ) holds

a in G

for G being GeneratorSet of A

for a being Element of A st ( for o being Element of Operations A holds not a in rng o ) holds

a in G

proof end;

registration

let A be free Universal_Algebra;

coherence

for b_{1} being GeneratorSet of A st b_{1} = Generators A holds

b_{1} is free

end;
coherence

for b

b

proof end;

definition

let A be free Universal_Algebra;

:: original: Generators

redefine func Generators A -> GeneratorSet of A;

coherence

Generators A is GeneratorSet of A

end;
:: original: Generators

redefine func Generators A -> GeneratorSet of A;

coherence

Generators A is GeneratorSet of A

proof end;

theorem :: AOFA_000:35

for A being free Universal_Algebra

for G being GeneratorSet of A

for B being Universal_Algebra

for h1, h2 being Function of A,B st h1 is_homomorphism A,B & h2 is_homomorphism A,B & h1 | G = h2 | G holds

h1 = h2

for G being GeneratorSet of A

for B being Universal_Algebra

for h1, h2 being Function of A,B st h1 is_homomorphism A,B & h2 is_homomorphism A,B & h1 | G = h2 | G holds

h1 = h2

proof end;

Lm2: for A being free Universal_Algebra

for o1, o2 being OperSymbol of A

for p1, p2 being FinSequence st p1 in dom (Den (o1,A)) & p2 in dom (Den (o2,A)) & (Den (o1,A)) . p1 = (Den (o2,A)) . p2 holds

o1 = o2

proof end;

theorem Th36: :: AOFA_000:36

for A being free Universal_Algebra

for o1, o2 being OperSymbol of A

for p1, p2 being FinSequence st p1 in dom (Den (o1,A)) & p2 in dom (Den (o2,A)) & (Den (o1,A)) . p1 = (Den (o2,A)) . p2 holds

( o1 = o2 & p1 = p2 )

for o1, o2 being OperSymbol of A

for p1, p2 being FinSequence st p1 in dom (Den (o1,A)) & p2 in dom (Den (o2,A)) & (Den (o1,A)) . p1 = (Den (o2,A)) . p2 holds

( o1 = o2 & p1 = p2 )

proof end;

theorem :: AOFA_000:37

for A being free Universal_Algebra

for o1, o2 being Element of Operations A

for p1, p2 being FinSequence st p1 in dom o1 & p2 in dom o2 & o1 . p1 = o2 . p2 holds

( o1 = o2 & p1 = p2 )

for o1, o2 being Element of Operations A

for p1, p2 being FinSequence st p1 in dom o1 & p2 in dom o2 & o1 . p1 = o2 . p2 holds

( o1 = o2 & p1 = p2 )

proof end;

theorem Th38: :: AOFA_000:38

for A being free Universal_Algebra

for o being OperSymbol of A

for p being FinSequence st p in dom (Den (o,A)) holds

for a being set st a in rng p holds

a <> (Den (o,A)) . p

for o being OperSymbol of A

for p being FinSequence st p in dom (Den (o,A)) holds

for a being set st a in rng p holds

a <> (Den (o,A)) . p

proof end;

theorem Th39: :: AOFA_000:39

for A being free Universal_Algebra

for G being GeneratorSet of A

for o being OperSymbol of A st ( for o9 being OperSymbol of A

for p being FinSequence st p in dom (Den (o9,A)) & (Den (o9,A)) . p in G holds

o9 <> o ) holds

for p being FinSequence st p in dom (Den (o,A)) holds

for n being Nat st (Den (o,A)) . p in G |^ (n + 1) holds

rng p c= G |^ n

for G being GeneratorSet of A

for o being OperSymbol of A st ( for o9 being OperSymbol of A

for p being FinSequence st p in dom (Den (o9,A)) & (Den (o9,A)) . p in G holds

o9 <> o ) holds

for p being FinSequence st p in dom (Den (o,A)) holds

for n being Nat st (Den (o,A)) . p in G |^ (n + 1) holds

rng p c= G |^ n

proof end;

theorem :: AOFA_000:40

for A being free Universal_Algebra

for o being OperSymbol of A

for p being FinSequence st p in dom (Den (o,A)) holds

for n being Nat st (Den (o,A)) . p in (Generators A) |^ (n + 1) holds

rng p c= (Generators A) |^ n

for o being OperSymbol of A

for p being FinSequence st p in dom (Den (o,A)) holds

for n being Nat st (Den (o,A)) . p in (Generators A) |^ (n + 1) holds

rng p c= (Generators A) |^ n

proof end;

begin

definition

let S be non empty UAStr ;

end;
attr S is with_empty-instruction means :Def10: :: AOFA_000:def 10

( 1 in dom the charact of S & the charact of S . 1 is non empty homogeneous quasi_total 0 -ary PartFunc of ( the carrier of S *), the carrier of S );

( 1 in dom the charact of S & the charact of S . 1 is non empty homogeneous quasi_total 0 -ary PartFunc of ( the carrier of S *), the carrier of S );

attr S is with_catenation means :Def11: :: AOFA_000:def 11

( 2 in dom the charact of S & the charact of S . 2 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of S *), the carrier of S );

( 2 in dom the charact of S & the charact of S . 2 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of S *), the carrier of S );

attr S is with_if-instruction means :Def12: :: AOFA_000:def 12

( 3 in dom the charact of S & the charact of S . 3 is non empty homogeneous quasi_total 3 -ary PartFunc of ( the carrier of S *), the carrier of S );

( 3 in dom the charact of S & the charact of S . 3 is non empty homogeneous quasi_total 3 -ary PartFunc of ( the carrier of S *), the carrier of S );

attr S is with_while-instruction means :Def13: :: AOFA_000:def 13

( 4 in dom the charact of S & the charact of S . 4 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of S *), the carrier of S );

( 4 in dom the charact of S & the charact of S . 4 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of S *), the carrier of S );

attr S is associative means :Def14: :: AOFA_000:def 14

the charact of S . 2 is non empty homogeneous quasi_total 2 -ary associative PartFunc of ( the carrier of S *), the carrier of S;

the charact of S . 2 is non empty homogeneous quasi_total 2 -ary associative PartFunc of ( the carrier of S *), the carrier of S;

:: deftheorem Def10 defines with_empty-instruction AOFA_000:def 10 :

for S being non empty UAStr holds

( S is with_empty-instruction iff ( 1 in dom the charact of S & the charact of S . 1 is non empty homogeneous quasi_total 0 -ary PartFunc of ( the carrier of S *), the carrier of S ) );

for S being non empty UAStr holds

( S is with_empty-instruction iff ( 1 in dom the charact of S & the charact of S . 1 is non empty homogeneous quasi_total 0 -ary PartFunc of ( the carrier of S *), the carrier of S ) );

:: deftheorem Def11 defines with_catenation AOFA_000:def 11 :

for S being non empty UAStr holds

( S is with_catenation iff ( 2 in dom the charact of S & the charact of S . 2 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of S *), the carrier of S ) );

for S being non empty UAStr holds

( S is with_catenation iff ( 2 in dom the charact of S & the charact of S . 2 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of S *), the carrier of S ) );

:: deftheorem Def12 defines with_if-instruction AOFA_000:def 12 :

for S being non empty UAStr holds

( S is with_if-instruction iff ( 3 in dom the charact of S & the charact of S . 3 is non empty homogeneous quasi_total 3 -ary PartFunc of ( the carrier of S *), the carrier of S ) );

for S being non empty UAStr holds

( S is with_if-instruction iff ( 3 in dom the charact of S & the charact of S . 3 is non empty homogeneous quasi_total 3 -ary PartFunc of ( the carrier of S *), the carrier of S ) );

:: deftheorem Def13 defines with_while-instruction AOFA_000:def 13 :

for S being non empty UAStr holds

( S is with_while-instruction iff ( 4 in dom the charact of S & the charact of S . 4 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of S *), the carrier of S ) );

for S being non empty UAStr holds

( S is with_while-instruction iff ( 4 in dom the charact of S & the charact of S . 4 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of S *), the carrier of S ) );

:: deftheorem Def14 defines associative AOFA_000:def 14 :

for S being non empty UAStr holds

( S is associative iff the charact of S . 2 is non empty homogeneous quasi_total 2 -ary associative PartFunc of ( the carrier of S *), the carrier of S );

for S being non empty UAStr holds

( S is associative iff the charact of S . 2 is non empty homogeneous quasi_total 2 -ary associative PartFunc of ( the carrier of S *), the carrier of S );

:: deftheorem Def15 defines unital AOFA_000:def 15 :

for S being non-empty UAStr holds

( S is unital iff ex f being non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of S *), the carrier of S st

( f = the charact of S . 2 & (Den ((In (1,(dom the charact of S))),S)) . {} is_a_unity_wrt f ) );

for S being non-empty UAStr holds

( S is unital iff ex f being non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of S *), the carrier of S st

( f = the charact of S . 2 & (Den ((In (1,(dom the charact of S))),S)) . {} is_a_unity_wrt f ) );

theorem Th41: :: AOFA_000:41

for X being non empty set

for x being Element of X

for c being non empty homogeneous quasi_total 2 -ary associative unital PartFunc of (X *),X st x is_a_unity_wrt c holds

for i being non empty homogeneous quasi_total 3 -ary PartFunc of (X *),X

for w being non empty homogeneous quasi_total 2 -ary PartFunc of (X *),X ex S being strict non-empty UAStr st

( the carrier of S = X & the charact of S = <*((0 -tuples_on X) --> x),c*> ^ <*i,w*> & S is with_empty-instruction & S is with_catenation & S is unital & S is associative & S is with_if-instruction & S is with_while-instruction & S is quasi_total & S is partial )

for x being Element of X

for c being non empty homogeneous quasi_total 2 -ary associative unital PartFunc of (X *),X st x is_a_unity_wrt c holds

for i being non empty homogeneous quasi_total 3 -ary PartFunc of (X *),X

for w being non empty homogeneous quasi_total 2 -ary PartFunc of (X *),X ex S being strict non-empty UAStr st

( the carrier of S = X & the charact of S = <*((0 -tuples_on X) --> x),c*> ^ <*i,w*> & S is with_empty-instruction & S is with_catenation & S is unital & S is associative & S is with_if-instruction & S is with_while-instruction & S is quasi_total & S is partial )

proof end;

registration

ex b_{1} being strict partial quasi_total non-empty UAStr st

( b_{1} is with_empty-instruction & b_{1} is with_catenation & b_{1} is with_if-instruction & b_{1} is with_while-instruction & b_{1} is unital & b_{1} is associative )
end;

cluster non empty strict partial quasi_total non-empty with_empty-instruction with_catenation with_if-instruction with_while-instruction associative unital for UAStr ;

existence ex b

( b

proof end;

definition

mode preIfWhileAlgebra is with_empty-instruction with_catenation with_if-instruction with_while-instruction Universal_Algebra;

end;
theorem Th42: :: AOFA_000:42

for A being non-empty with_empty-instruction UAStr holds dom (Den ((In (1,(dom the charact of A))),A)) = {{}}

proof end;

definition

let A be non-empty with_empty-instruction UAStr ;

(Den ((In (1,(dom the charact of A))),A)) . {} is Algorithm of A

end;
func EmptyIns A -> Algorithm of A equals :: AOFA_000:def 16

(Den ((In (1,(dom the charact of A))),A)) . {};

coherence (Den ((In (1,(dom the charact of A))),A)) . {};

(Den ((In (1,(dom the charact of A))),A)) . {} is Algorithm of A

proof end;

:: deftheorem defines EmptyIns AOFA_000:def 16 :

for A being non-empty with_empty-instruction UAStr holds EmptyIns A = (Den ((In (1,(dom the charact of A))),A)) . {};

for A being non-empty with_empty-instruction UAStr holds EmptyIns A = (Den ((In (1,(dom the charact of A))),A)) . {};

theorem :: AOFA_000:43

for A being with_empty-instruction Universal_Algebra

for o being Element of Operations A st o = Den ((In (1,(dom the charact of A))),A) holds

( arity o = 0 & EmptyIns A in rng o )

for o being Element of Operations A st o = Den ((In (1,(dom the charact of A))),A) holds

( arity o = 0 & EmptyIns A in rng o )

proof end;

theorem Th44: :: AOFA_000:44

for A being non-empty with_catenation UAStr holds dom (Den ((In (2,(dom the charact of A))),A)) = 2 -tuples_on the carrier of A

proof end;

definition

let A be non-empty with_catenation UAStr ;

let I1, I2 be Algorithm of A;

(Den ((In (2,(dom the charact of A))),A)) . <*I1,I2*> is Algorithm of A

end;
let I1, I2 be Algorithm of A;

func I1 \; I2 -> Algorithm of A equals :: AOFA_000:def 17

(Den ((In (2,(dom the charact of A))),A)) . <*I1,I2*>;

coherence (Den ((In (2,(dom the charact of A))),A)) . <*I1,I2*>;

(Den ((In (2,(dom the charact of A))),A)) . <*I1,I2*> is Algorithm of A

proof end;

:: deftheorem defines \; AOFA_000:def 17 :

for A being non-empty with_catenation UAStr

for I1, I2 being Algorithm of A holds I1 \; I2 = (Den ((In (2,(dom the charact of A))),A)) . <*I1,I2*>;

for A being non-empty with_catenation UAStr

for I1, I2 being Algorithm of A holds I1 \; I2 = (Den ((In (2,(dom the charact of A))),A)) . <*I1,I2*>;

theorem :: AOFA_000:45

for A being non-empty with_empty-instruction with_catenation unital UAStr

for I being Element of A holds

( (EmptyIns A) \; I = I & I \; (EmptyIns A) = I )

for I being Element of A holds

( (EmptyIns A) \; I = I & I \; (EmptyIns A) = I )

proof end;

theorem :: AOFA_000:46

for A being non-empty with_catenation associative UAStr

for I1, I2, I3 being Element of A holds (I1 \; I2) \; I3 = I1 \; (I2 \; I3)

for I1, I2, I3 being Element of A holds (I1 \; I2) \; I3 = I1 \; (I2 \; I3)

proof end;

theorem Th47: :: AOFA_000:47

for A being non-empty with_if-instruction UAStr holds dom (Den ((In (3,(dom the charact of A))),A)) = 3 -tuples_on the carrier of A

proof end;

definition

let A be non-empty with_if-instruction UAStr ;

let C, I1, I2 be Algorithm of A;

(Den ((In (3,(dom the charact of A))),A)) . <*C,I1,I2*> is Algorithm of A

end;
let C, I1, I2 be Algorithm of A;

func if-then-else (C,I1,I2) -> Algorithm of A equals :: AOFA_000:def 18

(Den ((In (3,(dom the charact of A))),A)) . <*C,I1,I2*>;

coherence (Den ((In (3,(dom the charact of A))),A)) . <*C,I1,I2*>;

(Den ((In (3,(dom the charact of A))),A)) . <*C,I1,I2*> is Algorithm of A

proof end;

:: deftheorem defines if-then-else AOFA_000:def 18 :

for A being non-empty with_if-instruction UAStr

for C, I1, I2 being Algorithm of A holds if-then-else (C,I1,I2) = (Den ((In (3,(dom the charact of A))),A)) . <*C,I1,I2*>;

for A being non-empty with_if-instruction UAStr

for C, I1, I2 being Algorithm of A holds if-then-else (C,I1,I2) = (Den ((In (3,(dom the charact of A))),A)) . <*C,I1,I2*>;

definition

let A be non-empty with_empty-instruction with_if-instruction UAStr ;

let C, I be Algorithm of A;

coherence

if-then-else (C,I,(EmptyIns A)) is Algorithm of A ;

end;
let C, I be Algorithm of A;

coherence

if-then-else (C,I,(EmptyIns A)) is Algorithm of A ;

:: deftheorem defines if-then AOFA_000:def 19 :

for A being non-empty with_empty-instruction with_if-instruction UAStr

for C, I being Algorithm of A holds if-then (C,I) = if-then-else (C,I,(EmptyIns A));

for A being non-empty with_empty-instruction with_if-instruction UAStr

for C, I being Algorithm of A holds if-then (C,I) = if-then-else (C,I,(EmptyIns A));

theorem Th48: :: AOFA_000:48

for A being non-empty with_while-instruction UAStr holds dom (Den ((In (4,(dom the charact of A))),A)) = 2 -tuples_on the carrier of A

proof end;

definition

let A be non-empty with_while-instruction UAStr ;

let C, I be Algorithm of A;

(Den ((In (4,(dom the charact of A))),A)) . <*C,I*> is Algorithm of A

end;
let C, I be Algorithm of A;

func while (C,I) -> Algorithm of A equals :: AOFA_000:def 20

(Den ((In (4,(dom the charact of A))),A)) . <*C,I*>;

coherence (Den ((In (4,(dom the charact of A))),A)) . <*C,I*>;

(Den ((In (4,(dom the charact of A))),A)) . <*C,I*> is Algorithm of A

proof end;

:: deftheorem defines while AOFA_000:def 20 :

for A being non-empty with_while-instruction UAStr

for C, I being Algorithm of A holds while (C,I) = (Den ((In (4,(dom the charact of A))),A)) . <*C,I*>;

for A being non-empty with_while-instruction UAStr

for C, I being Algorithm of A holds while (C,I) = (Den ((In (4,(dom the charact of A))),A)) . <*C,I*>;

definition

let A be preIfWhileAlgebra;

let I0, C, I, J be Element of A;

coherence

I0 \; (while (C,(I \; J))) is Element of A ;

end;
let I0, C, I, J be Element of A;

coherence

I0 \; (while (C,(I \; J))) is Element of A ;

:: deftheorem defines for-do AOFA_000:def 21 :

for A being preIfWhileAlgebra

for I0, C, I, J being Element of A holds for-do (I0,C,J,I) = I0 \; (while (C,(I \; J)));

for A being preIfWhileAlgebra

for I0, C, I, J being Element of A holds for-do (I0,C,J,I) = I0 \; (while (C,(I \; J)));

definition

let A be preIfWhileAlgebra;

((( the carrier of A \ {(EmptyIns A)}) \ (rng (Den ((In (3,(dom the charact of A))),A)))) \ (rng (Den ((In (4,(dom the charact of A))),A)))) \ { (I1 \; I2) where I1, I2 is Algorithm of A : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } is Subset of A ;

end;
func ElementaryInstructions A -> Subset of A equals :: AOFA_000:def 22

((( the carrier of A \ {(EmptyIns A)}) \ (rng (Den ((In (3,(dom the charact of A))),A)))) \ (rng (Den ((In (4,(dom the charact of A))),A)))) \ { (I1 \; I2) where I1, I2 is Algorithm of A : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } ;

coherence ((( the carrier of A \ {(EmptyIns A)}) \ (rng (Den ((In (3,(dom the charact of A))),A)))) \ (rng (Den ((In (4,(dom the charact of A))),A)))) \ { (I1 \; I2) where I1, I2 is Algorithm of A : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } ;

((( the carrier of A \ {(EmptyIns A)}) \ (rng (Den ((In (3,(dom the charact of A))),A)))) \ (rng (Den ((In (4,(dom the charact of A))),A)))) \ { (I1 \; I2) where I1, I2 is Algorithm of A : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } is Subset of A ;

:: deftheorem defines ElementaryInstructions AOFA_000:def 22 :

for A being preIfWhileAlgebra holds ElementaryInstructions A = ((( the carrier of A \ {(EmptyIns A)}) \ (rng (Den ((In (3,(dom the charact of A))),A)))) \ (rng (Den ((In (4,(dom the charact of A))),A)))) \ { (I1 \; I2) where I1, I2 is Algorithm of A : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } ;

for A being preIfWhileAlgebra holds ElementaryInstructions A = ((( the carrier of A \ {(EmptyIns A)}) \ (rng (Den ((In (3,(dom the charact of A))),A)))) \ (rng (Den ((In (4,(dom the charact of A))),A)))) \ { (I1 \; I2) where I1, I2 is Algorithm of A : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } ;

theorem Th50: :: AOFA_000:50

for A being preIfWhileAlgebra

for I1, I2 being Element of A st I1 <> I1 \; I2 & I2 <> I1 \; I2 holds

I1 \; I2 nin ElementaryInstructions A

for I1, I2 being Element of A st I1 <> I1 \; I2 & I2 <> I1 \; I2 holds

I1 \; I2 nin ElementaryInstructions A

proof end;

theorem Th51: :: AOFA_000:51

for A being preIfWhileAlgebra

for C, I1, I2 being Element of A holds if-then-else (C,I1,I2) nin ElementaryInstructions A

for C, I1, I2 being Element of A holds if-then-else (C,I1,I2) nin ElementaryInstructions A

proof end;

theorem Th52: :: AOFA_000:52

for A being preIfWhileAlgebra

for C, I being Element of A holds while (C,I) nin ElementaryInstructions A

for C, I being Element of A holds while (C,I) nin ElementaryInstructions A

proof end;

theorem Th53: :: AOFA_000:53

for A being preIfWhileAlgebra

for I being Element of A holds

( not I nin ElementaryInstructions A or I = EmptyIns A or ex I1, I2 being Element of A st

( I = I1 \; I2 & I1 <> I1 \; I2 & I2 <> I1 \; I2 ) or ex C, I1, I2 being Element of A st I = if-then-else (C,I1,I2) or ex C, J being Element of A st I = while (C,J) )

for I being Element of A holds

( not I nin ElementaryInstructions A or I = EmptyIns A or ex I1, I2 being Element of A st

( I = I1 \; I2 & I1 <> I1 \; I2 & I2 <> I1 \; I2 ) or ex C, I1, I2 being Element of A st I = if-then-else (C,I1,I2) or ex C, J being Element of A st I = while (C,J) )

proof end;

definition

let A be preIfWhileAlgebra;

end;
attr A is degenerated means :Def24: :: AOFA_000:def 24

( ex I1, I2 being Element of A st

( ( I1 <> EmptyIns A & I1 \; I2 = I2 ) or ( I2 <> EmptyIns A & I1 \; I2 = I1 ) or ( ( I1 <> EmptyIns A or I2 <> EmptyIns A ) & I1 \; I2 = EmptyIns A ) ) or ex C, I1, I2 being Element of A st if-then-else (C,I1,I2) = EmptyIns A or ex C, I being Element of A st while (C,I) = EmptyIns A or ex I1, I2, C, J1, J2 being Element of A st

( I1 <> EmptyIns A & I2 <> EmptyIns A & I1 \; I2 = if-then-else (C,J1,J2) ) or ex I1, I2, C, J being Element of A st

( I1 <> EmptyIns A & I2 <> EmptyIns A & I1 \; I2 = while (C,J) ) or ex C1, I1, I2, C2, J being Element of A st if-then-else (C1,I1,I2) = while (C2,J) );

( ex I1, I2 being Element of A st

( ( I1 <> EmptyIns A & I1 \; I2 = I2 ) or ( I2 <> EmptyIns A & I1 \; I2 = I1 ) or ( ( I1 <> EmptyIns A or I2 <> EmptyIns A ) & I1 \; I2 = EmptyIns A ) ) or ex C, I1, I2 being Element of A st if-then-else (C,I1,I2) = EmptyIns A or ex C, I being Element of A st while (C,I) = EmptyIns A or ex I1, I2, C, J1, J2 being Element of A st

( I1 <> EmptyIns A & I2 <> EmptyIns A & I1 \; I2 = if-then-else (C,J1,J2) ) or ex I1, I2, C, J being Element of A st

( I1 <> EmptyIns A & I2 <> EmptyIns A & I1 \; I2 = while (C,J) ) or ex C1, I1, I2, C2, J being Element of A st if-then-else (C1,I1,I2) = while (C2,J) );

attr A is well_founded means :Def25: :: AOFA_000:def 25

ElementaryInstructions A is GeneratorSet of A;

ElementaryInstructions A is GeneratorSet of A;

:: deftheorem Def23 defines infinite AOFA_000:def 23 :

for A being preIfWhileAlgebra holds

( A is infinite iff ElementaryInstructions A is infinite );

for A being preIfWhileAlgebra holds

( A is infinite iff ElementaryInstructions A is infinite );

:: deftheorem Def24 defines degenerated AOFA_000:def 24 :

for A being preIfWhileAlgebra holds

( A is degenerated iff ( ex I1, I2 being Element of A st

( ( I1 <> EmptyIns A & I1 \; I2 = I2 ) or ( I2 <> EmptyIns A & I1 \; I2 = I1 ) or ( ( I1 <> EmptyIns A or I2 <> EmptyIns A ) & I1 \; I2 = EmptyIns A ) ) or ex C, I1, I2 being Element of A st if-then-else (C,I1,I2) = EmptyIns A or ex C, I being Element of A st while (C,I) = EmptyIns A or ex I1, I2, C, J1, J2 being Element of A st

( I1 <> EmptyIns A & I2 <> EmptyIns A & I1 \; I2 = if-then-else (C,J1,J2) ) or ex I1, I2, C, J being Element of A st

( I1 <> EmptyIns A & I2 <> EmptyIns A & I1 \; I2 = while (C,J) ) or ex C1, I1, I2, C2, J being Element of A st if-then-else (C1,I1,I2) = while (C2,J) ) );

for A being preIfWhileAlgebra holds

( A is degenerated iff ( ex I1, I2 being Element of A st

( ( I1 <> EmptyIns A & I1 \; I2 = I2 ) or ( I2 <> EmptyIns A & I1 \; I2 = I1 ) or ( ( I1 <> EmptyIns A or I2 <> EmptyIns A ) & I1 \; I2 = EmptyIns A ) ) or ex C, I1, I2 being Element of A st if-then-else (C,I1,I2) = EmptyIns A or ex C, I being Element of A st while (C,I) = EmptyIns A or ex I1, I2, C, J1, J2 being Element of A st

( I1 <> EmptyIns A & I2 <> EmptyIns A & I1 \; I2 = if-then-else (C,J1,J2) ) or ex I1, I2, C, J being Element of A st

( I1 <> EmptyIns A & I2 <> EmptyIns A & I1 \; I2 = while (C,J) ) or ex C1, I1, I2, C2, J being Element of A st if-then-else (C1,I1,I2) = while (C2,J) ) );

:: deftheorem Def25 defines well_founded AOFA_000:def 25 :

for A being preIfWhileAlgebra holds

( A is well_founded iff ElementaryInstructions A is GeneratorSet of A );

for A being preIfWhileAlgebra holds

( A is well_founded iff ElementaryInstructions A is GeneratorSet of A );

theorem Th54: :: AOFA_000:54

( len ECIW-signature = 4 & dom ECIW-signature = Seg 4 & ECIW-signature . 1 = 0 & ECIW-signature . 2 = 2 & ECIW-signature . 3 = 3 & ECIW-signature . 4 = 2 )

proof end;

:: deftheorem Def27 defines ECIW-strict AOFA_000:def 27 :

for A being non empty partial non-empty UAStr holds

( A is ECIW-strict iff signature A = ECIW-signature );

for A being non empty partial non-empty UAStr holds

( A is ECIW-strict iff signature A = ECIW-signature );

theorem Th55: :: AOFA_000:55

for A being non empty partial non-empty UAStr st A is ECIW-strict holds

for o being OperSymbol of A holds

( o = 1 or o = 2 or o = 3 or o = 4 )

for o being OperSymbol of A holds

( o = 1 or o = 2 or o = 3 or o = 4 )

proof end;

registration

let X be non empty disjoint_with_NAT set ;

( FreeUnivAlgNSG (ECIW-signature,X) is with_empty-instruction & FreeUnivAlgNSG (ECIW-signature,X) is with_catenation & FreeUnivAlgNSG (ECIW-signature,X) is with_if-instruction & FreeUnivAlgNSG (ECIW-signature,X) is with_while-instruction )

end;
cluster FreeUnivAlgNSG (ECIW-signature,X) -> with_empty-instruction with_catenation with_if-instruction with_while-instruction ;

coherence ( FreeUnivAlgNSG (ECIW-signature,X) is with_empty-instruction & FreeUnivAlgNSG (ECIW-signature,X) is with_catenation & FreeUnivAlgNSG (ECIW-signature,X) is with_if-instruction & FreeUnivAlgNSG (ECIW-signature,X) is with_while-instruction )

proof end;

theorem Th56: :: AOFA_000:56

for X being non empty disjoint_with_NAT set

for I being Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds

( ex x being Element of X st I = root-tree x or ex n being Nat ex p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st

( n in Seg 4 & I = n -tree p & len p = ECIW-signature . n ) )

for I being Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds

( ex x being Element of X st I = root-tree x or ex n being Nat ex p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st

( n in Seg 4 & I = n -tree p & len p = ECIW-signature . n ) )

proof end;

theorem Th57: :: AOFA_000:57

for X being non empty disjoint_with_NAT set holds EmptyIns (FreeUnivAlgNSG (ECIW-signature,X)) = 1 -tree {}

proof end;

theorem Th58: :: AOFA_000:58

for X being non empty disjoint_with_NAT set

for p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st 1 -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds

p = {}

for p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st 1 -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds

p = {}

proof end;

theorem Th59: :: AOFA_000:59

for X being non empty disjoint_with_NAT set

for I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds I1 \; I2 = 2 -tree (I1,I2)

for I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds I1 \; I2 = 2 -tree (I1,I2)

proof end;

theorem Th60: :: AOFA_000:60

for X being non empty disjoint_with_NAT set

for p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st 2 -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds

ex I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st p = <*I1,I2*>

for p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st 2 -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds

ex I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st p = <*I1,I2*>

proof end;

theorem Th61: :: AOFA_000:61

for X being non empty disjoint_with_NAT set

for I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds

( I1 \; I2 <> I1 & I1 \; I2 <> I2 )

for I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds

( I1 \; I2 <> I1 & I1 \; I2 <> I2 )

proof end;

theorem :: AOFA_000:62

for X being non empty disjoint_with_NAT set

for I1, I2, J1, J2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st I1 \; I2 = J1 \; J2 holds

( I1 = J1 & I2 = J2 )

for I1, I2, J1, J2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st I1 \; I2 = J1 \; J2 holds

( I1 = J1 & I2 = J2 )

proof end;

theorem Th63: :: AOFA_000:63

for X being non empty disjoint_with_NAT set

for C, I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds if-then-else (C,I1,I2) = 3 -tree <*C,I1,I2*>

for C, I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds if-then-else (C,I1,I2) = 3 -tree <*C,I1,I2*>

proof end;

theorem Th64: :: AOFA_000:64

for X being non empty disjoint_with_NAT set

for p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st 3 -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds

ex C, I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st p = <*C,I1,I2*>

for p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st 3 -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds

ex C, I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st p = <*C,I1,I2*>

proof end;

theorem :: AOFA_000:65

for X being non empty disjoint_with_NAT set

for C1, C2, I1, I2, J1, J2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st if-then-else (C1,I1,I2) = if-then-else (C2,J1,J2) holds

( C1 = C2 & I1 = J1 & I2 = J2 )

for C1, C2, I1, I2, J1, J2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st if-then-else (C1,I1,I2) = if-then-else (C2,J1,J2) holds

( C1 = C2 & I1 = J1 & I2 = J2 )

proof end;

theorem Th66: :: AOFA_000:66

for X being non empty disjoint_with_NAT set

for C, I being Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds while (C,I) = 4 -tree (C,I)

for C, I being Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds while (C,I) = 4 -tree (C,I)

proof end;

theorem Th67: :: AOFA_000:67

for X being non empty disjoint_with_NAT set

for p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st 4 -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds

ex C, I being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st p = <*C,I*>

for p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st 4 -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds

ex C, I being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st p = <*C,I*>

proof end;

theorem Th68: :: AOFA_000:68

for X being non empty disjoint_with_NAT set

for I being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st I in ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,X)) holds

ex x being Element of X st I = x -tree {}

for I being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st I in ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,X)) holds

ex x being Element of X st I = x -tree {}

proof end;

theorem :: AOFA_000:69

for X being non empty disjoint_with_NAT set

for p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X))

for x being Element of X st x -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds

p = {}

for p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X))

for x being Element of X st x -tree p is Element of (FreeUnivAlgNSG (ECIW-signature,X)) holds

p = {}

proof end;

theorem Th70: :: AOFA_000:70

for X being non empty disjoint_with_NAT set holds

( ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,X)) = FreeGenSetNSG (ECIW-signature,X) & card X = card (FreeGenSetNSG (ECIW-signature,X)) )

( ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,X)) = FreeGenSetNSG (ECIW-signature,X) & card X = card (FreeGenSetNSG (ECIW-signature,X)) )

proof end;

registration
end;

registration

let X be infinite disjoint_with_NAT set ;

coherence

FreeUnivAlgNSG (ECIW-signature,X) is infinite

end;
coherence

FreeUnivAlgNSG (ECIW-signature,X) is infinite

proof end;

registration

let X be non empty disjoint_with_NAT set ;

coherence

FreeUnivAlgNSG (ECIW-signature,X) is ECIW-strict

end;
coherence

FreeUnivAlgNSG (ECIW-signature,X) is ECIW-strict

proof end;

theorem Th72: :: AOFA_000:72

for A being preIfWhileAlgebra st A is free holds

for C, I1, I2 being Element of A holds

( EmptyIns A <> I1 \; I2 & EmptyIns A <> if-then-else (C,I1,I2) & EmptyIns A <> while (C,I1) )

for C, I1, I2 being Element of A holds

( EmptyIns A <> I1 \; I2 & EmptyIns A <> if-then-else (C,I1,I2) & EmptyIns A <> while (C,I1) )

proof end;

theorem Th73: :: AOFA_000:73

for A being preIfWhileAlgebra st A is free holds

for I1, I2, C, J1, J2 being Element of A holds

( I1 \; I2 <> I1 & I1 \; I2 <> I2 & ( I1 \; I2 = J1 \; J2 implies ( I1 = J1 & I2 = J2 ) ) & I1 \; I2 <> if-then-else (C,J1,J2) & I1 \; I2 <> while (C,J1) )

for I1, I2, C, J1, J2 being Element of A holds

( I1 \; I2 <> I1 & I1 \; I2 <> I2 & ( I1 \; I2 = J1 \; J2 implies ( I1 = J1 & I2 = J2 ) ) & I1 \; I2 <> if-then-else (C,J1,J2) & I1 \; I2 <> while (C,J1) )

proof end;

theorem Th74: :: AOFA_000:74

for A being preIfWhileAlgebra st A is free holds

for C, I1, I2, D, J1, J2 being Element of A holds

( if-then-else (C,I1,I2) <> C & if-then-else (C,I1,I2) <> I1 & if-then-else (C,I1,I2) <> I2 & if-then-else (C,I1,I2) <> while (D,J1) & ( if-then-else (C,I1,I2) = if-then-else (D,J1,J2) implies ( C = D & I1 = J1 & I2 = J2 ) ) )

for C, I1, I2, D, J1, J2 being Element of A holds

( if-then-else (C,I1,I2) <> C & if-then-else (C,I1,I2) <> I1 & if-then-else (C,I1,I2) <> I2 & if-then-else (C,I1,I2) <> while (D,J1) & ( if-then-else (C,I1,I2) = if-then-else (D,J1,J2) implies ( C = D & I1 = J1 & I2 = J2 ) ) )

proof end;

theorem Th75: :: AOFA_000:75

for A being preIfWhileAlgebra st A is free holds

for C, I, D, J being Element of A holds

( while (C,I) <> C & while (C,I) <> I & ( while (C,I) = while (D,J) implies ( C = D & I = J ) ) )

for C, I, D, J being Element of A holds

( while (C,I) <> C & while (C,I) <> I & ( while (C,I) = while (D,J) implies ( C = D & I = J ) ) )

proof end;

registration

for b_{1} being preIfWhileAlgebra st b_{1} is free holds

( b_{1} is well_founded & not b_{1} is degenerated )
end;

cluster non empty partial quasi_total non-empty free with_empty-instruction with_catenation with_if-instruction with_while-instruction -> non degenerated well_founded for UAStr ;

coherence for b

( b

proof end;

registration

ex b_{1} being preIfWhileAlgebra st

( b_{1} is infinite & not b_{1} is degenerated & b_{1} is well_founded & b_{1} is ECIW-strict & b_{1} is free & b_{1} is strict )
end;

cluster non empty strict partial quasi_total non-empty free with_empty-instruction with_catenation with_if-instruction with_while-instruction infinite non degenerated well_founded ECIW-strict for UAStr ;

existence ex b

( b

proof end;

registration
end;

theorem Th76: :: AOFA_000:76

for A being preIfWhileAlgebra

for B being Subset of A

for n being Nat holds

( EmptyIns A in B |^ (n + 1) & ( for C, I1, I2 being Element of A st C in B |^ n & I1 in B |^ n & I2 in B |^ n holds

( I1 \; I2 in B |^ (n + 1) & if-then-else (C,I1,I2) in B |^ (n + 1) & while (C,I1) in B |^ (n + 1) ) ) )

for B being Subset of A

for n being Nat holds

( EmptyIns A in B |^ (n + 1) & ( for C, I1, I2 being Element of A st C in B |^ n & I1 in B |^ n & I2 in B |^ n holds

( I1 \; I2 in B |^ (n + 1) & if-then-else (C,I1,I2) in B |^ (n + 1) & while (C,I1) in B |^ (n + 1) ) ) )

proof end;

theorem Th77: :: AOFA_000:77

for A being ECIW-strict preIfWhileAlgebra

for x being set

for n being Nat holds

( not x in (ElementaryInstructions A) |^ (n + 1) or x in (ElementaryInstructions A) |^ n or x = EmptyIns A or ex I1, I2 being Element of A st

( x = I1 \; I2 & I1 in (ElementaryInstructions A) |^ n & I2 in (ElementaryInstructions A) |^ n ) or ex C, I1, I2 being Element of A st

( x = if-then-else (C,I1,I2) & C in (ElementaryInstructions A) |^ n & I1 in (ElementaryInstructions A) |^ n & I2 in (ElementaryInstructions A) |^ n ) or ex C, I being Element of A st

( x = while (C,I) & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n ) )

for x being set

for n being Nat holds

( not x in (ElementaryInstructions A) |^ (n + 1) or x in (ElementaryInstructions A) |^ n or x = EmptyIns A or ex I1, I2 being Element of A st

( x = I1 \; I2 & I1 in (ElementaryInstructions A) |^ n & I2 in (ElementaryInstructions A) |^ n ) or ex C, I1, I2 being Element of A st

( x = if-then-else (C,I1,I2) & C in (ElementaryInstructions A) |^ n & I1 in (ElementaryInstructions A) |^ n & I2 in (ElementaryInstructions A) |^ n ) or ex C, I being Element of A st

( x = while (C,I) & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n ) )

proof end;

theorem Th79: :: AOFA_000:79

for A being preIfWhileAlgebra holds

( A is well_founded iff for I being Element of A ex n being Nat st I in (ElementaryInstructions A) |^ n )

( A is well_founded iff for I being Element of A ex n being Nat st I in (ElementaryInstructions A) |^ n )

proof end;

scheme :: AOFA_000:sch 2

StructInd{ F_{1}() -> well_founded ECIW-strict preIfWhileAlgebra, F_{2}() -> Element of F_{1}(), P_{1}[ set ] } :

provided

StructInd{ F

provided

A1:
for I being Element of F_{1}() st I in ElementaryInstructions F_{1}() holds

P_{1}[I]
and

A2: P_{1}[ EmptyIns F_{1}()]
and

A3: for I1, I2 being Element of F_{1}() st P_{1}[I1] & P_{1}[I2] holds

P_{1}[I1 \; I2]
and

A4: for C, I1, I2 being Element of F_{1}() st P_{1}[C] & P_{1}[I1] & P_{1}[I2] holds

P_{1}[ if-then-else (C,I1,I2)]
and

A5: for C, I being Element of F_{1}() st P_{1}[C] & P_{1}[I] holds

P_{1}[ while (C,I)]

P

A2: P

A3: for I1, I2 being Element of F

P

A4: for C, I1, I2 being Element of F

P

A5: for C, I being Element of F

P

proof end;

begin

definition

let A be preIfWhileAlgebra;

let S be non empty set ;

let f be Function of [:S, the carrier of A:],S;

end;
let S be non empty set ;

let f be Function of [:S, the carrier of A:],S;

attr f is complying_with_empty-instruction means :Def28: :: AOFA_000:def 28

for s being Element of S holds f . (s,(EmptyIns A)) = s;

for s being Element of S holds f . (s,(EmptyIns A)) = s;

attr f is complying_with_catenation means :Def29: :: AOFA_000:def 29

for s being Element of S

for I1, I2 being Element of A holds f . (s,(I1 \; I2)) = f . ((f . (s,I1)),I2);

for s being Element of S

for I1, I2 being Element of A holds f . (s,(I1 \; I2)) = f . ((f . (s,I1)),I2);

:: deftheorem Def28 defines complying_with_empty-instruction AOFA_000:def 28 :

for A being preIfWhileAlgebra

for S being non empty set

for f being Function of [:S, the carrier of A:],S holds

( f is complying_with_empty-instruction iff for s being Element of S holds f . (s,(EmptyIns A)) = s );

for A being preIfWhileAlgebra

for S being non empty set

for f being Function of [:S, the carrier of A:],S holds

( f is complying_with_empty-instruction iff for s being Element of S holds f . (s,(EmptyIns A)) = s );

:: deftheorem Def29 defines complying_with_catenation AOFA_000:def 29 :

for A being preIfWhileAlgebra

for S being non empty set

for f being Function of [:S, the carrier of A:],S holds

( f is complying_with_catenation iff for s being Element of S

for I1, I2 being Element of A holds f . (s,(I1 \; I2)) = f . ((f . (s,I1)),I2) );

for A being preIfWhileAlgebra

for S being non empty set

for f being Function of [:S, the carrier of A:],S holds

( f is complying_with_catenation iff for s being Element of S

for I1, I2 being Element of A holds f . (s,(I1 \; I2)) = f . ((f . (s,I1)),I2) );

definition

let A be preIfWhileAlgebra;

let S be non empty set ;

let T be Subset of S;

let f be Function of [:S, the carrier of A:],S;

end;
let S be non empty set ;

let T be Subset of S;

let f be Function of [:S, the carrier of A:],S;

pred f complies_with_if_wrt T means :Def30: :: AOFA_000:def 30

for s being Element of S

for C, I1, I2 being Element of A holds

( ( f . (s,C) in T implies f . (s,(if-then-else (C,I1,I2))) = f . ((f . (s,C)),I1) ) & ( f . (s,C) nin T implies f . (s,(if-then-else (C,I1,I2))) = f . ((f . (s,C)),I2) ) );

for s being Element of S

for C, I1, I2 being Element of A holds

( ( f . (s,C) in T implies f . (s,(if-then-else (C,I1,I2))) = f . ((f . (s,C)),I1) ) & ( f . (s,C) nin T implies f . (s,(if-then-else (C,I1,I2))) = f . ((f . (s,C)),I2) ) );

:: deftheorem Def30 defines complies_with_if_wrt AOFA_000:def 30 :

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for f being Function of [:S, the carrier of A:],S holds

( f complies_with_if_wrt T iff for s being Element of S

for C, I1, I2 being Element of A holds

( ( f . (s,C) in T implies f . (s,(if-then-else (C,I1,I2))) = f . ((f . (s,C)),I1) ) & ( f . (s,C) nin T implies f . (s,(if-then-else (C,I1,I2))) = f . ((f . (s,C)),I2) ) ) );

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for f being Function of [:S, the carrier of A:],S holds

( f complies_with_if_wrt T iff for s being Element of S

for C, I1, I2 being Element of A holds

( ( f . (s,C) in T implies f . (s,(if-then-else (C,I1,I2))) = f . ((f . (s,C)),I1) ) & ( f . (s,C) nin T implies f . (s,(if-then-else (C,I1,I2))) = f . ((f . (s,C)),I2) ) ) );

:: deftheorem Def31 defines complies_with_while_wrt AOFA_000:def 31 :

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for f being Function of [:S, the carrier of A:],S holds

( f complies_with_while_wrt T iff for s being Element of S

for C, I being Element of A holds

( ( f . (s,C) in T implies f . (s,(while (C,I))) = f . ((f . ((f . (s,C)),I)),(while (C,I))) ) & ( f . (s,C) nin T implies f . (s,(while (C,I))) = f . (s,C) ) ) );

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for f being Function of [:S, the carrier of A:],S holds

( f complies_with_while_wrt T iff for s being Element of S

for C, I being Element of A holds

( ( f . (s,C) in T implies f . (s,(while (C,I))) = f . ((f . ((f . (s,C)),I)),(while (C,I))) ) & ( f . (s,C) nin T implies f . (s,(while (C,I))) = f . (s,C) ) ) );

theorem :: AOFA_000:80

for A being preIfWhileAlgebra

for C, I being Element of A

for S being non empty set

for T being Subset of S

for f being Function of [:S, the carrier of A:],S st f is complying_with_empty-instruction & f complies_with_if_wrt T holds

for s being Element of S st f . (s,C) nin T holds

f . (s,(if-then (C,I))) = f . (s,C)

for C, I being Element of A

for S being non empty set

for T being Subset of S

for f being Function of [:S, the carrier of A:],S st f is complying_with_empty-instruction & f complies_with_if_wrt T holds

for s being Element of S st f . (s,C) nin T holds

f . (s,(if-then (C,I))) = f . (s,C)

proof end;

theorem Th81: :: AOFA_000:81

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S holds

( pr1 (S, the carrier of A) is complying_with_empty-instruction & pr1 (S, the carrier of A) is complying_with_catenation & pr1 (S, the carrier of A) complies_with_if_wrt T & pr1 (S, the carrier of A) complies_with_while_wrt T )

for S being non empty set

for T being Subset of S holds

( pr1 (S, the carrier of A) is complying_with_empty-instruction & pr1 (S, the carrier of A) is complying_with_catenation & pr1 (S, the carrier of A) complies_with_if_wrt T & pr1 (S, the carrier of A) complies_with_while_wrt T )

proof end;

definition

let A be preIfWhileAlgebra;

let S be non empty set ;

let T be Subset of S;

ex b_{1} being Function of [:S, the carrier of A:],S st

( b_{1} is complying_with_empty-instruction & b_{1} is complying_with_catenation & b_{1} complies_with_if_wrt T & b_{1} complies_with_while_wrt T )

end;
let S be non empty set ;

let T be Subset of S;

mode ExecutionFunction of A,S,T -> Function of [:S, the carrier of A:],S means :Def32: :: AOFA_000:def 32

( it is complying_with_empty-instruction & it is complying_with_catenation & it complies_with_if_wrt T & it complies_with_while_wrt T );

existence ( it is complying_with_empty-instruction & it is complying_with_catenation & it complies_with_if_wrt T & it complies_with_while_wrt T );

ex b

( b

proof end;

:: deftheorem Def32 defines ExecutionFunction AOFA_000:def 32 :

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for b_{4} being Function of [:S, the carrier of A:],S holds

( b_{4} is ExecutionFunction of A,S,T iff ( b_{4} is complying_with_empty-instruction & b_{4} is complying_with_catenation & b_{4} complies_with_if_wrt T & b_{4} complies_with_while_wrt T ) );

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for b

( b

registration

let A be preIfWhileAlgebra;

let S be non empty set ;

let T be Subset of S;

for b_{1} being ExecutionFunction of A,S,T holds

( b_{1} is complying_with_empty-instruction & b_{1} is complying_with_catenation )
by Def32;

end;
let S be non empty set ;

let T be Subset of S;

cluster -> complying_with_empty-instruction complying_with_catenation for ExecutionFunction of A,S,T;

coherence for b

( b

definition

let A be preIfWhileAlgebra;

let I be Element of A;

let S be non empty set ;

let s be Element of S;

let T be Subset of S;

let f be ExecutionFunction of A,S,T;

end;
let I be Element of A;

let S be non empty set ;

let s be Element of S;

let T be Subset of S;

let f be ExecutionFunction of A,S,T;

:: deftheorem Def33 defines iteration_terminates_for AOFA_000:def 33 :

for A being preIfWhileAlgebra

for I being Element of A

for S being non empty set

for s being Element of S

for T being Subset of S

for f being ExecutionFunction of A,S,T holds

( f iteration_terminates_for I,s iff ex r being non empty FinSequence of S st

( r . 1 = s & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & r . (i + 1) = f . ((r . i),I) ) ) ) );

for A being preIfWhileAlgebra

for I being Element of A

for S being non empty set

for s being Element of S

for T being Subset of S

for f being ExecutionFunction of A,S,T holds

( f iteration_terminates_for I,s iff ex r being non empty FinSequence of S st

( r . 1 = s & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & r . (i + 1) = f . ((r . i),I) ) ) ) );

definition

let A be preIfWhileAlgebra;

let I be Element of A;

let S be non empty set ;

let s be Element of S;

let T be Subset of S;

let f be ExecutionFunction of A,S,T;

consistency

for b_{1} being R_eal holds verum;

existence

( ( for b_{1} being R_eal holds verum ) & ( f iteration_terminates_for I,s implies ex b_{1} being R_eal ex r being non empty FinSequence of S st

( b_{1} = (len r) - 1 & r . 1 = s & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & r . (i + 1) = f . ((r . i),I) ) ) ) ) & ( not f iteration_terminates_for I,s implies ex b_{1} being R_eal st b_{1} = +infty ) );

uniqueness

for b_{1}, b_{2} being R_eal holds

( ( f iteration_terminates_for I,s & ex r being non empty FinSequence of S st

( b_{1} = (len r) - 1 & r . 1 = s & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & r . (i + 1) = f . ((r . i),I) ) ) ) & ex r being non empty FinSequence of S st

( b_{2} = (len r) - 1 & r . 1 = s & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & r . (i + 1) = f . ((r . i),I) ) ) ) implies b_{1} = b_{2} ) & ( not f iteration_terminates_for I,s & b_{1} = +infty & b_{2} = +infty implies b_{1} = b_{2} ) );

end;
let I be Element of A;

let S be non empty set ;

let s be Element of S;

let T be Subset of S;

let f be ExecutionFunction of A,S,T;

func iteration-degree (I,s,f) -> R_eal means :Def34: :: AOFA_000:def 34

ex r being non empty FinSequence of S st

( it = (len r) - 1 & r . 1 = s & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & r . (i + 1) = f . ((r . i),I) ) ) ) if f iteration_terminates_for I,s

otherwise it = +infty ;

correctness ex r being non empty FinSequence of S st

( it = (len r) - 1 & r . 1 = s & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & r . (i + 1) = f . ((r . i),I) ) ) ) if f iteration_terminates_for I,s

otherwise it = +infty ;

consistency

for b

existence

( ( for b

( b

( r . i in T & r . (i + 1) = f . ((r . i),I) ) ) ) ) & ( not f iteration_terminates_for I,s implies ex b

uniqueness

for b

( ( f iteration_terminates_for I,s & ex r being non empty FinSequence of S st

( b

( r . i in T & r . (i + 1) = f . ((r . i),I) ) ) ) & ex r being non empty FinSequence of S st

( b

( r . i in T & r . (i + 1) = f . ((r . i),I) ) ) ) implies b

proof end;

:: deftheorem Def34 defines iteration-degree AOFA_000:def 34 :

for A being preIfWhileAlgebra

for I being Element of A

for S being non empty set

for s being Element of S

for T being Subset of S

for f being ExecutionFunction of A,S,T

for b_{7} being R_eal holds

( ( f iteration_terminates_for I,s implies ( b_{7} = iteration-degree (I,s,f) iff ex r being non empty FinSequence of S st

( b_{7} = (len r) - 1 & r . 1 = s & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & r . (i + 1) = f . ((r . i),I) ) ) ) ) ) & ( not f iteration_terminates_for I,s implies ( b_{7} = iteration-degree (I,s,f) iff b_{7} = +infty ) ) );

for A being preIfWhileAlgebra

for I being Element of A

for S being non empty set

for s being Element of S

for T being Subset of S

for f being ExecutionFunction of A,S,T

for b

( ( f iteration_terminates_for I,s implies ( b

( b

( r . i in T & r . (i + 1) = f . ((r . i),I) ) ) ) ) ) & ( not f iteration_terminates_for I,s implies ( b

theorem :: AOFA_000:82

for A being preIfWhileAlgebra

for I being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T holds

( f iteration_terminates_for I,s iff iteration-degree (I,s,f) < +infty )

for I being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T holds

( f iteration_terminates_for I,s iff iteration-degree (I,s,f) < +infty )

proof end;

theorem Th83: :: AOFA_000:83

for A being preIfWhileAlgebra

for I being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T st s nin T holds

( f iteration_terminates_for I,s & iteration-degree (I,s,f) = 0 )

for I being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T st s nin T holds

( f iteration_terminates_for I,s & iteration-degree (I,s,f) = 0 )

proof end;

theorem :: AOFA_000:84

for A being preIfWhileAlgebra

for I being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T st s in T holds

( ( f iteration_terminates_for I,s implies f iteration_terminates_for I,f . (s,I) ) & ( f iteration_terminates_for I,f . (s,I) implies f iteration_terminates_for I,s ) & iteration-degree (I,s,f) = 1. + (iteration-degree (I,(f . (s,I)),f)) )

for I being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T st s in T holds

( ( f iteration_terminates_for I,s implies f iteration_terminates_for I,f . (s,I) ) & ( f iteration_terminates_for I,f . (s,I) implies f iteration_terminates_for I,s ) & iteration-degree (I,s,f) = 1. + (iteration-degree (I,(f . (s,I)),f)) )

proof end;

theorem :: AOFA_000:85

for A being preIfWhileAlgebra

for I being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T holds iteration-degree (I,s,f) >= 0

for I being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T holds iteration-degree (I,s,f) >= 0

proof end;

scheme :: AOFA_000:sch 3

Termination{ F_{1}() -> preIfWhileAlgebra, F_{2}() -> Element of F_{1}(), F_{3}() -> non empty set , F_{4}() -> Element of F_{3}(), F_{5}() -> Subset of F_{3}(), F_{6}() -> ExecutionFunction of F_{1}(),F_{3}(),F_{5}(), F_{7}( set ) -> Nat, P_{1}[ set ] } :

provided

Termination{ F

provided

A1:
( F_{4}() in F_{5}() iff P_{1}[F_{4}()] )
and

A2: for s being Element of F_{3}() st P_{1}[s] holds

( ( P_{1}[F_{6}() . (s,F_{2}())] implies F_{6}() . (s,F_{2}()) in F_{5}() ) & ( F_{6}() . (s,F_{2}()) in F_{5}() implies P_{1}[F_{6}() . (s,F_{2}())] ) & F_{7}((F_{6}() . (s,F_{2}()))) < F_{7}(s) )

A2: for s being Element of F

( ( P

proof end;

scheme :: AOFA_000:sch 4

Termination2{ F_{1}() -> preIfWhileAlgebra, F_{2}() -> Element of F_{1}(), F_{3}() -> non empty set , F_{4}() -> Element of F_{3}(), F_{5}() -> Subset of F_{3}(), F_{6}() -> ExecutionFunction of F_{1}(),F_{3}(),F_{5}(), F_{7}( set ) -> Nat, P_{1}[ set ], P_{2}[ set ] } :

provided

Termination2{ F

provided

A1:
P_{1}[F_{4}()]
and

A2: ( F_{4}() in F_{5}() iff P_{2}[F_{4}()] )
and

A3: for s being Element of F_{3}() st P_{1}[s] & s in F_{5}() & P_{2}[s] holds

( P_{1}[F_{6}() . (s,F_{2}())] & ( P_{2}[F_{6}() . (s,F_{2}())] implies F_{6}() . (s,F_{2}()) in F_{5}() ) & ( F_{6}() . (s,F_{2}()) in F_{5}() implies P_{2}[F_{6}() . (s,F_{2}())] ) & F_{7}((F_{6}() . (s,F_{2}()))) < F_{7}(s) )

A2: ( F

A3: for s being Element of F

( P

proof end;

theorem Th86: :: AOFA_000:86

for A being preIfWhileAlgebra

for C, I being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T

for r being non empty FinSequence of S st r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & r . (i + 1) = f . ((r . i),(I \; C)) ) ) holds

f . (s,(while (C,I))) = r . (len r)

for C, I being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T

for r being non empty FinSequence of S st r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & r . (i + 1) = f . ((r . i),(I \; C)) ) ) holds

f . (s,(while (C,I))) = r . (len r)

proof end;

theorem Th87: :: AOFA_000:87

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for I being Element of A

for s being Element of S holds

( not f iteration_terminates_for I,s iff ((curry' f) . I) orbit s c= T )

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for I being Element of A

for s being Element of S holds

( not f iteration_terminates_for I,s iff ((curry' f) . I) orbit s c= T )

proof end;

scheme :: AOFA_000:sch 5

InvariantSch{ F_{1}() -> preIfWhileAlgebra, F_{2}() -> Element of F_{1}(), F_{3}() -> Element of F_{1}(), F_{4}() -> non empty set , F_{5}() -> Element of F_{4}(), F_{6}() -> Subset of F_{4}(), F_{7}() -> ExecutionFunction of F_{1}(),F_{4}(),F_{6}(), P_{1}[ set ], P_{2}[ set ] } :

InvariantSch{ F

( P_{1}[F_{7}() . (F_{5}(),(while (F_{2}(),F_{3}())))] & P_{2}[F_{7}() . (F_{5}(),(while (F_{2}(),F_{3}())))] )

provided
A1:
P_{1}[F_{5}()]
and

A2: F_{7}() iteration_terminates_for F_{3}() \; F_{2}(),F_{7}() . (F_{5}(),F_{2}())
and

A3: for s being Element of F_{4}() st P_{1}[s] & s in F_{6}() & P_{2}[s] holds

P_{1}[F_{7}() . (s,F_{3}())]
and

A4: for s being Element of F_{4}() st P_{1}[s] holds

( P_{1}[F_{7}() . (s,F_{2}())] & ( F_{7}() . (s,F_{2}()) in F_{6}() implies P_{2}[F_{7}() . (s,F_{2}())] ) & ( P_{2}[F_{7}() . (s,F_{2}())] implies F_{7}() . (s,F_{2}()) in F_{6}() ) )

A2: F

A3: for s being Element of F

P

A4: for s being Element of F

( P

proof end;

scheme :: AOFA_000:sch 6

coInvariantSch{ F_{1}() -> preIfWhileAlgebra, F_{2}() -> Element of F_{1}(), F_{3}() -> Element of F_{1}(), F_{4}() -> non empty set , F_{5}() -> Element of F_{4}(), F_{6}() -> Subset of F_{4}(), F_{7}() -> ExecutionFunction of F_{1}(),F_{4}(),F_{6}(), P_{1}[ set ] } :

provided

coInvariantSch{ F

provided

A1:
P_{1}[F_{7}() . (F_{5}(),(while (F_{2}(),F_{3}())))]
and

A2: F_{7}() iteration_terminates_for F_{3}() \; F_{2}(),F_{7}() . (F_{5}(),F_{2}())
and

A3: for s being Element of F_{4}() st P_{1}[F_{7}() . ((F_{7}() . (s,F_{2}())),F_{3}())] & F_{7}() . (s,F_{2}()) in F_{6}() holds

P_{1}[F_{7}() . (s,F_{2}())]
and

A4: for s being Element of F_{4}() st P_{1}[F_{7}() . (s,F_{2}())] holds

P_{1}[s]

A2: F

A3: for s being Element of F

P

A4: for s being Element of F

P

proof end;

theorem Th88: :: AOFA_000:88

for A being free preIfWhileAlgebra

for I1, I2 being Element of A

for n being Nat st I1 \; I2 in (ElementaryInstructions A) |^ n holds

ex i being Nat st

( n = i + 1 & I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )

for I1, I2 being Element of A

for n being Nat st I1 \; I2 in (ElementaryInstructions A) |^ n holds

ex i being Nat st

( n = i + 1 & I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )

proof end;

theorem Th89: :: AOFA_000:89

for A being free preIfWhileAlgebra

for C, I1, I2 being Element of A

for n being Nat st if-then-else (C,I1,I2) in (ElementaryInstructions A) |^ n holds

ex i being Nat st

( n = i + 1 & C in (ElementaryInstructions A) |^ i & I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )

for C, I1, I2 being Element of A

for n being Nat st if-then-else (C,I1,I2) in (ElementaryInstructions A) |^ n holds

ex i being Nat st

( n = i + 1 & C in (ElementaryInstructions A) |^ i & I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )

proof end;

theorem Th90: :: AOFA_000:90

for A being free preIfWhileAlgebra

for C, I being Element of A

for n being Nat st while (C,I) in (ElementaryInstructions A) |^ n holds

ex i being Nat st

( n = i + 1 & C in (ElementaryInstructions A) |^ i & I in (ElementaryInstructions A) |^ i )

for C, I being Element of A

for n being Nat st while (C,I) in (ElementaryInstructions A) |^ n holds

ex i being Nat st

( n = i + 1 & C in (ElementaryInstructions A) |^ i & I in (ElementaryInstructions A) |^ i )

proof end;

begin

scheme :: AOFA_000:sch 7

IndDef{ F_{1}() -> free ECIW-strict preIfWhileAlgebra, F_{2}() -> non empty set , F_{3}() -> Element of F_{2}(), F_{4}( set ) -> set , F_{5}( set , set ) -> Element of F_{2}(), F_{6}( set , set ) -> Element of F_{2}(), F_{7}( set , set , set ) -> Element of F_{2}() } :

IndDef{ F

ex f being Function of the carrier of F_{1}(),F_{2}() st

( ( for I being Element of F_{1}() st I in ElementaryInstructions F_{1}() holds

f . I = F_{4}(I) ) & f . (EmptyIns F_{1}()) = F_{3}() & ( for I1, I2 being Element of F_{1}() holds f . (I1 \; I2) = F_{5}((f . I1),(f . I2)) ) & ( for C, I1, I2 being Element of F_{1}() holds f . (if-then-else (C,I1,I2)) = F_{7}((f . C),(f . I1),(f . I2)) ) & ( for C, I being Element of F_{1}() holds f . (while (C,I)) = F_{6}((f . C),(f . I)) ) )

provided
( ( for I being Element of F

f . I = F

proof end;

theorem :: AOFA_000:91

for S being non empty set

for T being Subset of S

for A being free ECIW-strict preIfWhileAlgebra

for g being Function of [:S,(ElementaryInstructions A):],S

for s0 being Element of S ex f being ExecutionFunction of A,S,T st

( f | [:S,(ElementaryInstructions A):] = g & ( for s being Element of S

for C, I being Element of A st not f iteration_terminates_for I \; C,f . (s,C) holds

f . (s,(while (C,I))) = s0 ) )

for T being Subset of S

for A being free ECIW-strict preIfWhileAlgebra

for g being Function of [:S,(ElementaryInstructions A):],S

for s0 being Element of S ex f being ExecutionFunction of A,S,T st

( f | [:S,(ElementaryInstructions A):] = g & ( for s being Element of S

for C, I being Element of A st not f iteration_terminates_for I \; C,f . (s,C) holds

f . (s,(while (C,I))) = s0 ) )

proof end;

theorem :: AOFA_000:92

for S being non empty set

for T being Subset of S

for A being free ECIW-strict preIfWhileAlgebra

for g being Function of [:S,(ElementaryInstructions A):],S

for F being Function of (Funcs (S,S)),(Funcs (S,S)) st ( for h being Element of Funcs (S,S) holds (F . h) * h = F . h ) holds

ex f being ExecutionFunction of A,S,T st

( f | [:S,(ElementaryInstructions A):] = g & ( for C, I being Element of A

for s being Element of S st not f iteration_terminates_for I \; C,f . (s,C) holds

f . (s,(while (C,I))) = (F . ((curry' f) . (I \; C))) . (f . (s,C)) ) )

for T being Subset of S

for A being free ECIW-strict preIfWhileAlgebra

for g being Function of [:S,(ElementaryInstructions A):],S

for F being Function of (Funcs (S,S)),(Funcs (S,S)) st ( for h being Element of Funcs (S,S) holds (F . h) * h = F . h ) holds

ex f being ExecutionFunction of A,S,T st

( f | [:S,(ElementaryInstructions A):] = g & ( for C, I being Element of A

for s being Element of S st not f iteration_terminates_for I \; C,f . (s,C) holds

f . (s,(while (C,I))) = (F . ((curry' f) . (I \; C))) . (f . (s,C)) ) )

proof end;

theorem :: AOFA_000:93

for S being non empty set

for T being Subset of S

for A being free ECIW-strict preIfWhileAlgebra

for f1, f2 being ExecutionFunction of A,S,T st f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] & ( for s being Element of S

for C, I being Element of A st not f1 iteration_terminates_for I \; C,f1 . (s,C) holds

f1 . (s,(while (C,I))) = f2 . (s,(while (C,I))) ) holds

f1 = f2

for T being Subset of S

for A being free ECIW-strict preIfWhileAlgebra

for f1, f2 being ExecutionFunction of A,S,T st f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] & ( for s being Element of S

for C, I being Element of A st not f1 iteration_terminates_for I \; C,f1 . (s,C) holds

f1 . (s,(while (C,I))) = f2 . (s,(while (C,I))) ) holds

f1 = f2

proof end;

definition

let A be preIfWhileAlgebra;

let S be non empty set ;

let T be Subset of S;

let f be ExecutionFunction of A,S,T;

defpred S_{1}[ set ] means ( [:S,(ElementaryInstructions A):] c= $1 & [:S,{(EmptyIns A)}:] c= $1 & ( for s being Element of S

for C, I, J being Element of A holds

( ( [s,I] in $1 & [(f . (s,I)),J] in $1 implies [s,(I \; J)] in $1 ) & ( [s,C] in $1 & [(f . (s,C)),I] in $1 & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in $1 ) & ( [s,C] in $1 & [(f . (s,C)),J] in $1 & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in $1 ) & ( [s,C] in $1 & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in $1 & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in $1 ) ) ) );

ex b_{1} being Subset of [:S, the carrier of A:] st

( [:S,(ElementaryInstructions A):] c= b_{1} & [:S,{(EmptyIns A)}:] c= b_{1} & ( for s being Element of S

for C, I, J being Element of A holds

( ( [s,I] in b_{1} & [(f . (s,I)),J] in b_{1} implies [s,(I \; J)] in b_{1} ) & ( [s,C] in b_{1} & [(f . (s,C)),I] in b_{1} & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in b_{1} ) & ( [s,C] in b_{1} & [(f . (s,C)),J] in b_{1} & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in b_{1} ) & ( [s,C] in b_{1} & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in b_{1} & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in b_{1} ) ) ) & ( for P being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= P & [:S,{(EmptyIns A)}:] c= P & ( for s being Element of S

for C, I, J being Element of A holds

( ( [s,I] in P & [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . (s,C)),I] in P & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & [(f . (s,C)),J] in P & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds

b_{1} c= P ) )

for b_{1}, b_{2} being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= b_{1} & [:S,{(EmptyIns A)}:] c= b_{1} & ( for s being Element of S

for C, I, J being Element of A holds

( ( [s,I] in b_{1} & [(f . (s,I)),J] in b_{1} implies [s,(I \; J)] in b_{1} ) & ( [s,C] in b_{1} & [(f . (s,C)),I] in b_{1} & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in b_{1} ) & ( [s,C] in b_{1} & [(f . (s,C)),J] in b_{1} & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in b_{1} ) & ( [s,C] in b_{1} & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in b_{1} & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in b_{1} ) ) ) & ( for P being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= P & [:S,{(EmptyIns A)}:] c= P & ( for s being Element of S

for C, I, J being Element of A holds

( ( [s,I] in P & [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . (s,C)),I] in P & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & [(f . (s,C)),J] in P & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds

b_{1} c= P ) & [:S,(ElementaryInstructions A):] c= b_{2} & [:S,{(EmptyIns A)}:] c= b_{2} & ( for s being Element of S

for C, I, J being Element of A holds

( ( [s,I] in b_{2} & [(f . (s,I)),J] in b_{2} implies [s,(I \; J)] in b_{2} ) & ( [s,C] in b_{2} & [(f . (s,C)),I] in b_{2} & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in b_{2} ) & ( [s,C] in b_{2} & [(f . (s,C)),J] in b_{2} & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in b_{2} ) & ( [s,C] in b_{2} & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in b_{2} & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in b_{2} ) ) ) & ( for P being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= P & [:S,{(EmptyIns A)}:] c= P & ( for s being Element of S

for C, I, J being Element of A holds

( ( [s,I] in P & [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . (s,C)),I] in P & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & [(f . (s,C)),J] in P & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds

b_{2} c= P ) holds

b_{1} = b_{2}

end;
let S be non empty set ;

let T be Subset of S;

let f be ExecutionFunction of A,S,T;

defpred S

for C, I, J being Element of A holds

( ( [s,I] in $1 & [(f . (s,I)),J] in $1 implies [s,(I \; J)] in $1 ) & ( [s,C] in $1 & [(f . (s,C)),I] in $1 & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in $1 ) & ( [s,C] in $1 & [(f . (s,C)),J] in $1 & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in $1 ) & ( [s,C] in $1 & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in $1 & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in $1 ) ) ) );

func TerminatingPrograms (A,S,T,f) -> Subset of [:S, the carrier of A:] means :Def35: :: AOFA_000:def 35

( [:S,(ElementaryInstructions A):] c= it & [:S,{(EmptyIns A)}:] c= it & ( for s being Element of S

for C, I, J being Element of A holds

( ( [s,I] in it & [(f . (s,I)),J] in it implies [s,(I \; J)] in it ) & ( [s,C] in it & [(f . (s,C)),I] in it & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in it ) & ( [s,C] in it & [(f . (s,C)),J] in it & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in it ) & ( [s,C] in it & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in it & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in it ) ) ) & ( for P being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= P & [:S,{(EmptyIns A)}:] c= P & ( for s being Element of S

for C, I, J being Element of A holds

( ( [s,I] in P & [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . (s,C)),I] in P & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & [(f . (s,C)),J] in P & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds

it c= P ) );

existence ( [:S,(ElementaryInstructions A):] c= it & [:S,{(EmptyIns A)}:] c= it & ( for s being Element of S

for C, I, J being Element of A holds

( ( [s,I] in it & [(f . (s,I)),J] in it implies [s,(I \; J)] in it ) & ( [s,C] in it & [(f . (s,C)),I] in it & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in it ) & ( [s,C] in it & [(f . (s,C)),J] in it & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in it ) & ( [s,C] in it & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in it & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in it ) ) ) & ( for P being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= P & [:S,{(EmptyIns A)}:] c= P & ( for s being Element of S

for C, I, J being Element of A holds

( ( [s,I] in P & [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . (s,C)),I] in P & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & [(f . (s,C)),J] in P & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds

it c= P ) );

ex b

( [:S,(ElementaryInstructions A):] c= b

for C, I, J being Element of A holds

( ( [s,I] in b

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in b

for C, I, J being Element of A holds

( ( [s,I] in P & [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . (s,C)),I] in P & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & [(f . (s,C)),J] in P & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds

b

proof end;

uniqueness for b

for C, I, J being Element of A holds

( ( [s,I] in b

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in b

for C, I, J being Element of A holds

( ( [s,I] in P & [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . (s,C)),I] in P & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & [(f . (s,C)),J] in P & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds

b

for C, I, J being Element of A holds

( ( [s,I] in b

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in b

for C, I, J being Element of A holds

( ( [s,I] in P & [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . (s,C)),I] in P & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & [(f . (s,C)),J] in P & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds

b

b

proof end;

:: deftheorem Def35 defines TerminatingPrograms AOFA_000:def 35 :

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for b_{5} being Subset of [:S, the carrier of A:] holds

( b_{5} = TerminatingPrograms (A,S,T,f) iff ( [:S,(ElementaryInstructions A):] c= b_{5} & [:S,{(EmptyIns A)}:] c= b_{5} & ( for s being Element of S

for C, I, J being Element of A holds

( ( [s,I] in b_{5} & [(f . (s,I)),J] in b_{5} implies [s,(I \; J)] in b_{5} ) & ( [s,C] in b_{5} & [(f . (s,C)),I] in b_{5} & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in b_{5} ) & ( [s,C] in b_{5} & [(f . (s,C)),J] in b_{5} & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in b_{5} ) & ( [s,C] in b_{5} & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in b_{5} & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in b_{5} ) ) ) & ( for P being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= P & [:S,{(EmptyIns A)}:] c= P & ( for s being Element of S

for C, I, J being Element of A holds

( ( [s,I] in P & [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . (s,C)),I] in P & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & [(f . (s,C)),J] in P & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds

b_{5} c= P ) ) );

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for b

( b

for C, I, J being Element of A holds

( ( [s,I] in b

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in b

for C, I, J being Element of A holds

( ( [s,I] in P & [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . (s,C)),I] in P & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & [(f . (s,C)),J] in P & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds

b

definition

let A be preIfWhileAlgebra;

let I be Element of A;

end;
let I be Element of A;

attr I is absolutely-terminating means :Def36: :: AOFA_000:def 36

for S being non empty set

for s being Element of S

for T being Subset of S

for f being ExecutionFunction of A,S,T holds [s,I] in TerminatingPrograms (A,S,T,f);

for S being non empty set

for s being Element of S

for T being Subset of S

for f being ExecutionFunction of A,S,T holds [s,I] in TerminatingPrograms (A,S,T,f);

:: deftheorem Def36 defines absolutely-terminating AOFA_000:def 36 :

for A being preIfWhileAlgebra

for I being Element of A holds

( I is absolutely-terminating iff for S being non empty set

for s being Element of S

for T being Subset of S

for f being ExecutionFunction of A,S,T holds [s,I] in TerminatingPrograms (A,S,T,f) );

for A being preIfWhileAlgebra

for I being Element of A holds

( I is absolutely-terminating iff for S being non empty set

for s being Element of S

for T being Subset of S

for f being ExecutionFunction of A,S,T holds [s,I] in TerminatingPrograms (A,S,T,f) );

definition

let A be preIfWhileAlgebra;

let S be non empty set ;

let T be Subset of S;

let I be Element of A;

let f be ExecutionFunction of A,S,T;

end;
let S be non empty set ;

let T be Subset of S;

let I be Element of A;

let f be ExecutionFunction of A,S,T;

pred I is_terminating_wrt f means :Def37: :: AOFA_000:def 37

for s being Element of S holds [s,I] in TerminatingPrograms (A,S,T,f);

for s being Element of S holds [s,I] in TerminatingPrograms (A,S,T,f);

:: deftheorem Def37 defines is_terminating_wrt AOFA_000:def 37 :

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for I being Element of A

for f being ExecutionFunction of A,S,T holds

( I is_terminating_wrt f iff for s being Element of S holds [s,I] in TerminatingPrograms (A,S,T,f) );

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for I being Element of A

for f being ExecutionFunction of A,S,T holds

( I is_terminating_wrt f iff for s being Element of S holds [s,I] in TerminatingPrograms (A,S,T,f) );

definition

let A be preIfWhileAlgebra;

let S be non empty set ;

let T be Subset of S;

let I be Element of A;

let f be ExecutionFunction of A,S,T;

let Z be set ;

end;
let S be non empty set ;

let T be Subset of S;

let I be Element of A;

let f be ExecutionFunction of A,S,T;

let Z be set ;

pred I is_terminating_wrt f,Z means :Def38: :: AOFA_000:def 38

for s being Element of S st s in Z holds

[s,I] in TerminatingPrograms (A,S,T,f);

for s being Element of S st s in Z holds

[s,I] in TerminatingPrograms (A,S,T,f);

pred Z is_invariant_wrt I,f means :Def39: :: AOFA_000:def 39

for s being Element of S st s in Z holds

f . (s,I) in Z;

for s being Element of S st s in Z holds

f . (s,I) in Z;

:: deftheorem Def38 defines is_terminating_wrt AOFA_000:def 38 :

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for I being Element of A

for f being ExecutionFunction of A,S,T

for Z being set holds

( I is_terminating_wrt f,Z iff for s being Element of S st s in Z holds

[s,I] in TerminatingPrograms (A,S,T,f) );

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for I being Element of A

for f being ExecutionFunction of A,S,T

for Z being set holds

( I is_terminating_wrt f,Z iff for s being Element of S st s in Z holds

[s,I] in TerminatingPrograms (A,S,T,f) );

:: deftheorem Def39 defines is_invariant_wrt AOFA_000:def 39 :

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for I being Element of A

for f being ExecutionFunction of A,S,T

for Z being set holds

( Z is_invariant_wrt I,f iff for s being Element of S st s in Z holds

f . (s,I) in Z );

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for I being Element of A

for f being ExecutionFunction of A,S,T

for Z being set holds

( Z is_invariant_wrt I,f iff for s being Element of S st s in Z holds

f . (s,I) in Z );

theorem Th94: :: AOFA_000:94

for A being preIfWhileAlgebra

for I being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T st I in ElementaryInstructions A holds

[s,I] in TerminatingPrograms (A,S,T,f)

for I being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T st I in ElementaryInstructions A holds

[s,I] in TerminatingPrograms (A,S,T,f)

proof end;

theorem :: AOFA_000:95

for A being preIfWhileAlgebra

for I being Element of A st I in ElementaryInstructions A holds

I is absolutely-terminating

for I being Element of A st I in ElementaryInstructions A holds

I is absolutely-terminating

proof end;

theorem Th96: :: AOFA_000:96

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T holds [s,(EmptyIns A)] in TerminatingPrograms (A,S,T,f)

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T holds [s,(EmptyIns A)] in TerminatingPrograms (A,S,T,f)

proof end;

registration
end;

registration

let A be preIfWhileAlgebra;

existence

ex b_{1} being Element of A st b_{1} is absolutely-terminating

end;
existence

ex b

proof end;

theorem Th97: :: AOFA_000:97

for A being preIfWhileAlgebra

for I, J being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T st A is free & [s,(I \; J)] in TerminatingPrograms (A,S,T,f) holds

( [s,I] in TerminatingPrograms (A,S,T,f) & [(f . (s,I)),J] in TerminatingPrograms (A,S,T,f) )

for I, J being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T st A is free & [s,(I \; J)] in TerminatingPrograms (A,S,T,f) holds

( [s,I] in TerminatingPrograms (A,S,T,f) & [(f . (s,I)),J] in TerminatingPrograms (A,S,T,f) )

proof end;

registration

let A be preIfWhileAlgebra;

let I, J be absolutely-terminating Element of A;

coherence

I \; J is absolutely-terminating

end;
let I, J be absolutely-terminating Element of A;

coherence

I \; J is absolutely-terminating

proof end;

theorem Th98: :: AOFA_000:98

for A being preIfWhileAlgebra

for C, I, J being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T st A is free & [s,(if-then-else (C,I,J))] in TerminatingPrograms (A,S,T,f) holds

( [s,C] in TerminatingPrograms (A,S,T,f) & ( f . (s,C) in T implies [(f . (s,C)),I] in TerminatingPrograms (A,S,T,f) ) & ( f . (s,C) nin T implies [(f . (s,C)),J] in TerminatingPrograms (A,S,T,f) ) )

for C, I, J being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T st A is free & [s,(if-then-else (C,I,J))] in TerminatingPrograms (A,S,T,f) holds

( [s,C] in TerminatingPrograms (A,S,T,f) & ( f . (s,C) in T implies [(f . (s,C)),I] in TerminatingPrograms (A,S,T,f) ) & ( f . (s,C) nin T implies [(f . (s,C)),J] in TerminatingPrograms (A,S,T,f) ) )

proof end;

registration

let A be preIfWhileAlgebra;

let C, I, J be absolutely-terminating Element of A;

coherence

if-then-else (C,I,J) is absolutely-terminating

end;
let C, I, J be absolutely-terminating Element of A;

coherence

if-then-else (C,I,J) is absolutely-terminating

proof end;

registration

let A be preIfWhileAlgebra;

let C, I be absolutely-terminating Element of A;

coherence

if-then (C,I) is absolutely-terminating ;

end;
let C, I be absolutely-terminating Element of A;

coherence

if-then (C,I) is absolutely-terminating ;

theorem Th99: :: AOFA_000:99

for A being preIfWhileAlgebra

for C, I being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T st A is free & [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) holds

( [s,C] in TerminatingPrograms (A,S,T,f) & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) )

for C, I being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T st A is free & [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) holds

( [s,C] in TerminatingPrograms (A,S,T,f) & ex r being non empty FinSequence of S st

( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds

( r . i in T & [(r . i),(I \; C)] in TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) )

proof end;

theorem :: AOFA_000:100

for A being preIfWhileAlgebra

for C, I being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T st A is free & [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) & f . (s,C) in T holds

[(f . (s,C)),I] in TerminatingPrograms (A,S,T,f)

for C, I being Element of A

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T st A is free & [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) & f . (s,C) in T holds

[(f . (s,C)),I] in TerminatingPrograms (A,S,T,f)

proof end;

theorem :: AOFA_000:101

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T

for C, I being absolutely-terminating Element of A st f iteration_terminates_for I \; C,f . (s,C) holds

[s,(while (C,I))] in TerminatingPrograms (A,S,T,f)

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T

for C, I being absolutely-terminating Element of A st f iteration_terminates_for I \; C,f . (s,C) holds

[s,(while (C,I))] in TerminatingPrograms (A,S,T,f)

proof end;

Lm3: for S being non empty set

for T being Subset of S

for A being free ECIW-strict preIfWhileAlgebra

for f1, f2 being ExecutionFunction of A,S,T st f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] holds

for I being Element of A

for s being Element of S st [s,I] in TerminatingPrograms (A,S,T,f1) holds

( [s,I] in TerminatingPrograms (A,S,T,f2) & f1 . (s,I) = f2 . (s,I) )

proof end;

theorem :: AOFA_000:102

for S being non empty set

for T being Subset of S

for A being free ECIW-strict preIfWhileAlgebra

for f1, f2 being ExecutionFunction of A,S,T st f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] holds

TerminatingPrograms (A,S,T,f1) = TerminatingPrograms (A,S,T,f2)

for T being Subset of S

for A being free ECIW-strict preIfWhileAlgebra

for f1, f2 being ExecutionFunction of A,S,T st f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] holds

TerminatingPrograms (A,S,T,f1) = TerminatingPrograms (A,S,T,f2)

proof end;

theorem :: AOFA_000:103

for S being non empty set

for T being Subset of S

for A being free ECIW-strict preIfWhileAlgebra

for f1, f2 being ExecutionFunction of A,S,T st f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] holds

for s being Element of S

for I being Element of A st [s,I] in TerminatingPrograms (A,S,T,f1) holds

f1 . (s,I) = f2 . (s,I) by Lm3;

for T being Subset of S

for A being free ECIW-strict preIfWhileAlgebra

for f1, f2 being ExecutionFunction of A,S,T st f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] holds

for s being Element of S

for I being Element of A st [s,I] in TerminatingPrograms (A,S,T,f1) holds

f1 . (s,I) = f2 . (s,I) by Lm3;

theorem Th104: :: AOFA_000:104

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for I being absolutely-terminating Element of A holds I is_terminating_wrt f

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for I being absolutely-terminating Element of A holds I is_terminating_wrt f

proof end;

theorem :: AOFA_000:105

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for I being Element of A holds

( I is_terminating_wrt f iff I is_terminating_wrt f,S )

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for I being Element of A holds

( I is_terminating_wrt f iff I is_terminating_wrt f,S )

proof end;

theorem Th106: :: AOFA_000:106

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for I being Element of A st I is_terminating_wrt f holds

for P being set holds I is_terminating_wrt f,P

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for I being Element of A st I is_terminating_wrt f holds

for P being set holds I is_terminating_wrt f,P

proof end;

theorem :: AOFA_000:107

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for I being absolutely-terminating Element of A

for P being set holds I is_terminating_wrt f,P by Th104, Th106;

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for I being absolutely-terminating Element of A

for P being set holds I is_terminating_wrt f,P by Th104, Th106;

theorem :: AOFA_000:108

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for I being Element of A holds S is_invariant_wrt I,f

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for I being Element of A holds S is_invariant_wrt I,f

proof end;

theorem :: AOFA_000:109

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for P being set

for I, J being Element of A st P is_invariant_wrt I,f & P is_invariant_wrt J,f holds

P is_invariant_wrt I \; J,f

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for P being set

for I, J being Element of A st P is_invariant_wrt I,f & P is_invariant_wrt J,f holds

P is_invariant_wrt I \; J,f

proof end;

theorem :: AOFA_000:110

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for I, J being Element of A st I is_terminating_wrt f & J is_terminating_wrt f holds

I \; J is_terminating_wrt f

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for I, J being Element of A st I is_terminating_wrt f & J is_terminating_wrt f holds

I \; J is_terminating_wrt f

proof end;

theorem :: AOFA_000:111

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for P being set

for I, J being Element of A st I is_terminating_wrt f,P & J is_terminating_wrt f,P & P is_invariant_wrt I,f holds

I \; J is_terminating_wrt f,P

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for P being set

for I, J being Element of A st I is_terminating_wrt f,P & J is_terminating_wrt f,P & P is_invariant_wrt I,f holds

I \; J is_terminating_wrt f,P

proof end;

theorem :: AOFA_000:112

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for C, I, J being Element of A st C is_terminating_wrt f & I is_terminating_wrt f & J is_terminating_wrt f holds

if-then-else (C,I,J) is_terminating_wrt f

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for C, I, J being Element of A st C is_terminating_wrt f & I is_terminating_wrt f & J is_terminating_wrt f holds

if-then-else (C,I,J) is_terminating_wrt f

proof end;

theorem :: AOFA_000:113

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for P being set

for C, I, J being Element of A st C is_terminating_wrt f,P & I is_terminating_wrt f,P & J is_terminating_wrt f,P & P is_invariant_wrt C,f holds

if-then-else (C,I,J) is_terminating_wrt f,P

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for P being set

for C, I, J being Element of A st C is_terminating_wrt f,P & I is_terminating_wrt f,P & J is_terminating_wrt f,P & P is_invariant_wrt C,f holds

if-then-else (C,I,J) is_terminating_wrt f,P

proof end;

theorem Th114: :: AOFA_000:114

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T

for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f & f iteration_terminates_for I \; C,f . (s,C) holds

[s,(while (C,I))] in TerminatingPrograms (A,S,T,f)

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T

for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f & f iteration_terminates_for I \; C,f . (s,C) holds

[s,(while (C,I))] in TerminatingPrograms (A,S,T,f)

proof end;

theorem :: AOFA_000:115

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T

for P being set

for C, I being Element of A st C is_terminating_wrt f,P & I is_terminating_wrt f,P & P is_invariant_wrt C,f & P is_invariant_wrt I,f & f iteration_terminates_for I \; C,f . (s,C) & s in P holds

[s,(while (C,I))] in TerminatingPrograms (A,S,T,f)

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T

for P being set

for C, I being Element of A st C is_terminating_wrt f,P & I is_terminating_wrt f,P & P is_invariant_wrt C,f & P is_invariant_wrt I,f & f iteration_terminates_for I \; C,f . (s,C) & s in P holds

[s,(while (C,I))] in TerminatingPrograms (A,S,T,f)

proof end;

theorem Th116: :: AOFA_000:116

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T

for P being set

for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f,P & P is_invariant_wrt C,f & ( for s being Element of S st s in P & f . ((f . (s,I)),C) in T holds

f . (s,I) in P ) & f iteration_terminates_for I \; C,f . (s,C) & s in P holds

[s,(while (C,I))] in TerminatingPrograms (A,S,T,f)

for S being non empty set

for T being Subset of S

for s being Element of S

for f being ExecutionFunction of A,S,T

for P being set

for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f,P & P is_invariant_wrt C,f & ( for s being Element of S st s in P & f . ((f . (s,I)),C) in T holds

f . (s,I) in P ) & f iteration_terminates_for I \; C,f . (s,C) & s in P holds

[s,(while (C,I))] in TerminatingPrograms (A,S,T,f)

proof end;

theorem :: AOFA_000:117

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f & ( for s being Element of S holds f iteration_terminates_for I \; C,s ) holds

while (C,I) is_terminating_wrt f

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f & ( for s being Element of S holds f iteration_terminates_for I \; C,s ) holds

while (C,I) is_terminating_wrt f

proof end;

theorem :: AOFA_000:118

for A being preIfWhileAlgebra

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for P being set

for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f,P & P is_invariant_wrt C,f & ( for s being Element of S st s in P & f . ((f . (s,I)),C) in T holds

f . (s,I) in P ) & ( for s being Element of S st f . (s,C) in P holds

f iteration_terminates_for I \; C,f . (s,C) ) holds

while (C,I) is_terminating_wrt f,P

for S being non empty set

for T being Subset of S

for f being ExecutionFunction of A,S,T

for P being set

for C, I being Element of A st C is_terminating_wrt f & I is_terminating_wrt f,P & P is_invariant_wrt C,f & ( for s being Element of S st s in P & f . ((f . (s,I)),C) in T holds

f . (s,I) in P ) & ( for s being Element of S st f . (s,C) in P holds

f iteration_terminates_for I \; C,f . (s,C) ) holds

while (C,I) is_terminating_wrt f,P

proof end;