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 :
for F being non empty functional set
for x, f being set holds F \ (x,f) = { g where g is Element of F : g . x <> f } ;
theorem Th2:
:: deftheorem Def2 defines Variable AOFA_I00:def 2 :
for X, Y, Z being set
for f being Function of [:(Funcs (X,INT)),Y:],Z
for b5 being Element of X holds
( b5 is Variable of f iff verum );
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 :
for t1, t2, b3 being integer-yielding Function holds
( b3 = t1 div t2 iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds
b3 . s = (t1 . s) div (t2 . s) ) ) );
:: deftheorem Def4 defines mod AOFA_I00:def 4 :
for t1, t2, b3 being integer-yielding Function holds
( b3 = t1 mod t2 iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds
b3 . s = (t1 . s) mod (t2 . s) ) ) );
:: deftheorem Def5 defines leq AOFA_I00:def 5 :
for t1, t2, b3 being integer-yielding Function holds
( b3 = leq (t1,t2) iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds
b3 . s = IFGT ((t1 . s),(t2 . s),0,1) ) ) );
:: deftheorem Def6 defines gt AOFA_I00:def 6 :
for t1, t2, b3 being integer-yielding Function holds
( b3 = gt (t1,t2) iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds
b3 . s = IFGT ((t1 . s),(t2 . s),1,0) ) ) );
:: deftheorem Def7 defines eq AOFA_I00:def 7 :
for t1, t2, b3 being integer-yielding Function holds
( b3 = eq (t1,t2) iff ( dom b3 = (dom t1) /\ (dom t2) & ( for s being set st s in dom b3 holds
b3 . s = IFEQ ((t1 . s),(t2 . s),1,0) ) ) );
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 :
for X being non empty set
for f being Function of X,INT
for x being integer number
for b4 being Function of X,INT holds
( b4 = f + x iff for s being Element of X holds b4 . s = (f . s) + x );
:: deftheorem defines - AOFA_I00:def 9 :
for X being non empty set
for f being Function of X,INT
for x being integer number
for b4 being Function of X,INT holds
( b4 = f - x iff for s being Element of X holds b4 . s = (f . s) - x );
:: deftheorem Def10 defines * AOFA_I00:def 10 :
for X being non empty set
for f being Function of X,INT
for x being integer number
for b4 being Function of X,INT holds
( b4 = f * x iff for s being Element of X holds b4 . s = (f . s) * x );
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 :
for X being non empty set
for t1, t2, b4 being Function of X,INT holds
( b4 = t1 - t2 iff for s being Element of X holds b4 . s = (t1 . s) - (t2 . s) );
:: deftheorem defines + AOFA_I00:def 12 :
for X being non empty set
for t1, t2, b4 being Function of X,INT holds
( b4 = t1 + t2 iff for s being Element of X holds b4 . s = (t1 . s) + (t2 . s) );
:: deftheorem Def13 defines ** AOFA_I00:def 13 :
for N being set
for v, f, b4 being Function holds
( b4 = v ** (f,N) iff ( ex Y being set st
( ( for y being set holds
( y in Y iff ex h being Function st
( h in dom v & y in rng h ) ) ) & ( for a being set holds
( a in dom b4 iff ( a in Funcs (N,Y) & ex g being Function st
( a = g & g * f in dom v ) ) ) ) ) & ( for g being Function st g in dom b4 holds
b4 . g = v . (g * f) ) ) );
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 :
for A being preIfWhileAlgebra
for I being Element of A
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
( I is_assignment_wrt A,X,f iff ( I in ElementaryInstructions A & ex v being INT-Variable of X ex t being INT-Expression of X st
for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) );
:: deftheorem Def15 defines form_assignment_wrt AOFA_I00:def 15 :
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
for v being INT-Variable of X
for t being INT-Expression of X holds
( v,t form_assignment_wrt f iff ex I being Element of A st
( I in ElementaryInstructions A & ( for s being Element of Funcs (X,INT) holds f . (s,I) = s +* ((v . s),(t . s)) ) ) );
:: deftheorem defines INT-Variable AOFA_I00:def 16 :
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 st ex I being Element of A st I is_assignment_wrt A,X,f holds
for b5 being INT-Variable of X holds
( b5 is INT-Variable of A,f iff ex t being INT-Expression of X st b5,t form_assignment_wrt f );
:: deftheorem defines INT-Expression AOFA_I00:def 17 :
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 st ex I being Element of A st I is_assignment_wrt A,X,f holds
for b5 being INT-Expression of X holds
( b5 is INT-Expression of A,f iff ex v being INT-Variable of X st v,b5 form_assignment_wrt f );
:: deftheorem Def18 defines . AOFA_I00:def 18 :
for X being non empty set
for x being Element of X
for b3 being INT-Expression of X holds
( b3 = . x iff for s being Element of Funcs (X,INT) holds b3 . s = s . x );
:: deftheorem Def19 defines . AOFA_I00:def 19 :
for X being non empty set
for v being INT-Variable of X
for b3 being INT-Expression of X holds
( b3 = . v iff for s being Element of Funcs (X,INT) holds b3 . s = s . (v . s) );
:: deftheorem defines ^ AOFA_I00:def 20 :
for X being non empty set
for x being Element of X holds ^ x = (Funcs (X,INT)) --> x;
theorem
:: deftheorem defines . AOFA_I00:def 21 :
for X being non empty set
for i being integer number holds . (i,X) = (Funcs (X,INT)) --> i;
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 :
for A being preIfWhileAlgebra holds
( A is Euclidean iff for X being non empty countable set
for T being Subset of (Funcs (X,INT)) ex f being ExecutionFunction of A, Funcs (X,INT),T st f is Euclidean );
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 :
INT-ElemIns = [:(Funcs ((Funcs (NAT,INT)),NAT)),(Funcs ((Funcs (NAT,INT)),INT)):];
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 :
for X being non empty set holds INT-ElemIns X = [:(Funcs ((Funcs (X,INT)),X)),(Funcs ((Funcs (X,INT)),INT)):];
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:
registration
let A be
Euclidean preIfWhileAlgebra;
let X be non
empty countable set ;
let T be
Subset of
(Funcs (X,INT));
cluster non
empty Relation-like [:(Funcs (X,INT)), the carrier of A:] -defined Funcs (
X,
INT)
-valued Function-like V26(
[:(Funcs (X,INT)), the carrier of A:])
quasi_total Function-yielding complying_with_empty-instruction complying_with_catenation Euclidean ExecutionFunction of
A,
Funcs (
X,
INT),
T;
existence
ex b1 being ExecutionFunction of A, Funcs (X,INT),T st b1 is Euclidean
by Def23;
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 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 :
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 = t1 div t2 iff for s being Element of Funcs (X,INT) holds b7 . s = (t1 . s) div (t2 . s) );
:: deftheorem Def30 defines mod AOFA_I00:def 30 :
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 = t1 mod t2 iff for s being Element of Funcs (X,INT) holds b7 . s = (t1 . s) mod (t2 . s) );
:: 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 :
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 v being INT-Variable of A,f holds . v = . v;
:: deftheorem defines ^ AOFA_I00:def 35 :
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 x being Element of X holds x ^ (A,f) = ^ x;
:: deftheorem defines . AOFA_I00:def 36 :
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 x being Variable of f holds . x = . (^ x);
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 :
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 i being integer number holds . (i,A,f) = . (i,X);
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 :
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 v being INT-Variable of A,f
for t being INT-Expression of A,f holds v := t = 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)) ) ) } ;
theorem Th23:
:: deftheorem defines += AOFA_I00:def 39 :
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 v being INT-Variable of A,f
for t being INT-Expression of A,f holds v += t = v := ((. v) + t);
:: deftheorem defines *= AOFA_I00:def 40 :
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 v being INT-Variable of A,f
for t being INT-Expression of A,f holds v *= t = v := ((. v) (#) t);
:: deftheorem defines := AOFA_I00:def 41 :
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 x being Element of X
for t being INT-Expression of A,f holds x := t = (x ^ (A,f)) := t;
:: deftheorem defines := AOFA_I00:def 42 :
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 x being Element of X
for y being Variable of f holds x := y = x := (. y);
:: deftheorem defines := AOFA_I00:def 43 :
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 x being Element of X
for v being INT-Variable of A,f holds x := v = x := (. v);
:: deftheorem defines := AOFA_I00:def 44 :
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 v, w being INT-Variable of A,f holds v := w = v := (. w);
:: deftheorem defines := AOFA_I00:def 45 :
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 x being Variable of f
for i being integer number holds x := i = x := (. (i,A,f));
:: deftheorem defines swap AOFA_I00:def 46 :
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 v1, v2 being INT-Variable of A,f
for x being Variable of f holds swap (v1,x,v2) = ((x := v1) \; (v1 := v2)) \; (v2 := (. x));
:: deftheorem defines += AOFA_I00:def 47 :
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 x being Variable of f
for t being INT-Expression of A,f holds x += t = x := ((. x) + t);
:: deftheorem defines *= AOFA_I00:def 48 :
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 x being Variable of f
for t being INT-Expression of A,f holds x *= t = x := ((. x) (#) t);
:: deftheorem defines %= AOFA_I00:def 49 :
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 x being Variable of f
for t being INT-Expression of A,f holds x %= t = x := ((. x) mod t);
:: deftheorem defines /= AOFA_I00:def 50 :
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 x being Variable of f
for t being INT-Expression of A,f holds x /= t = x := ((. x) div t);
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 :
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 x being Variable of f
for i being integer number holds x += i = x := ((. x) + i);
:: deftheorem defines *= AOFA_I00:def 52 :
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 x being Variable of f
for i being integer number holds x *= i = x := ((. x) * i);
:: deftheorem defines %= AOFA_I00:def 53 :
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 x being Variable of f
for i being integer number holds x %= i = x := ((. x) mod (. (i,A,f)));
:: deftheorem defines /= AOFA_I00:def 54 :
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 x being Variable of f
for i being integer number holds x /= i = x := ((. x) div (. (i,A,f)));
:: deftheorem defines div AOFA_I00:def 55 :
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 x being Variable of f
for i being integer number holds x div i = (. x) div (. (i,A,f));
:: deftheorem defines := AOFA_I00:def 56 :
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 v being INT-Variable of A,f
for i being integer number holds v := i = v := (. (i,A,f));
:: deftheorem defines += AOFA_I00:def 57 :
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 v being INT-Variable of A,f
for i being integer number holds v += i = v := ((. v) + i);
:: deftheorem defines *= AOFA_I00:def 58 :
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 v being INT-Variable of A,f
for i being integer number holds v *= i = v := ((. v) * i);
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 :
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 t1 being INT-Expression of A,g holds t1 is_odd = b := (t1 mod (. (2,A,g)));
:: deftheorem defines is_even AOFA_I00:def 60 :
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 t1 being INT-Expression of A,g holds t1 is_even = b := ((t1 + 1) mod (. (2,A,g)));
:: deftheorem defines leq AOFA_I00:def 61 :
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 t1, t2 being INT-Expression of A,g holds t1 leq t2 = b := (leq (t1,t2));
:: deftheorem defines gt AOFA_I00:def 62 :
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 t1, t2 being INT-Expression of A,g holds t1 gt t2 = b := (gt (t1,t2));
:: deftheorem defines eq AOFA_I00:def 63 :
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 t1, t2 being INT-Expression of A,g holds t1 eq t2 = b := (eq (t1,t2));
:: deftheorem defines leq AOFA_I00:def 64 :
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 v1, v2 being INT-Variable of A,g holds v1 leq v2 = (. v1) leq (. v2);
:: deftheorem defines gt AOFA_I00:def 65 :
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 v1, v2 being INT-Variable of A,g holds v1 gt v2 = (. v1) gt (. v2);
:: deftheorem defines is_odd AOFA_I00:def 66 :
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 x1 being Variable of g holds x1 is_odd = (. x1) is_odd ;
:: deftheorem defines is_even AOFA_I00:def 67 :
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 x1 being Variable of g holds x1 is_even = (. x1) is_even ;
:: deftheorem defines leq AOFA_I00:def 68 :
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 x1, x2 being Variable of g holds x1 leq x2 = (. x1) leq (. x2);
:: deftheorem defines gt AOFA_I00:def 69 :
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 x1, x2 being Variable of g holds x1 gt x2 = (. x1) gt (. x2);
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 :
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 being Variable of g
for i being integer number holds x leq i = (. x) leq (. (i,A,g));
:: deftheorem defines geq AOFA_I00:def 71 :
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 being Variable of g
for i being integer number holds x geq i = (. x) geq (. (i,A,g));
:: deftheorem defines gt AOFA_I00:def 72 :
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 being Variable of g
for i being integer number holds x gt i = (. x) gt (. (i,A,g));
:: deftheorem defines lt AOFA_I00:def 73 :
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 being Variable of g
for i being integer number holds x lt i = (. x) lt (. (i,A,g));
:: deftheorem defines / AOFA_I00:def 74 :
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 being Variable of g
for i being integer number holds x / i = (. x) div (. (i,A,g));
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 :
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 x1, x2 being Variable of f holds x1 += x2 = x1 += (. x2);
:: deftheorem defines *= AOFA_I00:def 76 :
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 x1, x2 being Variable of f holds x1 *= x2 = x1 *= (. x2);
:: deftheorem defines %= AOFA_I00:def 77 :
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 x1, x2 being Variable of f holds x1 %= x2 = x1 := ((. x1) mod (. x2));
:: deftheorem defines /= AOFA_I00:def 78 :
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 x1, x2 being Variable of f holds x1 /= x2 = x1 := ((. x1) div (. x2));
:: deftheorem defines + AOFA_I00:def 79 :
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 x1, x2 being Variable of f holds x1 + x2 = (. x1) + (. x2);
:: deftheorem defines * AOFA_I00:def 80 :
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 x1, x2 being Variable of f holds x1 * x2 = (. x1) (#) (. x2);
:: deftheorem defines mod AOFA_I00:def 81 :
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 x1, x2 being Variable of f holds x1 mod x2 = (. x1) mod (. x2);
:: deftheorem defines div AOFA_I00:def 82 :
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 x1, x2 being Variable of f holds x1 div x2 = (. x1) div (. x2);
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