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 )
definition
let t1,
t2 be
INT -valued Function;
correctness
existence
ex b1 being INT -valued 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 INT -valued 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;
correctness
existence
ex b1 being INT -valued 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 INT -valued 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;
correctness
existence
ex b1 being INT -valued 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 INT -valued 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;
correctness
existence
ex b1 being INT -valued 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 INT -valued 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;
correctness
existence
ex b1 being INT -valued 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 INT -valued 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;
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;
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;
begin
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 ) ) ) );
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 ;
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)) );
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;
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) )
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) )
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;
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 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;
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) );
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 ;
correctness
coherence
x := ((. x) + i) is absolutely-terminating Element of A;
;
correctness
coherence
x := ((. x) * i) is absolutely-terminating Element of A;
;
correctness
coherence
x := ((. x) mod (. (i,A,f))) is absolutely-terminating Element of A;
;
correctness
coherence
x := ((. x) div (. (i,A,f))) is absolutely-terminating Element of A;
;
correctness
coherence
(. x) div (. (i,A,f)) is INT-Expression of A,f;
;
end;
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;
coherence
b := (t1 mod (. (2,A,g))) is absolutely-terminating Element of A
;
coherence
b := ((t1 + 1) mod (. (2,A,g))) is absolutely-terminating Element of A
;
let t2 be
INT-Expression of
A,
g;
coherence
b := (leq (t1,t2)) is absolutely-terminating Element of A
;
coherence
b := (gt (t1,t2)) is absolutely-terminating Element of A
;
coherence
b := (eq (t1,t2)) is absolutely-terminating Element of A
;
end;
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 ;
coherence
(. x) leq (. (i,A,g)) is absolutely-terminating Element of A
;
coherence
(. x) geq (. (i,A,g)) is absolutely-terminating Element of A
;
coherence
(. x) gt (. (i,A,g)) is absolutely-terminating Element of A
;
coherence
(. x) lt (. (i,A,g)) is absolutely-terminating Element of A
;
coherence
(. x) div (. (i,A,g)) is INT-Expression of A,g
;
end;
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 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 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
( (
t . s is
odd implies
g . (
s,
(t is_odd))
in (Funcs (X,INT)) \ (
b,
0) ) & (
g . (
s,
(t is_odd))
in (Funcs (X,INT)) \ (
b,
0) implies
t . s is
odd ) & (
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
( (
s . x is
odd implies
g . (
s,
(x is_odd))
in (Funcs (X,INT)) \ (
b,
0) ) & (
g . (
s,
(x is_odd))
in (Funcs (X,INT)) \ (
b,
0) implies
s . x is
odd ) & (
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
Nat 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
Nat 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
:: to suggest that Euclid algoritm could be annotated
:: in quite natural way (all needed expressions are allowed).