:: Mizar Analysis of Algorithms: Preliminaries
:: by Grzegorz Bancerek
::
:: Received July 9, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

notation
let x, y be set ;
antonym x nin y for x in y;
end;

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
proofend;

registration
let x, y be non empty set ;
cluster<*x,y*> ->  non-empty ;
coherence
 <*x,y*> is non-empty
proofend;
end;

registration
let p, q be non-empty FinSequence;
clusterp ^ q ->  non-empty ;
coherence
 p ^ q is non-empty
proofend;
end;

definition
let f be homogeneous Function;
let x be set ;
predx is_a_unity_wrt f means :Def1: :: AOFA_000:def 1
 for y, z being set st ( <*y,z*> in dom f or <*z,y*> in dom f ) holds
( <*x,y*> in dom f &amp; f . <*x,y*> = y &amp; <*y,x*> in dom f &amp; f . <*y,x*> = y );
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 &amp; f . <*x,y*> = y &amp; <*y,x*> in dom f &amp; f . <*y,x*> = y ) );

definition
let f be homogeneous Function;
attrf is associative  means :Def2: :: AOFA_000:def 2
 for x, y, z being set st <*x,y*> in dom f &amp; <*y,z*> in dom f &amp; <*(f . <*x,y*>),z*> in dom f &amp; <*x,(f . <*y,z*>)*> in dom f holds
f . <*(f . <*x,y*>),z*> = f . <*x,(f . <*y,z*>)*>;
attrf is unital  means :Def3: :: AOFA_000:def 3
 ex x being set st x is_a_unity_wrt f;
end;

:: 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 &amp; <*y,z*> in dom f &amp; <*(f . <*x,y*>),z*> in dom f &amp; <*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 );

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 funcZ --> y ->  PartFunc of (X *),Y;
coherence
 Z --> y is PartFunc of (X *),Y
proofend;
end;

registration
let X be non empty set ;
let x be Element of X;
let n be Nat;
cluster(n -tuples_on X) --> x ->  non empty homogeneous quasi_total for PartFunc of (X *),X;
coherence
 for b1 being PartFunc of (X *),X st b1 = (n -tuples_on X) --> x holds
( not b1 is empty &amp; b1 is quasi_total &amp; b1 is homogeneous )
proofend;
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
proofend;

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
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;

registration
let X be non empty set ;
let x be Element of X;
let n be Nat;
cluster(n -tuples_on X) --> x ->  homogeneous n -ary for homogeneous PartFunc of (X *),X;
coherence
 for b1 being homogeneous PartFunc of (X *),X st b1 = (n -tuples_on X) --> x holds
b1 is n -ary by Lm1;
end;

registration
let X be non empty set ;
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 b1 being non empty homogeneous quasi_total PartFunc of (X *),X st
( b1 is 2 -ary &amp; b1 is associative &amp; b1 is unital )
proofend;
cluster non empty Relation-like X * -defined X -valued Function-like homogeneous quasi_total 0 -ary for Element of bool [:(X *),X:];
existence
 ex b1 being non empty homogeneous quasi_total PartFunc of (X *),X st b1 is 0 -ary
proofend;
cluster non empty Relation-like X * -defined X -valued Function-like homogeneous quasi_total 3 -ary for Element of bool [:(X *),X:];
existence
 ex b1 being non empty homogeneous quasi_total PartFunc of (X *),X st b1 is 3 -ary
proofend;
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
proofend;

definition
let f, g be Function;
let X be set ;
func(f,X) +* g ->  Function equals :: AOFA_000:def 4
g +* (f | X);
coherence
 g +* (f | X) is Function ;
end;

:: deftheorem  defines +* AOFA_000:def_4_:_
 for f, g being Function
for X being set holds (f,X) +* g = g +* (f | X);

theorem Th4: :: AOFA_000:4
for f, g being Function
for x, X being set st x in X &amp; X c= dom f holds
((f,X) +* g) . x = f . x
proofend;

theorem Th5: :: AOFA_000:5
for f, g being Function
for x, X being set st x nin X &amp; x in dom g holds
((f,X) +* g) . x = g . x
proofend;

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)
proofend;
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 funcg * f ->  Element of Funcs (X,Z);
coherence
 f * g is Element of Funcs (X,Z)
proofend;
end;

definition
let f be Function;
let x be set ;
funcf 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))  }  is set ;
end;

:: 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))  }  ;

theorem Th6: :: AOFA_000:6
for f being Function
for x being set st x in dom f holds
x in f orbit x
proofend;

theorem :: AOFA_000:7
for f being Function
for x, y being set st rng f c= dom f &amp; y in f orbit x holds
f . y in f orbit x
proofend;

theorem :: AOFA_000:8
for f being Function
for x being set st x in dom f holds
f . x in f orbit x
proofend;

theorem Th9: :: AOFA_000:9
for f being Function
for x being set st x in dom f holds
f orbit (f . x) c= f orbit x
proofend;

definition
let f be Function;
assume B1: rng f c= dom f ;
let A, x be set ;
defpred S1[ 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: S1[ 0 ] by FUNCT_1:17;
A3: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_
S1[i_+_1]
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A4: S1[i] ; ::_thesis: S1[i + 1]
thus  S1[i + 1] ::_thesis: verum
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;
end;
A8: for i being Element of NAT holds S1[i] from NAT_1:sch_1(A2, A3);
func(A,x) iter f ->  Function means :: AOFA_000:def 6
( dom it = dom f &amp; ( for a being set st a in dom f holds
( ( f orbit a c= A implies it . a = x ) &amp; ( for n being Nat st (iter (f,n)) . a nin A &amp; ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) holds
it . a = (iter (f,n)) . a ) ) ) );
existence
 ex b1 being Function st
( dom b1 = dom f &amp; ( for a being set st a in dom f holds
( ( f orbit a c= A implies b1 . a = x ) &amp; ( for n being Nat st (iter (f,n)) . a nin A &amp; ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) holds
b1 . a = (iter (f,n)) . a ) ) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = dom f &amp; ( for a being set st a in dom f holds
( ( f orbit a c= A implies b1 . a = x ) &amp; ( for n being Nat st (iter (f,n)) . a nin A &amp; ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) holds
b1 . a = (iter (f,n)) . a ) ) ) &amp; dom b2 = dom f &amp; ( for a being set st a in dom f holds
( ( f orbit a c= A implies b2 . a = x ) &amp; ( for n being Nat st (iter (f,n)) . a nin A &amp; ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) holds
b2 . a = (iter (f,n)) . a ) ) ) holds
b1 = b2
proofend;
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 b4 being Function holds
( b4 = (A,x) iter f iff ( dom b4 = dom f &amp; ( for a being set st a in dom f holds
( ( f orbit a c= A implies b4 . a = x ) &amp; ( for n being Nat st (iter (f,n)) . a nin A &amp; ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) holds
b4 . a = (iter (f,n)) . a ) ) ) ) );

definition
let f be Function;
assume B1: rng f c= dom f ;
let A be set ;
let g be Function;
defpred S1[ 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: S1[ 0 ] by FUNCT_1:17;
A3: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_
S1[i_+_1]
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A4: S1[i] ; ::_thesis: S1[i + 1]
thus  S1[i + 1] ::_thesis: verum
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;
end;
A8: for i being Element of NAT holds S1[i] from NAT_1:sch_1(A2, A3);
func(A,g) iter f ->  Function means :Def7: :: AOFA_000:def 7
( dom it = dom f &amp; ( for a being set st a in dom f holds
( ( f orbit a c= A implies it . a = g . a ) &amp; ( for n being Nat st (iter (f,n)) . a nin A &amp; ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) holds
it . a = (iter (f,n)) . a ) ) ) );
existence
 ex b1 being Function st
( dom b1 = dom f &amp; ( for a being set st a in dom f holds
( ( f orbit a c= A implies b1 . a = g . a ) &amp; ( for n being Nat st (iter (f,n)) . a nin A &amp; ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) holds
b1 . a = (iter (f,n)) . a ) ) ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = dom f &amp; ( for a being set st a in dom f holds
( ( f orbit a c= A implies b1 . a = g . a ) &amp; ( for n being Nat st (iter (f,n)) . a nin A &amp; ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) holds
b1 . a = (iter (f,n)) . a ) ) ) &amp; dom b2 = dom f &amp; ( for a being set st a in dom f holds
( ( f orbit a c= A implies b2 . a = g . a ) &amp; ( for n being Nat st (iter (f,n)) . a nin A &amp; ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) holds
b2 . a = (iter (f,n)) . a ) ) ) holds
b1 = b2
proofend;
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, b4 being Function holds
( b4 = (A,g) iter f iff ( dom b4 = dom f &amp; ( for a being set st a in dom f holds
( ( f orbit a c= A implies b4 . a = g . a ) &amp; ( for n being Nat st (iter (f,n)) . a nin A &amp; ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) holds
b4 . a = (iter (f,n)) . a ) ) ) ) );

theorem Th10: :: AOFA_000:10
for f, g being Function
for a, A being set st rng f c= dom f &amp; a in dom f &amp; not f orbit a c= A holds
ex n being Nat st
( ((A,g) iter f) . a = (iter (f,n)) . a &amp; (iter (f,n)) . a nin A &amp; ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) )
proofend;

theorem Th11: :: AOFA_000:11
for f, g being Function
for a, A being set st rng f c= dom f &amp; a in dom f &amp; g * f = g &amp; a in A holds
((A,g) iter f) . a = ((A,g) iter f) . (f . a)
proofend;

theorem Th12: :: AOFA_000:12
for f, g being Function
for a, A being set st rng f c= dom f &amp; a in dom f &amp; a nin A holds
((A,g) iter f) . a = a
proofend;

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)
proofend;
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 &amp; signature A = S )
proofend;

theorem Th14: :: AOFA_000:14
for S being non empty FinSequence of NAT ex A being Universal_Algebra st
( the carrier of A = NAT &amp; signature A = S &amp; ( for i, j being Nat st i in dom S &amp; j = S . i holds
the charact of A . i = (j -tuples_on NAT) --> i ) )
proofend;

theorem :: AOFA_000:15
for S being non empty FinSequence of NAT
for i, j being Nat st i in dom S &amp; 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 &amp; signature A = S &amp; the charact of A . i = f )
proofend;

registration
let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
cluster  ->  Relation-like Function-like for Element of the carrier of (FreeUnivAlgNSG (f,D));
coherence
 for b1 being Element of (FreeUnivAlgNSG (f,D)) holds
( b1 is Relation-like &amp; b1 is Function-like ) ;
end;

registration
let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
cluster  ->  DecoratedTree-like for Element of the carrier of (FreeUnivAlgNSG (f,D));
coherence
 for b1 being Element of (FreeUnivAlgNSG (f,D)) holds b1 is DecoratedTree-like ;
cluster  ->  DTree-yielding for FinSequence of the carrier of (FreeUnivAlgNSG (f,D));
coherence
 for b1 being FinSequence of (FreeUnivAlgNSG (f,D)) holds b1 is DTree-yielding ;
end;

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 &amp; t = root-tree d ) or ex o being Symbol of G ex p being FinSequence of TS G st
( o ==> roots p &amp; t = o -tree p ) )
proofend;

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
proofend;

definition
let A be non-empty UAStr ;
let B be Subset of A;
let n be Nat;
funcB |^ 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 &amp; F . 0 = B &amp; ( 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)) &amp; rng p c= F . n )  }  ) );
existence
 ex b1 being Subset of A ex F being Function of NAT,(bool the carrier of A) st
( b1 = F . n &amp; F . 0 = B &amp; ( 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)) &amp; rng p c= F . n )  }  ) )
proofend;
uniqueness
 for b1, b2 being Subset of A st ex F being Function of NAT,(bool the carrier of A) st
( b1 = F . n &amp; F . 0 = B &amp; ( 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)) &amp; rng p c= F . n )  }  ) ) &amp; ex F being Function of NAT,(bool the carrier of A) st
( b2 = F . n &amp; F . 0 = B &amp; ( 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)) &amp; rng p c= F . n )  }  ) ) holds
b1 = b2
proofend;
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 b4 being Subset of A holds
( b4 = B |^ n iff ex F being Function of NAT,(bool the carrier of A) st
( b4 = F . n &amp; F . 0 = B &amp; ( 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)) &amp; rng p c= F . n )  }  ) ) );

theorem Th18: :: AOFA_000:18
for A being Universal_Algebra
for B being Subset of A holds B |^ 0 = B
proofend;

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)) &amp; rng p c= B |^ n )  }
proofend;

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 &amp; p in dom (Den (o,A)) &amp; rng p c= B |^ n ) ) )
proofend;

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
proofend;

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
proofend;

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 &amp; p in dom (Den (o,A)) &amp; rng p c= B |^ n ) ) )
proofend;

scheme :: AOFA_000:sch 1
MaxVal{ F1() ->  non empty set , F2() ->  set , P1[ set , set ] } :
 ex n being Nat st
for x being Element of F1() st x in F2() holds
P1[x,n]
provided
A1: F2() is finite and
A2: for x being Element of F1() st x in F2() holds
ex n being Nat st P1[x,n] and
A3: for x being Element of F1()
for n, m being Nat st P1[x,n] &amp; n <= m holds
P1[x,m]
proofend;

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  }  &amp; C is opers_closed )
proofend;

theorem Th25: :: AOFA_000:25
for A being Universal_Algebra
for B, C being Subset of A st C is opers_closed &amp; B c= C holds
union  {  (B |^ n) where n is Element of NAT : verum  }  c= C
proofend;

definition
let A be Universal_Algebra;
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  }  ) is Subset of A ;
end;

:: 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  }  );

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 )
proofend;

theorem :: AOFA_000:27
for A being Universal_Algebra
for B being Subset of A st B is opers_closed holds
Constants A c= B
proofend;

theorem Th28: :: AOFA_000:28
for A being Universal_Algebra st Constants A = {} holds
{} A is opers_closed
proofend;

theorem :: AOFA_000:29
for A being Universal_Algebra st Constants A = {} holds
for G being GeneratorSet of A holds G <> {}
proofend;

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 )
proofend;

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
proofend;

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
proofend;

theorem :: AOFA_000:33
for A being Universal_Algebra
for G being GeneratorSet of A holds Generators A c= G
proofend;

theorem Th34: :: AOFA_000:34
for A being free Universal_Algebra
for G being free GeneratorSet of A holds G = Generators A
proofend;

registration
let A be free Universal_Algebra;
cluster Generators A ->  free for GeneratorSet of A;
coherence
 for b1 being GeneratorSet of A st b1 = Generators A holds
b1 is free
proofend;
end;

definition
let A be free Universal_Algebra;
:: original:Generators
redefine func Generators A ->  GeneratorSet of A;
coherence
 Generators A is GeneratorSet of A
proofend;
end;

registration
let A, B be set ;
cluster[:A,B:] ->  disjoint_with_NAT ;
coherence
 [:A,B:] is disjoint_with_NAT
proofend;
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 &amp; h2 is_homomorphism A,B &amp; h1 | G = h2 | G holds
h1 = h2
proofend;

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)) &amp; p2 in dom (Den (o2,A)) &amp; (Den (o1,A)) . p1 = (Den (o2,A)) . p2 holds
o1 = o2
proofend;

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)) &amp; p2 in dom (Den (o2,A)) &amp; (Den (o1,A)) . p1 = (Den (o2,A)) . p2 holds
( o1 = o2 &amp; p1 = p2 )
proofend;

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 &amp; p2 in dom o2 &amp; o1 . p1 = o2 . p2 holds
( o1 = o2 &amp; p1 = p2 )
proofend;

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
proofend;

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)) &amp; (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
proofend;

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
proofend;

begin

definition
let S be non empty UAStr ;
attrS is with_empty-instruction  means :Def10: :: AOFA_000:def 10
( 1 in dom the charact of S &amp; the charact of S . 1 is non empty homogeneous quasi_total 0 -ary PartFunc of ( the carrier of S *), the carrier of S );
attrS is with_catenation  means :Def11: :: AOFA_000:def 11
( 2 in dom the charact of S &amp; the charact of S . 2 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of S *), the carrier of S );
attrS is with_if-instruction  means :Def12: :: AOFA_000:def 12
( 3 in dom the charact of S &amp; the charact of S . 3 is non empty homogeneous quasi_total 3 -ary PartFunc of ( the carrier of S *), the carrier of S );
attrS is with_while-instruction  means :Def13: :: AOFA_000:def 13
( 4 in dom the charact of S &amp; the charact of S . 4 is non empty homogeneous quasi_total 2 -ary PartFunc of ( the carrier of S *), the carrier of S );
attrS 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;
end;

:: 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 &amp; 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 &amp; 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 &amp; 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 &amp; 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 );

definition
let S be non-empty UAStr ;
attrS is unital  means :Def15: :: AOFA_000:def 15
 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 &amp; (Den ((In (1,(dom the charact of S))),S)) . {} is_a_unity_wrt f );
end;

:: 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 &amp; (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 &amp; the charact of S = <*((0 -tuples_on X) --> x),c*> ^ <*i,w*> &amp; S is with_empty-instruction &amp; S is with_catenation &amp; S is unital &amp; S is associative &amp; S is with_if-instruction &amp; S is with_while-instruction &amp; S is quasi_total &amp; S is partial )
proofend;

registration
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 b1 being strict partial quasi_total non-empty UAStr st
( b1 is with_empty-instruction &amp; b1 is with_catenation &amp; b1 is with_if-instruction &amp; b1 is with_while-instruction &amp; b1 is unital &amp; b1 is associative )
proofend;
end;

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

definition
let A be non empty UAStr ;
mode Algorithm of A is Element of A;
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)) = {{}}
proofend;

definition
let A be non-empty with_empty-instruction UAStr ;
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)) . {} is Algorithm of A
proofend;
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)) . {};

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 &amp; EmptyIns A in rng o )
proofend;

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
proofend;

definition
let A be non-empty with_catenation UAStr ;
let I1, I2 be Algorithm of A;
funcI1 \; 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*> is Algorithm of A
proofend;
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*>;

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 &amp; I \; (EmptyIns A) = I )
proofend;

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)
proofend;

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
proofend;

definition
let A be non-empty with_if-instruction UAStr ;
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*> is Algorithm of A
proofend;
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*>;

definition
let A be non-empty with_empty-instruction with_if-instruction UAStr ;
let C, I be Algorithm of A;
func if-then (C,I) ->  Algorithm of A equals :: AOFA_000:def 19
 if-then-else (C,I,(EmptyIns A));
coherence
 if-then-else (C,I,(EmptyIns A)) is Algorithm of A ;
end;

:: 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));

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
proofend;

definition
let A be non-empty with_while-instruction UAStr ;
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*> is Algorithm of A
proofend;
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*>;

definition
let A be preIfWhileAlgebra;
let I0, C, I, J be Element of A;
func for-do (I0,C,J,I) ->  Element of A equals :: AOFA_000:def 21
I0 \; (while (C,(I \; J)));
coherence
 I0 \; (while (C,(I \; J))) is Element of A ;
end;

:: 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)));

definition
let A be preIfWhileAlgebra;
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 &amp; 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 &amp; I2 <> I1 \; I2 )  }  is Subset of A ;
end;

:: 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 &amp; I2 <> I1 \; I2 )  }  ;

theorem Th49: :: AOFA_000:49
for A being preIfWhileAlgebra holds EmptyIns A nin ElementaryInstructions A
proofend;

theorem Th50: :: AOFA_000:50
for A being preIfWhileAlgebra
for I1, I2 being Element of A st I1 <> I1 \; I2 &amp; I2 <> I1 \; I2 holds
I1 \; I2 nin ElementaryInstructions A
proofend;

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
proofend;

theorem Th52: :: AOFA_000:52
for A being preIfWhileAlgebra
for C, I being Element of A holds while (C,I) nin ElementaryInstructions A
proofend;

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 &amp; I1 <> I1 \; I2 &amp; 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) )
proofend;

definition
let A be preIfWhileAlgebra;
attrA is infinite  means :Def23: :: AOFA_000:def 23
 ElementaryInstructions A is infinite ;
attrA is degenerated  means :Def24: :: AOFA_000:def 24
( ex I1, I2 being Element of A st
( ( I1 <> EmptyIns A &amp; I1 \; I2 = I2 ) or ( I2 <> EmptyIns A &amp; I1 \; I2 = I1 ) or ( ( I1 <> EmptyIns A or I2 <> EmptyIns A ) &amp; 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 &amp; I2 <> EmptyIns A &amp; I1 \; I2 = if-then-else (C,J1,J2) ) or ex I1, I2, C, J being Element of A st
( I1 <> EmptyIns A &amp; I2 <> EmptyIns A &amp; 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) );
attrA is well_founded  means :Def25: :: AOFA_000:def 25
 ElementaryInstructions A is GeneratorSet of A;
end;

:: deftheorem Def23 defines infinite AOFA_000:def_23_:_
 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 &amp; I1 \; I2 = I2 ) or ( I2 <> EmptyIns A &amp; I1 \; I2 = I1 ) or ( ( I1 <> EmptyIns A or I2 <> EmptyIns A ) &amp; 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 &amp; I2 <> EmptyIns A &amp; I1 \; I2 = if-then-else (C,J1,J2) ) or ex I1, I2, C, J being Element of A st
( I1 <> EmptyIns A &amp; I2 <> EmptyIns A &amp; 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 );

definition
func ECIW-signature  ->  non empty FinSequence of NAT  equals :: AOFA_000:def 26
<*0,2*> ^ <*3,2*>;
coherence
 <*0,2*> ^ <*3,2*> is non empty FinSequence of NAT ;
end;

:: deftheorem  defines ECIW-signature AOFA_000:def_26_:_
 ECIW-signature = <*0,2*> ^ <*3,2*>;

theorem Th54: :: AOFA_000:54
( len ECIW-signature = 4 &amp; dom ECIW-signature = Seg 4 &amp; ECIW-signature . 1 = 0 &amp; ECIW-signature . 2 = 2 &amp; ECIW-signature . 3 = 3 &amp; ECIW-signature . 4 = 2 )
proofend;

definition
let A be non empty partial non-empty UAStr ;
attrA is ECIW-strict  means :Def27: :: AOFA_000:def 27
 signature A = ECIW-signature ;
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 );

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 )
proofend;

registration
let X be non empty disjoint_with_NAT set ;
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 &amp; FreeUnivAlgNSG (ECIW-signature,X) is with_catenation &amp; FreeUnivAlgNSG (ECIW-signature,X) is with_if-instruction &amp; FreeUnivAlgNSG (ECIW-signature,X) is with_while-instruction )
proofend;
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 &amp; I = n -tree p &amp; len p = ECIW-signature . n ) )
proofend;

theorem Th57: :: AOFA_000:57
for X being non empty disjoint_with_NAT set holds EmptyIns (FreeUnivAlgNSG (ECIW-signature,X)) = 1 -tree {}
proofend;

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 = {}
proofend;

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)
proofend;

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*>
proofend;

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 &amp; I1 \; I2 <> I2 )
proofend;

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 &amp; I2 = J2 )
proofend;

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*>
proofend;

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*>
proofend;

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 &amp; I1 = J1 &amp; I2 = J2 )
proofend;

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)
proofend;

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*>
proofend;

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 {}
proofend;

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 = {}
proofend;

theorem Th70: :: AOFA_000:70
for X being non empty disjoint_with_NAT set holds
( ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,X)) = FreeGenSetNSG (ECIW-signature,X) &amp; card X = card (FreeGenSetNSG (ECIW-signature,X)) )
proofend;

registration
cluster infinite disjoint_with_NAT for set ;
existence
 ex b1 being set st
( b1 is infinite &amp; b1 is disjoint_with_NAT )
proofend;
end;

registration
let X be infinite disjoint_with_NAT set ;
cluster FreeUnivAlgNSG (ECIW-signature,X) ->  infinite ;
coherence
 FreeUnivAlgNSG (ECIW-signature,X) is infinite
proofend;
end;

registration
let X be non empty disjoint_with_NAT set ;
cluster FreeUnivAlgNSG (ECIW-signature,X) ->  ECIW-strict ;
coherence
 FreeUnivAlgNSG (ECIW-signature,X) is ECIW-strict
proofend;
end;

theorem Th71: :: AOFA_000:71
for A being preIfWhileAlgebra holds Generators A c= ElementaryInstructions A
proofend;

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 &amp; EmptyIns A <> if-then-else (C,I1,I2) &amp; EmptyIns A <> while (C,I1) )
proofend;

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 &amp; I1 \; I2 <> I2 &amp; ( I1 \; I2 = J1 \; J2 implies ( I1 = J1 &amp; I2 = J2 ) ) &amp; I1 \; I2 <> if-then-else (C,J1,J2) &amp; I1 \; I2 <> while (C,J1) )
proofend;

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 &amp; if-then-else (C,I1,I2) <> I1 &amp; if-then-else (C,I1,I2) <> I2 &amp; if-then-else (C,I1,I2) <> while (D,J1) &amp; ( if-then-else (C,I1,I2) = if-then-else (D,J1,J2) implies ( C = D &amp; I1 = J1 &amp; I2 = J2 ) ) )
proofend;

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 &amp; while (C,I) <> I &amp; ( while (C,I) = while (D,J) implies ( C = D &amp; I = J ) ) )
proofend;

registration
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 b1 being preIfWhileAlgebra st b1 is free holds
( b1 is well_founded &amp; not b1 is degenerated )
proofend;
end;

registration
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 b1 being preIfWhileAlgebra st
( b1 is infinite &amp; not b1 is degenerated &amp; b1 is well_founded &amp; b1 is ECIW-strict &amp; b1 is free &amp; b1 is strict )
proofend;
end;

definition
mode IfWhileAlgebra is non degenerated well_founded ECIW-strict preIfWhileAlgebra;
end;

registration
let A be infinite preIfWhileAlgebra;
cluster ElementaryInstructions A ->  infinite ;
coherence
 not ElementaryInstructions A is finite by Def23;
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) &amp; ( for C, I1, I2 being Element of A st C in B |^ n &amp; I1 in B |^ n &amp; I2 in B |^ n holds
( I1 \; I2 in B |^ (n + 1) &amp; if-then-else (C,I1,I2) in B |^ (n + 1) &amp; while (C,I1) in B |^ (n + 1) ) ) )
proofend;

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 &amp; I1 in (ElementaryInstructions A) |^ n &amp; I2 in (ElementaryInstructions A) |^ n ) or ex C, I1, I2 being Element of A st
( x = if-then-else (C,I1,I2) &amp; C in (ElementaryInstructions A) |^ n &amp; I1 in (ElementaryInstructions A) |^ n &amp; I2 in (ElementaryInstructions A) |^ n ) or ex C, I being Element of A st
( x = while (C,I) &amp; C in (ElementaryInstructions A) |^ n &amp; I in (ElementaryInstructions A) |^ n ) )
proofend;

theorem :: AOFA_000:78
for A being Universal_Algebra
for B being Subset of A holds Constants A c= B |^ 1
proofend;

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 )
proofend;

scheme :: AOFA_000:sch 2
StructInd{ F1() ->  well_founded ECIW-strict preIfWhileAlgebra, F2() ->  Element of F1(), P1[ set ] } :
 P1[F2()]
provided
A1: for I being Element of F1() st I in ElementaryInstructions F1() holds
P1[I] and
A2: P1[ EmptyIns F1()] and
A3: for I1, I2 being Element of F1() st P1[I1] &amp; P1[I2] holds
P1[I1 \; I2] and
A4: for C, I1, I2 being Element of F1() st P1[C] &amp; P1[I1] &amp; P1[I2] holds
P1[ if-then-else (C,I1,I2)] and
A5: for C, I being Element of F1() st P1[C] &amp; P1[I] holds
P1[ while (C,I)]
proofend;

begin

definition
let A be preIfWhileAlgebra;
let S be non empty set ;
let f be Function of [:S, the carrier of A:],S;
attrf is complying_with_empty-instruction  means :Def28: :: AOFA_000:def 28
 for s being Element of S holds f . (s,(EmptyIns A)) = s;
attrf 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);
end;

:: 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 );

:: 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) );

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;
predf 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) ) &amp; ( f . (s,C) nin T implies f . (s,(if-then-else (C,I1,I2))) = f . ((f . (s,C)),I2) ) );
predf complies_with_while_wrt T means :Def31: :: AOFA_000:def 31
 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))) ) &amp; ( f . (s,C) nin T implies f . (s,(while (C,I))) = f . (s,C) ) );
end;

:: 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) ) &amp; ( 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))) ) &amp; ( 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 &amp; 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)
proofend;

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 &amp; pr1 (S, the carrier of A) is complying_with_catenation &amp; pr1 (S, the carrier of A) complies_with_if_wrt T &amp; pr1 (S, the carrier of A) complies_with_while_wrt T )
proofend;

definition
let A be preIfWhileAlgebra;
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 &amp; it is complying_with_catenation &amp; it complies_with_if_wrt T &amp; it complies_with_while_wrt T );
existence
 ex b1 being Function of [:S, the carrier of A:],S st
( b1 is complying_with_empty-instruction &amp; b1 is complying_with_catenation &amp; b1 complies_with_if_wrt T &amp; b1 complies_with_while_wrt T )
proofend;
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 b4 being Function of [:S, the carrier of A:],S holds
( b4 is ExecutionFunction of A,S,T iff ( b4 is complying_with_empty-instruction &amp; b4 is complying_with_catenation &amp; b4 complies_with_if_wrt T &amp; b4 complies_with_while_wrt T ) );

registration
let A be preIfWhileAlgebra;
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 b1 being ExecutionFunction of A,S,T holds
( b1 is complying_with_empty-instruction &amp; b1 is complying_with_catenation ) by Def32;
end;

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;
predf iteration_terminates_for I,s means :Def33: :: AOFA_000:def 33
 ex r being non empty FinSequence of S st
( r . 1 = s &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; r . (i + 1) = f . ((r . i),I) ) ) );
end;

:: 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 &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; 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;
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 &amp; r . 1 = s &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; r . (i + 1) = f . ((r . i),I) ) ) ) if f iteration_terminates_for I,s
otherwise it = +infty ;
correctness
consistency
for b1 being R_eal holds verum;
existence
( ( for b1 being R_eal holds verum ) &amp; ( f iteration_terminates_for I,s implies ex b1 being R_eal ex r being non empty FinSequence of S st
( b1 = (len r) - 1 &amp; r . 1 = s &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; r . (i + 1) = f . ((r . i),I) ) ) ) ) &amp; ( not f iteration_terminates_for I,s implies ex b1 being R_eal st b1 = +infty ) );
uniqueness
for b1, b2 being R_eal holds
( ( f iteration_terminates_for I,s &amp; ex r being non empty FinSequence of S st
( b1 = (len r) - 1 &amp; r . 1 = s &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; r . (i + 1) = f . ((r . i),I) ) ) ) &amp; ex r being non empty FinSequence of S st
( b2 = (len r) - 1 &amp; r . 1 = s &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; r . (i + 1) = f . ((r . i),I) ) ) ) implies b1 = b2 ) &amp; ( not f iteration_terminates_for I,s &amp; b1 = +infty &amp; b2 = +infty implies b1 = b2 ) );
proofend;
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 b7 being R_eal holds
( ( f iteration_terminates_for I,s implies ( b7 = iteration-degree (I,s,f) iff ex r being non empty FinSequence of S st
( b7 = (len r) - 1 &amp; r . 1 = s &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; r . (i + 1) = f . ((r . i),I) ) ) ) ) ) &amp; ( not f iteration_terminates_for I,s implies ( b7 = iteration-degree (I,s,f) iff b7 = +infty ) ) );

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 )
proofend;

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 &amp; iteration-degree (I,s,f) = 0 )
proofend;

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) ) &amp; ( f iteration_terminates_for I,f . (s,I) implies f iteration_terminates_for I,s ) &amp; iteration-degree (I,s,f) = 1. + (iteration-degree (I,(f . (s,I)),f)) )
proofend;

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
proofend;

scheme :: AOFA_000:sch 3
Termination{ F1() ->  preIfWhileAlgebra, F2() ->  Element of F1(), F3() ->  non empty set , F4() ->  Element of F3(), F5() ->  Subset of F3(), F6() ->  ExecutionFunction of F1(),F3(),F5(), F7( set ) ->  Nat, P1[ set ] } :
 F6() iteration_terminates_for F2(),F4()
provided
A1: ( F4() in F5() iff P1[F4()] ) and
A2: for s being Element of F3() st P1[s] holds
( ( P1[F6() . (s,F2())] implies F6() . (s,F2()) in F5() ) &amp; ( F6() . (s,F2()) in F5() implies P1[F6() . (s,F2())] ) &amp; F7((F6() . (s,F2()))) < F7(s) )
proofend;

scheme :: AOFA_000:sch 4
Termination2{ F1() ->  preIfWhileAlgebra, F2() ->  Element of F1(), F3() ->  non empty set , F4() ->  Element of F3(), F5() ->  Subset of F3(), F6() ->  ExecutionFunction of F1(),F3(),F5(), F7( set ) ->  Nat, P1[ set ], P2[ set ] } :
 F6() iteration_terminates_for F2(),F4()
provided
A1: P1[F4()] and
A2: ( F4() in F5() iff P2[F4()] ) and
A3: for s being Element of F3() st P1[s] &amp; s in F5() &amp; P2[s] holds
( P1[F6() . (s,F2())] &amp; ( P2[F6() . (s,F2())] implies F6() . (s,F2()) in F5() ) &amp; ( F6() . (s,F2()) in F5() implies P2[F6() . (s,F2())] ) &amp; F7((F6() . (s,F2()))) < F7(s) )
proofend;

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) &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; r . (i + 1) = f . ((r . i),(I \; C)) ) ) holds
f . (s,(while (C,I))) = r . (len r)
proofend;

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 )
proofend;

scheme :: AOFA_000:sch 5
InvariantSch{ F1() ->  preIfWhileAlgebra, F2() ->  Element of F1(), F3() ->  Element of F1(), F4() ->  non empty set , F5() ->  Element of F4(), F6() ->  Subset of F4(), F7() ->  ExecutionFunction of F1(),F4(),F6(), P1[ set ], P2[ set ] } :
 ( P1[F7() . (F5(),(while (F2(),F3())))] &amp; P2[F7() . (F5(),(while (F2(),F3())))] )
provided
A1: P1[F5()] and
A2: F7() iteration_terminates_for F3() \; F2(),F7() . (F5(),F2()) and
A3: for s being Element of F4() st P1[s] &amp; s in F6() &amp; P2[s] holds
P1[F7() . (s,F3())] and
A4: for s being Element of F4() st P1[s] holds
( P1[F7() . (s,F2())] &amp; ( F7() . (s,F2()) in F6() implies P2[F7() . (s,F2())] ) &amp; ( P2[F7() . (s,F2())] implies F7() . (s,F2()) in F6() ) )
proofend;

scheme :: AOFA_000:sch 6
coInvariantSch{ F1() ->  preIfWhileAlgebra, F2() ->  Element of F1(), F3() ->  Element of F1(), F4() ->  non empty set , F5() ->  Element of F4(), F6() ->  Subset of F4(), F7() ->  ExecutionFunction of F1(),F4(),F6(), P1[ set ] } :
 P1[F5()]
provided
A1: P1[F7() . (F5(),(while (F2(),F3())))] and
A2: F7() iteration_terminates_for F3() \; F2(),F7() . (F5(),F2()) and
A3: for s being Element of F4() st P1[F7() . ((F7() . (s,F2())),F3())] &amp; F7() . (s,F2()) in F6() holds
P1[F7() . (s,F2())] and
A4: for s being Element of F4() st P1[F7() . (s,F2())] holds
P1[s]
proofend;

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 &amp; I1 in (ElementaryInstructions A) |^ i &amp; I2 in (ElementaryInstructions A) |^ i )
proofend;

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 &amp; C in (ElementaryInstructions A) |^ i &amp; I1 in (ElementaryInstructions A) |^ i &amp; I2 in (ElementaryInstructions A) |^ i )
proofend;

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 &amp; C in (ElementaryInstructions A) |^ i &amp; I in (ElementaryInstructions A) |^ i )
proofend;

begin

scheme :: AOFA_000:sch 7
IndDef{ F1() ->  free ECIW-strict preIfWhileAlgebra, F2() ->  non empty set , F3() ->  Element of F2(), F4( set ) ->  set , F5( set , set ) ->  Element of F2(), F6( set , set ) ->  Element of F2(), F7( set , set , set ) ->  Element of F2() } :
 ex f being Function of the carrier of F1(),F2() st
( ( for I being Element of F1() st I in ElementaryInstructions F1() holds
f . I = F4(I) ) &amp; f . (EmptyIns F1()) = F3() &amp; ( for I1, I2 being Element of F1() holds f . (I1 \; I2) = F5((f . I1),(f . I2)) ) &amp; ( for C, I1, I2 being Element of F1() holds f . (if-then-else (C,I1,I2)) = F7((f . C),(f . I1),(f . I2)) ) &amp; ( for C, I being Element of F1() holds f . (while (C,I)) = F6((f . C),(f . I)) ) )
provided
A1: for I being Element of F1() st I in ElementaryInstructions F1() holds
F4(I) in F2()
proofend;

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 &amp; ( 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 ) )
proofend;

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 &amp; ( 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)) ) )
proofend;

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):] &amp; ( 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
proofend;

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 S1[ set ] means ( [:S,(ElementaryInstructions A):] c= $1 &amp; [:S,{(EmptyIns A)}:] c= $1 &amp; ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in $1 &amp; [(f . (s,I)),J] in $1 implies [s,(I \; J)] in $1 ) &amp; ( [s,C] in $1 &amp; [(f . (s,C)),I] in $1 &amp; f . (s,C) in T implies [s,(if-then-else (C,I,J))] in $1 ) &amp; ( [s,C] in $1 &amp; [(f . (s,C)),J] in $1 &amp; f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in $1 ) &amp; ( [s,C] in $1 &amp; ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; [(r . i),(I \; C)] in $1 &amp; 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 &amp; [:S,{(EmptyIns A)}:] c= it &amp; ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in it &amp; [(f . (s,I)),J] in it implies [s,(I \; J)] in it ) &amp; ( [s,C] in it &amp; [(f . (s,C)),I] in it &amp; f . (s,C) in T implies [s,(if-then-else (C,I,J))] in it ) &amp; ( [s,C] in it &amp; [(f . (s,C)),J] in it &amp; f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in it ) &amp; ( [s,C] in it &amp; ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; [(r . i),(I \; C)] in it &amp; r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in it ) ) ) &amp; ( for P being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= P &amp; [:S,{(EmptyIns A)}:] c= P &amp; ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in P &amp; [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) &amp; ( [s,C] in P &amp; [(f . (s,C)),I] in P &amp; f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) &amp; ( [s,C] in P &amp; [(f . (s,C)),J] in P &amp; f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) &amp; ( [s,C] in P &amp; ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; [(r . i),(I \; C)] in P &amp; r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds
it c= P ) );
existence
 ex b1 being Subset of [:S, the carrier of A:] st
( [:S,(ElementaryInstructions A):] c= b1 &amp; [:S,{(EmptyIns A)}:] c= b1 &amp; ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in b1 &amp; [(f . (s,I)),J] in b1 implies [s,(I \; J)] in b1 ) &amp; ( [s,C] in b1 &amp; [(f . (s,C)),I] in b1 &amp; f . (s,C) in T implies [s,(if-then-else (C,I,J))] in b1 ) &amp; ( [s,C] in b1 &amp; [(f . (s,C)),J] in b1 &amp; f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in b1 ) &amp; ( [s,C] in b1 &amp; ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; [(r . i),(I \; C)] in b1 &amp; r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in b1 ) ) ) &amp; ( for P being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= P &amp; [:S,{(EmptyIns A)}:] c= P &amp; ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in P &amp; [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) &amp; ( [s,C] in P &amp; [(f . (s,C)),I] in P &amp; f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) &amp; ( [s,C] in P &amp; [(f . (s,C)),J] in P &amp; f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) &amp; ( [s,C] in P &amp; ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; [(r . i),(I \; C)] in P &amp; r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds
b1 c= P ) )
proofend;
uniqueness
 for b1, b2 being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= b1 &amp; [:S,{(EmptyIns A)}:] c= b1 &amp; ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in b1 &amp; [(f . (s,I)),J] in b1 implies [s,(I \; J)] in b1 ) &amp; ( [s,C] in b1 &amp; [(f . (s,C)),I] in b1 &amp; f . (s,C) in T implies [s,(if-then-else (C,I,J))] in b1 ) &amp; ( [s,C] in b1 &amp; [(f . (s,C)),J] in b1 &amp; f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in b1 ) &amp; ( [s,C] in b1 &amp; ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; [(r . i),(I \; C)] in b1 &amp; r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in b1 ) ) ) &amp; ( for P being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= P &amp; [:S,{(EmptyIns A)}:] c= P &amp; ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in P &amp; [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) &amp; ( [s,C] in P &amp; [(f . (s,C)),I] in P &amp; f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) &amp; ( [s,C] in P &amp; [(f . (s,C)),J] in P &amp; f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) &amp; ( [s,C] in P &amp; ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; [(r . i),(I \; C)] in P &amp; r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds
b1 c= P ) &amp; [:S,(ElementaryInstructions A):] c= b2 &amp; [:S,{(EmptyIns A)}:] c= b2 &amp; ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in b2 &amp; [(f . (s,I)),J] in b2 implies [s,(I \; J)] in b2 ) &amp; ( [s,C] in b2 &amp; [(f . (s,C)),I] in b2 &amp; f . (s,C) in T implies [s,(if-then-else (C,I,J))] in b2 ) &amp; ( [s,C] in b2 &amp; [(f . (s,C)),J] in b2 &amp; f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in b2 ) &amp; ( [s,C] in b2 &amp; ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; [(r . i),(I \; C)] in b2 &amp; r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in b2 ) ) ) &amp; ( for P being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= P &amp; [:S,{(EmptyIns A)}:] c= P &amp; ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in P &amp; [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) &amp; ( [s,C] in P &amp; [(f . (s,C)),I] in P &amp; f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) &amp; ( [s,C] in P &amp; [(f . (s,C)),J] in P &amp; f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) &amp; ( [s,C] in P &amp; ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; [(r . i),(I \; C)] in P &amp; r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds
b2 c= P ) holds
b1 = b2
proofend;
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 b5 being Subset of [:S, the carrier of A:] holds
( b5 = TerminatingPrograms (A,S,T,f) iff ( [:S,(ElementaryInstructions A):] c= b5 &amp; [:S,{(EmptyIns A)}:] c= b5 &amp; ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in b5 &amp; [(f . (s,I)),J] in b5 implies [s,(I \; J)] in b5 ) &amp; ( [s,C] in b5 &amp; [(f . (s,C)),I] in b5 &amp; f . (s,C) in T implies [s,(if-then-else (C,I,J))] in b5 ) &amp; ( [s,C] in b5 &amp; [(f . (s,C)),J] in b5 &amp; f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in b5 ) &amp; ( [s,C] in b5 &amp; ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; [(r . i),(I \; C)] in b5 &amp; r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in b5 ) ) ) &amp; ( for P being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= P &amp; [:S,{(EmptyIns A)}:] c= P &amp; ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in P &amp; [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) &amp; ( [s,C] in P &amp; [(f . (s,C)),I] in P &amp; f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) &amp; ( [s,C] in P &amp; [(f . (s,C)),J] in P &amp; f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) &amp; ( [s,C] in P &amp; ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; [(r . i),(I \; C)] in P &amp; r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds
b5 c= P ) ) );

definition
let A be preIfWhileAlgebra;
let I be Element of A;
attrI 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);
end;

:: 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) );

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;
predI 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);
end;

:: 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) );

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 ;
predI 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);
predZ 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;
end;

:: 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) );

:: 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 );

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)
proofend;

theorem :: AOFA_000:95
for A being preIfWhileAlgebra
for I being Element of A st I in ElementaryInstructions A holds
I is absolutely-terminating
proofend;

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)
proofend;

registration
let A be preIfWhileAlgebra;
cluster EmptyIns A ->  absolutely-terminating ;
coherence
 EmptyIns A is absolutely-terminating
proofend;
end;

registration
let A be preIfWhileAlgebra;
cluster absolutely-terminating for Element of the carrier of A;
existence
 ex b1 being Element of A st b1 is absolutely-terminating
proofend;
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 &amp; [s,(I \; J)] in TerminatingPrograms (A,S,T,f) holds
( [s,I] in TerminatingPrograms (A,S,T,f) &amp; [(f . (s,I)),J] in TerminatingPrograms (A,S,T,f) )
proofend;

registration
let A be preIfWhileAlgebra;
let I, J be absolutely-terminating Element of A;
clusterI \; J ->  absolutely-terminating ;
coherence
 I \; J is absolutely-terminating
proofend;
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 &amp; [s,(if-then-else (C,I,J))] in TerminatingPrograms (A,S,T,f) holds
( [s,C] in TerminatingPrograms (A,S,T,f) &amp; ( f . (s,C) in T implies [(f . (s,C)),I] in TerminatingPrograms (A,S,T,f) ) &amp; ( f . (s,C) nin T implies [(f . (s,C)),J] in TerminatingPrograms (A,S,T,f) ) )
proofend;

registration
let A be preIfWhileAlgebra;
let C, I, J be absolutely-terminating Element of A;
cluster if-then-else (C,I,J) ->  absolutely-terminating ;
coherence
 if-then-else (C,I,J) is absolutely-terminating
proofend;
end;

registration
let A be preIfWhileAlgebra;
let C, I be absolutely-terminating Element of A;
cluster if-then (C,I) ->  absolutely-terminating ;
coherence
 if-then (C,I) is absolutely-terminating ;
end;

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 &amp; [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) holds
( [s,C] in TerminatingPrograms (A,S,T,f) &amp; ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) &amp; r . (len r) nin T &amp; ( for i being Nat st 1 <= i &amp; i < len r holds
( r . i in T &amp; [(r . i),(I \; C)] in TerminatingPrograms (A,S,T,f) &amp; r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) )
proofend;

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 &amp; [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) &amp; f . (s,C) in T holds
[(f . (s,C)),I] in TerminatingPrograms (A,S,T,f)
proofend;

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)
proofend;

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) &amp; f1 . (s,I) = f2 . (s,I) )
proofend;

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)
proofend;

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;

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
proofend;

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 )
proofend;

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
proofend;

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;

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
proofend;

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 &amp; P is_invariant_wrt J,f holds
P is_invariant_wrt I \; J,f
proofend;

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 &amp; J is_terminating_wrt f holds
I \; J is_terminating_wrt f
proofend;

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 &amp; J is_terminating_wrt f,P &amp; P is_invariant_wrt I,f holds
I \; J is_terminating_wrt f,P
proofend;

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 &amp; I is_terminating_wrt f &amp; J is_terminating_wrt f holds
if-then-else (C,I,J) is_terminating_wrt f
proofend;

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 &amp; I is_terminating_wrt f,P &amp; J is_terminating_wrt f,P &amp; P is_invariant_wrt C,f holds
if-then-else (C,I,J) is_terminating_wrt f,P
proofend;

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 &amp; I is_terminating_wrt f &amp; f iteration_terminates_for I \; C,f . (s,C) holds
[s,(while (C,I))] in TerminatingPrograms (A,S,T,f)
proofend;

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 &amp; I is_terminating_wrt f,P &amp; P is_invariant_wrt C,f &amp; P is_invariant_wrt I,f &amp; f iteration_terminates_for I \; C,f . (s,C) &amp; s in P holds
[s,(while (C,I))] in TerminatingPrograms (A,S,T,f)
proofend;

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 &amp; I is_terminating_wrt f,P &amp; P is_invariant_wrt C,f &amp; ( for s being Element of S st s in P &amp; f . ((f . (s,I)),C) in T holds
f . (s,I) in P ) &amp; f iteration_terminates_for I \; C,f . (s,C) &amp; s in P holds
[s,(while (C,I))] in TerminatingPrograms (A,S,T,f)
proofend;

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 &amp; I is_terminating_wrt f &amp; ( for s being Element of S holds f iteration_terminates_for I \; C,s ) holds
while (C,I) is_terminating_wrt f
proofend;

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 &amp; I is_terminating_wrt f,P &amp; P is_invariant_wrt C,f &amp; ( for s being Element of S st s in P &amp; f . ((f . (s,I)),C) in T holds
f . (s,I) in P ) &amp; ( 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
proofend;