AOFA_000: Mizar Analysis of Algorithms: Preliminaries

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

proof end;

end;

registration

let p, q be non-empty FinSequence;

cluster p ^ q -> 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 :

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 :

:: deftheorem Def3 defines unital AOFA_000:def 3 :

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

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;

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

proof end;

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

proof end;

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

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

end;

:: deftheorem defines +* AOFA_000:def 4 :

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

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

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

end;

:: deftheorem defines orbit AOFA_000:def 5 :

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 S₁[ 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: S₁[ 0 ] ;

A4: now :: thesis:

let i be Nat; :: thesis:
assume A5: S₁[i] ; :: thesis:
thus S₁[i + 1] :: thesis:

let a be set ; :: thesis:
assume a in dom f ; :: thesis:
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:

end;

end;

A9: for i being Nat holds S₁[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 ) ) ) );

proof end;

proof end;

end;

:: deftheorem defines iter AOFA_000:def 6 :

definition

let f be Function;
assume A1: rng f c= dom f ;
let A be set ;
let g be Function;
defpred S₁[ 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: S₁[ 0 ] ;

A4: now :: thesis:

let i be Nat; :: thesis:
assume A5: S₁[i] ; :: thesis:
thus S₁[i + 1] :: thesis:

let a be set ; :: thesis:
assume a in dom f ; :: thesis:
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:

end;

end;

A9: for i being Nat holds S₁[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 ) ) ) );

proof end;

proof end;

end;

:: deftheorem Def7 defines iter AOFA_000:def 7 :

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

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

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

cluster -> DTree-yielding for FinSequence of the carrier of (FreeUnivAlgNSG (f,D));

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

proof end;

proof end;

end;

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

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{ F₁() -> non empty set , F₂() -> set , P₁[ object , object ] } :

ex n being Nat st
for x being Element of F₁() st x in F₂() holds
P₁[x,n]

provided

A1: F₂() is finite and
A2: for x being Element of F₁() st x in F₂() holds
ex n being Nat st P₁[x,n] and
A3: for x being Element of F₁()
for n, m being Nat st P₁[x,n] & n <= m holds
P₁[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 } );

end;

:: deftheorem defines Generators AOFA_000:def 9 :

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;

proof end;

end;

definition

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

proof end;

end;

registration

let A, B be set ;

cluster [:A,B:] -> 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 :

:: deftheorem Def11 defines with_catenation AOFA_000:def 11 :

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

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

:: deftheorem Def14 defines associative AOFA_000:def 14 :

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 :

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 ;

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)) . {};

proof end;

end;

:: deftheorem defines EmptyIns AOFA_000:def 16 :

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

proof end;

end;

:: deftheorem defines \; AOFA_000:def 17 :

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

proof end;

end;

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

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

end;

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

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

proof end;

end;

:: deftheorem defines while AOFA_000:def 20 :

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

end;

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

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

end;

:: deftheorem defines ElementaryInstructions AOFA_000:def 22 :

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 :

:: deftheorem Def24 defines degenerated AOFA_000:def 24 :

:: deftheorem Def25 defines well_founded AOFA_000:def 25 :

definition

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

end;

:: deftheorem defines ECIW-signature AOFA_000:def 26 :

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 :

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 ;

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 ;

proof end;

end;

registration

let X be infinite disjoint_with_NAT set ;

cluster FreeUnivAlgNSG (ECIW-signature,X) -> infinite ;

proof end;

end;

registration

let X be non empty disjoint_with_NAT set ;

cluster FreeUnivAlgNSG (ECIW-signature,X) -> ECIW-strict ;

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

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 ;

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 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{ F₁() -> well_founded ECIW-strict preIfWhileAlgebra, F₂() -> Element of F₁(), P₁[ set ] } :

P₁[F₂()]

provided

A1: for I being Element of F₁() st I in ElementaryInstructions F₁() holds
P₁[I] and
A2: P₁[ EmptyIns F₁()] and
A3: for I1, I2 being Element of F₁() st P₁[I1] & P₁[I2] holds
P₁[I1 \; I2] and
A4: for C, I1, I2 being Element of F₁() st P₁[C] & P₁[I1] & P₁[I2] holds
P₁[ if-then-else (C,I1,I2)] and
A5: for C, I being Element of F₁() st P₁[C] & P₁[I] holds
P₁[ 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 :

:: deftheorem Def29 defines complying_with_catenation AOFA_000:def 29 :

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 :

:: deftheorem defines complies_with_while_wrt AOFA_000:def 31 :

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

proof end;

end;

:: deftheorem Def32 defines ExecutionFunction AOFA_000:def 32 :

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

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 ;

proof end;

end;

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

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{ F₁() -> preIfWhileAlgebra, F₂() -> Element of F₁(), F₃() -> non empty set , F₄() -> Element of F₃(), F₅() -> Subset of F₃(), F₆() -> ExecutionFunction of F₁(),F₃(),F₅(), F₇( set ) -> Nat, P₁[ set ] } :

F₆() iteration_terminates_for F₂(),F₄()

provided

A1: ( F₄() in F₅() iff P₁[F₄()] ) and
A2: for s being Element of F₃() st P₁[s] holds
( ( P₁[F₆() . (s,F₂())] implies F₆() . (s,F₂()) in F₅() ) & ( F₆() . (s,F₂()) in F₅() implies P₁[F₆() . (s,F₂())] ) & F₇((F₆() . (s,F₂()))) < F₇(s) )

proof end;

scheme :: AOFA_000:sch 4
Termination2{ F₁() -> preIfWhileAlgebra, F₂() -> Element of F₁(), F₃() -> non empty set , F₄() -> Element of F₃(), F₅() -> Subset of F₃(), F₆() -> ExecutionFunction of F₁(),F₃(),F₅(), F₇( set ) -> Nat, P₁[ set ], P₂[ set ] } :

F₆() iteration_terminates_for F₂(),F₄()

provided

A1: P₁[F₄()] and
A2: ( F₄() in F₅() iff P₂[F₄()] ) and
A3: for s being Element of F₃() st P₁[s] & s in F₅() & P₂[s] holds
( P₁[F₆() . (s,F₂())] & ( P₂[F₆() . (s,F₂())] implies F₆() . (s,F₂()) in F₅() ) & ( F₆() . (s,F₂()) in F₅() implies P₂[F₆() . (s,F₂())] ) & F₇((F₆() . (s,F₂()))) < F₇(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{ F₁() -> preIfWhileAlgebra, F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄() -> non empty set , F₅() -> Element of F₄(), F₆() -> Subset of F₄(), F₇() -> ExecutionFunction of F₁(),F₄(),F₆(), P₁[ set ], P₂[ set ] } :

( P₁[F₇() . (F₅(),(while (F₂(),F₃())))] & P₂[F₇() . (F₅(),(while (F₂(),F₃())))] )

provided

A1: P₁[F₅()] and
A2: F₇() iteration_terminates_for F₃() \; F₂(),F₇() . (F₅(),F₂()) and
A3: for s being Element of F₄() st P₁[s] & s in F₆() & P₂[s] holds
P₁[F₇() . (s,F₃())] and
A4: for s being Element of F₄() st P₁[s] holds
( P₁[F₇() . (s,F₂())] & ( F₇() . (s,F₂()) in F₆() implies P₂[F₇() . (s,F₂())] ) & ( P₂[F₇() . (s,F₂())] implies F₇() . (s,F₂()) in F₆() ) )

proof end;

scheme :: AOFA_000:sch 6
coInvariantSch{ F₁() -> preIfWhileAlgebra, F₂() -> Element of F₁(), F₃() -> Element of F₁(), F₄() -> non empty set , F₅() -> Element of F₄(), F₆() -> Subset of F₄(), F₇() -> ExecutionFunction of F₁(),F₄(),F₆(), P₁[ set ] } :

P₁[F₅()]

provided

A1: P₁[F₇() . (F₅(),(while (F₂(),F₃())))] and
A2: F₇() iteration_terminates_for F₃() \; F₂(),F₇() . (F₅(),F₂()) and
A3: for s being Element of F₄() st P₁[F₇() . ((F₇() . (s,F₂())),F₃())] & F₇() . (s,F₂()) in F₆() holds
P₁[F₇() . (s,F₂())] and
A4: for s being Element of F₄() st P₁[F₇() . (s,F₂())] holds
P₁[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{ F₁() -> free ECIW-strict preIfWhileAlgebra, F₂() -> non empty set , F₃() -> Element of F₂(), F₄( set ) -> set , F₅( set , set ) -> Element of F₂(), F₆( set , set ) -> Element of F₂(), F₇( set , set , set ) -> Element of F₂() } :

ex f being Function of the carrier of F₁(),F₂() st
( ( for I being Element of F₁() st I in ElementaryInstructions F₁() holds
f . I = F₄(I) ) & f . (EmptyIns F₁()) = F₃() & ( for I1, I2 being Element of F₁() holds f . (I1 \; I2) = F₅((f . I1),(f . I2)) ) & ( for C, I1, I2 being Element of F₁() holds f . (if-then-else (C,I1,I2)) = F₇((f . C),(f . I1),(f . I2)) ) & ( for C, I being Element of F₁() holds f . (while (C,I)) = F₆((f . C),(f . I)) ) )

provided

A1: for I being Element of F₁() st I in ElementaryInstructions F₁() holds
F₄(I) in F₂()

proof end;

theorem :: AOFA_000:91

for S being non empty set
for T being Subset of S
for A being free ECIW-strict preIfWhileAlgebra
for g being Function of [:S,(ElementaryInstructions A):],S
for s0 being Element of S ex f being ExecutionFunction of A,S,T st
( f | [:S,(ElementaryInstructions A):] = g & ( for s being Element of S
for C, I being Element of A st not f iteration_terminates_for I \; C,f . (s,C) holds
f . (s,(while (C,I))) = s0 ) )

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 S₁[ 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 ) );

proof end;

proof end;

end;

:: deftheorem Def35 defines TerminatingPrograms AOFA_000:def 35 :

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 :

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 :

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 :

:: deftheorem defines is_invariant_wrt AOFA_000:def 39 :

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

end;

registration

let A be preIfWhileAlgebra;

cluster absolutely-terminating for Element of the carrier of A;

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 ;

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 ;

proof end;

end;

registration

let A be preIfWhileAlgebra;
let C, I be absolutely-terminating Element of A;

cluster if-then (C,I) -> 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;