begin
theorem Th1:
for
x,
y,
z,
a,
b,
c being
set st
a <> b &
b <> c &
c <> a holds
ex
f being
Function st
(
f . a = x &
f . b = y &
f . c = z )
:: deftheorem defines \ AOFA_I00:def 1 :
theorem Th2:
:: deftheorem Def2 defines Variable AOFA_I00:def 2 :
definition
let t1,
t2 be
integer-yielding Function;
func t1 div t2 -> integer-yielding Function means :
Def3:
(
dom it = (dom t1) /\ (dom t2) & ( for
s being
set st
s in dom it holds
it . s = (t1 . s) div (t2 . s) ) );
correctness
existence
ex b1 being integer-yielding Function st
( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = (t1 . s) div (t2 . s) ) );
uniqueness
for b1, b2 being integer-yielding Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = (t1 . s) div (t2 . s) ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds
b2 . s = (t1 . s) div (t2 . s) ) holds
b1 = b2;
func t1 mod t2 -> integer-yielding Function means :
Def4:
(
dom it = (dom t1) /\ (dom t2) & ( for
s being
set st
s in dom it holds
it . s = (t1 . s) mod (t2 . s) ) );
correctness
existence
ex b1 being integer-yielding Function st
( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = (t1 . s) mod (t2 . s) ) );
uniqueness
for b1, b2 being integer-yielding Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = (t1 . s) mod (t2 . s) ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds
b2 . s = (t1 . s) mod (t2 . s) ) holds
b1 = b2;
func leq t1,
t2 -> integer-yielding Function means :
Def5:
(
dom it = (dom t1) /\ (dom t2) & ( for
s being
set st
s in dom it holds
it . s = IFGT (t1 . s),
(t2 . s),
0 ,1 ) );
correctness
existence
ex b1 being integer-yielding Function st
( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = IFGT (t1 . s),(t2 . s),0 ,1 ) );
uniqueness
for b1, b2 being integer-yielding Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = IFGT (t1 . s),(t2 . s),0 ,1 ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds
b2 . s = IFGT (t1 . s),(t2 . s),0 ,1 ) holds
b1 = b2;
func gt t1,
t2 -> integer-yielding Function means :
Def6:
(
dom it = (dom t1) /\ (dom t2) & ( for
s being
set st
s in dom it holds
it . s = IFGT (t1 . s),
(t2 . s),1,
0 ) );
correctness
existence
ex b1 being integer-yielding Function st
( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = IFGT (t1 . s),(t2 . s),1,0 ) );
uniqueness
for b1, b2 being integer-yielding Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = IFGT (t1 . s),(t2 . s),1,0 ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds
b2 . s = IFGT (t1 . s),(t2 . s),1,0 ) holds
b1 = b2;
func eq t1,
t2 -> integer-yielding Function means :
Def7:
(
dom it = (dom t1) /\ (dom t2) & ( for
s being
set st
s in dom it holds
it . s = IFEQ (t1 . s),
(t2 . s),1,
0 ) );
correctness
existence
ex b1 being integer-yielding Function st
( dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = IFEQ (t1 . s),(t2 . s),1,0 ) );
uniqueness
for b1, b2 being integer-yielding Function st dom b1 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b1 holds
b1 . s = IFEQ (t1 . s),(t2 . s),1,0 ) & dom b2 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b2 holds
b2 . s = IFEQ (t1 . s),(t2 . s),1,0 ) holds
b1 = b2;
end;
:: deftheorem Def3 defines div AOFA_I00:def 3 :
:: deftheorem Def4 defines mod AOFA_I00:def 4 :
:: deftheorem Def5 defines leq AOFA_I00:def 5 :
:: deftheorem Def6 defines gt AOFA_I00:def 6 :
:: deftheorem Def7 defines eq AOFA_I00:def 7 :
definition
let X be non
empty set ;
let f be
Function of
X,
INT ;
let x be
integer number ;
+redefine func f + x -> Function of
X,
INT means :
Def8:
for
s being
Element of
X holds
it . s = (f . s) + x;
compatibility
for b1 being Function of X,INT holds
( b1 = x + f iff for s being Element of X holds b1 . s = (f . s) + x )
coherence
x + f is Function of X,INT
-redefine func f - x -> Function of
X,
INT means
for
s being
Element of
X holds
it . s = (f . s) - x;
compatibility
for b1 being Function of X,INT holds
( b1 = f - x iff for s being Element of X holds b1 . s = (f . s) - x )
coherence
f - x is Function of X,INT
*redefine func f * x -> Function of
X,
INT means :
Def10:
for
s being
Element of
X holds
it . s = (f . s) * x;
compatibility
for b1 being Function of X,INT holds
( b1 = f * x iff for s being Element of X holds b1 . s = (f . s) * x )
coherence
f * x is Function of X,INT
end;
:: deftheorem Def8 defines + AOFA_I00:def 8 :
:: deftheorem defines - AOFA_I00:def 9 :
:: deftheorem Def10 defines * AOFA_I00:def 10 :
definition
let X be
set ;
let f,
g be
Function of
X,
INT ;
divredefine func f div g -> Function of
X,
INT ;
coherence
f div g is Function of X,INT
modredefine func f mod g -> Function of
X,
INT ;
coherence
f mod g is Function of X,INT
leqredefine func leq f,
g -> Function of
X,
INT ;
coherence
leq f,g is Function of X,INT
gtredefine func gt f,
g -> Function of
X,
INT ;
coherence
gt f,g is Function of X,INT
eqredefine func eq f,
g -> Function of
X,
INT ;
coherence
eq f,g is Function of X,INT
end;
:: deftheorem Def11 defines - AOFA_I00:def 11 :
:: deftheorem defines + AOFA_I00:def 12 :
:: deftheorem Def13 defines ** AOFA_I00:def 13 :
definition
let X,
Y,
Z,
N be non
empty set ;
let v be
Element of
Funcs (Funcs X,Y),
Z;
let f be
Function of
X,
N;
**redefine func v ** f,
N -> Element of
Funcs (Funcs N,Y),
Z;
coherence
v ** f,N is Element of Funcs (Funcs N,Y),Z
end;
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem
theorem
theorem Th11:
theorem
theorem
begin
:: deftheorem Def14 defines is_assignment_wrt AOFA_I00:def 14 :
:: deftheorem Def15 defines form_assignment_wrt AOFA_I00:def 15 :
:: deftheorem defines INT-Variable AOFA_I00:def 16 :
:: deftheorem defines INT-Expression AOFA_I00:def 17 :
:: deftheorem Def18 defines . AOFA_I00:def 18 :
:: deftheorem Def19 defines . AOFA_I00:def 19 :
:: deftheorem defines ^ AOFA_I00:def 20 :
theorem
:: deftheorem defines . AOFA_I00:def 21 :
theorem
definition
let A be
preIfWhileAlgebra;
let X be non
empty set ;
let T be
Subset of
(Funcs X,INT );
let f be
ExecutionFunction of
A,
Funcs X,
INT ,
T;
attr f is
Euclidean means :
Def22:
( ( for
v being
INT-Variable of
A,
f for
t being
INT-Expression of
A,
f holds
v,
t form_assignment_wrt f ) & ( for
i being
integer number holds
. i,
X is
INT-Expression of
A,
f ) & ( for
v being
INT-Variable of
A,
f holds
. v is
INT-Expression of
A,
f ) & ( for
x being
Element of
X holds
^ x is
INT-Variable of
A,
f ) & ex
a being
INT-Array of
X st
(
a | (card X) is
one-to-one & ( for
t being
INT-Expression of
A,
f holds
a * t is
INT-Variable of
A,
f ) ) & ( for
t being
INT-Expression of
A,
f holds
- t is
INT-Expression of
A,
f ) & ( for
t1,
t2 being
INT-Expression of
A,
f holds
(
t1 (#) t2 is
INT-Expression of
A,
f &
t1 + t2 is
INT-Expression of
A,
f &
t1 div t2 is
INT-Expression of
A,
f &
t1 mod t2 is
INT-Expression of
A,
f &
leq t1,
t2 is
INT-Expression of
A,
f &
gt t1,
t2 is
INT-Expression of
A,
f ) ) );
end;
:: deftheorem Def22 defines Euclidean AOFA_I00:def 22 :
for
A being
preIfWhileAlgebra for
X being non
empty set for
T being
Subset of
(Funcs X,INT ) for
f being
ExecutionFunction of
A,
Funcs X,
INT ,
T holds
(
f is
Euclidean iff ( ( for
v being
INT-Variable of
A,
f for
t being
INT-Expression of
A,
f holds
v,
t form_assignment_wrt f ) & ( for
i being
integer number holds
. i,
X is
INT-Expression of
A,
f ) & ( for
v being
INT-Variable of
A,
f holds
. v is
INT-Expression of
A,
f ) & ( for
x being
Element of
X holds
^ x is
INT-Variable of
A,
f ) & ex
a being
INT-Array of
X st
(
a | (card X) is
one-to-one & ( for
t being
INT-Expression of
A,
f holds
a * t is
INT-Variable of
A,
f ) ) & ( for
t being
INT-Expression of
A,
f holds
- t is
INT-Expression of
A,
f ) & ( for
t1,
t2 being
INT-Expression of
A,
f holds
(
t1 (#) t2 is
INT-Expression of
A,
f &
t1 + t2 is
INT-Expression of
A,
f &
t1 div t2 is
INT-Expression of
A,
f &
t1 mod t2 is
INT-Expression of
A,
f &
leq t1,
t2 is
INT-Expression of
A,
f &
gt t1,
t2 is
INT-Expression of
A,
f ) ) ) );
:: deftheorem Def23 defines Euclidean AOFA_I00:def 23 :
definition
func INT-ElemIns -> infinite disjoint_with_NAT set equals
[:(Funcs (Funcs NAT ,INT ),NAT ),(Funcs (Funcs NAT ,INT ),INT ):];
coherence
[:(Funcs (Funcs NAT ,INT ),NAT ),(Funcs (Funcs NAT ,INT ),INT ):] is infinite disjoint_with_NAT set
;
end;
:: deftheorem defines INT-ElemIns AOFA_I00:def 24 :
definition
mode INT-Exec -> ExecutionFunction of
FreeUnivAlgNSG ECIW-signature ,
INT-ElemIns ,
Funcs NAT ,
INT ,
(Funcs NAT ,INT ) \ 0 ,
0 means :
Def25:
for
s being
Element of
Funcs NAT ,
INT for
v being
Element of
Funcs (Funcs NAT ,INT ),
NAT for
e being
Element of
Funcs (Funcs NAT ,INT ),
INT holds
it . s,
(root-tree [v,e]) = s +* (v . s),
(e . s);
existence
ex b1 being ExecutionFunction of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns , Funcs NAT ,INT ,(Funcs NAT ,INT ) \ 0 ,0 st
for s being Element of Funcs NAT ,INT
for v being Element of Funcs (Funcs NAT ,INT ),NAT
for e being Element of Funcs (Funcs NAT ,INT ),INT holds b1 . s,(root-tree [v,e]) = s +* (v . s),(e . s)
end;
:: deftheorem Def25 defines INT-Exec AOFA_I00:def 25 :
for
b1 being
ExecutionFunction of
FreeUnivAlgNSG ECIW-signature ,
INT-ElemIns ,
Funcs NAT ,
INT ,
(Funcs NAT ,INT ) \ 0 ,
0 holds
(
b1 is
INT-Exec iff for
s being
Element of
Funcs NAT ,
INT for
v being
Element of
Funcs (Funcs NAT ,INT ),
NAT for
e being
Element of
Funcs (Funcs NAT ,INT ),
INT holds
b1 . s,
(root-tree [v,e]) = s +* (v . s),
(e . s) );
definition
let X be non
empty set ;
func INT-ElemIns X -> infinite disjoint_with_NAT set equals
[:(Funcs (Funcs X,INT ),X),(Funcs (Funcs X,INT ),INT ):];
coherence
[:(Funcs (Funcs X,INT ),X),(Funcs (Funcs X,INT ),INT ):] is infinite disjoint_with_NAT set
;
end;
:: deftheorem defines INT-ElemIns AOFA_I00:def 26 :
definition
let X be non
empty set ;
let x be
Element of
X;
mode INT-Exec of
x -> ExecutionFunction of
FreeUnivAlgNSG ECIW-signature ,
(INT-ElemIns X),
Funcs X,
INT ,
(Funcs X,INT ) \ x,
0 means
for
s being
Element of
Funcs X,
INT for
v being
Element of
Funcs (Funcs X,INT ),
X for
e being
Element of
Funcs (Funcs X,INT ),
INT holds
it . s,
(root-tree [v,e]) = s +* (v . s),
(e . s);
existence
ex b1 being ExecutionFunction of FreeUnivAlgNSG ECIW-signature ,(INT-ElemIns X), Funcs X,INT ,(Funcs X,INT ) \ x,0 st
for s being Element of Funcs X,INT
for v being Element of Funcs (Funcs X,INT ),X
for e being Element of Funcs (Funcs X,INT ),INT holds b1 . s,(root-tree [v,e]) = s +* (v . s),(e . s)
end;
:: deftheorem defines INT-Exec AOFA_I00:def 27 :
for
X being non
empty set for
x being
Element of
X for
b3 being
ExecutionFunction of
FreeUnivAlgNSG ECIW-signature ,
(INT-ElemIns X),
Funcs X,
INT ,
(Funcs X,INT ) \ x,
0 holds
(
b3 is
INT-Exec of
x iff for
s being
Element of
Funcs X,
INT for
v being
Element of
Funcs (Funcs X,INT ),
X for
e being
Element of
Funcs (Funcs X,INT ),
INT holds
b3 . s,
(root-tree [v,e]) = s +* (v . s),
(e . s) );
definition
let X be non
empty set ;
let T be
Subset of
(Funcs X,INT );
let c be
Enumeration of
X;
assume A1:
rng c c= NAT
;
mode INT-Exec of
c,
T -> ExecutionFunction of
FreeUnivAlgNSG ECIW-signature ,
INT-ElemIns ,
Funcs X,
INT ,
T means :
Def28:
for
s being
Element of
Funcs X,
INT for
v being
Element of
Funcs (Funcs X,INT ),
X for
e being
Element of
Funcs (Funcs X,INT ),
INT holds
it . s,
(root-tree [((c * v) ** c,NAT ),(e ** c,NAT )]) = s +* (v . s),
(e . s);
existence
ex b1 being ExecutionFunction of FreeUnivAlgNSG ECIW-signature ,INT-ElemIns , Funcs X,INT ,T st
for s being Element of Funcs X,INT
for v being Element of Funcs (Funcs X,INT ),X
for e being Element of Funcs (Funcs X,INT ),INT holds b1 . s,(root-tree [((c * v) ** c,NAT ),(e ** c,NAT )]) = s +* (v . s),(e . s)
end;
:: deftheorem Def28 defines INT-Exec AOFA_I00:def 28 :
for
X being non
empty set for
T being
Subset of
(Funcs X,INT ) for
c being
Enumeration of
X st
rng c c= NAT holds
for
b4 being
ExecutionFunction of
FreeUnivAlgNSG ECIW-signature ,
INT-ElemIns ,
Funcs X,
INT ,
T holds
(
b4 is
INT-Exec of
c,
T iff for
s being
Element of
Funcs X,
INT for
v being
Element of
Funcs (Funcs X,INT ),
X for
e being
Element of
Funcs (Funcs X,INT ),
INT holds
b4 . s,
(root-tree [((c * v) ** c,NAT ),(e ** c,NAT )]) = s +* (v . s),
(e . s) );
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
definition
let A be
Euclidean preIfWhileAlgebra;
let X be non
empty countable set ;
let T be
Subset of
(Funcs X,INT );
let f be
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
T;
let t be
INT-Expression of
A,
f;
let i be
integer number ;
+redefine func t + i -> INT-Expression of
A,
f;
coherence
i + t is INT-Expression of A,f
-redefine func t - i -> INT-Expression of
A,
f;
coherence
t - i is INT-Expression of A,f
*redefine func t * i -> INT-Expression of
A,
f;
coherence
t * i is INT-Expression of A,f
end;
definition
let A be
Euclidean preIfWhileAlgebra;
let X be non
empty countable set ;
let T be
Subset of
(Funcs X,INT );
let f be
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
T;
let t1,
t2 be
INT-Expression of
A,
f;
-redefine func t1 - t2 -> INT-Expression of
A,
f;
coherence
t1 - t2 is INT-Expression of A,f
+redefine func t1 + t2 -> INT-Expression of
A,
f;
coherence
t1 + t2 is INT-Expression of A,f
by Def22;
(#)redefine func t1 (#) t2 -> INT-Expression of
A,
f;
coherence
t1 (#) t2 is INT-Expression of A,f
by Def22;
end;
definition
let A be
Euclidean preIfWhileAlgebra;
let X be non
empty countable set ;
let T be
Subset of
(Funcs X,INT );
let f be
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
T;
let t1,
t2 be
INT-Expression of
A,
f;
divredefine func t1 div t2 -> INT-Expression of
A,
f means :
Def29:
for
s being
Element of
Funcs X,
INT holds
it . s = (t1 . s) div (t2 . s);
coherence
t1 div t2 is INT-Expression of A,f
by Def22;
compatibility
for b1 being INT-Expression of A,f holds
( b1 = t1 div t2 iff for s being Element of Funcs X,INT holds b1 . s = (t1 . s) div (t2 . s) )
modredefine func t1 mod t2 -> INT-Expression of
A,
f means :
Def30:
for
s being
Element of
Funcs X,
INT holds
it . s = (t1 . s) mod (t2 . s);
coherence
t1 mod t2 is INT-Expression of A,f
by Def22;
compatibility
for b1 being INT-Expression of A,f holds
( b1 = t1 mod t2 iff for s being Element of Funcs X,INT holds b1 . s = (t1 . s) mod (t2 . s) )
leqredefine func leq t1,
t2 -> INT-Expression of
A,
f means :
Def31:
for
s being
Element of
Funcs X,
INT holds
it . s = IFGT (t1 . s),
(t2 . s),
0 ,1;
compatibility
for b1 being INT-Expression of A,f holds
( b1 = leq t1,t2 iff for s being Element of Funcs X,INT holds b1 . s = IFGT (t1 . s),(t2 . s),0 ,1 )
coherence
leq t1,t2 is INT-Expression of A,f
by Def22;
gtredefine func gt t1,
t2 -> INT-Expression of
A,
f means :
Def32:
for
s being
Element of
Funcs X,
INT holds
it . s = IFGT (t1 . s),
(t2 . s),1,
0 ;
coherence
gt t1,t2 is INT-Expression of A,f
by Def22;
compatibility
for b1 being INT-Expression of A,f holds
( b1 = gt t1,t2 iff for s being Element of Funcs X,INT holds b1 . s = IFGT (t1 . s),(t2 . s),1,0 )
end;
:: deftheorem Def29 defines div AOFA_I00:def 29 :
:: deftheorem Def30 defines mod AOFA_I00:def 30 :
:: deftheorem Def31 defines leq AOFA_I00:def 31 :
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
T being
Subset of
(Funcs X,INT ) for
f being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
T for
t1,
t2,
b7 being
INT-Expression of
A,
f holds
(
b7 = leq t1,
t2 iff for
s being
Element of
Funcs X,
INT holds
b7 . s = IFGT (t1 . s),
(t2 . s),
0 ,1 );
:: deftheorem Def32 defines gt AOFA_I00:def 32 :
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
T being
Subset of
(Funcs X,INT ) for
f being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
T for
t1,
t2,
b7 being
INT-Expression of
A,
f holds
(
b7 = gt t1,
t2 iff for
s being
Element of
Funcs X,
INT holds
b7 . s = IFGT (t1 . s),
(t2 . s),1,
0 );
definition
let A be
Euclidean preIfWhileAlgebra;
let X be non
empty countable set ;
let T be
Subset of
(Funcs X,INT );
let f be
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
T;
let t1,
t2 be
INT-Expression of
A,
f;
eqredefine func eq t1,
t2 -> INT-Expression of
A,
f means
for
s being
Element of
Funcs X,
INT holds
it . s = IFEQ (t1 . s),
(t2 . s),1,
0 ;
compatibility
for b1 being INT-Expression of A,f holds
( b1 = eq t1,t2 iff for s being Element of Funcs X,INT holds b1 . s = IFEQ (t1 . s),(t2 . s),1,0 )
coherence
eq t1,t2 is INT-Expression of A,f
end;
:: deftheorem defines eq AOFA_I00:def 33 :
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
T being
Subset of
(Funcs X,INT ) for
f being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
T for
t1,
t2,
b7 being
INT-Expression of
A,
f holds
(
b7 = eq t1,
t2 iff for
s being
Element of
Funcs X,
INT holds
b7 . s = IFEQ (t1 . s),
(t2 . s),1,
0 );
:: deftheorem defines . AOFA_I00:def 34 :
:: deftheorem defines ^ AOFA_I00:def 35 :
:: deftheorem defines . AOFA_I00:def 36 :
theorem Th22:
definition
let A be
Euclidean preIfWhileAlgebra;
let X be non
empty countable set ;
let T be
Subset of
(Funcs X,INT );
let f be
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
T;
let i be
integer number ;
func . i,
A,
f -> INT-Expression of
A,
f equals
. i,
X;
coherence
. i,X is INT-Expression of A,f
by Def22;
end;
:: deftheorem defines . AOFA_I00:def 37 :
definition
let A be
Euclidean preIfWhileAlgebra;
let X be non
empty countable set ;
let T be
Subset of
(Funcs X,INT );
let f be
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
T;
let v be
INT-Variable of
A,
f;
let t be
INT-Expression of
A,
f;
func v := t -> Element of
A equals
choose { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) ) } ;
coherence
choose { I where I is Element of A : ( I in ElementaryInstructions A & ( for s being Element of Funcs X,INT holds f . s,I = s +* (v . s),(t . s) ) ) } is Element of A
end;
:: deftheorem defines := AOFA_I00:def 38 :
theorem Th23:
:: deftheorem defines += AOFA_I00:def 39 :
:: deftheorem defines *= AOFA_I00:def 40 :
:: deftheorem defines := AOFA_I00:def 41 :
:: deftheorem defines := AOFA_I00:def 42 :
:: deftheorem defines := AOFA_I00:def 43 :
:: deftheorem defines := AOFA_I00:def 44 :
:: deftheorem defines := AOFA_I00:def 45 :
:: deftheorem defines swap AOFA_I00:def 46 :
:: deftheorem defines += AOFA_I00:def 47 :
:: deftheorem defines *= AOFA_I00:def 48 :
:: deftheorem defines %= AOFA_I00:def 49 :
:: deftheorem defines /= AOFA_I00:def 50 :
definition
let A be
Euclidean preIfWhileAlgebra;
let X be non
empty countable set ;
let T be
Subset of
(Funcs X,INT );
let f be
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
T;
let x be
Variable of
f;
let i be
integer number ;
func x += i -> absolutely-terminating Element of
A equals
x := ((. x) + i);
correctness
coherence
x := ((. x) + i) is absolutely-terminating Element of A;
;
func x *= i -> absolutely-terminating Element of
A equals
x := ((. x) * i);
correctness
coherence
x := ((. x) * i) is absolutely-terminating Element of A;
;
func x %= i -> absolutely-terminating Element of
A equals
x := ((. x) mod (. i,A,f));
correctness
coherence
x := ((. x) mod (. i,A,f)) is absolutely-terminating Element of A;
;
func x /= i -> absolutely-terminating Element of
A equals
x := ((. x) div (. i,A,f));
correctness
coherence
x := ((. x) div (. i,A,f)) is absolutely-terminating Element of A;
;
func x div i -> INT-Expression of
A,
f equals
(. x) div (. i,A,f);
correctness
coherence
(. x) div (. i,A,f) is INT-Expression of A,f;
;
end;
:: deftheorem defines += AOFA_I00:def 51 :
:: deftheorem defines *= AOFA_I00:def 52 :
:: deftheorem defines %= AOFA_I00:def 53 :
:: deftheorem defines /= AOFA_I00:def 54 :
:: deftheorem defines div AOFA_I00:def 55 :
:: deftheorem defines := AOFA_I00:def 56 :
:: deftheorem defines += AOFA_I00:def 57 :
:: deftheorem defines *= AOFA_I00:def 58 :
definition
let A be
Euclidean preIfWhileAlgebra;
let X be non
empty countable set ;
let b be
Element of
X;
let g be
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 ;
let t1 be
INT-Expression of
A,
g;
func t1 is_odd -> absolutely-terminating Element of
A equals
b := (t1 mod (. 2,A,g));
coherence
b := (t1 mod (. 2,A,g)) is absolutely-terminating Element of A
;
func t1 is_even -> absolutely-terminating Element of
A equals
b := ((t1 + 1) mod (. 2,A,g));
coherence
b := ((t1 + 1) mod (. 2,A,g)) is absolutely-terminating Element of A
;
let t2 be
INT-Expression of
A,
g;
func t1 leq t2 -> absolutely-terminating Element of
A equals
b := (leq t1,t2);
coherence
b := (leq t1,t2) is absolutely-terminating Element of A
;
func t1 gt t2 -> absolutely-terminating Element of
A equals
b := (gt t1,t2);
coherence
b := (gt t1,t2) is absolutely-terminating Element of A
;
func t1 eq t2 -> absolutely-terminating Element of
A equals
b := (eq t1,t2);
coherence
b := (eq t1,t2) is absolutely-terminating Element of A
;
end;
:: deftheorem defines is_odd AOFA_I00:def 59 :
:: deftheorem defines is_even AOFA_I00:def 60 :
:: deftheorem defines leq AOFA_I00:def 61 :
:: deftheorem defines gt AOFA_I00:def 62 :
:: deftheorem defines eq AOFA_I00:def 63 :
:: deftheorem defines leq AOFA_I00:def 64 :
:: deftheorem defines gt AOFA_I00:def 65 :
:: deftheorem defines is_odd AOFA_I00:def 66 :
:: deftheorem defines is_even AOFA_I00:def 67 :
:: deftheorem defines leq AOFA_I00:def 68 :
:: deftheorem defines gt AOFA_I00:def 69 :
definition
let A be
Euclidean preIfWhileAlgebra;
let X be non
empty countable set ;
let b be
Element of
X;
let g be
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 ;
let x be
Variable of
g;
let i be
integer number ;
func x leq i -> absolutely-terminating Element of
A equals
(. x) leq (. i,A,g);
coherence
(. x) leq (. i,A,g) is absolutely-terminating Element of A
;
func x geq i -> absolutely-terminating Element of
A equals
(. x) geq (. i,A,g);
coherence
(. x) geq (. i,A,g) is absolutely-terminating Element of A
;
func x gt i -> absolutely-terminating Element of
A equals
(. x) gt (. i,A,g);
coherence
(. x) gt (. i,A,g) is absolutely-terminating Element of A
;
func x lt i -> absolutely-terminating Element of
A equals
(. x) lt (. i,A,g);
coherence
(. x) lt (. i,A,g) is absolutely-terminating Element of A
;
func x / i -> INT-Expression of
A,
g equals
(. x) div (. i,A,g);
coherence
(. x) div (. i,A,g) is INT-Expression of A,g
;
end;
:: deftheorem defines leq AOFA_I00:def 70 :
:: deftheorem defines geq AOFA_I00:def 71 :
:: deftheorem defines gt AOFA_I00:def 72 :
:: deftheorem defines lt AOFA_I00:def 73 :
:: deftheorem defines / AOFA_I00:def 74 :
definition
let A be
Euclidean preIfWhileAlgebra;
let X be non
empty countable set ;
let T be
Subset of
(Funcs X,INT );
let f be
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
T;
let x1,
x2 be
Variable of
f;
func x1 += x2 -> absolutely-terminating Element of
A equals
x1 += (. x2);
coherence
x1 += (. x2) is absolutely-terminating Element of A
;
func x1 *= x2 -> absolutely-terminating Element of
A equals
x1 *= (. x2);
coherence
x1 *= (. x2) is absolutely-terminating Element of A
;
func x1 %= x2 -> absolutely-terminating Element of
A equals
x1 := ((. x1) mod (. x2));
coherence
x1 := ((. x1) mod (. x2)) is absolutely-terminating Element of A
;
func x1 /= x2 -> absolutely-terminating Element of
A equals
x1 := ((. x1) div (. x2));
coherence
x1 := ((. x1) div (. x2)) is absolutely-terminating Element of A
;
func x1 + x2 -> INT-Expression of
A,
f equals
(. x1) + (. x2);
coherence
(. x1) + (. x2) is INT-Expression of A,f
;
func x1 * x2 -> INT-Expression of
A,
f equals
(. x1) (#) (. x2);
coherence
(. x1) (#) (. x2) is INT-Expression of A,f
;
func x1 mod x2 -> INT-Expression of
A,
f equals
(. x1) mod (. x2);
coherence
(. x1) mod (. x2) is INT-Expression of A,f
;
func x1 div x2 -> INT-Expression of
A,
f equals
(. x1) div (. x2);
coherence
(. x1) div (. x2) is INT-Expression of A,f
;
end;
:: deftheorem defines += AOFA_I00:def 75 :
:: deftheorem defines *= AOFA_I00:def 76 :
:: deftheorem defines %= AOFA_I00:def 77 :
:: deftheorem defines /= AOFA_I00:def 78 :
:: deftheorem defines + AOFA_I00:def 79 :
:: deftheorem defines * AOFA_I00:def 80 :
:: deftheorem defines mod AOFA_I00:def 81 :
:: deftheorem defines div AOFA_I00:def 82 :
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
s being
Element of
Funcs X,
INT for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
x being
Variable of
g for
i being
integer number holds
( (
s . x <= i implies
(g . s,(x leq i)) . b = 1 ) & (
s . x > i implies
(g . s,(x leq i)) . b = 0 ) & (
s . x >= i implies
(g . s,(x geq i)) . b = 1 ) & (
s . x < i implies
(g . s,(x geq i)) . b = 0 ) & ( for
z being
Element of
X st
z <> b holds
(
(g . s,(x leq i)) . z = s . z &
(g . s,(x geq i)) . z = s . z ) ) )
theorem Th35:
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
s being
Element of
Funcs X,
INT for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
x,
y being
Variable of
g holds
( (
s . x <= s . y implies
(g . s,(x leq y)) . b = 1 ) & (
s . x > s . y implies
(g . s,(x leq y)) . b = 0 ) & ( for
z being
Element of
X st
z <> b holds
(g . s,(x leq y)) . z = s . z ) )
theorem
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
s being
Element of
Funcs X,
INT for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
x being
Variable of
g for
i being
integer number holds
( (
s . x <= i implies
g . s,
(x leq i) in (Funcs X,INT ) \ b,
0 ) & (
g . s,
(x leq i) in (Funcs X,INT ) \ b,
0 implies
s . x <= i ) & (
s . x >= i implies
g . s,
(x geq i) in (Funcs X,INT ) \ b,
0 ) & (
g . s,
(x geq i) in (Funcs X,INT ) \ b,
0 implies
s . x >= i ) )
theorem
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
s being
Element of
Funcs X,
INT for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
x,
y being
Variable of
g holds
( (
s . x <= s . y implies
g . s,
(x leq y) in (Funcs X,INT ) \ b,
0 ) & (
g . s,
(x leq y) in (Funcs X,INT ) \ b,
0 implies
s . x <= s . y ) & (
s . x >= s . y implies
g . s,
(x geq y) in (Funcs X,INT ) \ b,
0 ) & (
g . s,
(x geq y) in (Funcs X,INT ) \ b,
0 implies
s . x >= s . y ) )
theorem Th38:
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
s being
Element of
Funcs X,
INT for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
x being
Variable of
g for
i being
integer number holds
( (
s . x > i implies
(g . s,(x gt i)) . b = 1 ) & (
s . x <= i implies
(g . s,(x gt i)) . b = 0 ) & (
s . x < i implies
(g . s,(x lt i)) . b = 1 ) & (
s . x >= i implies
(g . s,(x lt i)) . b = 0 ) & ( for
z being
Element of
X st
z <> b holds
(
(g . s,(x gt i)) . z = s . z &
(g . s,(x lt i)) . z = s . z ) ) )
theorem Th39:
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
s being
Element of
Funcs X,
INT for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
x,
y being
Variable of
g holds
( (
s . x > s . y implies
(g . s,(x gt y)) . b = 1 ) & (
s . x <= s . y implies
(g . s,(x gt y)) . b = 0 ) & (
s . x < s . y implies
(g . s,(x lt y)) . b = 1 ) & (
s . x >= s . y implies
(g . s,(x lt y)) . b = 0 ) & ( for
z being
Element of
X st
z <> b holds
(
(g . s,(x gt y)) . z = s . z &
(g . s,(x lt y)) . z = s . z ) ) )
theorem Th40:
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
s being
Element of
Funcs X,
INT for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
x being
Variable of
g for
i being
integer number holds
( (
s . x > i implies
g . s,
(x gt i) in (Funcs X,INT ) \ b,
0 ) & (
g . s,
(x gt i) in (Funcs X,INT ) \ b,
0 implies
s . x > i ) & (
s . x < i implies
g . s,
(x lt i) in (Funcs X,INT ) \ b,
0 ) & (
g . s,
(x lt i) in (Funcs X,INT ) \ b,
0 implies
s . x < i ) )
theorem
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
s being
Element of
Funcs X,
INT for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
x,
y being
Variable of
g holds
( (
s . x > s . y implies
g . s,
(x gt y) in (Funcs X,INT ) \ b,
0 ) & (
g . s,
(x gt y) in (Funcs X,INT ) \ b,
0 implies
s . x > s . y ) & (
s . x < s . y implies
g . s,
(x lt y) in (Funcs X,INT ) \ b,
0 ) & (
g . s,
(x lt y) in (Funcs X,INT ) \ b,
0 implies
s . x < s . y ) )
theorem
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem
theorem Th48:
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
s being
Element of
Funcs X,
INT for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
t being
INT-Expression of
A,
g holds
(
(g . s,(t is_odd )) . b = (t . s) mod 2 &
(g . s,(t is_even )) . b = ((t . s) + 1) mod 2 & ( for
z being
Element of
X st
z <> b holds
(
(g . s,(t is_odd )) . z = s . z &
(g . s,(t is_even )) . z = s . z ) ) )
theorem Th49:
theorem Th50:
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
s being
Element of
Funcs X,
INT for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
t being
INT-Expression of
A,
g holds
( ( not
t . s is
even implies
g . s,
(t is_odd ) in (Funcs X,INT ) \ b,
0 ) & (
g . s,
(t is_odd ) in (Funcs X,INT ) \ b,
0 implies not
t . s is
even ) & (
t . s is
even implies
g . s,
(t is_even ) in (Funcs X,INT ) \ b,
0 ) & (
g . s,
(t is_even ) in (Funcs X,INT ) \ b,
0 implies
t . s is
even ) )
theorem
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
s being
Element of
Funcs X,
INT for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
x being
Variable of
g holds
( ( not
s . x is
even implies
g . s,
(x is_odd ) in (Funcs X,INT ) \ b,
0 ) & (
g . s,
(x is_odd ) in (Funcs X,INT ) \ b,
0 implies not
s . x is
even ) & (
s . x is
even implies
g . s,
(x is_even ) in (Funcs X,INT ) \ b,
0 ) & (
g . s,
(x is_even ) in (Funcs X,INT ) \ b,
0 implies
s . x is
even ) )
scheme
ForToIteration{
F1()
-> Euclidean preIfWhileAlgebra,
F2()
-> non
empty countable set ,
F3()
-> Element of
F2(),
F4()
-> Element of
F1(),
F5()
-> Element of
F1(),
F6()
-> Euclidean ExecutionFunction of
F1(),
Funcs F2(),
INT ,
(Funcs F2(),INT ) \ F3(),
0 ,
F7()
-> Variable of
F6(),
F8()
-> Variable of
F6(),
F9()
-> Element of
Funcs F2(),
INT ,
F10()
-> INT-Expression of
F1(),
F6(),
P1[
set ] } :
(
P1[
F6()
. F9(),
F5()] & (
F10()
. F9()
<= F9()
. F8() implies
(F6() . F9(),F5()) . F7()
= (F9() . F8()) + 1 ) & (
F10()
. F9()
> F9()
. F8() implies
(F6() . F9(),F5()) . F7()
= F10()
. F9() ) &
(F6() . F9(),F5()) . F8()
= F9()
. F8() )
provided
A1:
F5()
= for-do (F7() := F10()),
(F7() leq F8()),
(F7() += 1),
F4()
and A2:
P1[
F6()
. F9(),
(F7() := F10())]
and A3:
for
s being
Element of
Funcs F2(),
INT st
P1[
s] holds
(
P1[
F6()
. s,
(F4() \; (F7() += 1))] &
P1[
F6()
. s,
(F7() leq F8())] )
and A4:
for
s being
Element of
Funcs F2(),
INT st
P1[
s] holds
(
(F6() . s,F4()) . F7()
= s . F7() &
(F6() . s,F4()) . F8()
= s . F8() )
and A5:
(
F8()
<> F7() &
F8()
<> F3() &
F7()
<> F3() )
scheme
ForDowntoIteration{
F1()
-> Euclidean preIfWhileAlgebra,
F2()
-> non
empty countable set ,
F3()
-> Element of
F2(),
F4()
-> Element of
F1(),
F5()
-> Element of
F1(),
F6()
-> Euclidean ExecutionFunction of
F1(),
Funcs F2(),
INT ,
(Funcs F2(),INT ) \ F3(),
0 ,
F7()
-> Variable of
F6(),
F8()
-> Variable of
F6(),
F9()
-> Element of
Funcs F2(),
INT ,
F10()
-> INT-Expression of
F1(),
F6(),
P1[
set ] } :
(
P1[
F6()
. F9(),
F5()] & (
F10()
. F9()
>= F9()
. F8() implies
(F6() . F9(),F5()) . F7()
= (F9() . F8()) - 1 ) & (
F10()
. F9()
< F9()
. F8() implies
(F6() . F9(),F5()) . F7()
= F10()
. F9() ) &
(F6() . F9(),F5()) . F8()
= F9()
. F8() )
provided
A1:
F5()
= for-do (F7() := F10()),
((. F8()) leq (. F7())),
(F7() += (- 1)),
F4()
and A2:
P1[
F6()
. F9(),
(F7() := F10())]
and A3:
for
s being
Element of
Funcs F2(),
INT st
P1[
s] holds
(
P1[
F6()
. s,
(F4() \; (F7() += (- 1)))] &
P1[
F6()
. s,
(F8() leq F7())] )
and A4:
for
s being
Element of
Funcs F2(),
INT st
P1[
s] holds
(
(F6() . s,F4()) . F7()
= s . F7() &
(F6() . s,F4()) . F8()
= s . F8() )
and A5:
(
F8()
<> F7() &
F8()
<> F3() &
F7()
<> F3() )
begin
theorem Th52:
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
s being
Element of
Funcs X,
INT for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
I being
Element of
A for
i,
n being
Variable of
g st ex
d being
Function st
(
d . b = 0 &
d . n = 1 &
d . i = 2 ) & ( for
s being
Element of
Funcs X,
INT holds
(
(g . s,I) . n = s . n &
(g . s,I) . i = s . i ) ) holds
g iteration_terminates_for (I \; (i += 1)) \; (i leq n),
g . s,
(i leq n)
theorem Th53:
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
s being
Element of
Funcs X,
INT for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
P being
set for
I being
Element of
A for
i,
n being
Variable of
g st ex
d being
Function st
(
d . b = 0 &
d . n = 1 &
d . i = 2 ) & ( for
s being
Element of
Funcs X,
INT st
s in P holds
(
(g . s,I) . n = s . n &
(g . s,I) . i = s . i &
g . s,
I in P &
g . s,
(i leq n) in P &
g . s,
(i += 1) in P ) ) &
s in P holds
g iteration_terminates_for (I \; (i += 1)) \; (i leq n),
g . s,
(i leq n)
theorem Th54:
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
T being
Subset of
(Funcs X,INT ) for
f being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
T for
t being
INT-Expression of
A,
f for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
I being
Element of
A st
I is_terminating_wrt g holds
for
i,
n being
Variable of
g st ex
d being
Function st
(
d . b = 0 &
d . n = 1 &
d . i = 2 ) & ( for
s being
Element of
Funcs X,
INT holds
(
(g . s,I) . n = s . n &
(g . s,I) . i = s . i ) ) holds
for-do (i := t),
(i leq n),
(i += 1),
I is_terminating_wrt g
theorem
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
T being
Subset of
(Funcs X,INT ) for
f being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
T for
t being
INT-Expression of
A,
f for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
P being
set for
I being
Element of
A st
I is_terminating_wrt g,
P holds
for
i,
n being
Variable of
g st ex
d being
Function st
(
d . b = 0 &
d . n = 1 &
d . i = 2 ) & ( for
s being
Element of
Funcs X,
INT st
s in P holds
(
(g . s,I) . n = s . n &
(g . s,I) . i = s . i ) ) &
P is_invariant_wrt i := t,
g &
P is_invariant_wrt I,
g &
P is_invariant_wrt i leq n,
g &
P is_invariant_wrt i += 1,
g holds
for-do (i := t),
(i leq n),
(i += 1),
I is_terminating_wrt g,
P
begin
theorem
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
n,
s,
i being
Variable of
g st ex
d being
Function st
(
d . n = 1 &
d . s = 2 &
d . i = 3 &
d . b = 4 ) holds
(s := 1) \; (for-do (i := 2),(i leq n),(i += 1),(s *= i)) is_terminating_wrt g
theorem
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
n,
s,
i being
Variable of
g st ex
d being
Function st
(
d . n = 1 &
d . s = 2 &
d . i = 3 &
d . b = 4 ) holds
for
q being
Element of
Funcs X,
INT for
N being
natural number st
N = q . n holds
(g . q,((s := 1) \; (for-do (i := 2),(i leq n),(i += 1),(s *= i)))) . s = N !
theorem
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
x,
n,
s,
i being
Variable of
g st ex
d being
Function st
(
d . n = 1 &
d . s = 2 &
d . i = 3 &
d . b = 4 ) holds
(s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)) is_terminating_wrt g
theorem
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
x,
n,
s,
i being
Variable of
g st ex
d being
Function st
(
d . x = 0 &
d . n = 1 &
d . s = 2 &
d . i = 3 &
d . b = 4 ) holds
for
q being
Element of
Funcs X,
INT for
N being
natural number st
N = q . n holds
(g . q,((s := 1) \; (for-do (i := 1),(i leq n),(i += 1),(s *= x)))) . s = (q . x) |^ N
theorem
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
n,
x,
y,
z,
i being
Variable of
g st ex
d being
Function st
(
d . b = 0 &
d . n = 1 &
d . x = 2 &
d . y = 3 &
d . z = 4 &
d . i = 5 ) holds
((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))) is_terminating_wrt g
theorem
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
n,
x,
y,
z,
i being
Variable of
g st ex
d being
Function st
(
d . b = 0 &
d . n = 1 &
d . x = 2 &
d . y = 3 &
d . z = 4 &
d . i = 5 ) holds
for
s being
Element of
Funcs X,
INT for
N being
Element of
NAT st
N = s . n holds
(g . s,(((x := 0 ) \; (y := 1)) \; (for-do (i := 1),(i leq n),(i += 1),(((z := x) \; (x := y)) \; (y += z))))) . x = Fib N
Lm1:
for A being Euclidean preIfWhileAlgebra
for X being non empty countable set
for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0
for x, y, z being Variable of g st ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . z = 3 ) holds
for s being Element of Funcs X,INT holds
( (g . s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) . x = s . y & (g . s,((((z := x) \; (z %= y)) \; (x := y)) \; (y := z))) . y = (s . x) mod (s . y) & ( for n, m being Element of NAT holds
not ( m = s . y & ( s in (Funcs X,INT ) \ b,0 implies m > 0 ) & ( m > 0 implies s in (Funcs X,INT ) \ b,0 ) & not g iteration_terminates_for ((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) \; (y gt 0 ),s ) ) )
theorem
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
x,
y,
z being
Variable of
g st ex
d being
Function st
(
d . b = 0 &
d . x = 1 &
d . y = 2 &
d . z = 3 ) holds
while (y gt 0 ),
((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)) is_terminating_wrt g,
{ s where s is Element of Funcs X,INT : ( s . x > s . y & s . y >= 0 ) }
theorem
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
x,
y,
z being
Variable of
g st ex
d being
Function st
(
d . b = 0 &
d . x = 1 &
d . y = 2 &
d . z = 3 ) holds
for
s being
Element of
Funcs X,
INT for
n,
m being
Element of
NAT st
n = s . x &
m = s . y &
n > m holds
(g . s,(while (y gt 0 ),((((z := x) \; (z %= y)) \; (x := y)) \; (y := z)))) . x = n gcd m
Lm2:
for A being Euclidean preIfWhileAlgebra
for X being non empty countable set
for b being Element of X
for g being Euclidean ExecutionFunction of A, Funcs X,INT ,(Funcs X,INT ) \ b,0
for x, y, z being Variable of g st ex d being Function st
( d . b = 0 & d . x = 1 & d . y = 2 & d . z = 3 ) holds
for s being Element of Funcs X,INT holds
( (g . s,((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z))) . x = s . y & (g . s,((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z))) . y = abs ((s . x) - (s . y)) & ( for n, m being Element of NAT st n = s . x & m = s . y & ( s in (Funcs X,INT ) \ b,0 implies m > 0 ) & ( m > 0 implies s in (Funcs X,INT ) \ b,0 ) holds
g iteration_terminates_for ((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) \; (y gt 0 ),s ) )
theorem
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
x,
y,
z being
Variable of
g st ex
d being
Function st
(
d . b = 0 &
d . x = 1 &
d . y = 2 &
d . z = 3 ) holds
while (y gt 0 ),
((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)) is_terminating_wrt g,
{ s where s is Element of Funcs X,INT : ( s . x >= 0 & s . y >= 0 ) }
theorem
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
x,
y,
z being
Variable of
g st ex
d being
Function st
(
d . b = 0 &
d . x = 1 &
d . y = 2 &
d . z = 3 ) holds
for
s being
Element of
Funcs X,
INT for
n,
m being
Element of
NAT st
n = s . x &
m = s . y &
n > 0 holds
(g . s,(while (y gt 0 ),((((z := ((. x) - (. y))) \; (if-then (z lt 0 ),(z *= (- 1)))) \; (x := y)) \; (y := z)))) . x = n gcd m
theorem
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
x,
y,
m being
Variable of
g st ex
d being
Function st
(
d . b = 0 &
d . x = 1 &
d . y = 2 &
d . m = 3 ) holds
(y := 1) \; (while (m gt 0 ),(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))) is_terminating_wrt g,
{ s where s is Element of Funcs X,INT : s . m >= 0 }
theorem
for
A being
Euclidean preIfWhileAlgebra for
X being non
empty countable set for
b being
Element of
X for
g being
Euclidean ExecutionFunction of
A,
Funcs X,
INT ,
(Funcs X,INT ) \ b,
0 for
x,
y,
m being
Variable of
g st ex
d being
Function st
(
d . b = 0 &
d . x = 1 &
d . y = 2 &
d . m = 3 ) holds
for
s being
Element of
Funcs X,
INT for
n being
Nat st
n = s . m holds
(g . s,((y := 1) \; (while (m gt 0 ),(((if-then (m is_odd ),(y *= x)) \; (m /= 2)) \; (x *= x))))) . y = (s . x) |^ n