:: Mizar Analysis of Algorithms: Preliminaries
:: by Grzegorz Bancerek
::
:: Received July 9, 2007
:: Copyright (c) 2007-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FUNCT_1, TARSKI, RELAT_1, XBOOLE_0, FINSEQ_1, ORDINAL4,
UNIALG_1, BINOP_1, GROUP_1, FINSEQ_2, SUBSET_1, FUNCOP_1, PARTFUN1,
NAT_1, FUNCT_2, CARD_1, COMPUT_1, TREES_3, TREES_4, FINSET_1, TREES_1,
MEMBERED, XXREAL_0, ARYTM_3, FUNCT_4, FUNCT_7, STRUCT_0, INCPROJ, CARD_3,
FREEALG, DTCONSTR, TREES_2, LANG1, TDGROUP, MSUALG_1, ORDINAL1, MSAFREE,
NEWTON, ZFMISC_1, UNIALG_2, PRELAMB, CQC_SIM1, MSUALG_3, WELLORD1,
MCART_1, SUPINF_1, ARYTM_1, SUPINF_2, MESFUNC1, FUNCT_5, SETFAM_1,
AOFA_000;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ENUMSET1, SETFAM_1, ORDINAL1,
MEMBERED, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSET_1, LANG1,
BINOP_1, CARD_1, CARD_3, FINSEQ_1, FINSEQ_2, XXREAL_2, NUMBERS, XCMPLX_0,
XXREAL_0, TREES_1, TREES_2, TREES_3, NAT_1, NAT_D, SUPINF_1, MESFUNC1,
FUNCOP_1, FUNCT_4, FUNCT_5, FUNCT_7, ABIAN, MARGREL1, STRUCT_0, UNIALG_1,
UNIALG_2, ALG_1, FREEALG, PUA2MSS1, COMPUT_1, SUPINF_2, TREES_4,
DTCONSTR, FINSEQ_4, RECDEF_1;
constructors PUA2MSS1, COMPUT_1, BORSUK_1, SUPINF_2, FINSEQ_4, FACIRC_1,
ALG_1, FREEALG, FINSEQOP, WELLORD2, CAT_2, ABIAN, RECDEF_1, MESFUNC1,
SUPINF_1, NAT_D, MARGREL1, FUNCT_5, XTUPLE_0;
registrations FUNCT_1, FINSEQ_2, FUNCT_2, FINSEQ_1, UNIALG_1, NAT_1, STRUCT_0,
PUA2MSS1, DTCONSTR, FREEALG, FUNCT_7, SUBSET_1, XXREAL_0, XREAL_0,
TREES_2, TREES_3, MEMBERED, XBOOLE_0, FINSET_1, TREES_1, FACIRC_1,
RELAT_1, VALUED_0, CARD_1, XXREAL_2, RELSET_1, FINSEQ_3, MARGREL1,
XTUPLE_0, ORDINAL1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
begin :: Binary operations, orbits, and iterations
notation
let x be object,y be set;
antonym x nin y for x in y;
end;
theorem :: 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;
registration
let x,y be non empty set;
cluster <*x,y*> -> non-empty;
end;
registration
let p,q be non-empty FinSequence;
cluster p^q -> non-empty;
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;
definition
let f be homogeneous Function;
attr f is associative means
:: 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
:: AOFA_000:def 3
ex x being set st x is_a_unity_wrt f;
end;
definition
let X be set;
let Y be non empty set;
let Z be FinSequenceSet of X;
let y be Element of Y;
redefine func Z --> y -> PartFunc of X*,Y;
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 quasi_total homogeneous for PartFunc of X*, X;
end;
theorem :: AOFA_000:2
for X being non empty set, x being Element of X
for n being Nat holds arity ((n-tuples_on X) --> x) = n;
registration
let X be non empty set;
let x be Element of X;
let n be Nat;
cluster (n-tuples_on X) --> x -> n-ary for homogeneous PartFunc of X*, X;
end;
registration
let X be non empty set;
cluster 2-ary associative unital
for non empty quasi_total homogeneous PartFunc of X*, X;
cluster 0-ary for non empty quasi_total homogeneous PartFunc of X*, X;
cluster 3-ary for non empty quasi_total homogeneous PartFunc of X*, X;
end;
theorem :: 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;
definition
let f,g be Function;
let X be set;
func (f,X)+*g -> Function equals
:: AOFA_000:def 4
g+*(f|X);
end;
theorem :: AOFA_000:4
for f,g being Function, x,X being set holds
x in X & X c= dom f implies ((f,X)+*g).x = f.x;
theorem :: AOFA_000:5
for f,g being Function, x,X being set holds
x nin X & x in dom g implies ((f,X)+*g).x = g.x;
definition
let X,Y be non empty set;
let f,g be Element of Funcs(X,Y);
let A be set;
redefine func (f,A)+*g -> Element of Funcs(X,Y);
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);
redefine func g*f -> Element of Funcs(X,Z);
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;
theorem :: AOFA_000:6
for f being Function, x being set st x in dom f holds x in f orbit x;
theorem :: AOFA_000:7
for f being Function, x,y being set
st rng f c= dom f & y in f orbit x holds f.y in f orbit x;
theorem :: AOFA_000:8
for f being Function, x being set st x in dom f holds f.x in f orbit x;
theorem :: AOFA_000:9
for f being Function, x being set st x in dom f
holds f orbit (f.x) c= f orbit x;
definition
let f be Function such that
rng f c= dom f;
let A be set;
let x be set;
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;
end;
definition
let f be Function such that
rng f c= dom f;
let A be set;
let g be Function;
func (A,g) iter f -> Function means
:: 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;
end;
theorem :: AOFA_000:10
for f,g being Function, a,A being set st rng f c= dom f & a in dom f holds
not f orbit a c= A implies
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;
theorem :: AOFA_000:11
for f,g being Function, a,A being set
st rng f c= dom f & a in dom f & g*f = g holds
a in A implies ((A,g) iter f).a = ((A,g) iter f).(f.a);
theorem :: AOFA_000:12
for f,g being Function, a,A being set st rng f c= dom f & a in dom f holds
a nin A implies ((A,g) iter f).a = a;
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);
redefine func (A,g) iter f -> Element of Funcs(X,X);
end;
begin :: Free universal algebras
theorem :: AOFA_000:13
for X being non empty set, S being non empty FinSequence of NAT
ex A being Universal_Algebra st the carrier of A = X & signature A = S;
theorem :: 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;
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
for X being non empty set, 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;
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 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 FreeUnivAlgNSG(f,D);
cluster -> DTree-yielding for FinSequence of FreeUnivAlgNSG(f,D);
end;
theorem :: AOFA_000:16
for G being non empty DTConstrStr for t being set st t in TS G holds
(ex d being Symbol of G st d in Terminals G & t = root-tree d) or
ex o being Symbol of G, p being FinSequence of TS G
st o ==> roots p & t = o-tree p;
theorem :: AOFA_000:17
for X being disjoint_with_NAT non empty set
for S being non empty FinSequence of NAT for i being Nat st i in dom S
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;
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
:: 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};
end;
theorem :: AOFA_000:18
for A being Universal_Algebra, B being Subset of A holds B|^0 = B;
theorem :: AOFA_000:19
for A being Universal_Algebra, 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};
theorem :: AOFA_000:20
for A being Universal_Algebra, 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 st
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;
theorem :: AOFA_000:21
for A being Universal_Algebra, B being Subset of A
for n,m being Nat st n <= m holds B|^n c= B|^m;
theorem :: AOFA_000:22
for A being Universal_Algebra for B1,B2 being Subset of A st B1 c= B2
for n being Nat holds B1|^n c= B2|^n;
theorem :: AOFA_000:23
for A being Universal_Algebra, 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 st
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;
scheme :: AOFA_000:sch 1
MaxVal{A() -> non empty set, B() -> set, P[object,object]}:
ex n being Nat st
for x being Element of A() st x in B() holds P[x,n]
provided
B() is finite and
for x being Element of A() st x in B() ex n being Nat st P[x,n] and
for x being Element of A()
for n,m being Nat st P[x,n] & n <= m holds P[x,m];
theorem :: AOFA_000:24
for A being Universal_Algebra, B being Subset of A ex C being Subset of A
st C = union the set of all B|^n where n is Element of NAT &
C is opers_closed;
theorem :: AOFA_000:25
for A being Universal_Algebra, B,C being Subset of A
st C is opers_closed & B c= C
holds union the set of all B|^n where n is Element of NAT c= C;
definition
let A be Universal_Algebra;
func Generators A -> Subset of A equals
:: AOFA_000:def 9
(the carrier of A) \
union the set of all rng o where o is Element of Operations A;
end;
theorem :: AOFA_000:26
for A being Universal_Algebra, a being Element of A holds
a in Generators A iff not ex o being Element of Operations A st a in rng o;
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;
theorem :: AOFA_000:28
for A being Universal_Algebra st Constants A = {} holds {} A is opers_closed;
theorem :: AOFA_000:29
for A being Universal_Algebra st Constants A = {}
for G being GeneratorSet of A holds G <> {};
theorem :: 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;
theorem :: 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;
theorem :: AOFA_000:32
for A being Universal_Algebra for G being GeneratorSet of A
for a being Element of A
st not ex o being Element of Operations A st a in rng o holds a in G;
theorem :: AOFA_000:33
for A being Universal_Algebra, G being GeneratorSet of A
holds Generators A c= G;
theorem :: AOFA_000:34
for A being free Universal_Algebra for G being free GeneratorSet of A
holds G = Generators A;
registration
let A be free Universal_Algebra;
cluster Generators A -> free for GeneratorSet of A;
end;
definition
let A be free Universal_Algebra;
redefine func Generators A -> GeneratorSet of A;
end;
registration
let A,B be set;
cluster [:A,B:] -> disjoint_with_NAT;
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;
theorem :: 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)
holds Den(o1,A).p1 = Den(o2,A).p2 implies o1 = o2 & p1 = p2;
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
holds o1.p1 = o2.p2 implies o1 = o2 & p1 = p2;
theorem :: 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) for a being set st a in rng p
holds a <> Den(o,A).p;
theorem :: 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, p being FinSequence
st p in dom Den(o9,A) & Den(o9,A).p in G holds o9 <> o
for p being FinSequence st p in dom Den(o,A)
for n being Nat st Den(o,A).p in G|^(n+1) holds rng p c= G|^n;
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)
for n being Nat st Den(o,A).p in (Generators A)|^(n+1)
holds rng p c= (Generators A)|^n;
begin :: If-while Algebra
definition
let S be non empty UAStr;
attr S is with_empty-instruction means
:: AOFA_000:def 10
1 in dom the charact of S &
(the charact of S).1 is 0-ary non empty homogeneous
quasi_total PartFunc of (the carrier of S)*, the carrier of S;
attr S is with_catenation means
:: AOFA_000:def 11
2 in dom the charact of S &
(the charact of S).2 is 2-ary non empty homogeneous
quasi_total PartFunc of (the carrier of S)*, the carrier of S;
attr S is with_if-instruction means
:: AOFA_000:def 12
3 in dom the charact of S &
(the charact of S).3 is 3-ary non empty homogeneous
quasi_total PartFunc of (the carrier of S)*, the carrier of S;
attr S is with_while-instruction means
:: AOFA_000:def 13
4 in dom the charact of S &
(the charact of S).4 is 2-ary non empty homogeneous
quasi_total PartFunc of (the carrier of S)*, the carrier of S;
attr S is associative means
:: AOFA_000:def 14
(the charact of S).2 is 2-ary associative non empty homogeneous
quasi_total PartFunc of (the carrier of S)*, the carrier of S;
end;
definition
let S be non-empty UAStr;
attr S is unital means
:: AOFA_000:def 15
ex f being 2-ary non empty homogeneous
quasi_total 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;
theorem :: AOFA_000:41
for X being non empty set, x being Element of X
for c being 2-ary associative unital
non empty quasi_total homogeneous PartFunc of X*, X st x is_a_unity_wrt c
for i being 3-ary non empty quasi_total homogeneous PartFunc of X*, X
for w being 2-ary non empty quasi_total homogeneous PartFunc of X*, X
ex S being non-empty strict UAStr st the carrier of S = X &
the charact of S = <*(0-tuples_on X)-->x,c*>^<*i,w*> &
S is with_empty-instruction with_catenation unital associative
with_if-instruction with_while-instruction quasi_total partial;
registration
cluster with_empty-instruction with_catenation with_if-instruction
with_while-instruction unital associative
for quasi_total partial non-empty strict UAStr;
end;
definition
mode preIfWhileAlgebra is with_empty-instruction
with_catenation with_if-instruction with_while-instruction
Universal_Algebra;
end;
reserve A for preIfWhileAlgebra,
C,I,J for Element of A;
reserve S for non empty set,
T for Subset of S,
s for Element of S;
definition
let A be non empty UAStr;
mode Algorithm of A is Element of A;
end;
theorem :: AOFA_000:42
for A being with_empty-instruction non-empty UAStr
holds dom Den(In(1, dom the charact of A), A) = {{}};
definition
let A be with_empty-instruction non-empty UAStr;
func EmptyIns A -> Algorithm of A equals
:: AOFA_000:def 16
Den(In(1, dom the charact of A), A).{};
end;
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;
theorem :: AOFA_000:44
for A being with_catenation non-empty UAStr
holds dom Den(In(2, dom the charact of A), A) = 2-tuples_on the carrier of A;
definition
let A be with_catenation non-empty 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*>;
end;
theorem :: AOFA_000:45
for A being with_empty-instruction with_catenation unital non-empty UAStr
for I being Element of A holds EmptyIns A\;I = I & I\;EmptyIns A = I;
theorem :: AOFA_000:46
for A being associative with_catenation non-empty UAStr
for I1,I2,I3 being Element of A holds (I1\;I2)\;I3 = I1\;(I2\;I3);
theorem :: AOFA_000:47
for A being with_if-instruction non-empty UAStr
holds dom Den(In(3, dom the charact of A), A) = 3-tuples_on the carrier of A;
definition
let A be with_if-instruction non-empty 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*>;
end;
definition
let A be with_empty-instruction with_if-instruction non-empty 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;
theorem :: AOFA_000:48
for A being with_while-instruction non-empty UAStr
holds dom Den(In(4, dom the charact of A), A) = 2-tuples_on the carrier of A;
definition
let A be with_while-instruction non-empty 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*>;
end;
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;
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;
theorem :: AOFA_000:49
for A being preIfWhileAlgebra holds EmptyIns A nin ElementaryInstructions A;
theorem :: 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;
theorem :: 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;
theorem :: AOFA_000:52
for A being preIfWhileAlgebra for C,I being Element of A
holds while(C,I) nin ElementaryInstructions A;
theorem :: AOFA_000:53
for A being preIfWhileAlgebra for I being Element of A
st I nin ElementaryInstructions A holds 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);
definition
let A be preIfWhileAlgebra;
attr A is infinite means
:: AOFA_000:def 23
ElementaryInstructions A is infinite;
attr A is degenerated means
:: 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
:: AOFA_000:def 25
ElementaryInstructions A is GeneratorSet of A;
end;
definition
func ECIW-signature -> non empty FinSequence of NAT equals
:: AOFA_000:def 26
<*0, 2*>^<*3, 2*>;
end;
theorem :: 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;
definition
let A be partial non-empty non empty UAStr;
attr A is ECIW-strict means
:: AOFA_000:def 27
signature A = ECIW-signature;
end;
theorem :: AOFA_000:55
for A being partial non-empty non empty UAStr st A is ECIW-strict
for o being OperSymbol of A holds o = 1 or o = 2 or o = 3 or o = 4;
registration
let X be disjoint_with_NAT non empty set;
cluster FreeUnivAlgNSG(ECIW-signature,X) -> with_empty-instruction
with_catenation with_if-instruction with_while-instruction;
end;
theorem :: AOFA_000:56
for X being disjoint_with_NAT non empty 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, p being FinSequence of FreeUnivAlgNSG(ECIW-signature,X)
st n in Seg 4 & I = n-tree p & len p = ECIW-signature.n;
theorem :: AOFA_000:57
for X being disjoint_with_NAT non empty set
holds EmptyIns FreeUnivAlgNSG(ECIW-signature,X) = 1-tree {};
theorem :: AOFA_000:58
for X being disjoint_with_NAT non empty set
for p being FinSequence of FreeUnivAlgNSG(ECIW-signature,X)
st 1-tree p is Element of FreeUnivAlgNSG(ECIW-signature,X) holds p = {};
theorem :: AOFA_000:59
for X being disjoint_with_NAT non empty set
for I1,I2 being Element of FreeUnivAlgNSG(ECIW-signature,X)
holds I1\;I2 = 2-tree(I1,I2);
theorem :: AOFA_000:60
for X being disjoint_with_NAT non empty set
for p being FinSequence of FreeUnivAlgNSG(ECIW-signature,X)
st 2-tree p is Element of FreeUnivAlgNSG(ECIW-signature,X)
ex I1,I2 being Element of FreeUnivAlgNSG(ECIW-signature,X) st p = <*I1,I2*>;
theorem :: AOFA_000:61
for X being disjoint_with_NAT non empty set
for I1,I2 being Element of FreeUnivAlgNSG(ECIW-signature,X)
holds I1\;I2 <> I1 & I1\;I2 <> I2;
theorem :: AOFA_000:62
for X being disjoint_with_NAT non empty set
for I1,I2,J1,J2 being Element of FreeUnivAlgNSG(ECIW-signature,X)
holds I1\;I2 = J1\;J2 implies I1 = J1 & I2 = J2;
theorem :: AOFA_000:63
for X being disjoint_with_NAT non empty set
for C,I1,I2 being Element of FreeUnivAlgNSG(ECIW-signature,X)
holds if-then-else(C,I1,I2) = 3-tree<*C,I1,I2*>;
theorem :: AOFA_000:64
for X being disjoint_with_NAT non empty set
for p being FinSequence of FreeUnivAlgNSG(ECIW-signature,X)
st 3-tree p is Element of FreeUnivAlgNSG(ECIW-signature,X)
ex C,I1,I2 being Element of FreeUnivAlgNSG(ECIW-signature,X)
st p = <*C,I1,I2*>;
theorem :: AOFA_000:65
for X being disjoint_with_NAT non empty 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 :: AOFA_000:66
for X being disjoint_with_NAT non empty set
for C,I being Element of FreeUnivAlgNSG(ECIW-signature,X)
holds while(C,I) = 4-tree(C,I);
theorem :: AOFA_000:67
for X being disjoint_with_NAT non empty set
for p being FinSequence of FreeUnivAlgNSG(ECIW-signature,X)
st 4-tree p is Element of FreeUnivAlgNSG(ECIW-signature,X)
ex C,I being Element of FreeUnivAlgNSG(ECIW-signature,X) st p = <*C,I*>;
theorem :: AOFA_000:68
for X being disjoint_with_NAT non empty set
for I being Element of FreeUnivAlgNSG(ECIW-signature,X)
st I in ElementaryInstructions FreeUnivAlgNSG(ECIW-signature,X)
ex x being Element of X st I = x-tree {};
theorem :: AOFA_000:69
for X being disjoint_with_NAT non empty 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 = {};
theorem :: AOFA_000:70
for X being disjoint_with_NAT non empty set
holds ElementaryInstructions FreeUnivAlgNSG(ECIW-signature,X) =
FreeGenSetNSG(ECIW-signature,X) &
card X = card FreeGenSetNSG(ECIW-signature,X);
registration
cluster infinite disjoint_with_NAT for set;
end;
registration
let X be infinite disjoint_with_NAT set;
cluster FreeUnivAlgNSG(ECIW-signature,X) -> infinite;
end;
registration
let X be disjoint_with_NAT non empty set;
cluster FreeUnivAlgNSG(ECIW-signature,X) -> ECIW-strict;
end;
theorem :: AOFA_000:71
for A being preIfWhileAlgebra holds Generators A c= ElementaryInstructions A;
theorem :: AOFA_000:72
for A being preIfWhileAlgebra st A is free 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);
theorem :: AOFA_000:73
for A being preIfWhileAlgebra st A is free
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);
theorem :: AOFA_000:74
for A being preIfWhileAlgebra st A is free
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 :: AOFA_000:75
for A being preIfWhileAlgebra st A is free 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);
registration
cluster free -> well_founded non degenerated for preIfWhileAlgebra;
end;
registration
cluster infinite non degenerated well_founded ECIW-strict free
strict for preIfWhileAlgebra;
end;
definition
mode IfWhileAlgebra is
non degenerated well_founded ECIW-strict preIfWhileAlgebra;
end;
registration
let A be infinite preIfWhileAlgebra;
cluster ElementaryInstructions A -> infinite;
end;
theorem :: 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);
theorem :: AOFA_000:77
for A being ECIW-strict preIfWhileAlgebra
for x being set, n being Nat st x in (ElementaryInstructions A)|^(n+1)
holds 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;
theorem :: AOFA_000:78
for A being Universal_Algebra for B being Subset of A
holds Constants A c= B|^1;
theorem :: 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
;
scheme :: AOFA_000:sch 2
StructInd{ A() -> well_founded ECIW-strict preIfWhileAlgebra,
I() -> (Element of A()), P[set] }: P[I()]
provided
for I being Element of A() st I in ElementaryInstructions A() holds P[I]
and
P[EmptyIns A()] and
for I1,I2 being Element of A() st P[I1] & P[I2] holds P[I1\;I2] and
for C,I1,I2 being Element of A() st P[C] & P[I1] & P[I2]
holds P[if-then-else(C,I1,I2)] and
for C,I being Element of A() st P[C] & P[I] holds P[while(C,I)];
begin :: Execution function
definition
let A be preIfWhileAlgebra;
let S be non empty set; :: states
let f be Function of [:S, the carrier of A:], S;
attr f is complying_with_empty-instruction means
:: AOFA_000:def 28
for s being Element of S holds f.(s, EmptyIns A) = s;
attr f is complying_with_catenation means
:: 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;
definition
let A be preIfWhileAlgebra;
let S be non empty set; :: states
let T be Subset of S; :: true states
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;
theorem :: AOFA_000:80
for f being Function of [:S, the carrier of A:], S
st f is complying_with_empty-instruction & f complies_with_if_wrt T
for s being Element of S holds
f.(s,C) nin T implies f.(s,if-then(C,I)) = f.(s,C);
theorem :: AOFA_000:81
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;
definition
let A be preIfWhileAlgebra;
let S be non empty set; :: states
let T be Subset of S; :: true states
mode ExecutionFunction of A,S,T -> Function of [:S, the carrier of A:], S
means
:: 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;
end;
registration
let A be preIfWhileAlgebra;
let S be non empty set; :: states
let T be Subset of S; :: true states
cluster -> complying_with_empty-instruction complying_with_catenation
for ExecutionFunction of A,S,T;
end;
definition
let A be preIfWhileAlgebra;
let I be Element of A;
let S be non empty set; :: states
let s be Element of S;
let T be Subset of S; :: true states
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;
definition
let A be preIfWhileAlgebra;
let I be Element of A;
let S be non empty set; :: states
let s be Element of S;
let T be Subset of S; :: true states
let f be ExecutionFunction of A, S, T;
func iteration-degree(I,s,f) -> R_eal means
:: 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;
end;
reserve f for ExecutionFunction of A,S,T;
theorem :: AOFA_000:82
f iteration_terminates_for I,s iff iteration-degree(I,s,f) < +infty;
theorem :: AOFA_000:83
s nin T implies f iteration_terminates_for I,s & iteration-degree(I,s,f) = 0;
theorem :: AOFA_000:84
s in T implies
(f iteration_terminates_for I,s iff f iteration_terminates_for I, f.(s,I)) &
iteration-degree(I,s,f) = 1.+iteration-degree(I,f.(s,I),f);
theorem :: AOFA_000:85
iteration-degree(I,s,f) >= 0;
scheme :: AOFA_000:sch 3
Termination {A() -> preIfWhileAlgebra, I() -> (Element of A()),
S() -> non empty set, s() -> (Element of S()), T() -> Subset of S(),
f() -> ExecutionFunction of A(),S(),T(), F(set) -> Nat, P[set] }:
f() iteration_terminates_for I(),s()
provided
s() in T() iff P[s()] and
for s being Element of S() st P[s]
holds (P[f().(s,I())] iff f().(s,I()) in T()) & F(f().(s,I())) < F(s);
scheme :: AOFA_000:sch 4
Termination2 {A() -> preIfWhileAlgebra, I() -> (Element of A()),
S() -> non empty set, s() -> (Element of S()), T() -> Subset of S(),
f() -> ExecutionFunction of A(),S(),T(), F(set) -> Nat, P,R[set] }:
f() iteration_terminates_for I(),s()
provided
P[s()] and
s() in T() iff R[s()] and
for s being Element of S() st P[s] & s in T() & R[s]
holds P[f().(s, I())] & (R[f().(s,I())] iff f().(s,I()) in T()) &
F(f().(s,I())) < F(s);
theorem :: AOFA_000:86
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;
theorem :: AOFA_000:87
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;
scheme :: AOFA_000:sch 5
InvariantSch {A() -> preIfWhileAlgebra, C,I() -> (Element of A()),
S() -> non empty set, s() -> (Element of S()), T() -> Subset of S(),
f() -> ExecutionFunction of A(),S(),T(), P,R[set] }:
P[f().(s(),while(C(),I()))] & not R[f().(s(),while(C(),I()))]
provided
P[s()] and
f() iteration_terminates_for I()\;C(), f().(s(),C()) and
for s being Element of S() st P[s] & s in T() & R[s] holds P[f().(s,I())]
and
for s being Element of S() st P[s] holds
P[f().(s,C())] & (f().(s,C()) in T() iff R[f().(s,C())]);
scheme :: AOFA_000:sch 6
coInvariantSch {A() -> preIfWhileAlgebra, C,I() -> (Element of A()),
S() -> non empty set, s() -> (Element of S()), T() -> Subset of S(),
f() -> ExecutionFunction of A(),S(),T(), P[set] }: P[s()]
provided
P[f().(s(),while(C(),I()))] and
f() iteration_terminates_for I()\;C(), f().(s(),C()) and
for s being Element of S() st P[f().(f().(s,C()),I())] & f().(s,C()) in T()
holds P[f().(s,C())] and
for s being Element of S() st P[f().(s,C())] holds P[s];
theorem :: 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
ex i being Nat st n = i+1 &
I1 in (ElementaryInstructions A)|^i & I2 in (ElementaryInstructions A)|^i;
theorem :: 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
ex i being Nat st n = i+1 & C in (ElementaryInstructions A)|^i &
I1 in (ElementaryInstructions A)|^i & I2 in (ElementaryInstructions A)|^i;
theorem :: 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
ex i being Nat st n = i+1 &
C in (ElementaryInstructions A)|^i & I in (ElementaryInstructions A)|^i;
begin :: Existence and uniqueness of execution function and termination
scheme :: AOFA_000:sch 7
IndDef {A() -> free ECIW-strict preIfWhileAlgebra,
S() -> non empty set, Emp() -> (Element of S()), ElemF(set) -> set,
ConF, WhiF(set,set) -> (Element of S()),
IfF(set,set,set) -> Element of S()}:
ex f being Function of the carrier of A(), S() st
(for I being Element of A() st I in ElementaryInstructions A()
holds f.I = ElemF(I)) & f.EmptyIns A() = Emp() &
(for I1,I2 being Element of A() holds f.(I1\;I2) = ConF(f.I1,f.I2)) &
(for C,I1,I2 being Element of A()
holds f.if-then-else(C,I1,I2) = IfF(f.C,f.I1,f.I2)) &
for C,I being Element of A() holds f.while(C,I) = WhiF(f.C,f.I)
provided
for I being Element of A() st I in ElementaryInstructions A()
holds ElemF(I) in S();
theorem :: AOFA_000:91
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 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
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 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;
func TerminatingPrograms(A,S,T,f) -> Subset of [:S, the carrier of A:] means
:: 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;
end;
definition
let A be preIfWhileAlgebra;
let I be Element of A;
attr I is absolutely-terminating means
:: AOFA_000:def 36
for S being non empty set, 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;
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;
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;
theorem :: AOFA_000:94
I in ElementaryInstructions A implies [s, I] in TerminatingPrograms(A,S,T,f);
theorem :: AOFA_000:95
I in ElementaryInstructions A implies I is absolutely-terminating;
theorem :: AOFA_000:96
[s, EmptyIns A] in TerminatingPrograms(A,S,T,f);
registration
let A;
cluster EmptyIns A -> absolutely-terminating;
end;
registration
let A;
cluster absolutely-terminating for Element of A;
end;
theorem :: AOFA_000:97
A is free & [s, I\;J] in TerminatingPrograms(A,S,T,f) implies
[s,I] in TerminatingPrograms(A,S,T,f) &
[f.(s,I), J] in TerminatingPrograms(A,S,T,f);
registration
let A;
let I,J be absolutely-terminating Element of A;
cluster I\;J -> absolutely-terminating;
end;
theorem :: AOFA_000:98
A is free & [s, if-then-else(C,I,J)] in TerminatingPrograms(A,S,T,f)
implies [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));
registration
let A;
let C,I,J be absolutely-terminating Element of A;
cluster if-then-else(C,I,J) -> absolutely-terminating;
end;
registration
let A;
let C,I be absolutely-terminating Element of A;
cluster if-then(C,I) -> absolutely-terminating;
end;
theorem :: AOFA_000:99
A is free & [s, while(C,I)] in TerminatingPrograms(A,S,T,f)
implies [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
A is free & [s, while(C,I)] in TerminatingPrograms(A,S,T,f) & f.(s,C) in T
implies [f.(s,C), I] in TerminatingPrograms(A,S,T,f);
theorem :: AOFA_000:101
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);
theorem :: AOFA_000:102
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 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 I being Element of A st [s,I] in TerminatingPrograms(A,S,T,f1)
holds f1.(s, I) = f2.(s, I);
theorem :: AOFA_000:104
for I being absolutely-terminating Element of A holds I is_terminating_wrt f;
theorem :: AOFA_000:105
for I being Element of A holds
I is_terminating_wrt f iff I is_terminating_wrt f, S;
theorem :: AOFA_000:106
for I being Element of A st I is_terminating_wrt f
for P being set holds I is_terminating_wrt f, P;
theorem :: AOFA_000:107
for I being absolutely-terminating Element of A
for P being set holds I is_terminating_wrt f, P;
theorem :: AOFA_000:108
for I being Element of A holds S is_invariant_wrt I, f;
theorem :: AOFA_000:109
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;
theorem :: AOFA_000:110
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;
theorem :: AOFA_000:111
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;
theorem :: AOFA_000:112
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;
theorem :: AOFA_000:113
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 :: AOFA_000:114
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 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 :: AOFA_000:116
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 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
for C,I being Element of A
st C is_terminating_wrt f & I is_terminating_wrt f &
for s holds f iteration_terminates_for I\;C, s
holds while(C,I) is_terminating_wrt f;
theorem :: AOFA_000:118
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 st s in P & f.(f.(s,I),C) in T
holds f.(s,I) in P) &
for 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;