:: Mizar Analysis of Algorithms: Preliminaries
:: by Grzegorz Bancerek
::
:: Received July 9, 2007
:: Copyright (c) 2007 Association of Mizar Users
theorem Th1: :: AOFA_000:1
:: deftheorem Def1 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 :
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 :
theorem Th2: :: AOFA_000:2
theorem Th3: :: AOFA_000:3
:: deftheorem defines +* AOFA_000:def 4 :
theorem Th4: :: AOFA_000:4
theorem Th5: :: AOFA_000:5
:: deftheorem defines orbit AOFA_000:def 5 :
theorem Th6: :: AOFA_000:6
theorem :: AOFA_000:7
theorem :: AOFA_000:8
theorem Th9: :: AOFA_000:9
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:
(dom f) \/ (rng f) = dom f
by A1, XBOOLE_1:12;
then
iter f,
0 = id (dom f)
by FUNCT_7:70;
then A3:
S1[
0 ]
by FUNCT_1:34;
A4:
now
let i be
Element of
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) &
rng (iter f,i) c= dom f )
by A2, FUNCT_1:def 5, FUNCT_7:74;
iter f,
(i + 1) = f * (iter f,i)
by FUNCT_7:73;
hence
a in dom (iter f,(i + 1))
by A6, A7, FUNCT_1:21;
:: thesis: verum
end;
end;
A8:
for
i being
Element of
NAT holds
S1[
i]
from NAT_1:sch 1(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 ) ) ) )
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;
:: 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 S1[
Nat]
means for
a being
set st
a in dom f holds
a in dom (iter f,$1);
A2:
(dom f) \/ (rng f) = dom f
by A1, XBOOLE_1:12;
then
iter f,
0 = id (dom f)
by FUNCT_7:70;
then A3:
S1[
0 ]
by FUNCT_1:34;
A4:
now
let i be
Element of
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) &
rng (iter f,i) c= dom f )
by A2, FUNCT_1:def 5, FUNCT_7:74;
iter f,
(i + 1) = f * (iter f,i)
by FUNCT_7:73;
hence
a in dom (iter f,(i + 1))
by A6, A7, FUNCT_1:21;
:: thesis: verum
end;
end;
A8:
for
i being
Element of
NAT holds
S1[
i]
from NAT_1:sch 1(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 ) ) ) )
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;
:: deftheorem Def7 defines iter AOFA_000:def 7 :
theorem Th10: :: AOFA_000:10
theorem Th11: :: AOFA_000:11
theorem Th12: :: AOFA_000:12
theorem Th13: :: AOFA_000:13
theorem Th14: :: AOFA_000:14
theorem :: AOFA_000:15
theorem Th16: :: AOFA_000:16
theorem Th17: :: AOFA_000:17
definition
let A be
non-empty UAStr ;
let B be
Subset of
A;
let n be
Nat;
func B |^ n -> Subset of
A means :
Def8:
:: AOFA_000:def 8
ex
F being
Function of
NAT ,
bool the
carrier of
A st
(
it = F . n &
F . 0 = B & ( for
n being
Nat holds
F . (n + 1) = (F . n) \/ { ((Den o,A) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den o,A) & rng p c= F . n ) } ) );
existence
ex 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;
:: deftheorem Def8 defines |^ AOFA_000:def 8 :
theorem Th18: :: AOFA_000:18
theorem Th19: :: AOFA_000:19
theorem Th20: :: AOFA_000:20
theorem Th21: :: AOFA_000:21
theorem Th22: :: AOFA_000:22
theorem Th23: :: AOFA_000:23
theorem Th24: :: AOFA_000:24
theorem Th25: :: AOFA_000:25
:: deftheorem defines Generators AOFA_000:def 9 :
theorem Th26: :: AOFA_000:26
theorem :: AOFA_000:27
theorem Th28: :: AOFA_000:28
theorem :: AOFA_000:29
theorem Th30: :: AOFA_000:30
theorem Th31: :: AOFA_000:31
theorem Th32: :: AOFA_000:32
theorem :: AOFA_000:33
theorem Th34: :: AOFA_000:34
theorem :: AOFA_000:35
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
theorem Th36: :: AOFA_000:36
theorem :: AOFA_000:37
theorem Th38: :: AOFA_000:38
theorem Th39: :: AOFA_000:39
theorem :: AOFA_000:40
:: 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 :
:: deftheorem Def15 defines unital AOFA_000:def 15 :
theorem Th41: :: AOFA_000:41
theorem Th42: :: AOFA_000:42
:: deftheorem defines EmptyIns AOFA_000:def 16 :
theorem :: AOFA_000:43
theorem Th44: :: AOFA_000:44
:: deftheorem defines \; AOFA_000:def 17 :
theorem :: AOFA_000:45
theorem :: AOFA_000:46
theorem Th47: :: AOFA_000:47
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
end;
:: deftheorem defines if-then-else AOFA_000:def 18 :
:: deftheorem defines if-then AOFA_000:def 19 :
theorem Th48: :: AOFA_000:48
:: deftheorem defines while AOFA_000:def 20 :
:: 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 ) } ;
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 :
theorem Th49: :: AOFA_000:49
theorem Th50: :: AOFA_000:50
theorem Th51: :: AOFA_000:51
theorem Th52: :: AOFA_000:52
theorem Th53: :: AOFA_000:53
definition
let A be
preIfWhileAlgebra;
attr A is
infinite means :
Def23:
:: AOFA_000:def 23
not
ElementaryInstructions A is
finite;
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 :
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 :
:: deftheorem defines ECIW-signature AOFA_000:def 26 :
theorem Th54: :: AOFA_000:54
:: deftheorem Def27 defines ECIW-strict AOFA_000:def 27 :
theorem Th55: :: AOFA_000:55
theorem Th56: :: AOFA_000:56
theorem Th57: :: AOFA_000:57
theorem Th58: :: AOFA_000:58
theorem Th59: :: AOFA_000:59
theorem Th60: :: AOFA_000:60
theorem Th61: :: AOFA_000:61
theorem :: AOFA_000:62
theorem Th63: :: AOFA_000:63
theorem Th64: :: AOFA_000:64
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 )
theorem Th66: :: AOFA_000:66
theorem Th67: :: AOFA_000:67
theorem Th68: :: AOFA_000:68
theorem :: AOFA_000:69
theorem Th70: :: AOFA_000:70
theorem Th71: :: AOFA_000:71
theorem Th72: :: AOFA_000:72
theorem Th73: :: AOFA_000:73
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 ) ) )
theorem Th75: :: AOFA_000:75
theorem Th76: :: AOFA_000:76
theorem Th77: :: AOFA_000:77
theorem :: AOFA_000:78
theorem Th79: :: AOFA_000:79
:: 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 :
Def30:
:: AOFA_000:def 30
for
s being
Element of
S for
C,
I1,
I2 being
Element of
A holds
( (
f . s,
C in T implies
f . s,
(if-then-else C,I1,I2) = f . (f . s,C),
I1 ) & (
f . s,
C nin T implies
f . s,
(if-then-else C,I1,I2) = f . (f . s,C),
I2 ) );
pred f complies_with_while_wrt T means :
Def31:
:: AOFA_000:def 31
for
s being
Element of
S for
C,
I being
Element of
A holds
( (
f . s,
C in T implies
f . s,
(while C,I) = f . (f . (f . s,C),I),
(while C,I) ) & (
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 ) ) );
theorem :: AOFA_000:80
theorem Th81: :: AOFA_000:81
:: deftheorem Def32 defines ExecutionFunction AOFA_000:def 32 :
:: deftheorem Def33 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 ;
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;
:: deftheorem Def34 defines iteration-degree AOFA_000:def 34 :
theorem :: AOFA_000:82
theorem Th83: :: AOFA_000:83
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) )
theorem :: AOFA_000:85
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 ] } :
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 :: 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 ] } :
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) )
theorem Th86: :: AOFA_000:86
theorem Th87: :: AOFA_000:87
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() ) )
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 ] } :
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]
theorem Th88: :: AOFA_000:88
theorem Th89: :: AOFA_000:89
theorem Th90: :: AOFA_000:90
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
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 ) )
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) ) )
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
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 ) )
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 ) ) );
:: deftheorem Def36 defines absolutely-terminating AOFA_000:def 36 :
:: deftheorem Def37 defines is_terminating_wrt AOFA_000:def 37 :
:: deftheorem Def38 defines is_terminating_wrt AOFA_000:def 38 :
:: deftheorem Def39 defines is_invariant_wrt AOFA_000:def 39 :
theorem Th94: :: AOFA_000:94
theorem :: AOFA_000:95
theorem Th96: :: AOFA_000:96
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 )
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 ) )
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) ) ) ) )
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
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
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 :: 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
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
theorem :: AOFA_000:105
theorem Th106: :: AOFA_000:106
theorem :: AOFA_000:107
theorem :: AOFA_000:108
theorem :: AOFA_000:109
theorem :: AOFA_000:110
theorem :: AOFA_000:111
theorem :: AOFA_000:112
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
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
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
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
theorem :: AOFA_000:117
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