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


notation
let x be object ;
let 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
proof end;

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

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

definition
let f be homogeneous Function;
let x be set ;
pred x is_a_unity_wrt f means :: 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 & f . <*x,y*> = y & <*y,x*> in dom f & f . <*y,x*> = y );
end;

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

definition
let f be homogeneous Function;
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*>)*>;
attr f 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 & <*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 );

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
proof end;
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 & b1 is quasi_total & b1 is homogeneous )
proof end;
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
proof end;

Lm1: 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

by Th2;

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 Relation-like X * -defined X -valued non empty 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 & b1 is associative & b1 is unital )
proof end;
cluster Relation-like X * -defined X -valued non empty 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
proof end;
cluster Relation-like X * -defined X -valued non empty 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
proof end;
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
proof end;

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 & X c= dom f holds
((f,X) +* g) . x = f . x
proof end;

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

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

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

:: deftheorem defines orbit AOFA_000:def 5 :
for f being Function
for x being object 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
proof end;

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

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

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

definition
let f be Function;
assume A1: 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));
A2: field f = dom f by A1, XBOOLE_1:12;
then iter (f,0) = id (dom f) by FUNCT_7:68;
then A3: S1[ 0 ] ;
A4: now :: thesis: for i being Nat st S1[i] holds
S1[i + 1]
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A5: 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 A6: a in dom (iter (f,i)) by A5;
then A7: (iter (f,i)) . a in rng (iter (f,i)) by FUNCT_1:def 3;
A8: rng (iter (f,i)) c= dom f by A2, FUNCT_7:72;
iter (f,(i + 1)) = f * (iter (f,i)) by FUNCT_7:71;
hence a in dom (iter (f,(i + 1))) by A6, A7, A8, FUNCT_1:11; :: thesis: verum
end;
end;
A9: for i being Nat holds S1[i] from NAT_1:sch 2(A3, A4);
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
ex b1 being Function st
( dom b1 = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies b1 . 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
b1 . a = (iter (f,n)) . a ) ) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies b1 . 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
b1 . a = (iter (f,n)) . a ) ) ) & dom b2 = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies b2 . 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
b2 . a = (iter (f,n)) . a ) ) ) holds
b1 = b2
proof end;
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 & ( for a being set st a in dom f holds
( ( f orbit a c= A implies b4 . 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
b4 . a = (iter (f,n)) . a ) ) ) ) );

definition
let f be Function;
assume A1: 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));
A2: field f = dom f by A1, XBOOLE_1:12;
then iter (f,0) = id (dom f) by FUNCT_7:68;
then A3: S1[ 0 ] ;
A4: now :: thesis: for i being Nat st S1[i] holds
S1[i + 1]
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A5: 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 A6: a in dom (iter (f,i)) by A5;
then A7: (iter (f,i)) . a in rng (iter (f,i)) by FUNCT_1:def 3;
A8: rng (iter (f,i)) c= dom f by A2, FUNCT_7:72;
iter (f,(i + 1)) = f * (iter (f,i)) by FUNCT_7:71;
hence a in dom (iter (f,(i + 1))) by A6, A7, A8, FUNCT_1:11; :: thesis: verum
end;
end;
A9: for i being Nat holds S1[i] from NAT_1:sch 2(A3, A4);
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
ex b1 being Function st
( dom b1 = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies b1 . 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
b1 . a = (iter (f,n)) . a ) ) ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies b1 . 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
b1 . a = (iter (f,n)) . a ) ) ) & dom b2 = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies b2 . 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
b2 . a = (iter (f,n)) . a ) ) ) holds
b1 = b2
proof end;
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 & ( for a being set st a in dom f holds
( ( f orbit a c= A implies b4 . 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
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 & 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)
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
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)
proof end;
end;

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

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 & 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 & 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
proof end;

definition
let A be non-empty UAStr ;
let B be Subset of A;
let n be natural Number ;
func B |^ n -> Subset of A means :Def8: :: AOFA_000:def 8
ex F being sequence of (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 b1 being Subset of A ex F being sequence of (bool the carrier of A) st
( b1 = 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 ) } ) )
proof end;
uniqueness
for b1, b2 being Subset of A st ex F being sequence of (bool the carrier of A) st
( b1 = 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 sequence of (bool the carrier of A) st
( b2 = 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
b1 = b2
proof end;
end;

:: deftheorem Def8 defines |^ AOFA_000:def 8 :
for A being non-empty UAStr
for B being Subset of A
for n being natural Number
for b4 being Subset of A holds
( b4 = B |^ n iff ex F being sequence of (bool the carrier of A) st
( b4 = 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 ) } ) ) );

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

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 ) }
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 ) ) )
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
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
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 ) ) )
proof end;

scheme :: AOFA_000:sch 1
MaxVal{ F1() -> non empty set , F2() -> set , P1[ object , object ] } :
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] & n <= m holds
P1[x,m]
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 )
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
proof end;

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

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

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

theorem :: AOFA_000:29
for A being Universal_Algebra st Constants A = {} holds
for G being GeneratorSet of A holds G <> {}
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 )
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
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
proof end;

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

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

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

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

registration
let A, B be set ;
cluster [:A,B:] -> disjoint_with_NAT ;
coherence
[:A,B:] is disjoint_with_NAT
proof end;
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 & h2 is_homomorphism & 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 )
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 )
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
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
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
proof end;

definition
let S be non empty UAStr ;
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 );
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 );
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 );
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 );
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;
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 & 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 ) );

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

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

:: 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 ;
attr S 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 & (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 & (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 )
proof end;

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 & b1 is with_catenation & b1 is with_if-instruction & b1 is with_while-instruction & b1 is unital & b1 is associative )
proof end;
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)) = {{}}
proof end;

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
proof end;
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 & 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;
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*> is Algorithm of A
proof end;
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 & 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)
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;
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
proof end;
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
proof end;

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
proof end;
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 & 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 ) } 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 & I2 <> I1 \; I2 ) } ;

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

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

definition
let A be preIfWhileAlgebra;
attr A is infinite means :Def23: :: AOFA_000:def 23
ElementaryInstructions A is infinite ;
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) );
attr A 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 & 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 );

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 & dom ECIW-signature = Seg 4 & ECIW-signature . 1 = 0 & ECIW-signature . 2 = 2 & ECIW-signature . 3 = 3 & ECIW-signature . 4 = 2 )
proof end;

definition
let A be non empty partial non-empty UAStr ;
attr A 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 )
proof end;

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 & 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;
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 ) )
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 = {}
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)
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*>
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 )
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 )
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*>
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*>
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 )
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)
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*>
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 {}
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 = {}
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)) )
proof end;

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

registration
let X be infinite disjoint_with_NAT set ;
cluster FreeUnivAlgNSG (ECIW-signature,X) -> infinite ;
coherence
FreeUnivAlgNSG (ECIW-signature,X) is infinite
proof end;
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
by FREEALG:4;
end;

theorem Th71: :: AOFA_000:71
for A being preIfWhileAlgebra holds Generators A c= ElementaryInstructions A
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) )
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) )
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 ) ) )
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 ) ) )
proof end;

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 & not b1 is degenerated )
proof end;
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 & not b1 is degenerated & b1 is well_founded & b1 is ECIW-strict & b1 is free & b1 is strict )
proof end;
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) & ( 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 ) )
proof end;

theorem :: AOFA_000:78
for A being Universal_Algebra
for B being Subset of A holds Constants A c= B |^ 1
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 ) by Th30;

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] & P1[I2] holds
P1[I1 \; I2] and
A4: for C, I1, I2 being Element of F1() st P1[C] & P1[I1] & P1[I2] holds
P1[ if-then-else (C,I1,I2)] and
A5: for C, I being Element of F1() st P1[C] & P1[I] holds
P1[ while (C,I)]
proof end;

definition
let A be preIfWhileAlgebra;
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;
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);
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;
pred f complies_with_if_wrt T means :: 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) ) );
pred f complies_with_while_wrt T means :: 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))) ) & ( f . (s,C) nin T implies f . (s,(while (C,I))) = f . (s,C) ) );
end;

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

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

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

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 & it is complying_with_catenation & it complies_with_if_wrt T & 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 & b1 is complying_with_catenation & b1 complies_with_if_wrt T & b1 complies_with_while_wrt T )
proof end;
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 & b4 is complying_with_catenation & b4 complies_with_if_wrt T & 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 & 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;
:: iteration of I started in s terminates wrt f
pred f iteration_terminates_for I,s means :: AOFA_000:def 33
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) ) ) );
end;

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

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 & 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
consistency
for b1 being R_eal holds verum
;
existence
( ( for b1 being R_eal holds verum ) & ( 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 & 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 b1 being R_eal st b1 = +infty ) )
;
uniqueness
for b1, b2 being R_eal holds
( ( f iteration_terminates_for I,s & ex r being non empty FinSequence of S st
( b1 = (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
( b2 = (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 b1 = b2 ) & ( not f iteration_terminates_for I,s & b1 = +infty & b2 = +infty implies b1 = b2 ) )
;
proof end;
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 & 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 ( 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 )
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 )
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)) )
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
proof end;

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() ) & ( F6() . (s,F2()) in F5() implies P1[F6() . (s,F2())] ) & F7((F6() . (s,F2()))) < F7(s) )
proof end;

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] & s in F5() & P2[s] holds
( P1[F6() . (s,F2())] & ( P2[F6() . (s,F2())] implies F6() . (s,F2()) in F5() ) & ( F6() . (s,F2()) in F5() implies P2[F6() . (s,F2())] ) & F7((F6() . (s,F2()))) < F7(s) )
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)
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 )
proof end;

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())))] & 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] & s in F6() & P2[s] holds
P1[F7() . (s,F3())] and
A4: for s being Element of F4() st P1[s] holds
( P1[F7() . (s,F2())] & ( F7() . (s,F2()) in F6() implies P2[F7() . (s,F2())] ) & ( P2[F7() . (s,F2())] implies F7() . (s,F2()) in F6() ) )
proof end;

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())] & 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]
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 )
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 )
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 )
proof end;

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) ) & f . (EmptyIns F1()) = F3() & ( for I1, I2 being Element of F1() holds f . (I1 \; I2) = F5((f . I1),(f . I2)) ) & ( for C, I1, I2 being Element of F1() holds f . (if-then-else (C,I1,I2)) = F7((f . C),(f . I1),(f . I2)) ) & ( 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()
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 ) )
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)) ) )
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
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 S1[ 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 ) ) ) );
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
ex b1 being Subset of [:S, the carrier of A:] st
( [:S,(ElementaryInstructions A):] c= b1 & [:S,{(EmptyIns A)}:] c= b1 & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in b1 & [(f . (s,I)),J] in b1 implies [s,(I \; J)] in b1 ) & ( [s,C] in b1 & [(f . (s,C)),I] in b1 & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in b1 ) & ( [s,C] in b1 & [(f . (s,C)),J] in b1 & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in b1 ) & ( [s,C] in b1 & 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 b1 & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in b1 ) ) ) & ( 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
b1 c= P ) )
proof end;
uniqueness
for b1, b2 being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= b1 & [:S,{(EmptyIns A)}:] c= b1 & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in b1 & [(f . (s,I)),J] in b1 implies [s,(I \; J)] in b1 ) & ( [s,C] in b1 & [(f . (s,C)),I] in b1 & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in b1 ) & ( [s,C] in b1 & [(f . (s,C)),J] in b1 & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in b1 ) & ( [s,C] in b1 & 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 b1 & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in b1 ) ) ) & ( 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
b1 c= P ) & [:S,(ElementaryInstructions A):] c= b2 & [:S,{(EmptyIns A)}:] c= b2 & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in b2 & [(f . (s,I)),J] in b2 implies [s,(I \; J)] in b2 ) & ( [s,C] in b2 & [(f . (s,C)),I] in b2 & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in b2 ) & ( [s,C] in b2 & [(f . (s,C)),J] in b2 & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in b2 ) & ( [s,C] in b2 & 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 b2 & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in b2 ) ) ) & ( 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
b2 c= P ) holds
b1 = b2
proof end;
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 & [:S,{(EmptyIns A)}:] c= b5 & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in b5 & [(f . (s,I)),J] in b5 implies [s,(I \; J)] in b5 ) & ( [s,C] in b5 & [(f . (s,C)),I] in b5 & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in b5 ) & ( [s,C] in b5 & [(f . (s,C)),J] in b5 & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in b5 ) & ( [s,C] in b5 & 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 b5 & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in b5 ) ) ) & ( 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
b5 c= P ) ) );

definition
let A be preIfWhileAlgebra;
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);
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;
pred I is_terminating_wrt f means :: AOFA_000:def 37
for s being Element of S holds [s,I] in TerminatingPrograms (A,S,T,f);
end;

:: deftheorem 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 ;
pred I is_terminating_wrt f,Z means :: AOFA_000:def 38
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 :: AOFA_000:def 39
for s being Element of S st s in Z holds
f . (s,I) in Z;
end;

:: deftheorem 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 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)
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 by Th94;

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

registration
let A be preIfWhileAlgebra;
cluster EmptyIns A -> absolutely-terminating ;
coherence
EmptyIns A is absolutely-terminating
by Th96;
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
proof end;
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) )
proof end;

registration
let A be preIfWhileAlgebra;
let I, J be absolutely-terminating Element of A;
cluster I \; J -> absolutely-terminating ;
coherence
I \; J is absolutely-terminating
proof end;
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) ) )
proof end;

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
proof end;
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 & [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)
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)
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)
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;

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

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

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 ;

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 ;

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