begin
definition
let f be
homogeneous Function;
attr f is
associative means :
Def2:
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*>)*>;
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*>)*> );
definition
let f be
Function;
assume B1:
rng f c= dom f
;
let A,
x be
set ;
defpred S1[
Nat]
means for
a being
set st
a in dom f holds
a in dom (iter (f,$1));
A1:
field f = dom f
by B1, XBOOLE_1:12;
then
iter (
f,
0)
= id (dom f)
by FUNCT_7:68;
then A2:
S1[
0 ]
by FUNCT_1:17;
A3:
now for i being Element of NAT st S1[i] holds
S1[i + 1]
let i be
Element of
NAT ;
( S1[i] implies S1[i + 1] )assume A4:
S1[
i]
;
S1[i + 1]thus
S1[
i + 1]
verum
proof
let a be
set ;
( a in dom f implies a in dom (iter (f,(i + 1))) )
assume
a in dom f
;
a in dom (iter (f,(i + 1)))
then A5:
a in dom (iter (f,i))
by A4;
then A6:
(iter (f,i)) . a in rng (iter (f,i))
by FUNCT_1:def 3;
A7:
rng (iter (f,i)) c= dom f
by A1, FUNCT_7:72;
iter (
f,
(i + 1))
= f * (iter (f,i))
by FUNCT_7:71;
hence
a in dom (iter (f,(i + 1)))
by A5, A6, A7, FUNCT_1:11;
verum
end;
end;
A8:
for
i being
Element of
NAT holds
S1[
i]
from NAT_1:sch 1(A2, A3);
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 ) ) ) )
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
end;
definition
let f be
Function;
assume B1:
rng f c= dom f
;
let A be
set ;
let g be
Function;
defpred S1[
Nat]
means for
a being
set st
a in dom f holds
a in dom (iter (f,$1));
A1:
field f = dom f
by B1, XBOOLE_1:12;
then
iter (
f,
0)
= id (dom f)
by FUNCT_7:68;
then A2:
S1[
0 ]
by FUNCT_1:17;
A3:
now for i being Element of NAT st S1[i] holds
S1[i + 1]
let i be
Element of
NAT ;
( S1[i] implies S1[i + 1] )assume A4:
S1[
i]
;
S1[i + 1]thus
S1[
i + 1]
verum
proof
let a be
set ;
( a in dom f implies a in dom (iter (f,(i + 1))) )
assume
a in dom f
;
a in dom (iter (f,(i + 1)))
then A5:
a in dom (iter (f,i))
by A4;
then A6:
(iter (f,i)) . a in rng (iter (f,i))
by FUNCT_1:def 3;
A7:
rng (iter (f,i)) c= dom f
by A1, FUNCT_7:72;
iter (
f,
(i + 1))
= f * (iter (f,i))
by FUNCT_7:71;
hence
a in dom (iter (f,(i + 1)))
by A5, A6, A7, FUNCT_1:11;
verum
end;
end;
A8:
for
i being
Element of
NAT holds
S1[
i]
from NAT_1:sch 1(A2, A3);
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 ) ) ) )
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
end;
begin
definition
let A be
non-empty UAStr ;
let B be
Subset of
A;
let n be
Nat;
existence
ex b1 being Subset of A ex F being Function of NAT,(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 ) } ) )
uniqueness
for b1, b2 being Subset of A st ex F being Function of NAT,(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 Function of NAT,(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
end;
scheme
MaxVal{
F1()
-> non
empty set ,
F2()
-> set ,
P1[
set ,
set ] } :
ex
n being
Nat st
for
x being
Element of
F1() st
x in F2() holds
P1[
x,
n]
provided
A1:
F2() is
finite
and A2:
for
x being
Element of
F1() st
x in F2() holds
ex
n being
Nat st
P1[
x,
n]
and A3:
for
x being
Element of
F1()
for
n,
m being
Nat st
P1[
x,
n] &
n <= m holds
P1[
x,
m]
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
begin
definition
let A be
preIfWhileAlgebra;
attr A is
degenerated means :
Def24:
( 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) );
end;
::
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) ) );
theorem
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 )
theorem Th74:
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 ) ) )
begin
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 :
Def30:
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 :
Def31:
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 Def30 defines
complies_with_if_wrt AOFA_000:def 30 :
for A being preIfWhileAlgebra
for S being non empty set
for T being Subset of S
for f being Function of [:S, the carrier of A:],S holds
( f complies_with_if_wrt T iff for s being Element of S
for C, I1, I2 being Element of A holds
( ( f . (s,C) in T implies f . (s,(if-then-else (C,I1,I2))) = f . ((f . (s,C)),I1) ) & ( f . (s,C) nin T implies f . (s,(if-then-else (C,I1,I2))) = f . ((f . (s,C)),I2) ) ) );
::
deftheorem Def31 defines
complies_with_while_wrt AOFA_000:def 31 :
for A being preIfWhileAlgebra
for S being non empty set
for T being Subset of S
for f being Function of [:S, the carrier of A:],S holds
( f complies_with_while_wrt T iff for s being Element of S
for C, I being Element of A holds
( ( f . (s,C) in T implies f . (s,(while (C,I))) = f . ((f . ((f . (s,C)),I)),(while (C,I))) ) & ( f . (s,C) nin T implies f . (s,(while (C,I))) = f . (s,C) ) ) );
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;
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 ) );
end;
theorem
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)) )
scheme
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 ] } :
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) )
scheme
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 ] } :
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) )
scheme
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() ) )
scheme
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 ] } :
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]
begin
scheme
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
theorem
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 ) )
theorem
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)) ) )
theorem
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
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:
(
[: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 ) )
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
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 ) ) );
theorem Th97:
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) )
theorem Th98:
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) ) )
theorem Th99:
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)) ) ) ) )
theorem
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)
theorem
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)
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) )
theorem
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)
theorem
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
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
theorem Th114:
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)
theorem
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)
theorem Th116:
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)
theorem
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