:: Mizar Analysis of Algorithms: Algorithms over Integers
:: by Grzegorz Bancerek
::
:: Received March 18, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, FUNCT_1, FUNCOP_1, RELAT_1, AOFA_000, FUNCT_4, XBOOLE_0,
SUBSET_1, TARSKI, ZFMISC_1, FUNCT_2, ZF_LANG, VALUED_0, VALUED_1, INT_1,
XXREAL_0, CARD_1, ARYTM_3, ARYTM_1, FINSET_1, ORDINAL2, MEMBER_1, CARD_3,
NAT_1, POWER, ORDINAL4, EUCLMETR, FREEALG, TREES_4, LANG1, MCART_1,
STRUCT_0, GRAPHSP, ABIAN, FUNCT_7, REALSET1, NEWTON, PRE_FF, INT_2,
COMPLEX1, AOFA_I00, REAL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, MCART_1, ORDINAL1,
RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSET_1, LANG1, BINOP_1,
CARD_1, CARD_2, CARD_3, VALUED_0, PRE_FF, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, POWER, INT_1, INT_2, NAT_1, NAT_D, NEWTON, ABIAN, FUNCOP_1,
FUNCT_4, FUNCT_7, STRUCT_0, FREEALG, TREES_4, AOFA_000, VALUED_1;
constructors REAL_1, BORSUK_1, PREPOWER, POWER, NAT_D, NEWTON, ABIAN,
SQUARE_1, PRE_FF, WSIERP_1, WELLORD2, CARD_2, CAT_2, AOFA_000, XTUPLE_0,
FUNCT_4;
registrations RELSET_1, FUNCT_1, FUNCOP_1, FUNCT_2, NUMBERS, NAT_1, STRUCT_0,
FREEALG, INT_1, CARD_1, CARD_3, VALUED_0, VALUED_1, MEMBERED, XREAL_0,
XCMPLX_0, XXREAL_0, XBOOLE_0, FINSET_1, POWER, AOFA_000, ABIAN, XTUPLE_0,
ORDINAL1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, AOFA_000;
equalities XCMPLX_0, CARD_2, FREEALG, BINOP_1, AOFA_000, FUNCOP_1, VALUED_1;
expansions TARSKI, FUNCT_1, FUNCT_2, AOFA_000;
theorems XBOOLE_1, ZFMISC_1, RELAT_1, FUNCT_2, FUNCOP_1, TARSKI, NEWTON,
XREAL_1, INT_1, FUNCT_7, NAT_1, ORDINAL1, FUNCT_4, FREEALG, PRE_FF,
INT_2, ABSVALUE, WSIERP_1, TREES_4, NUMBERS, FUNCT_1, CARD_2, CARD_1,
WELLORD2, FUNCT_5, AOFA_000, XXREAL_0, POWER, FIB_NUM2, ORDINAL3, NAT_D,
PREPOWER, VALUED_1, CARD_3, XTUPLE_0, SUBSET_1;
schemes FUNCT_1, FUNCT_2, XBOOLE_0, AOFA_000, TARSKI, CLASSES1;
begin :: Preliminaries
theorem Th1:
for x,y,z,a,b,c being set st a <> b & b <> c & c <> a ex f being
Function st f.a = x & f.b = y & f.c = z
proof
let x,y,z,a,b,c be set such that
A1: a <> b and
A2: b <> c and
A3: c <> a;
set fb = b.-->y;
A5: a nin dom fb by A1,TARSKI:def 1;
A6: b in dom fb by TARSKI:def 1;
set fc = c.-->z;
set fa = a.-->x;
take f = fa+*fb+*fc;
a nin dom fc by A3,TARSKI:def 1;
hence f.a = (fa+*fb).a by FUNCT_4:11
.= fa.a by A5,FUNCT_4:11
.= x by FUNCOP_1:72;
b nin dom fc by A2,TARSKI:def 1;
hence f.b = (fa+*fb).b by FUNCT_4:11
.= fb.b by A6,FUNCT_4:13
.= y by FUNCOP_1:72;
c in dom fc by TARSKI:def 1;
hence f.c = fc.c by FUNCT_4:13
.= z by FUNCOP_1:72;
end;
definition
let F be non empty functional set;
let x be set;
let f be set;
func F\(x,f) -> Subset of F equals
{g where g is Element of F: g.x <> f};
coherence
proof
set X = {g where g is Element of F: g.x <> f};
X c= F
proof
let a be object;
assume a in X;
then ex g being Element of F st g = a & g.x <> f;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th2:
for F being non empty functional set, x,y be set, g being Element
of F holds g in F\(x,y) iff g.x <> y
proof
let F be non empty functional set;
let x,y be set;
let g be Element of F;
g in F\(x,y) iff ex f being Element of F st g = f & f.x <> y;
hence thesis;
end;
definition
let X be set;
let Y,Z be set;
let f be Function of [:Funcs(X,INT),Y:],Z;
mode Variable of f -> Element of X means
: Def2:
not contradiction;
existence;
end;
notation
let f be real-valued Function;
let x be Real;
synonym f*x for x(#)f;
end;
definition
let t1,t2 be INT-valued Function;
func t1 div t2 -> INT-valued Function means
: Def3:
dom it = (dom t1) /\ (dom t2) &
for s being object st s in dom it holds it.s = (t1.s) div (t2.s);
correctness
proof
deffunc F(object) = (t1.$1) div (t2.$1);
consider f being Function such that
A1: dom f = (dom t1) /\ (dom t2) & for x being object st x in (dom t1) /\
(dom t2) holds f.x = F(x) from FUNCT_1:sch 3;
f is INT-valued
proof
let y be object;
assume y in rng f;
then consider x being object such that
A2: x in dom f and
A3: f.x = y by FUNCT_1:def 3;
f.x = F(x) by A1,A2;
hence thesis by A3,INT_1:def 2;
end;
hence ex f being INT-valued Function st dom f = (dom t1)/\(dom t2) &
for x being object st x in dom f holds f.x = F(x) by A1;
let f1,f2 be INT-valued Function such that
A4: dom f1 = (dom t1) /\ dom t2 and
A5: for s being object st s in dom f1 holds f1.s = F(s) and
A6: dom f2 = (dom t1) /\ dom t2 and
A7: for s being object st s in dom f2 holds f2.s = F(s);
now
let s be object;
assume
A8: s in (dom t1) /\ dom t2;
hence f1.s = F(s) by A4,A5
.= f2.s by A6,A7,A8;
end;
hence thesis by A4,A6;
end;
func t1 mod t2 -> INT-valued Function means
: Def4:
dom it = (dom t1) /\ (dom t2) &
for s being object st s in dom it holds it.s = (t1.s) mod (t2.s);
correctness
proof
deffunc F(object) = (t1.$1) mod (t2.$1);
consider f being Function such that
A9: dom f = (dom t1) /\ (dom t2) & for x being object st x in (dom t1)
/\ (dom t2) holds f.x = F(x) from FUNCT_1:sch 3;
f is INT-valued
proof
let y be object;
assume y in rng f;
then consider x being object such that
A10: x in dom f and
A11: f.x = y by FUNCT_1:def 3;
f.x = F(x) by A9,A10;
hence thesis by A11,INT_1:def 2;
end;
hence ex f being INT-valued Function st dom f = (dom t1)/\(dom t2) &
for x being object st x in dom f holds f.x = F(x) by A9;
let f1,f2 be INT-valued Function such that
A12: dom f1 = (dom t1) /\ dom t2 and
A13: for s being object st s in dom f1 holds f1.s = F(s) and
A14: dom f2 = (dom t1) /\ dom t2 and
A15: for s being object st s in dom f2 holds f2.s = F(s);
now
let s be object;
assume
A16: s in (dom t1) /\ dom t2;
hence f1.s = F(s) by A12,A13
.= f2.s by A14,A15,A16;
end;
hence thesis by A12,A14;
end;
func leq(t1,t2) -> INT-valued Function means
: Def5:
dom it = (dom t1) /\ (dom t2) &
for s being object st s in dom it holds it.s = IFGT(t1.s,t2.s,0,1);
correctness
proof
deffunc F(object) = IFGT(t1.$1,t2.$1,0,1);
consider f being Function such that
A17: dom f = (dom t1) /\ (dom t2) & for x being object st x in (dom t1)
/\ (dom t2) holds f.x = F(x) from FUNCT_1:sch 3;
f is INT-valued
proof
let y be object;
assume y in rng f;
then consider x being object such that
A18: x in dom f and
A19: f.x = y by FUNCT_1:def 3;
f.x = F(x) by A17,A18;
hence thesis by A19,INT_1:def 2;
end;
hence ex f being INT-valued Function st dom f = (dom t1)/\(dom t2) &
for x being object st x in dom f holds f.x = F(x) by A17;
let f1,f2 be INT-valued Function such that
A20: dom f1 = (dom t1) /\ dom t2 and
A21: for s being object st s in dom f1 holds f1.s = F(s) and
A22: dom f2 = (dom t1) /\ dom t2 and
A23: for s being object st s in dom f2 holds f2.s = F(s);
now
let s be object;
assume
A24: s in (dom t1) /\ dom t2;
hence f1.s = F(s) by A20,A21
.= f2.s by A22,A23,A24;
end;
hence thesis by A20,A22;
end;
func gt(t1,t2) -> INT-valued Function means
: Def6:
dom it = (dom t1) /\ (dom t2) &
for s being object st s in dom it holds it.s = IFGT(t1.s,t2.s,1,0);
correctness
proof
deffunc F(object) = IFGT(t1.$1,t2.$1,1,0);
consider f being Function such that
A25: dom f = (dom t1) /\ (dom t2) & for x being object st x in (dom t1)
/\ (dom t2) holds f.x = F(x) from FUNCT_1:sch 3;
f is INT-valued
proof
let y be object;
assume y in rng f;
then consider x being object such that
A26: x in dom f and
A27: f.x = y by FUNCT_1:def 3;
f.x = F(x) by A25,A26;
hence thesis by A27,INT_1:def 2;
end;
hence ex f being INT-valued Function st dom f = (dom t1)/\(dom t2) &
for x being object st x in dom f holds f.x = F(x) by A25;
let f1,f2 be INT-valued Function such that
A28: dom f1 = (dom t1) /\ dom t2 and
A29: for s being object st s in dom f1 holds f1.s = F(s) and
A30: dom f2 = (dom t1) /\ dom t2 and
A31: for s being object st s in dom f2 holds f2.s = F(s);
now
let s be object;
assume
A32: s in (dom t1) /\ dom t2;
hence f1.s = F(s) by A28,A29
.= f2.s by A30,A31,A32;
end;
hence thesis by A28,A30;
end;
func eq(t1,t2) -> INT-valued Function means
: Def7:
dom it = (dom t1) /\ (dom t2) &
for s being object st s in dom it holds it.s = IFEQ(t1.s,t2.s,1,0);
correctness
proof
deffunc F(object) = IFEQ(t1.$1,t2.$1,1,0);
consider f being Function such that
A33: dom f = (dom t1) /\ (dom t2) & for x being object st x in (dom t1)
/\ (dom t2) holds f.x = F(x) from FUNCT_1:sch 3;
f is INT-valued
proof
let y be object;
assume y in rng f;
then consider x being object such that
A34: x in dom f and
A35: f.x = y by FUNCT_1:def 3;
f.x = F(x) by A33,A34;
hence thesis by A35,INT_1:def 2;
end;
hence ex f being INT-valued Function st dom f = (dom t1)/\(dom t2) &
for x being object st x in dom f holds f.x = F(x) by A33;
let f1,f2 be INT-valued Function such that
A36: dom f1 = (dom t1) /\ dom t2 and
A37: for s being object st s in dom f1 holds f1.s = F(s) and
A38: dom f2 = (dom t1) /\ dom t2 and
A39: for s being object st s in dom f2 holds f2.s = F(s);
now
let s be object;
assume
A40: s in (dom t1) /\ dom t2;
hence f1.s = F(s) by A36,A37
.= f2.s by A38,A39,A40;
end;
hence thesis by A36,A38;
end;
end;
definition
let X be non empty set;
let f be Function of X, INT;
let x be Integer;
redefine func f+x -> Function of X, INT means :: redefines + (VALUED_1, synonym) → + (VALUED_1, definition)
: Def8:
for s being Element of X holds it.s = f.s+x;
compatibility
proof
let ti be Function of X, INT;
A1: dom f = X by FUNCT_2:def 1;
dom (f+x) = dom f by VALUED_1:def 2;
hence ti = f+x implies for s being Element of X holds ti.s = f.s+x by A1,
VALUED_1:def 2;
A2: dom ti = X by FUNCT_2:def 1;
assume for s being Element of X holds ti.s = f.s+x;
then for s being object st s in X holds ti.s = x+f.s;
hence thesis by A1,A2,VALUED_1:def 2;
end;
coherence
proof
x+f is Function of X, INT;
hence thesis;
end;
redefine func f-x -> Function of X, INT means :: redefines - (VALUED_1, definition)
for s being Element of X holds it.s = f .s-x;
compatibility
proof
let ti be Function of X, INT;
A3: dom ti = X by FUNCT_2:def 1;
A4: dom f = X by FUNCT_2:def 1;
hence ti = f-x implies for s being Element of X holds ti.s = f.s-x by
VALUED_1:3;
assume
A5: for s being Element of X holds ti.s = f.s-x;
A6: now
let s be object;
assume
A7: s in dom ti;
hence ti.s = f.s-x by A5
.= (f-x).s by A4,A7,VALUED_1:3;
end;
thus ti = f-x by A3,A6;
end;
coherence
proof
thus f-x is Function of X, INT;
end;
redefine func f*x -> Function of X, INT means :: redefines * (AOFA_I00, synonym) → (#) (VALUED_1, definition)
: Def10:
for s being Element of X holds it.s = f.s*x;
compatibility
proof
let ti be Function of X, INT;
A8: dom (f*x) = dom f by VALUED_1:def 5;
A9: dom f = X by FUNCT_2:def 1;
hence ti = f*x implies for s being Element of X holds ti.s = f.s*x by A8,
VALUED_1:def 5;
A10: dom ti = X by FUNCT_2:def 1;
assume for s being Element of X holds ti.s = f.s*x;
then for s being object st s in dom (f*x) holds ti.s = x*f.s;
hence thesis by A8,A9,A10,VALUED_1:def 5;
end;
coherence
proof
x(#)f is Function of X, INT;
hence thesis;
end;
end;
definition
let X be set;
let f,g be Function of X, INT;
redefine func f div g -> Function of X, INT; :: redefines div (AOFA_I00, definition)
coherence
proof
A1: dom g = X by FUNCT_2:def 1;
A2: dom (f div g) = (dom f) /\ dom g by Def3;
A3: dom f = X by FUNCT_2:def 1;
rng (f div g) c= INT;
hence thesis by A2,A3,A1,FUNCT_2:2;
end;
redefine func f mod g -> Function of X, INT; :: redefines mod (AOFA_I00, definition)
coherence
proof
A4: dom g = X by FUNCT_2:def 1;
A5: dom (f mod g) = (dom f) /\ dom g by Def4;
A6: dom f = X by FUNCT_2:def 1;
rng (f mod g) c= INT;
hence thesis by A5,A6,A4,FUNCT_2:2;
end;
redefine func leq(f,g) -> Function of X, INT; :: redefines leq (AOFA_I00, definition)
coherence
proof
A7: dom g = X by FUNCT_2:def 1;
A8: dom leq(f,g) = (dom f) /\ dom g by Def5;
A9: dom f = X by FUNCT_2:def 1;
rng leq(f,g) c= INT;
hence thesis by A8,A9,A7,FUNCT_2:2;
end;
redefine func gt(f,g) -> Function of X, INT; :: redefines gt (AOFA_I00, definition)
coherence
proof
A10: dom g = X by FUNCT_2:def 1;
A11: dom gt(f,g) = (dom f) /\ dom g by Def6;
A12: dom f = X by FUNCT_2:def 1;
rng gt(f,g) c= INT;
hence thesis by A11,A12,A10,FUNCT_2:2;
end;
redefine func eq(f,g) -> Function of X, INT; :: redefines eq (AOFA_I00, definition)
coherence
proof
A13: dom g = X by FUNCT_2:def 1;
A14: dom eq(f,g) = (dom f) /\ dom g by Def7;
A15: dom f = X by FUNCT_2:def 1;
rng eq(f,g) c= INT;
hence thesis by A14,A15,A13,FUNCT_2:2;
end;
end;
definition
let X be non empty set;
let t1,t2 be Function of X, INT;
redefine func t1-t2 -> Function of X, INT means :: redefines - (VALUED_1, definition)
: Def11:
for s being Element of X holds it.s = (t1.s)-(t2.s);
compatibility
proof
let ti be Function of X, INT;
thus ti = t1-t2 implies for s being Element of X holds ti.s = (t1.s)-(t2.s
) by VALUED_1:15;
assume
A1: for s being Element of X holds ti.s = (t1.s)-(t2.s);
A2: now
let s be object;
assume
A3: s in X;
hence ti.s = (t1.s)-(t2.s) by A1
.= (t1-t2).s by A3,VALUED_1:15;
end;
thus ti = t1-t2 by A2;
end;
coherence
proof
thus t1-t2 is Function of X, INT;
end;
redefine func t1+t2 -> Function of X, INT means :: redefines + (VALUED_1, definition)
for s being Element of X holds it.s = (t1.s)+(t2.s);
compatibility
proof
let ti be Function of X, INT;
A4: dom t1 = X by FUNCT_2:def 1;
A5: dom t2 = X by FUNCT_2:def 1;
A6: dom (t1+t2) = (dom t1)/\dom t2 by VALUED_1:def 1;
hence
ti = t1+t2 implies for s being Element of X holds ti.s = (t1.s)+(t2.s
) by A4,A5,VALUED_1:def 1;
A7: dom ti = X by FUNCT_2:def 1;
assume for s being Element of X holds ti.s = (t1.s)+(t2.s);
then for s being object st s in X holds ti.s = (t1.s)+(t2.s);
hence ti = t1+t2 by A6,A4,A5,A7,VALUED_1:def 1;
end;
coherence
proof
thus t1+t2 is Function of X, INT;
end;
end;
registration
let A be non empty set;
let B be infinite set;
cluster Funcs(A, B) -> infinite;
coherence
proof
A1: card card B = card B;
card A = card card A;
then
A2: card Funcs(A, B) = exp(card B, card A) by A1,FUNCT_5:61;
set a = the Element of A;
A3: card {a} = 1 by CARD_1:30;
{a} c= A by ZFMISC_1:31;
then 1 c= card A by A3,CARD_1:11;
then exp(card B, 1) c= card Funcs(A, B) by A2,CARD_2:93;
hence thesis by CARD_2:27;
end;
end;
definition
let N be set;
let v be Function;
let f be Function;
func v**(f,N) -> Function means
: Def13:
(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 it 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 it holds it.g = v.(g*f);
uniqueness
proof
let F1,F2 be Function;
given Y1 being set such that
A1: for y being set holds y in Y1 iff ex h being Function st h in dom
v & y in rng h and
A2: for a being set holds a in dom F1 iff a in Funcs(N,Y1) & ex g
being Function st a = g & g*f in dom v;
assume
A3: for g being Function st g in dom F1 holds F1.g = v.(g*f);
given Y2 being set such that
A4: for y being set holds y in Y2 iff ex h being Function st h in dom
v & y in rng h and
A5: for a being set holds a in dom F2 iff a in Funcs(N,Y2) & ex g
being Function st a = g & g*f in dom v;
now
let a be object;
a in Y1 iff ex h being Function st h in dom v & a in rng h by A1;
hence a in Y1 iff a in Y2 by A4;
end;
then
A6: Y1 = Y2 by TARSKI:2;
now
let a be object;
a in dom F1 iff a in Funcs(N,Y1) & ex g being Function st a = g & g
*f in dom v by A2;
hence a in dom F1 iff a in dom F2 by A5,A6;
end;
then
A7: dom F1 = dom F2 by TARSKI:2;
assume
A8: for g being Function st g in dom F2 holds F2.g = v.(g*f);
now
let a be object;
assume
A9: a in dom F1;
then consider g being Function such that
A10: a = g and
g*f in dom v by A2;
thus F1.a = v.(g*f) by A3,A9,A10
.= F2.a by A8,A7,A9,A10;
end;
hence thesis by A7;
end;
existence
proof
defpred F[object,object] means
ex g being Function st g = $1 & $2 = v.(g*f);
defpred R[object] means ex g being Function st g = $1 & g*f in dom v;
defpred P[object,object] means
ex g being Function st $1 = g & $2 = rng g;
A11: for x,y,z being object st P[x,y] & P[x,z] holds y = z;
consider X being set such that
A12: for x being object holds x in X iff
ex y being object st y in dom v & P[y,x] from TARSKI:sch 1(A11);
set Y = union X;
consider D being set such that
A13: for x being object holds x in D iff x in Funcs(N,Y) & R[x] from
XBOOLE_0:sch 1;
A14: for x being object st x in D ex y being object st F[x,y]
proof
let x be object;
assume x in D;
then consider y being Function such that
A15: y = x and
y*f in dom v by A13;
take v.(y*f);
thus thesis by A15;
end;
consider F being Function such that
A16: dom F = D & for g being object st g in D holds F[g,F.g] from
CLASSES1:sch 1(A14);
take F;
hereby
take Y;
hereby
let y be set;
hereby
assume y in Y;
then consider a being set such that
A17: y in a and
A18: a in X by TARSKI:def 4;
ex z being object st z in dom v & P[z,a] by A12,A18;
hence ex h being Function st h in dom v & y in rng h by A17;
end;
given h being Function such that
A19: h in dom v and
A20: y in rng h;
rng h in X by A12,A19;
hence y in Y by A20,TARSKI:def 4;
end;
let a be set;
thus a in dom F iff a in Funcs(N,Y) & ex g being Function st a = g & g*f
in dom v by A13,A16;
end;
let g be Function;
assume g in dom F;
then F[g,F.g] by A16;
hence thesis;
end;
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); :: redefines ** (AOFA_I00, definition)
coherence
proof
consider Y0 being set such that
A1: for y being set holds y in Y0 iff ex h being Function st h in dom
v & y in rng h and
A2: for a being set holds a in dom (v**(f,N)) iff a in Funcs(N,Y0) &
ex g being Function st a = g & g*f in dom v by Def13;
A3: dom v = Funcs(X,Y) by FUNCT_2:def 1;
A4: Y0 = Y
proof
thus Y0 c= Y
proof
let y be object;
assume y in Y0;
then consider h being Function such that
A5: h in dom v and
A6: y in rng h by A1;
rng h c= Y by A5,FUNCT_2:92;
hence thesis by A6;
end;
let y be object;
assume y in Y;
then reconsider y as Element of Y;
reconsider h = X-->y as Function of X,Y;
A7: rng h = {y} by FUNCOP_1:8;
A8: h in Funcs(X,Y) by FUNCT_2:8;
y in {y} by TARSKI:def 1;
hence thesis by A3,A1,A7,A8;
end;
A9: dom (v**(f,N)) = Funcs(N,Y)
proof
thus dom (v**(f,N)) c= Funcs(N,Y)
by A2,A4;
let a be object;
assume
A10: a in Funcs(N,Y);
then reconsider g = a as Function of N,Y by FUNCT_2:66;
g*f in Funcs(X,Y) by FUNCT_2:8;
hence thesis by A3,A2,A4,A10;
end;
rng (v**(f,N)) c= Z
proof
let a be object;
assume a in rng (v**(f,N));
then consider g being object such that
A11: g in dom (v**(f,N)) and
A12: a = (v**(f,N)).g by FUNCT_1:def 3;
reconsider g as Element of Funcs(N,Y) by A9,A11;
reconsider gf = g*f as Element of Funcs(X,Y) by FUNCT_2:8;
a = v.gf by A11,A12,Def13;
hence thesis;
end;
hence thesis by A9,FUNCT_2:def 2;
end;
end;
theorem Th3:
for f1,f2,g being Function st rng g c= dom f2 holds (f1+*f2)*g = f2*g
proof
let f1,f2,g be Function;
assume
A1: rng g c= dom f2;
A2: now
let x be object;
assume
A3: x in dom g;
then
A4: (f2*g).x = f2.(g.x) by FUNCT_1:13;
A5: g.x in rng g by A3,FUNCT_1:3;
((f1+*f2)*g).x = (f1+*f2).(g.x) by A3,FUNCT_1:13;
hence ((f1+*f2)*g).x = (f2*g).x by A1,A4,A5,FUNCT_4:13;
end;
dom (f1+*f2) = dom f1 \/ dom f2 by FUNCT_4:def 1;
then
A6: dom ((f1+*f2)*g) = dom g by A1,RELAT_1:27,XBOOLE_1:10;
dom (f2*g) = dom g by A1,RELAT_1:27;
hence thesis by A6,A2;
end;
theorem Th4:
for X,N,I being non empty set for s being Function of X,I for c
being Function of X,N st c is one-to-one for n being Element of I holds (N-->n)
+*(s*c") is Function of N,I
proof
let X,N,I be non empty set;
let s be Function of X,I;
let c be Function of X,N;
assume c is one-to-one;
then
A1: dom (c") = rng c by FUNCT_1:33;
let n be Element of I;
set f = N-->n, g = s*c";
A2: dom g c= dom (c") by RELAT_1:25;
rng g c= rng s by RELAT_1:26;
then rng g c= I by XBOOLE_1:1;
then
A3: rng f \/ rng g c= I by XBOOLE_1:8;
A5: rng (f+*g) c= rng f \/ rng g by FUNCT_4:17;
dom (f+*g) = dom f \/ dom g by FUNCT_4:def 1;
then dom (f+*g) = N by A2,A1,XBOOLE_1:1,12;
hence thesis by A5,A3,FUNCT_2:2,XBOOLE_1:1;
end;
theorem Th5:
for N,X,I being non empty set for v1,v2 being Function st dom v1
= dom v2 & dom v1 = Funcs(X,I) for f being Function of X, N st f is one-to-one
& v1**(f,N) = v2**(f,N) holds v1 = v2
proof
let N,X,I be non empty set;
let v1,v2 be Function such that
A1: dom v1 = dom v2 and
A2: dom v1 = Funcs(X,I);
reconsider rv1 = rng v1, rv2 = rng v2 as non empty set by A1,A2,RELAT_1:42;
reconsider Z = rv1\/rv2 as non empty set;
A3: rng v2 c= Z by XBOOLE_1:7;
rng v1 c= Z by XBOOLE_1:7;
then reconsider f1 = v1, f2 = v2 as Element of Funcs(Funcs(X,I),Z) by A1,A2
,A3,FUNCT_2:def 2;
let f be Function of X, N such that
A4: f is one-to-one and
A5: v1**(f,N) = v2**(f,N);
A6: dom (f2**(f,N)) = Funcs(N,I) by FUNCT_2:def 1;
A7: dom (f1**(f,N)) = Funcs(N,I) by FUNCT_2:def 1;
now
set i = the Element of I;
let a be object;
A8: dom f = X by FUNCT_2:def 1;
assume a in Funcs(X,I);
then reconsider h = a as Element of Funcs(X,I);
set g = (N-->i)+*(h*f");
A9: dom h = X by FUNCT_2:def 1;
rng (f") = dom f by A4,FUNCT_1:33;
then dom (h*f") = dom (f") by A9,RELAT_1:27
.= rng f by A4,FUNCT_1:33;
then
A10: g*f = (h*f")*f by Th3
.= h*(f"*f) by RELAT_1:36
.= h*id X by A4,A8,FUNCT_1:39
.= a by A9,RELAT_1:52;
g is Function of N,I by A4,Th4;
then
A11: g in Funcs(N,I) by FUNCT_2:8;
then (v1**(f,N)).g = v1.a by A7,A10,Def13;
hence v1.a = v2.a by A5,A6,A11,A10,Def13;
end;
hence thesis by A1,A2;
end;
registration
let X be set;
cluster one-to-one onto for Function of X, card X;
existence
proof
X, card X are_equipotent by CARD_1:def 2;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = X and
A3: rng f = card X by WELLORD2:def 4;
reconsider f as Function of X,card X by A2,A3,FUNCT_2:2;
take f;
thus f is one-to-one by A1;
thus rng f = card X by A3;
end;
cluster one-to-one onto for Function of card X, X;
existence
proof
X, card X are_equipotent by CARD_1:def 2;
then consider f being Function such that
A4: f is one-to-one and
A5: dom f = card X and
A6: rng f = X by WELLORD2:def 4;
reconsider f as Function of card X, X by A5,A6,FUNCT_2:2;
take f;
thus f is one-to-one by A4;
thus rng f = X by A6;
end;
end;
definition
let X be set;
mode Enumeration of X is one-to-one onto Function of X, card X;
mode Denumeration of X is one-to-one onto Function of card X, X;
end;
theorem Th6:
for X being set, f being Function holds f is Enumeration of X iff
dom f = X & rng f = card X & f is one-to-one
proof
let X be set, f be Function;
card X = {} implies X = {};
hence thesis by FUNCT_2:2,def 1,def 3;
end;
theorem Th7:
for X being set, f being Function holds f is Denumeration of X
iff dom f = card X & rng f = X & f is one-to-one
proof
let X be set, f be Function;
X = {} implies card X = {};
hence thesis by FUNCT_2:2,def 1,def 3;
end;
theorem Th8:
for X being non empty set, x,y being Element of X for f being
Enumeration of X holds f+*(x,f.y)+*(y,f.x) is Enumeration of X
proof
let X be non empty set, x,y be Element of X;
let f be Enumeration of X;
set g = f+*(x,f.y)+*(y,f.x);
set A = dom g;
A1: dom (f+*(x,f.y)) = dom f by FUNCT_7:30;
A2: A = dom (f+*(x,f.y)) by FUNCT_7:30;
A3: dom f = X by Th6;
A4: rng f = card X by Th6;
A5: rng (f+*(x,f.y)+*(y,f.x)) = rng f
proof
{f.x} c= rng f by A4,ZFMISC_1:31;
then
A6: rng f \/ {f.x} = rng f by XBOOLE_1:12;
A7: rng g c= rng (f+*(x,f.y)) \/ {f.x} by FUNCT_7:100;
{f.y} c= rng f by A4,ZFMISC_1:31;
then rng f \/ {f.y} = rng f by XBOOLE_1:12;
then rng (f+*(x,f.y)) \/ {f.x} c= rng f by A6,FUNCT_7:100,XBOOLE_1:9;
hence rng g c= rng f by A7;
let z be object;
assume z in rng f;
then consider a being object such that
A8: a in dom f and
A9: z = f.a by FUNCT_1:def 3;
per cases;
suppose
A10: a <> x & a <> y;
then
A11: g.a = (f+*(x,f.y)).a by FUNCT_7:32;
(f+*(x,f.y)).a = z by A9,A10,FUNCT_7:32;
hence thesis by A1,A2,A8,A11,FUNCT_1:def 3;
end;
suppose
a = x;
then g.y = z by A1,A3,A9,FUNCT_7:31;
hence thesis by A1,A2,A3,FUNCT_1:def 3;
end;
suppose
A12: a = y;
then
A13: x <> y implies g.x = (f+*(x,z)).x by A9,FUNCT_7:32;
A14: (f+*(x,z)).x = z by A3,FUNCT_7:31;
x = y implies g.x = z by A1,A3,A9,A12,FUNCT_7:31;
hence thesis by A1,A2,A3,A14,A13,FUNCT_1:def 3;
end;
end;
f+*(x,f.y)+*(y,f.x) is one-to-one
proof
let a,b being object;
A15: a <> y implies g.a = (f+*(x,f.y)).a by FUNCT_7:32;
A16: a <> x implies (f+*(x,f.y)).a = f.a by FUNCT_7:32;
A17: b = y implies g.b = f.x by A1,A3,FUNCT_7:31;
A18: b <> y implies g.b = (f+*(x,f.y)).b by FUNCT_7:32;
A19: b = x implies (f+*(x,f.y)).b = f.y by A3,FUNCT_7:31;
A20: a = x implies (f+*(x,f.y)).a = f.y by A3,FUNCT_7:31;
A21: b <> x implies (f+*(x,f.y)).b = f.b by FUNCT_7:32;
a = y implies g.a = f.x by A1,A3,FUNCT_7:31;
hence thesis by A2,A3,A15,A20,A16,A17,A18,A19,A21,FUNCT_1:def 4;
end;
hence thesis by A1,A2,A3,A4,A5,Th6;
end;
theorem
for X being non empty set, x being Element of X ex f being Enumeration
of X st f.x = 0
proof
let X be non empty set, x be Element of X;
set f = the Enumeration of X;
A1: 0 in card X by ORDINAL3:8;
A2: rng f = card X by Th6;
dom f = X by Th6;
then consider y being object such that
A3: y in X and
A4: 0 = f.y by A1,A2,FUNCT_1:def 3;
reconsider y as Element of X by A3;
reconsider g = f+*(y,f.x)+*(x,0) as Enumeration of X by A4,Th8;
take g;
dom f = X by Th6;
then dom (f+*(y,f.x)) = X by FUNCT_7:30;
hence thesis by FUNCT_7:31;
end;
theorem
for X being non empty set, f being Denumeration of X holds f.0 in X by
FUNCT_2:5,ORDINAL3:8;
theorem Th11:
for X being countable set, f being Enumeration of X holds rng f c= NAT
proof
let X be countable set, f be Enumeration of X;
card X c= NAT by CARD_3:def 14;
hence thesis;
end;
definition
let X be set;
let f be Enumeration of X;
redefine func f" -> Denumeration of X; :: redefines " (FUNCT_1, definition)
coherence
proof
rng f = card X by Th6;
then
A1: dom (f") = card X by FUNCT_1:33;
dom f = X by Th6;
then rng (f") = X by FUNCT_1:33;
hence thesis by A1,Th7;
end;
end;
definition
let X be set;
let f be Denumeration of X;
redefine func f" -> Enumeration of X; :: redefines " (FUNCT_1, definition)
coherence
proof
rng f = X by Th7;
then
A1: dom (f") = X by FUNCT_1:33;
dom f = card X by Th7;
then rng (f") = card X by FUNCT_1:33;
hence thesis by A1,Th6;
end;
end;
theorem
for n,m being Nat holds 0 to_power (n+m) = (0 to_power n)*(0 to_power m)
proof
let n,m be Nat;
per cases;
suppose
A1: n > 0 or m > 0;
then 0 to_power n = 0 or 0 to_power m = 0 by POWER:def 2;
hence thesis by A1,POWER:def 2;
end;
suppose
A2: n = 0 & m = 0;
then 0 to_power (n+m) = 1 by POWER:24;
hence thesis by A2;
end;
end;
theorem
for x being Real for n,m being Nat holds (x to_power n)
to_power m = x to_power (n*m) by NEWTON:9;
begin :: If-while algebra over integers
definition
let X be non empty set;
mode INT-Variable of X is Function of Funcs(X, INT), X;
mode INT-Expression of X is Function of Funcs(X, INT), INT;
mode INT-Array of X is Function of INT, X;
end;
reserve A for preIfWhileAlgebra;
definition
let A;
let I be Element of A;
let X be non empty set;
let T be Subset of Funcs(X, INT);
let f be ExecutionFunction of A, Funcs(X, INT), T;
pred I is_assignment_wrt A,X,f means
I in ElementaryInstructions A &
ex v being INT-Variable of X, t being INT-Expression of X st for s being
Element of Funcs(X, INT) holds f.(s, I) = s+*(v.s,t.s);
end;
definition
let A;
let X be non empty set;
let T be Subset of Funcs(X, INT);
let f be ExecutionFunction of A, Funcs(X, INT), T;
let v be INT-Variable of X;
let t be INT-Expression of X;
pred v,t form_assignment_wrt f means
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);
end;
definition
let A;
let X be non empty set;
let T be Subset of Funcs(X, INT);
let f be ExecutionFunction of A, Funcs(X, INT), T such that
A1: ex I being Element of A st I is_assignment_wrt A,X,f;
mode INT-Variable of A,f -> INT-Variable of X means
ex t being INT-Expression of X st it,t form_assignment_wrt f;
existence
proof
consider I being Element of A such that
A2: I is_assignment_wrt A,X,f by A1;
consider v being (INT-Variable of X), t being INT-Expression of X such
that
A3: for s being Element of Funcs(X, INT) holds f.(s, I) = s+*(v.s,t.s)
by A2;
take v,t,I;
thus thesis by A2,A3;
end;
end;
definition
let A;
let X be non empty set;
let T be Subset of Funcs(X, INT);
let f be ExecutionFunction of A, Funcs(X, INT), T such that
A1: ex I being Element of A st I is_assignment_wrt A,X,f;
mode INT-Expression of A,f -> INT-Expression of X means
ex v being INT-Variable of X st v,it form_assignment_wrt f;
existence
proof
consider I being Element of A such that
A2: I is_assignment_wrt A,X,f by A1;
consider v being (INT-Variable of X), t being INT-Expression of X such
that
A3: for s being Element of Funcs(X, INT) holds f.(s, I) = s+*(v.s,t.s)
by A2;
take t,v,I;
thus thesis by A2,A3;
end;
end;
definition
let X,Y be non empty set;
let f be Element of Funcs(X,Y);
let x be Element of X;
redefine func f.x -> Element of Y; :: redefines . (FUNCT_1, definition)
coherence
proof
f.x in rng f by FUNCT_2:4;
hence thesis;
end;
end;
definition
let X be non empty set;
let x be Element of X;
func .x -> INT-Expression of X means
: Def18:
for s being Element of Funcs(X, INT) holds it.s = s.x;
correctness
proof
deffunc F(Element of Funcs(X,INT)) = $1.x;
thus ex f being Function of Funcs(X, INT), INT st for x being Element of
Funcs(X, INT) holds f.x = F(x) from FUNCT_2:sch 4;
let f1,f2 be INT-Expression of X such that
A1: for s being Element of Funcs(X, INT) holds f1.s = s.x and
A2: for s being Element of Funcs(X, INT) holds f2.s = s.x;
now
let s be Element of Funcs(X, INT);
thus f1.s = s.x by A1
.= f2.s by A2;
end;
hence thesis;
end;
end;
definition
let X be non empty set;
let v be INT-Variable of X;
func .v -> INT-Expression of X means
: Def19:
for s being Element of Funcs(X, INT) holds it.s = s.(v.s);
correctness
proof
deffunc F(Element of Funcs(X,INT)) = $1.(v.$1);
thus ex f being Function of Funcs(X, INT), INT st for x being Element of
Funcs(X, INT) holds f.x = F(x) from FUNCT_2:sch 4;
let f1,f2 be INT-Expression of X such that
A1: for s being Element of Funcs(X, INT) holds f1.s = s.(v.s) and
A2: for s being Element of Funcs(X, INT) holds f2.s = s.(v.s);
now
let s be Element of Funcs(X, INT);
thus f1.s = s.(v.s) by A1
.= f2.s by A2;
end;
hence thesis;
end;
end;
definition
let X be non empty set;
let x be Element of X;
func ^x -> INT-Variable of X equals
Funcs(X, INT) --> x;
correctness;
end;
theorem
for X being non empty set for x being Element of X holds .x = .(^x)
proof
let X be non empty set;
let x be Element of X;
for s being Element of Funcs(X, INT) holds .(^x).s = s.x
proof
let s be Element of Funcs(X, INT);
thus .(^x).s = s.((^x).s) by Def19
.= s.x;
end;
hence thesis by Def18;
end;
definition
let X be non empty set;
let i be Integer;
func .(i,X) -> INT-Expression of X equals
Funcs(X,INT) --> i;
correctness
proof
i in INT by INT_1:def 2;
hence thesis by FUNCOP_1:45;
end;
end;
theorem
for X being non empty set, t being INT-Expression of X holds t+ .(0,X)
= t & t(#).(1,X) = t
proof
let X be non empty set;
let t be INT-Expression of X;
now
let s be Element of Funcs(X,INT);
dom (t+ .(0,X)) = Funcs(X,INT) by FUNCT_2:def 1;
hence (t+ .(0,X)).s = (t.s)+(.(0,X).s) by VALUED_1:def 1
.= t.s;
end;
hence t+ .(0,X) = t;
now
let s be Element of Funcs(X,INT);
dom (t(#).(1,X)) = Funcs(X,INT) by FUNCT_2:def 1;
hence (t(#).(1,X)).s = (t.s)*(.(1,X).s) by VALUED_1:def 4
.= (t.s)*1
.= t.s;
end;
hence thesis;
end;
:: The word "Euclidean" is chosen in following definition
:: to suggest that Euclid algoritm could be annotated
:: in quite natural way (all needed expressions are allowed).
definition
let A;
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, t being
INT-Expression of A,f holds v,t form_assignment_wrt f) & (for i being Integer
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;
:: Remark:
:: Incorrect definition of "mod" in INT_1: 5 mod 0 = 0 i 5 div 0 = 0
:: and 5 <> 0*(5 div 0)+(5 mod 0)
:: In our case "mod" is still expressible with "basic" operations
:: but in complicated way:
:: f1 mod f2
:: = (gt(f2,(dom f2)-->0)+gt((dom f2)-->0,f2))(#)(f1-f2(#)(f1 div f2))
:: To avoid complications "mod" is mentioned in the definition above.
definition
let A;
attr A is Euclidean means
: Def23:
for X being non empty countable set, T
being Subset of Funcs(X, INT) ex f being ExecutionFunction of A, Funcs(X, INT),
T st f is Euclidean;
end;
definition
func INT-ElemIns -> infinite disjoint_with_NAT set equals
[:Funcs(Funcs(NAT, INT), NAT), Funcs(Funcs(NAT, INT), INT):];
coherence;
end;
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
proof
reconsider i0 = 0 as Element of INT by INT_1:def 1;
set Q = Funcs(NAT, INT), T = Q\(0,0);
set S = ECIW-signature, G = INT-ElemIns;
set A = FreeUnivAlgNSG(S,G);
A1: Terminals DTConUA(S,G) = G by FREEALG:3;
reconsider q0 = NAT-->i0 as Element of Q by FUNCT_2:8;
defpred P[object,object] means
ex s being (Element of Q), v being (Element of
Funcs(Q, NAT)), e being Element of Funcs(Q, INT) st $1 = [s, root-tree [v,e]] &
$2 = s+*(v.s,e.s);
A2: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
A3: for x being object st x in [:Q,ElementaryInstructions A:]
ex y being object st y in Q & P[x,y]
proof
let x be object;
assume x in [:Q,ElementaryInstructions A:];
then consider s, I being object such that
A4: s in Q and
A5: I in ElementaryInstructions A and
A6: x = [s,I] by ZFMISC_1:def 2;
reconsider s as Element of Q by A4;
consider a being Symbol of DTConUA(S,G) such that
A7: I = root-tree a and
A8: a in Terminals DTConUA(S,G) by A2,A5;
consider v,e being object such that
A9: v in Funcs(Funcs(NAT, INT), NAT) and
A10: e in Funcs(Funcs(NAT, INT), INT) and
A11: a = [v,e] by A1,A8,ZFMISC_1:def 2;
reconsider e as Element of Funcs(Q, INT) by A10;
reconsider v as Element of Funcs(Q, NAT) by A9;
take y = s+*(v.s,e.s);
thus y in Q by FUNCT_2:8;
take s,v,e;
thus x = [s, root-tree [v,e]] & y = s+*(v.s,e.s) by A6,A7,A11;
end;
consider g being Function such that
A12: dom g = [:Q,ElementaryInstructions A:] & rng g c= Q and
A13: for x being object st x in [:Q,ElementaryInstructions A:] holds P[x,
g.x] from FUNCT_1:sch 6(A3);
reconsider g as Function of [:Q,ElementaryInstructions A:], Q by A12,
FUNCT_2:2;
consider f being ExecutionFunction of A, Q, T such that
A14: f|[:Q,ElementaryInstructions A:] = g and
for s being Element of Q for C,I being Element of A st not f
iteration_terminates_for I\;C, f.(s,C) holds f.(s, while(C,I)) = q0 by
AOFA_000:91;
take f;
let s be Element of Funcs(NAT, INT);
let v be Element of Funcs(Funcs(NAT, INT), NAT);
let e be Element of Funcs(Funcs(NAT, INT), INT);
set I = root-tree [v,e];
[v,e] in G by ZFMISC_1:87;
then I in ElementaryInstructions A by A2,A1;
then
A15: [s,I] in [:Q,ElementaryInstructions A:] by ZFMISC_1:87;
then consider
s9 being (Element of Q), v9 being (Element of Funcs(Q, NAT)), e9
being Element of Funcs(Q, INT) such that
A16: [s,I] = [s9, root-tree [v9,e9]] and
A17: g.[s,I] = s9+*(v9.s9,e9.s9) by A13;
I = root-tree [v9,e9] by A16,XTUPLE_0:1;
then
A18: [v,e] = [v9,e9] by TREES_4:4;
then
A19: v = v9 by XTUPLE_0:1;
A20: e = e9 by A18,XTUPLE_0:1;
s = s9 by A16,XTUPLE_0:1;
hence thesis by A14,A15,A17,A19,A20,FUNCT_1:49;
end;
end;
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;
end;
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
proof
reconsider i0 = 0 as Element of INT by INT_1:def 1;
set Q = Funcs(X, INT), T = Q\(x,0);
set S = ECIW-signature, G = INT-ElemIns X;
set A = FreeUnivAlgNSG(S,G);
A1: Terminals DTConUA(S,G) = G by FREEALG:3;
reconsider q0 = X-->i0 as Element of Q by FUNCT_2:8;
defpred P[object,object] means
ex s being (Element of Q), v being (Element of
Funcs(Q, X)), e being Element of Funcs(Q, INT) st $1 = [s, root-tree [v,e]] &
$2 = s+*(v.s,e.s);
A2: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
A3: for x being object st x in [:Q,ElementaryInstructions A:]
ex y being object st y in Q & P[x,y]
proof
let x be object;
assume x in [:Q,ElementaryInstructions A:];
then consider s, I being object such that
A4: s in Q and
A5: I in ElementaryInstructions A and
A6: x = [s,I] by ZFMISC_1:def 2;
reconsider s as Element of Q by A4;
consider a being Symbol of DTConUA(S,G) such that
A7: I = root-tree a and
A8: a in Terminals DTConUA(S,G) by A2,A5;
consider v,e being object such that
A9: v in Funcs(Funcs(X, INT), X) and
A10: e in Funcs(Funcs(X, INT), INT) and
A11: a = [v,e] by A1,A8,ZFMISC_1:def 2;
reconsider e as Element of Funcs(Q, INT) by A10;
reconsider v as Element of Funcs(Q, X) by A9;
take y = s+*(v.s,e.s);
thus y in Q by FUNCT_2:8;
take s,v,e;
thus x = [s, root-tree [v,e]] & y = s+*(v.s,e.s) by A6,A7,A11;
end;
consider g being Function such that
A12: dom g = [:Q,ElementaryInstructions A:] & rng g c= Q and
A13: for x being object st x in [:Q,ElementaryInstructions A:] holds P[x,
g.x] from FUNCT_1:sch 6(A3);
reconsider g as Function of [:Q,ElementaryInstructions A:], Q by A12,
FUNCT_2:2;
consider f being ExecutionFunction of A, Q, T such that
A14: f|[:Q,ElementaryInstructions A:] = g and
for s being Element of Q for C,I being Element of A st not f
iteration_terminates_for I\;C, f.(s,C) holds f.(s, while(C,I)) = q0 by
AOFA_000:91;
take f;
let s be Element of Funcs(X, INT);
let v be Element of Funcs(Funcs(X, INT), X);
let e be Element of Funcs(Funcs(X, INT), INT);
set I = root-tree [v,e];
[v,e] in G by ZFMISC_1:87;
then I in ElementaryInstructions A by A2,A1;
then
A15: [s,I] in [:Q,ElementaryInstructions A:] by ZFMISC_1:87;
then consider
s9 being (Element of Q), v9 being (Element of Funcs(Q, X)), e9
being Element of Funcs(Q, INT) such that
A16: [s,I] = [s9, root-tree [v9,e9]] and
A17: g.[s,I] = s9+*(v9.s9,e9.s9) by A13;
I = root-tree [v9,e9] by A16,XTUPLE_0:1;
then
A18: [v,e] = [v9,e9] by TREES_4:4;
then
A19: v = v9 by XTUPLE_0:1;
A20: e = e9 by A18,XTUPLE_0:1;
s = s9 by A16,XTUPLE_0:1;
hence thesis by A14,A15,A17,A19,A20,FUNCT_1:49;
end;
end;
definition
let X be non empty set;
let T be Subset of Funcs(X, INT);
let c be Enumeration of X such that
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
proof
dom c = X by Th6;
then reconsider c9 = c as Function of X, NAT by A1,FUNCT_2:2;
reconsider i0 = 0 as Element of INT by INT_1:def 1;
set Q = Funcs(X, INT);
set S = ECIW-signature, G = INT-ElemIns;
set A = FreeUnivAlgNSG(S,G);
reconsider q0 = X-->i0 as Element of Q by FUNCT_2:8;
A2: Terminals DTConUA(S,G) = G by FREEALG:3;
defpred P[object,object] means
ex s being (Element of Q) st $1`1 = s & (($2 = s
& not ex v being (Element of Funcs(Q, X)), e being Element of Funcs(Q, INT) st
$1`2 = root-tree [(c*v)**(c9,NAT),e**(c9,NAT)]) or ex v being (Element of Funcs
(Q, X)), e being Element of Funcs(Q, INT) st $1`2 = root-tree [(c*v)**(c9,NAT),
e**(c9,NAT)] & $2 = s+*(v.s,e.s));
A3: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
A4: for x being object st x in [:Q,ElementaryInstructions A:]
ex y being object st y in Q & P[x,y]
proof
let x be object;
assume x in [:Q,ElementaryInstructions A:];
then consider s, I being object such that
A5: s in Q and
A6: I in ElementaryInstructions A and
A7: x = [s,I] by ZFMISC_1:def 2;
A8: x`1 = s by A7;
reconsider s as Element of Q by A5;
A9: x`2 = I by A7;
consider a being Symbol of DTConUA(S,G) such that
A10: I = root-tree a and
a in Terminals DTConUA(S,G) by A3,A6;
per cases;
suppose
ex v being (Element of Funcs(Q, X)), e being Element of Funcs
(Q, INT) st a = [(c*v)**(c9,NAT),e**(c9,NAT)];
then consider
v being (Element of Funcs(Q, X)), e being Element of Funcs(Q,
INT) such that
A11: a = [(c*v)**(c9,NAT),e**(c9,NAT)];
take y = s+*(v.s,e.s);
thus y in Q by FUNCT_2:8;
thus thesis by A8,A9,A10,A11;
end;
suppose
A12: not ex v being (Element of Funcs(Q, X)), e being Element of
Funcs(Q, INT) st a = [(c*v)**(c9,NAT),e**(c9,NAT)];
take y = s;
thus y in Q;
not ex v being (Element of Funcs(Q, X)), e being Element of Funcs
(Q, INT) st x`2 = root-tree [(c*v)**(c9,NAT),e**(c9,NAT)] by A9,A10,A12,
TREES_4:4;
hence thesis by A8;
end;
end;
consider g being Function such that
A13: dom g = [:Q,ElementaryInstructions A:] & rng g c= Q and
A14: for x being object st x in [:Q,ElementaryInstructions A:] holds P[x,
g.x] from FUNCT_1:sch 6(A4);
reconsider g as Function of [:Q,ElementaryInstructions A:], Q by A13,
FUNCT_2:2;
consider f being ExecutionFunction of A, Q, T such that
A15: f|[:Q,ElementaryInstructions A:] = g and
for s being Element of Q for C,I being Element of A st not f
iteration_terminates_for I\;C, f.(s,C) holds f.(s, while(C,I)) = q0 by
AOFA_000:91;
take f;
let s be Element of Funcs(X, INT);
let v be Element of Funcs(Funcs(X, INT), X);
let e be Element of Funcs(Funcs(X, INT), INT);
reconsider vv = v as Function of Funcs(X, INT), X;
reconsider cv = c9*vv as Element of Funcs(Funcs(X, INT), NAT) by FUNCT_2:8;
set v0 = cv**(c9,NAT), e0 = e**(c9,NAT);
set I = root-tree [v0,e0];
[v0,e0] in G by ZFMISC_1:87;
then I in ElementaryInstructions A by A3,A2;
then
A16: [s,I] in [:Q,ElementaryInstructions A:] by ZFMISC_1:87;
then P[[s,I],g.[s,I]] by A14;
then consider
v9 being (Element of Funcs(Q, X)), e9 being Element of Funcs(Q,
INT) such that
A17: [s,I]`2 = root-tree [(c*v9)**(c9,NAT),e9**(c9,NAT)] and
A18: g.[s,I] = s+*(v9.s,e9.s);
A19: dom (c9*v9) = Q by FUNCT_2:def 1;
A20: dom e = Q by FUNCT_2:def 1;
A21: dom v = Q by FUNCT_2:def 1;
A22: dom cv = Q by FUNCT_2:def 1;
A23: dom c9 = X by FUNCT_2:def 1;
A24: rng v c= X;
A25: dom e9 = Q by FUNCT_2:def 1;
A26: dom v9 = Q by FUNCT_2:def 1;
A27: [v0,e0] = [(c*v9)**(c9,NAT),e9**(c9,NAT)] by A17,TREES_4:4;
then v0 = (c*v9)**(c9,NAT) by XTUPLE_0:1;
then
A28: cv = c*v9 by A22,A19,Th5;
e0 = e9**(c9,NAT) by A27,XTUPLE_0:1;
then
A29: e = e9 by A20,A25,Th5;
rng v9 c= X;
then v = v9 by A24,A23,A26,A21,A28,FUNCT_1:27;
hence thesis by A15,A16,A18,A29,FUNCT_1:49;
end;
end;
theorem Th16:
for f being INT-Exec for v being INT-Variable of NAT for t being
INT-Expression of NAT holds v,t form_assignment_wrt f
proof
let f be INT-Exec;
set S = ECIW-signature, G = INT-ElemIns;
set X = NAT;
set A = FreeUnivAlgNSG(S,G);
let v be INT-Variable of NAT;
let t be INT-Expression of NAT;
reconsider v9 = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:8;
reconsider t9 = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:8;
A1: Terminals DTConUA(S,G) = G by FREEALG:3;
A2: [v9,t9] in G by ZFMISC_1:87;
A3: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
then root-tree [v9,t9] in ElementaryInstructions A by A1,A2;
then reconsider I = root-tree [v9,t9] as Element of A;
take I;
thus I in ElementaryInstructions A by A3,A1,A2;
thus thesis by Def25;
end;
theorem Th17:
for f being INT-Exec for v being INT-Variable of NAT holds v is
INT-Variable of FreeUnivAlgNSG(ECIW-signature, INT-ElemIns), f
proof
set t = the INT-Expression of NAT;
let f be INT-Exec;
set S = ECIW-signature, G = INT-ElemIns;
set X = NAT;
set A = FreeUnivAlgNSG(S,G);
let v be INT-Variable of NAT;
A1: Terminals DTConUA(S,G) = G by FREEALG:3;
reconsider t9 = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:8;
reconsider v9 = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:8;
A2: [v9,t9] in G by ZFMISC_1:87;
A3: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
then root-tree [v9,t9] in ElementaryInstructions A by A1,A2;
then reconsider I = root-tree [v9,t9] as Element of A;
hereby
take I;
thus I is_assignment_wrt A,X,f
proof
thus I in ElementaryInstructions A by A3,A1,A2;
take v,t;
thus thesis by Def25;
end;
end;
take t;
thus thesis by Th16;
end;
theorem Th18:
for f being INT-Exec for t being INT-Expression of NAT holds t
is INT-Expression of FreeUnivAlgNSG(ECIW-signature, INT-ElemIns), f
proof
set v = the INT-Variable of NAT;
let f be INT-Exec;
set S = ECIW-signature, G = INT-ElemIns;
set X = NAT;
set A = FreeUnivAlgNSG(S,G);
let t be INT-Expression of NAT;
A1: Terminals DTConUA(S,G) = G by FREEALG:3;
reconsider t9 = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:8;
reconsider v9 = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:8;
A2: [v9,t9] in G by ZFMISC_1:87;
A3: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
then root-tree [v9,t9] in ElementaryInstructions A by A1,A2;
then reconsider I = root-tree [v9,t9] as Element of A;
hereby
take I;
thus I is_assignment_wrt A,X,f
proof
thus I in ElementaryInstructions A by A3,A1,A2;
take v,t;
thus thesis by Def25;
end;
end;
take v;
thus thesis by Th16;
end;
registration
cluster -> Euclidean for INT-Exec;
coherence
proof
set X = NAT;
set a = (INT --> 0)+*(id X);
A1: dom id X = X by RELAT_1:45;
A2: INT \/ X = INT by NUMBERS:17,XBOOLE_1:12;
dom (INT --> 0) = INT;
then
A3: dom a = INT by A1,A2,FUNCT_4:def 1;
rng a c= NAT;
then reconsider a as INT-Array of X by A3,FUNCT_2:2;
let f be INT-Exec;
set S = ECIW-signature, G = INT-ElemIns;
set A = FreeUnivAlgNSG(S,G);
thus for v being INT-Variable of A,f, t being INT-Expression of A,f holds
v,t form_assignment_wrt f by Th16;
thus for i being Integer holds .(i,X) is INT-Expression of A,f by Th18;
thus for v being INT-Variable of A,f holds .v is INT-Expression of A,f
by Th18;
thus for x being Element of X holds ^x is INT-Variable of A,f by Th17;
hereby
take a;
dom id X = X by RELAT_1:45;
hence a|card X is one-to-one by FUNCT_4:23;
thus for t being INT-Expression of A,f holds a*t is INT-Variable of A,f
by Th17;
end;
thus thesis by Th18;
end;
end;
theorem Th19:
for X being non empty countable set for T being Subset of Funcs(
X, INT) for c being Enumeration of X for f being INT-Exec of c,T for v being
INT-Variable of X for t being INT-Expression of X holds v,t form_assignment_wrt
f
proof
set S = ECIW-signature, G = INT-ElemIns;
let X be non empty countable set;
let T be Subset of Funcs(X, INT);
let c be Enumeration of X;
set A = FreeUnivAlgNSG(S,G);
let f be INT-Exec of c,T;
let v be INT-Variable of X;
let t be INT-Expression of X;
reconsider v9 = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:8;
reconsider t9 = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:8;
A1: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
A2: rng c c= NAT by Th11;
dom c = X by Th6;
then reconsider c9 = c as Function of X,NAT by A2,FUNCT_2:2;
reconsider cv = c9*v as Element of Funcs(Funcs(X,INT),NAT) by FUNCT_2:8;
set v1 = cv**(c9,NAT), t1 = t9**(c9,NAT);
A3: Terminals DTConUA(S,G) = G by FREEALG:3;
A4: [v1,t1] in G by ZFMISC_1:87;
then root-tree [v1,t1] in ElementaryInstructions A by A1,A3;
then reconsider I = root-tree [v1,t1] as Element of A;
take I;
for s being Element of Funcs(X, INT) holds f.(s, root-tree [(c*v9)**(c,
NAT),t9**(c,NAT)]) = s+*(v9.s,t9.s) by A2,Def28;
hence thesis by A1,A3,A4;
end;
theorem Th20:
for X being non empty countable set for T being Subset of Funcs(
X, INT) for c being Enumeration of X for f being INT-Exec of c,T for v being
INT-Variable of X holds v is INT-Variable of FreeUnivAlgNSG(ECIW-signature,
INT-ElemIns), f
proof
set S = ECIW-signature, G = INT-ElemIns;
let X be non empty countable set;
let T be Subset of Funcs(X, INT);
let c be Enumeration of X;
set A = FreeUnivAlgNSG(S,G);
let f be INT-Exec of c,T;
let v be INT-Variable of X;
set t = the INT-Expression of X;
A1: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
A2: rng c c= NAT by Th11;
dom c = X by Th6;
then reconsider c9 = c as Function of X,NAT by A2,FUNCT_2:2;
reconsider cv = c9*v as Element of Funcs(Funcs(X,INT),NAT) by FUNCT_2:8;
reconsider v9 = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:8;
reconsider t9 = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:8;
A3: Terminals DTConUA(S,G) = G by FREEALG:3;
set v1 = cv**(c9,NAT), t1 = t9**(c9,NAT);
A4: [v1,t1] in G by ZFMISC_1:87;
then root-tree [v1,t1] in ElementaryInstructions A by A1,A3;
then reconsider I = root-tree [v1,t1] as Element of A;
hereby
take I;
thus I is_assignment_wrt A,X,f
proof
thus I in ElementaryInstructions A by A1,A3,A4;
take v,t;
for s being Element of Funcs(X, INT) holds f.(s, root-tree [(c*v9)**
(c,NAT),t9**(c,NAT)]) = s+*(v9.s,t9.s) by A2,Def28;
hence thesis;
end;
end;
take t;
thus thesis by Th19;
end;
theorem Th21:
for X being non empty countable set for T being Subset of Funcs(
X, INT) for c being Enumeration of X for f being INT-Exec of c,T for t being
INT-Expression of X holds t is INT-Expression of FreeUnivAlgNSG(ECIW-signature,
INT-ElemIns), f
proof
set S = ECIW-signature, G = INT-ElemIns;
let X be non empty countable set;
let T be Subset of Funcs(X, INT);
let c be Enumeration of X;
set A = FreeUnivAlgNSG(S,G);
let f be INT-Exec of c,T;
set v = the INT-Variable of X;
let t be INT-Expression of X;
A1: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
A2: rng c c= NAT by Th11;
dom c = X by Th6;
then reconsider c9 = c as Function of X,NAT by A2,FUNCT_2:2;
reconsider cv = c9*v as Element of Funcs(Funcs(X,INT),NAT) by FUNCT_2:8;
reconsider v9 = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:8;
reconsider t9 = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:8;
A3: Terminals DTConUA(S,G) = G by FREEALG:3;
set v1 = cv**(c9,NAT), t1 = t9**(c9,NAT);
A4: [v1,t1] in G by ZFMISC_1:87;
then root-tree [v1,t1] in ElementaryInstructions A by A1,A3;
then reconsider I = root-tree [v1,t1] as Element of A;
hereby
take I;
thus I is_assignment_wrt A,X,f
proof
thus I in ElementaryInstructions A by A1,A3,A4;
take v,t;
for s being Element of Funcs(X, INT) holds f.(s, root-tree [(c*v9)**
(c,NAT),t9**(c,NAT)]) = s+*(v9.s,t9.s) by A2,Def28;
hence thesis;
end;
end;
take v;
thus thesis by Th19;
end;
registration
let X be countable non empty set;
let T be Subset of Funcs(X, INT);
let c be Enumeration of X;
cluster -> Euclidean for INT-Exec of c,T;
coherence
proof
A1: rng c c= NAT by Th11;
card X = rng c by Th6;
then
A2: INT \/ card X = INT by A1,NUMBERS:17,XBOOLE_1:1,12;
set x = c".0;
set a = (INT --> x)+*(c");
A3: dom (INT --> x) = INT;
A4: rng (INT --> x) = {x} by FUNCOP_1:8;
x in X by FUNCT_2:5,ORDINAL3:8;
then {x} c= X by ZFMISC_1:31;
then
A5: {x} \/ X = X by XBOOLE_1:12;
rng (c") = X by Th7;
then
A6: rng a c= X by A4,A5,FUNCT_4:17;
dom (c") = card X by Th7;
then dom a = INT by A3,A2,FUNCT_4:def 1;
then reconsider a as INT-Array of X by A6,FUNCT_2:2;
let f be INT-Exec of c,T;
set S = ECIW-signature, G = INT-ElemIns;
set A = FreeUnivAlgNSG(S,G);
thus for v being INT-Variable of A,f, t being INT-Expression of A,f holds
v,t form_assignment_wrt f by Th19;
thus for i being Integer holds .(i,X) is INT-Expression of A,f by
Th21;
thus for v being INT-Variable of A,f holds .v is INT-Expression of A,f by
Th21;
thus for x being Element of X holds ^x is INT-Variable of A,f by Th20;
hereby
take a;
dom (c") = card X by Th7;
hence a|card X is one-to-one by FUNCT_4:23;
thus for t being INT-Expression of A,f holds a*t is INT-Variable of A,f
by Th20;
end;
thus thesis by Th21;
end;
end;
registration
cluster FreeUnivAlgNSG(ECIW-signature, INT-ElemIns) -> Euclidean;
coherence
proof
let X be non empty countable set, T be Subset of Funcs(X, INT);
set c = the Enumeration of X;
set f = the INT-Exec of c, T;
take f;
thus thesis;
end;
end;
registration
cluster Euclidean non degenerated for preIfWhileAlgebra;
existence
proof
take FreeUnivAlgNSG(ECIW-signature, INT-ElemIns);
thus thesis;
end;
end;
registration
let A be Euclidean preIfWhileAlgebra;
let X be non empty countable set;
let T be Subset of Funcs(X, INT);
cluster Euclidean for ExecutionFunction of A, Funcs(X, INT), T;
existence by Def23;
end;
:: Arithmetic of Expressions
reserve A for Euclidean preIfWhileAlgebra;
reserve X for non empty countable set;
reserve T for Subset of Funcs(X, INT);
reserve f for Euclidean ExecutionFunction of A, Funcs(X, INT), T;
definition
let A,X,T,f;
let t be INT-Expression of A,f;
redefine func -t -> INT-Expression of A,f; :: redefines - (VALUED_1, definition)
coherence by Def22;
end;
definition
let A,X,T,f;
let t be INT-Expression of A,f;
let i be Integer;
redefine func t+i -> INT-Expression of A,f; :: redefines + (VALUED_1, synonym) → + (VALUED_1, definition)
coherence
proof
A1: dom (t+.(i,X)) = Funcs(X,INT) by FUNCT_2:def 1;
A2: now
let a be object;
assume a in Funcs(X,INT);
then reconsider s = a as Element of Funcs(X,INT);
thus (t+.(i,X)).a = (t.s)+(.(i,X).s) by A1,VALUED_1:def 1
.= i+(t.a);
end;
.(i,X) is INT-Expression of A,f by Def22;
then
A3: t+.(i,X) is INT-Expression of A,f by Def22;
dom t = Funcs(X,INT) by FUNCT_2:def 1;
hence thesis by A3,A1,A2,VALUED_1:def 2;
end;
redefine func t-i -> INT-Expression of A,f; :: redefines - (VALUED_1, definition)
coherence
proof
.(i,X) is INT-Expression of A,f by Def22;
then -.(i,X) is INT-Expression of A,f by Def22;
then
A4: t+-.(i,X) is INT-Expression of A,f by Def22;
A5: dom t = Funcs(X,INT) by FUNCT_2:def 1;
A6: dom (t+-.(i,X)) = Funcs(X,INT) by FUNCT_2:def 1;
A7: now
let a be object;
assume a in Funcs(X,INT);
then reconsider s = a as Element of Funcs(X,INT);
thus (t+-.(i,X)).a = (t.s)+(-.(i,X)).s by A6,VALUED_1:def 1
.= (t.s)+-(.(i,X).s) by VALUED_1:8
.= (t.s)-i
.= (t-i).a by A5,VALUED_1:3;
end;
dom (t-i) = dom t by VALUED_1:3;
hence thesis by A4,A6,A5,A7,FUNCT_1:2;
end;
redefine func t*i -> INT-Expression of A,f; :: redefines * (AOFA_I00, synonym) → (#) (VALUED_1, definition)
coherence
proof
A8: dom (t(#).(i,X)) = Funcs(X,INT) by FUNCT_2:def 1;
A9: now
let a be object;
assume a in Funcs(X,INT);
then reconsider s = a as Element of Funcs(X,INT);
thus (t(#).(i,X)).a = (t.s)*(.(i,X).s) by A8,VALUED_1:def 4
.= i*(t.a);
end;
.(i,X) is INT-Expression of A,f by Def22;
then
A10: t(#).(i,X) is INT-Expression of A,f by Def22;
dom t = Funcs(X,INT) by FUNCT_2:def 1;
hence thesis by A10,A8,A9,VALUED_1:def 5;
end;
end;
definition
let A,X,T,f;
let t1,t2 be INT-Expression of A,f;
redefine func t1-t2 -> INT-Expression of A,f; :: redefines - (VALUED_1, definition)
coherence
proof
-t2 is INT-Expression of A,f;
hence thesis by Def22;
end;
redefine func t1+t2 -> INT-Expression of A,f; :: redefines + (VALUED_1, definition)
coherence by Def22;
redefine func t1(#)t2 -> INT-Expression of A,f; :: redefines (#) (VALUED_1, definition)
coherence by Def22;
end;
definition
let A,X,T,f;
let t1,t2 be INT-Expression of A,f;
redefine func t1 div t2 -> INT-Expression of A,f means :: redefines div (AOFA_I00, definition)
: Def29:
for s being Element of Funcs(X, INT) holds it.s = t1.s div t2.s;
coherence by Def22;
compatibility
proof
let ti be INT-Expression of A,f;
A1: dom t1 = Funcs(X, INT) by FUNCT_2:def 1;
A2: dom t2 = Funcs(X, INT) by FUNCT_2:def 1;
A3: dom (t1 div t2) = (dom t1)/\dom t2 by Def3;
hence
ti = t1 div t2 implies for s being Element of Funcs(X, INT) holds ti.
s = t1.s div t2.s by A1,A2,Def3;
A4: dom ti = Funcs(X, INT) by FUNCT_2:def 1;
assume for s being Element of Funcs(X, INT) holds ti.s = t1.s div t2.s;
then for s being object st s in Funcs(X, INT) holds ti.s = t1.s div t2.s;
hence ti = t1 div t2 by A3,A1,A2,A4,Def3;
end;
redefine func t1 mod t2 -> INT-Expression of A,f means :: redefines mod (AOFA_I00, definition)
: Def30:
for s being Element of Funcs(X, INT) holds it.s = t1.s mod t2.s;
coherence by Def22;
compatibility
proof
let ti be INT-Expression of A,f;
A5: dom t1 = Funcs(X, INT) by FUNCT_2:def 1;
A6: dom t2 = Funcs(X, INT) by FUNCT_2:def 1;
A7: dom (t1 mod t2) = (dom t1)/\dom t2 by Def4;
hence
ti = t1 mod t2 implies for s being Element of Funcs(X, INT) holds ti.
s = t1.s mod t2.s by A5,A6,Def4;
A8: dom ti = Funcs(X, INT) by FUNCT_2:def 1;
assume for s being Element of Funcs(X, INT) holds ti.s = t1.s mod t2.s;
then for s being object st s in Funcs(X, INT) holds ti.s = t1.s mod t2.s;
hence ti = t1 mod t2 by A7,A5,A6,A8,Def4;
end;
redefine func leq(t1,t2) -> INT-Expression of A,f means :: redefines leq (AOFA_I00, definition)
: Def31:
for s being Element of Funcs(X, INT) holds it.s = IFGT(t1.s,t2.s,0,1);
compatibility
proof
let ti be INT-Expression of A,f;
A9: dom t1 = Funcs(X, INT) by FUNCT_2:def 1;
A10: dom t2 = Funcs(X, INT) by FUNCT_2:def 1;
A11: dom leq(t1,t2) = (dom t1)/\dom t2 by Def5;
hence
ti = leq(t1,t2) implies for s being Element of Funcs(X, INT) holds ti
.s = IFGT(t1.s,t2.s,0,1) by A9,A10,Def5;
A12: dom ti = Funcs(X, INT) by FUNCT_2:def 1;
assume
for s being Element of Funcs(X, INT) holds ti.s = IFGT(t1.s,t2.s, 0,1);
then
for s being object st s in Funcs(X, INT)
holds ti.s = IFGT(t1.s,t2.s,0,1 );
hence ti = leq(t1,t2) by A11,A9,A10,A12,Def5;
end;
coherence by Def22;
redefine func gt(t1,t2) -> INT-Expression of A,f means :: redefines gt (AOFA_I00, definition)
: Def32:
for s being Element of Funcs(X, INT) holds it.s = IFGT(t1.s,t2.s,1,0);
coherence by Def22;
compatibility
proof
let ti be INT-Expression of A,f;
A13: dom t1 = Funcs(X, INT) by FUNCT_2:def 1;
A14: dom t2 = Funcs(X, INT) by FUNCT_2:def 1;
A15: dom gt(t1,t2) = (dom t1)/\dom t2 by Def6;
hence
ti = gt(t1,t2) implies for s being Element of Funcs(X, INT) holds ti.
s = IFGT(t1.s,t2.s,1,0) by A13,A14,Def6;
A16: dom ti = Funcs(X, INT) by FUNCT_2:def 1;
assume
for s being Element of Funcs(X, INT) holds ti.s = IFGT(t1.s,t2.s, 1,0);
then
for s being object st s in Funcs(X, INT)
holds ti.s = IFGT(t1.s,t2.s,1,0 );
hence ti = gt(t1,t2) by A15,A13,A14,A16,Def6;
end;
end;
definition
let A,X,T,f;
let t1,t2 be INT-Expression of A,f;
redefine func eq(t1,t2) -> INT-Expression of A,f means :: redefines eq (AOFA_I00, definition)
for s being Element of Funcs(X , INT) holds it.s = IFEQ(t1.s,t2.s,1,0);
compatibility
proof
let ti be INT-Expression of A,f;
A1: dom t1 = Funcs(X, INT) by FUNCT_2:def 1;
A2: dom t2 = Funcs(X, INT) by FUNCT_2:def 1;
A3: dom eq(t1,t2) = (dom t1)/\dom t2 by Def7;
hence
ti = eq(t1,t2) implies for s being Element of Funcs(X, INT) holds ti.
s = IFEQ(t1.s,t2.s,1,0) by A1,A2,Def7;
A4: dom ti = Funcs(X, INT) by FUNCT_2:def 1;
assume
for s being Element of Funcs(X, INT) holds ti.s = IFEQ(t1.s,t2.s,1 ,0);
then
for s being object st s in Funcs(X, INT)
holds ti.s = IFEQ(t1.s,t2.s,1,0);
hence ti = eq(t1,t2) by A3,A1,A2,A4,Def7;
end;
coherence
proof
reconsider l1 = leq(t1,t2), l2 = leq(t2,t1) as INT-Expression of A,f;
A5: dom (l1(#)l2) = Funcs(X,INT) by FUNCT_2:def 1;
A6: dom eq(t1,t2) = Funcs(X,INT) by FUNCT_2:def 1;
now
let a be object;
assume a in Funcs(X,INT);
then reconsider s = a as Element of Funcs(X,INT);
A7: t1.s = t2.s or t1.s < t2.s or t2.s < t1.s by XXREAL_0:1;
A8: l2.s = IFGT(t2.s,t1.s,0,1) by Def31;
A9: (l1(#)l2).s = (l1.s)*(l2.s) by A5,VALUED_1:def 4;
A10: l1.s = IFGT(t1.s,t2.s,0,1) by Def31;
eq(t1,t2).s = IFEQ(t1.s,t2.s,1,0) by A6,Def7;
then
eq(t1,t2).s = 1 & l1.s = 1 & l2.s = 1 or eq(t1,t2).s = 0 & l1.s = 0
& l2.s = 1 or eq(t1,t2).s = 0 & l1.s = 1 & l2.s = 0 by A8,A10,A7,
FUNCOP_1:def 8,XXREAL_0:def 11;
hence eq(t1,t2).a = (l1(#)l2).a by A9;
end;
hence thesis by A6,A5,FUNCT_1:2;
end;
end;
definition
let A,X,T,f;
let v be INT-Variable of A,f;
func .v -> INT-Expression of A,f equals
.v;
coherence by Def22;
end;
definition
let A,X,T,f;
let x be Element of X;
func x^(A,f) -> INT-Variable of A,f equals
^x;
coherence by Def22;
end;
notation
let A,X,T,f;
let x be Variable of f;
synonym ^x for x^(A,f);
end;
definition
let A,X,T,f;
let x be Variable of f;
func .x -> INT-Expression of A,f equals
.(^x);
coherence;
end;
theorem Th22:
for x being Variable of f for s being Element of Funcs(X, INT)
holds (.x).s = s.x
proof
let x be Variable of f;
let s be Element of Funcs(X, INT);
thus (.x).s = s.((x^(A,f)).s) by Def19
.= s.x;
end;
definition
let A,X,T,f;
let i be Integer;
func .(i,A,f) -> INT-Expression of A,f equals
.(i,X);
coherence by Def22;
end;
definition :: "choose" function may cause some problems in further development.
let A,X,T,f;
let v be INT-Variable of A,f;
let t be INT-Expression of A,f;
func v:=t -> Element of A equals
the Element of {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
proof
set Y = {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)};
A1: Y c= the carrier of A
proof
let i be object;
assume i in Y;
then ex I being Element of A st i = I & I in ElementaryInstructions A &
for s being Element of Funcs(X, INT) holds f.(s,I) = s+*(v.s,t.s);
hence thesis;
end;
v,t form_assignment_wrt f by Def22;
then consider I0 being Element of A such that
A2: I0 in ElementaryInstructions A and
A3: for s being Element of Funcs(X, INT) holds f.(s,I0) = s+*(v.s,t.s);
I0 in Y by A2,A3;
then the Element of Y in Y;
hence thesis by A1;
end;
end;
theorem Th23:
for v being INT-Variable of A,f for t being INT-Expression of A,
f holds v:=t in ElementaryInstructions A
proof
let v be INT-Variable of A,f;
let t be INT-Expression of A,f;
set Y = {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)};
v,t form_assignment_wrt f by Def22;
then consider I0 being Element of A such that
A1: I0 in ElementaryInstructions A and
A2: for s being Element of Funcs(X, INT) holds f.(s,I0) = s+*(v.s,t.s);
I0 in Y by A1,A2;
then v:=t in Y;
then ex I being Element of A st v:=t = I & I in ElementaryInstructions A &
for s being Element of Funcs(X, INT) holds f.(s,I) = s+*(v.s,t.s);
hence thesis;
end;
registration
let A,X,T,f;
let v be INT-Variable of A,f;
let t be INT-Expression of A,f;
cluster v:=t -> absolutely-terminating;
coherence by Th23,AOFA_000:95;
end;
definition
let A,X,T,f;
let v be INT-Variable of A,f;
let t be INT-Expression of A,f;
func v+=t -> absolutely-terminating Element of A equals
v:=(.v+t);
coherence;
func v*=t -> absolutely-terminating Element of A equals
v:=(.v(#)t);
coherence;
end;
definition
let A,X,T,f;
let x be Element of X;
let t be INT-Expression of A,f;
func x:=t -> absolutely-terminating Element of A equals
x^(A,f):=t;
correctness;
end;
definition
let A,X,T,f;
let x be Element of X;
let y be Variable of f;
func x:=y -> absolutely-terminating Element of A equals
x:=.y;
correctness;
end;
definition
let A,X,T,f;
let x be Element of X;
let v be INT-Variable of A,f;
func x:=v -> absolutely-terminating Element of A equals
x:=.v;
correctness;
end;
definition
let A,X,T,f;
let v,w be INT-Variable of A,f;
func v:=w -> absolutely-terminating Element of A equals
v:=.w;
correctness;
end;
definition
let A,X,T,f;
let x be Variable of f;
let i be Integer;
func x:=i -> absolutely-terminating Element of A equals
x:=.(i,A,f);
correctness;
end;
definition
let A,X,T,f;
let v1,v2 be INT-Variable of A,f;
let x be Variable of f;
func swap(v1,x,v2) -> absolutely-terminating Element of A equals
x:=v1\;v1:=
v2\;v2:=.x;
coherence;
end;
definition
let A,X,T,f;
let x be Variable of f;
let t be INT-Expression of A,f;
func x+=t -> absolutely-terminating Element of A equals
x:=(.x+t);
correctness;
func x*=t -> absolutely-terminating Element of A equals
x:=(.x(#)t);
correctness;
func x%=t -> absolutely-terminating Element of A equals
x:=(.x mod t);
correctness;
func x/=t -> absolutely-terminating Element of A equals
x:=(.x div t);
correctness;
end;
definition
let A,X,T,f;
let x be Variable of f;
let i be Integer;
func x+=i -> absolutely-terminating Element of A equals
x:=(.x+i);
correctness;
func x*=i -> absolutely-terminating Element of A equals
x:=(.x*i);
correctness;
func x%=i -> absolutely-terminating Element of A equals
x:=(.x mod .(i,A,f));
correctness;
func x/=i -> absolutely-terminating Element of A equals
x:=(.x div .(i,A,f));
correctness;
func x div i -> INT-Expression of A,f equals
.x div .(i,A,f);
correctness;
end;
definition
let A,X,T,f;
let v be INT-Variable of A,f;
let i be Integer;
func v:=i -> absolutely-terminating Element of A equals
v:=.(i,A,f);
correctness;
end;
definition
let A,X,T,f;
let v be INT-Variable of A,f;
let i be Integer;
func v+=i -> absolutely-terminating Element of A equals
v:=(.v+i);
correctness;
func v*=i -> absolutely-terminating Element of A equals
v:=(.v*i);
correctness;
end;
definition
let A,X;
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;
func t1 is_even -> absolutely-terminating Element of A equals
b:=((t1+1) mod
.(2,A,g));
coherence;
let t2 be INT-Expression of A,g;
func t1 leq t2 -> absolutely-terminating Element of A equals
b:=leq(t1,t2);
coherence;
func t1 gt t2 -> absolutely-terminating Element of A equals
b:=gt(t1,t2);
coherence;
func t1 eq t2 -> absolutely-terminating Element of A equals
b:=eq(t1,t2);
coherence;
end;
notation
let A,X;
let b be Element of X;
let g be Euclidean ExecutionFunction of A, Funcs(X,INT), Funcs(X, INT)\(b,0);
let t1,t2 be INT-Expression of A,g;
synonym t2 geq t1 for t1 leq t2;
synonym t2 lt t1 for t1 gt t2;
end;
definition
let A,X;
let b be Element of X;
let g be Euclidean ExecutionFunction of A, Funcs(X,INT), Funcs(X, INT)\(b,0);
let v1,v2 be INT-Variable of A,g;
func v1 leq v2 -> absolutely-terminating Element of A equals
.v1 leq .v2;
coherence;
func v1 gt v2 -> absolutely-terminating Element of A equals
.v1 gt .v2;
coherence;
end;
notation
let A,X;
let b be Element of X;
let g be Euclidean ExecutionFunction of A, Funcs(X,INT), Funcs(X, INT)\(b,0);
let v1,v2 be INT-Variable of A,g;
synonym v2 geq v1 for v1 leq v2;
synonym v2 lt v1 for v1 gt v2;
end;
definition
let A,X;
let b be Element of X;
let g be Euclidean ExecutionFunction of A, Funcs(X,INT), Funcs(X, INT)\(b,0);
let x1 be Variable of g;
func x1 is_odd -> absolutely-terminating Element of A equals
.x1 is_odd;
coherence;
func x1 is_even -> absolutely-terminating Element of A equals
.x1 is_even;
coherence;
let x2 be Variable of g;
func x1 leq x2 -> absolutely-terminating Element of A equals
.x1 leq .x2;
coherence;
func x1 gt x2 -> absolutely-terminating Element of A equals
.x1 gt .x2;
coherence;
end;
notation
let A,X;
let b be Element of X;
let g be Euclidean ExecutionFunction of A, Funcs(X,INT), Funcs(X, INT)\(b,0);
let x1,x2 be Variable of g;
synonym x2 geq x1 for x1 leq x2;
synonym x2 lt x1 for x1 gt x2;
end;
definition
let A,X;
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;
func x leq i -> absolutely-terminating Element of A equals
.x leq .(i,A,g);
coherence;
func x geq i -> absolutely-terminating Element of A equals
.x geq .(i,A,g);
coherence;
func x gt i -> absolutely-terminating Element of A equals
.x gt .(i,A,g);
coherence;
func x lt i -> absolutely-terminating Element of A equals
.x lt .(i,A,g);
coherence;
func x / i -> INT-Expression of A,g equals
(.x) div .(i,A,g);
coherence;
end;
definition
let A,X,T,f;
let x1,x2 be Variable of f;
func x1+=x2 -> absolutely-terminating Element of A equals
x1+=.x2;
coherence;
func x1*=x2 -> absolutely-terminating Element of A equals
x1*=.x2;
coherence;
func x1%=x2 -> absolutely-terminating Element of A equals
x1:=(.x1 mod .x2);
coherence;
func x1/=x2 -> absolutely-terminating Element of A equals
x1:=(.x1 div .x2);
coherence;
func x1+x2 -> INT-Expression of A,f equals
(.x1)+(.x2);
coherence;
func x1*x2 -> INT-Expression of A,f equals
(.x1)(#)(.x2);
coherence;
func x1 mod x2 -> INT-Expression of A,f equals
(.x1)mod(.x2);
coherence;
func x1 div x2 -> INT-Expression of A,f equals
(.x1)div(.x2);
coherence;
end;
reserve A for Euclidean preIfWhileAlgebra,
X for non empty countable set,
z for (Element of X),
s,s9 for (Element of Funcs(X, INT)),
T for Subset of Funcs(X, INT),
f for Euclidean ExecutionFunction of A, Funcs(X, INT), T,
v for INT-Variable of A,f,
t for INT-Expression of A,f;
reserve i for Integer;
theorem Th24:
f.(s, v:=t).(v.s) = t.s & for z st z <> v.s holds f.(s, v:=t).z = s.z
proof
set Y = {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)};
v,t form_assignment_wrt f by Def22;
then consider I0 being Element of A such that
A1: I0 in ElementaryInstructions A and
A2: for s being Element of Funcs(X, INT) holds f.(s,I0) = s+*(v.s,t.s);
I0 in Y by A1,A2;
then v:=t in Y;
then
ex I being Element of A st v:=t = I & I in ElementaryInstructions A &
for s being Element of Funcs(X, INT) holds f.(s,I) = s+*(v.s,t.s);
then
A3: f.(s, v:=t) = s+*(v.s,t.s);
dom s = X by FUNCT_2:def 1;
hence thesis by A3,FUNCT_7:31,32;
end;
theorem Th25:
for x being Variable of f for i being Integer holds f.(s,
x:=i).x = i & for z st z <> x holds f.(s, x:=i).z = s.z
proof
let x be Variable of f;
let i be Integer;
A1: .(i,A,f).s = i;
(^x).s = x;
hence thesis by A1,Th24;
end;
theorem Th26:
for x being Variable of f for t being INT-Expression of A,f
holds f.(s, x:=t).x = t.s & for z st z <> x holds f.(s, x:=t).z = s.z
proof
let x be Variable of f;
let t be INT-Expression of A,f;
(^x).s = x;
hence thesis by Th24;
end;
theorem Th27:
for x,y being Variable of f holds f.(s, x:=y).x = s.y & for z st
z <> x holds f.(s, x:=y).z = s.z
proof
let x,y be Variable of f;
(.y).s = s.y by Th22;
hence thesis by Th26;
end;
theorem Th28:
for x being Variable of f holds f.(s, x+=i).x = s.x+i & for z st
z <> x holds f.(s, x+=i).z = s.z
proof
let x be Variable of f;
A2: .(^(x qua Element of X)).s = s.((^(x qua Element of X)).s) by Def19;
(.x+i).s = ((.x).s+i) by Def8;
hence thesis by A2,Th24;
end;
theorem Th29:
for x being Variable of f for t being INT-Expression of A,f
holds f.(s, x+=t).x = s.x+t.s & for z st z <> x holds f.(s, x+=t).z = s.z
proof
let x be Variable of f;
let t be INT-Expression of A,f;
A1: (^x).s = x;
dom (.x+t) = Funcs(X, INT) by FUNCT_2:def 1;
then
A2: (.x+t).s = (.x).s+t.s by VALUED_1:def 1;
(.x).s = s.x by Th22;
hence thesis by A1,A2,Th24;
end;
theorem Th30:
for x,y being Variable of f holds f.(s, x+=y).x = s.x+s.y & for
z st z <> x holds f.(s, x+=y).z = s.z
proof
let x,y be Variable of f;
(.y).s = s.y by Th22;
hence thesis by Th29;
end;
theorem Th31:
for x being Variable of f holds f.(s, x*=i).x = s.x*i & for z st
z <> x holds f.(s, x*=i).z = s.z
proof
let x be Variable of f;
A2: .(^(x qua Element of X)).s = s.((^(x qua Element of X)).s) by Def19;
(.x*i).s = ((.x).s*i) by Def10;
hence thesis by A2,Th24;
end;
theorem Th32:
for x being Variable of f for t being INT-Expression of A,f
holds f.(s, x*=t).x = s.x*t.s & for z st z <> x holds f.(s, x*=t).z = s.z
proof
let x be Variable of f;
let t be INT-Expression of A,f;
A1: (^x).s = x;
dom (.x(#)t) = Funcs(X, INT) by FUNCT_2:def 1;
then
A2: (.x(#)t).s = (.x).s*t.s by VALUED_1:def 4;
(.x).s = s.x by Th22;
hence thesis by A1,A2,Th24;
end;
theorem Th33:
for x,y being Variable of f holds f.(s, x*=y).x = s.x*s.y & for
z st z <> x holds f.(s, x*=y).z = s.z
proof
let x,y be Variable of f;
A1: dom (.x(#).y) = Funcs(X, INT) by FUNCT_2:def 1;
(^x).s = x;
hence f.(s, x*=y).x = (.x(#).y).s by Th24
.= ((.x).s)*(.y.s) by A1,VALUED_1:def 4
.= (s.x)*(.y.s) by Th22
.= (s.x)*(s.y) by Th22;
thus thesis by Th26;
end;
theorem Th34:
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 for i
being Integer 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 st z <> b holds g.(s, x leq i).z = s.
z & g.(s, x geq i).z = s.z
proof
let b be Element of X;
let f be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
reconsider b9 = b as Variable of f by Def2;
let x be Variable of f;
let i be Integer;
set v = ^b9;
A2: v.s = b;
A3: (.x).s < i implies IFGT(i,(.x).s,0,1) = 0 by XXREAL_0:def 11;
A4: (.x).s >= i implies IFGT(i,(.x).s,0,1) = 1 by XXREAL_0:def 11;
A5: leq(.(i,A,f),.x).s = IFGT(.(i,A,f).s,(.x).s,0,1) by Def31;
A6: (.x).s > i implies IFGT((.x).s,i,0,1) = 0 by XXREAL_0:def 11;
A7: leq(.x,.(i,A,f)).s = IFGT((.x).s,.(i,A,f).s,0,1) by Def31;
A8: (.x).s <= i implies IFGT((.x).s,i,0,1) = 1 by XXREAL_0:def 11;
(.x).s = s.((^x).s) by Def19;
hence thesis by A2,A8,A6,A4,A3,A7,A5,Th24;
end;
theorem Th35:
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 st z <> b holds g.(s, x leq y).z = s.z
proof
let b be Element of X;
let f be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
reconsider b9 = b as Variable of f by Def2;
let x,y be Variable of f;
set v = ^b9;
A1: v.s = b;
A2: (.x).s <= .y.s implies IFGT((.x).s,(.y).s,0,1) = 1 by XXREAL_0:def 11;
(.x).s = s.((^x).s) by Def19;
then
A3: s.x = (.x).s;
A4: (.x).s > .y.s implies IFGT((.x).s,(.y).s,0,1) = 0 by XXREAL_0:def 11;
A5: leq(.x,.y).s = IFGT((.x).s,(.y).s,0,1) by Def31;
(.y).s = s.((^y).s) by Def19;
hence thesis by A3,A1,A2,A4,A5,Th24;
end;
theorem
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
holds (s.x <= i iff g.(s, x leq i) in Funcs(X,INT)\(b,0)) & (s.x >= i
iff g.(s, x geq i) in Funcs(X,INT)\(b,0))
proof
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;
g.(s, x leq i) in Funcs(X,INT)\(b,0) iff g.(s, x leq i).b <> 0 by Th2;
hence s.x <= i iff g.(s, x leq i) in Funcs(X,INT)\(b,0) by Th34;
g.(s, x geq i) in Funcs(X,INT)\(b,0) iff g.(s, x geq i).b <> 0 by Th2;
hence thesis by Th34;
end;
theorem
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
iff g.(s, x leq y) in Funcs(X,INT)\(b,0)) & (s.x >= s.y iff g.(s, x geq y) in
Funcs(X,INT)\(b,0))
proof
let b be Element of X;
let g be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
let x,y be Variable of g;
g.(s, x leq y) in Funcs(X,INT)\(b,0) iff g.(s, x leq y).b <> 0 by Th2;
hence s.x <= s.y iff g.(s, x leq y) in Funcs(X,INT)\(b,0) by Th35;
g.(s, x geq y) in Funcs(X,INT)\(b,0) iff g.(s, x geq y).b <> 0 by Th2;
hence thesis by Th35;
end;
theorem Th38:
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 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 st z <> b holds g.(s, x gt i).z = s.z & g.
(s, x lt i).z = s.z
proof
let b be Element of X;
let f be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
reconsider b9 = b as Variable of f by Def2;
let x be Variable of f;
let i be Integer;
set v = ^b9;
A2: v.s = b;
A3: (.x).s >= i implies IFGT(i,(.x).s,1,0) = 0 by XXREAL_0:def 11;
A4: (.x).s < i implies IFGT(i,(.x).s,1,0) = 1 by XXREAL_0:def 11;
A5: gt(.(i,A,f),.x).s = IFGT((.(i,A,f)).s,(.x).s,1,0) by Def32;
A6: (.x).s <= i implies IFGT((.x).s,i,1,0) = 0 by XXREAL_0:def 11;
A7: gt(.x,.(i,A,f)).s = IFGT((.x).s,(.(i,A,f)).s,1,0) by Def32;
A8: (.x).s > i implies IFGT((.x).s,i,1,0) = 1 by XXREAL_0:def 11;
(.x).s = s.((^x).s) by Def19;
hence thesis by A2,A8,A6,A4,A3,A7,A5,Th24;
end;
theorem Th39:
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 st z <> b holds g.(s, x gt y).z = s.z & g.(s, x lt y).z = s.z
proof
let b be Element of X;
let f be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
reconsider b9 = b as Variable of f by Def2;
let x,y be Variable of f;
set v = ^b9;
A1: v.s = b;
A2: (.x).s > .y.s implies IFGT((.x).s,(.y).s,1,0) = 1 by XXREAL_0:def 11;
A3: gt(.x,.y).s = IFGT((.x).s,(.y).s,1,0) by Def32;
A4: (.x).s < .y.s implies IFGT((.y).s,(.x).s,1,0) = 1 by XXREAL_0:def 11;
(.x).s = s.((^x).s) by Def19;
then
A5: s.x = (.x).s;
A6: (.x).s <= .y.s implies IFGT((.x).s,(.y).s,1,0) = 0 by XXREAL_0:def 11;
A7: gt(.y,.x).s = IFGT((.y).s,(.x).s,1,0) by Def32;
A8: (.x).s >= .y.s implies IFGT((.y).s,(.x).s,1,0) = 0 by XXREAL_0:def 11;
(.y).s = s.((^y).s) by Def19;
hence thesis by A5,A1,A2,A6,A4,A8,A3,A7,Th24;
end;
theorem Th40:
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 holds (s.x > i iff g.(s, x gt i) in Funcs(X,INT)\(b,0)) & (s.x <
i iff g.(s, x lt i) in Funcs(X,INT)\(b,0))
proof
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;
g.(s, x gt i) in Funcs(X,INT)\(b,0) iff g.(s, x gt i).b <> 0 by Th2;
hence s.x > i iff g.(s, x gt i) in Funcs(X,INT)\(b,0) by Th38;
g.(s, x lt i) in Funcs(X,INT)\(b,0) iff g.(s, x lt i).b <> 0 by Th2;
hence thesis by Th38;
end;
theorem
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
iff g.(s, x gt y) in Funcs(X,INT)\(b,0)) & (s.x < s.y iff g.(s, x lt y) in
Funcs(X,INT)\(b,0))
proof
let b be Element of X;
let g be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
let x,y be Variable of g;
g.(s, x gt y) in Funcs(X,INT)\(b,0) iff g.(s, x gt y).b <> 0 by Th2;
hence s.x > s.y iff g.(s, x gt y) in Funcs(X,INT)\(b,0) by Th39;
g.(s, x lt y) in Funcs(X,INT)\(b,0) iff g.(s, x lt y).b <> 0 by Th2;
hence thesis by Th39;
end;
theorem
for x being Variable of f holds f.(s, x%=i).x = s.x mod i & for z st z
<> x holds f.(s, x%=i).z = s.z
proof
let x be Variable of f;
A3: .(^(x qua Element of X)).s = s.((^(x qua Element of X)).s) by Def19;
(.x mod .(i,A,f)).s = (.x).s mod (.(i,A,f).s) by Def30;
hence thesis by A3,Th24;
end;
theorem Th43:
for x being Variable of f for t being INT-Expression of A,f
holds f.(s, x%=t).x = s.x mod t.s & for z st z <> x holds f.(s, x%=t).z = s.z
proof
let x be Variable of f;
let t be INT-Expression of A,f;
A1: (^x).s = x;
A2: (.x).s = s.x by Th22;
(.x mod t).s = (.x).s mod t.s by Def30;
hence thesis by A1,A2,Th24;
end;
theorem Th44:
for x,y being Variable of f holds f.(s, x%=y).x = s.x mod s.y &
for z st z <> x holds f.(s, x%=y).z = s.z
proof
let x,y be Variable of f;
A1: x%=y = x%=.y;
(.y).s = s.y by Th22;
hence thesis by A1,Th43;
end;
theorem Th45:
for x being Variable of f holds f.(s, x/=i).x = s.x div i & for
z st z <> x holds f.(s, x/=i).z = s.z
proof
let x be Variable of f;
A3: .(^(x qua Element of X)).s = s.((^(x qua Element of X)).s) by Def19;
(.x div .(i,A,f)).s = (.x).s div (.(i,A,f).s) by Def29;
hence thesis by A3,Th24;
end;
theorem Th46:
for x being Variable of f for t being INT-Expression of A,f
holds f.(s, x/=t).x = s.x div t.s & for z st z <> x holds f.(s, x/=t).z = s.z
proof
let x be Variable of f;
let t be INT-Expression of A,f;
A1: (^x).s = x;
A2: (.x).s = s.x by Th22;
(.x div t).s = (.x).s div t.s by Def29;
hence thesis by A1,A2,Th24;
end;
theorem
for x,y being Variable of f holds f.(s, x/=y).x = s.x div s.y & for z
st z <> x holds f.(s, x/=y).z = s.z
proof
let x,y be Variable of f;
A1: x/=y = x/=.y;
(.y).s = s.y by Th22;
hence thesis by A1,Th46;
end;
theorem Th48:
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 st
z <> b holds g.(s, t is_odd).z = s.z & g.(s, t is_even).z = s.z
proof
let b be Element of X;
let f be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
let t be INT-Expression of A,f;
reconsider y = b as Variable of f by Def2;
A1: t is_odd = y:=(t mod .(2,A,f));
dom(t+1) = Funcs(X,INT) by FUNCT_2:def 1;
then
A2: (t+1).s = 1+(t.s) by VALUED_1:def 2;
A3: .(2,A,f).s = 2;
then
A4: ((t+1) mod .(2,A,f)).s = ((t+1).s) mod 2 by Def30;
(t mod .(2,A,f)).s = (t.s) mod 2 by A3,Def30;
hence thesis by A1,A2,A4,Th26;
end;
theorem Th49:
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 g.(s, x
is_odd).b = s.x mod 2 & g.(s, x is_even).b = (s.x+1) mod 2 & for z st z <> b
holds g.(s, x is_odd).z = s.z
proof
let b be Element of X;
let f be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
let x be Variable of f;
(.x).s = s.x by Th22;
hence thesis by Th48;
end;
theorem Th50:
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 iff g.(s, t is_odd) in Funcs(X,INT)\(b,0)) & (t.s is even iff g.(s,
t is_even) in Funcs(X,INT)\(b,0))
proof
let b be Element of X;
let f be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
let t be INT-Expression of A,f;
A1: (t.s) mod 2 = 0 or (t.s) mod 2 = 1 by PRE_FF:6;
A2: t.s = ((t.s) div 2)*2 + ((t.s) mod 2) by INT_1:59;
f.(s, t is_odd).b = (t.s) mod 2 by Th48;
hence t.s is odd iff f.(s, t is_odd) in Funcs(X,INT)\(b,0) by A1,A2,Th2;
A3: (t.s+1) mod 2 = 0 or (t.s+1) mod 2 = 1 by PRE_FF:6;
A4: t.s+1 = ((t.s+1) div 2)*2 + ((t.s+1) mod 2) by INT_1:59;
f.(s, t is_even).b = (t.s+1) mod 2 by Th48;
hence thesis by A3,A4,Th2;
end;
theorem
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
iff g.(s, x is_odd) in Funcs(X,INT)\(b,0)) & (s.x is even iff g.(s, x is_even)
in Funcs(X,INT)\(b,0))
proof
let b be Element of X;
let f be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
let x be Variable of f;
(.x).s = s.x by Th22;
hence thesis by Th50;
end;
scheme
ForToIteration {A() -> Euclidean preIfWhileAlgebra, X() -> countable non
empty set, b() -> (Element of X()), I,F() -> (Element of A()), g() -> Euclidean
ExecutionFunction of A(), Funcs(X(),INT), Funcs(X(),INT)\(b(),0), i,n() -> (
Variable of g()), s() -> (Element of Funcs(X(),INT)), a() -> INT-Expression of
A(),g(), P[set] }: P[g().(s(),F())] & (a().s() <= s().n() implies g().(s(),F())
.i() = s().n()+1) & (a().s() > s().n() implies g().(s(),F()).i() = a().s()) & g
().(s(),F()).n() = s().n()
provided
A1: F() = for-do(i():=a(), i() leq n(), i()+=1, I()) and
A2: P[g().(s(),i():=a())] and
A3: for s being Element of Funcs(X(),INT) st P[s] holds P[g().(s,I()\;i(
)+=1)] & P[g().(s, i() leq n())] and
A4: for s being Element of Funcs(X(),INT) st P[s] holds g().(s,I()).i()
= s.i() & g().(s,I()).n() = s.n() and
A5: n() <> i() & n() <> b() & i() <> b()
proof
set C = i() leq n();
set S = Funcs(X(),INT);
reconsider s1 = g().(s(),i():=a()) as Element of S;
reconsider s2 = g().(s1,C) as Element of S;
A6: P[s2] by A2,A3;
defpred Q[Element of S] means P[$1] & (a().s() <= s().n() implies $1.i()-1
<= s().n()) & $1.n() = s().n();
A7: s1.i() = a().s() by Th26;
then
A8: s2.i() = a().s() by A5,Th35;
defpred R[Element of S] means $1.i() <= $1.n();
set T = S\(b(),0);
A9: g() complies_with_while_wrt T by AOFA_000:def 32;
set II = I()\;i()+=1;
A10: g().(s(),F()) = g().(s1,while(C, II)) by A1,AOFA_000:def 29;
a().s()-1 < a().s() by XREAL_1:44;
then
A11: Q[s1] by A2,A5,A7,Th26,XXREAL_0:2;
A12: s1.n() = s().n() by A5,Th26;
then
A13: s2.n() = s().n() by A5,Th35;
per cases;
suppose
A14: a().s() <= s().n();
deffunc F(Element of S) = In($1.n()+1-$1.i(),NAT);
defpred PR[Element of S] means P[$1] & R[$1];
A15: for s being Element of S st Q[s] & s in T & R[s] holds Q[g().(s,II)
qua Element of S]
proof
let s be Element of S;
assume that
A16: Q[s] and
s in T and
A17: R[s];
thus P[g().(s,II)] by A3,A16;
reconsider s9 = g().(s,I()) as Element of S;
reconsider s99 = g().(s9,i()+=1) as Element of S;
A18: s99 = g().(s,II) by AOFA_000:def 29;
A19: s99.i() = s9.i()+1 by Th28;
s9.n() = s.n() by A4,A16;
hence thesis by A4,A5,A16,A17,A19,A18,Th28;
end;
A20: for s being Element of S st PR[s] holds (PR[g().(s,II\;C) qua Element
of S] iff g().(s,II\;C) in T) & F(g().(s,II\;C) qua Element of S) < F(s)
proof
let s be Element of S;
reconsider s9 = g().(s,I()) as Element of S;
reconsider s99 = g().(s9,i()+=1) as Element of S;
reconsider s999 = g().(s99,C) as Element of S;
A21: g().(s,II\;C) = g().(g().(s,II),C) by AOFA_000:def 29;
A22: s99.n() = s9.n() by A5,Th28;
A23: s99.i() <= s99.n() implies s999.b() = 1 by Th35;
A24: s99.i() > s99.n() implies s999.b() = 0 by Th35;
assume
A25: PR[s];
then reconsider j = s.n()-s.i() as Element of NAT by INT_1:5;
A26: s999.i() = s99.i() by A5,Th35;
A27: s99 = g().(s,II) by AOFA_000:def 29;
then P[s99] by A3,A25;
hence
PR[g().(s,II\;C) qua Element of S] iff g().(s,II\;C) in T by A3,A5,A21
,A27,A26,A24,A23,Th2,Th35;
A28: s99.i() = s9.i()+1 by Th28;
A29: s9.n() = s.n() by A4,A25;
A30: s9.i() = s.i() by A4,A25;
s999.n() = s99.n() by A5,Th35;
then F(s999) = j by A26,A30,A29,A28,A22;
then F(s999)+1 = F(s);
hence thesis by A21,A27,NAT_1:13;
end;
A31: for s being Element of S st Q[s] holds Q[g().(s,C) qua Element of S]
& (g().(s,C) in T iff R[g().(s,C) qua Element of S])
proof
let s be Element of S;
A32: s.i() > s.n() implies g().(s,C).b() = 0 by Th35;
assume
A33: Q[s];
hence P[g().(s,C)] by A3;
A34: s.i() <= s.n() implies g().(s,C).b() = 1 by Th35;
g().(s,C).i() = s.i() by A5,Th35;
hence thesis by A5,A33,A32,A34,Th2,Th35;
end;
s2.b() = 1 by A7,A12,A14,Th35;
then
A35: g().(s1,C) in T iff PR[g().(s1,C) qua Element of S] by A2,A3,A5,A12,A8,A14
,Th35;
A36: g() iteration_terminates_for II\;C, g().(s1,C) from AOFA_000:sch 3(
A35,A20);
A37: Q[g().(s1,while(C,II)) qua Element of S] & not R[g().(s1,while(C,II))
qua Element of S] from AOFA_000:sch 5(A11,A36,A15,A31);
then (g().(s(),F()) qua Element of S).i() >= s().n()+1 by A10,INT_1:7;
then (g().(s(),F()) qua Element of S).i()-1 >= s().n()+1-1 by XREAL_1:13;
then (g().(s(),F()) qua Element of S).i()-1 = s().n() by A10,A14,A37,
XXREAL_0:1;
hence thesis by A1,A14,A37,AOFA_000:def 29;
end;
suppose
A38: a().s() > s().n();
then s2.b() = 0 by A7,A12,Th35;
then s2 nin T by Th2;
hence thesis by A9,A8,A13,A10,A6,A38;
end;
end;
scheme
ForDowntoIteration {A() -> Euclidean preIfWhileAlgebra, X() -> countable non
empty set, b() -> (Element of X()), I,F() -> (Element of A()), f() -> Euclidean
ExecutionFunction of A(), Funcs(X(),INT), Funcs(X(),INT)\(b(),0), i,n() -> (
Variable of f()), s() -> (Element of Funcs(X(),INT)), a() -> INT-Expression of
A(),f(), P[set] }: P[f().(s(),F())] & (a().s() >= s().n() implies f().(s(),F())
.i() = s().n()-1) & (a().s() < s().n() implies f().(s(),F()).i() = a().s()) & f
().(s(),F()).n() = s().n()
provided
A1: F() = for-do(i():=a(),.n() leq .i(),i()+=-1,I()) and
A2: P[f().(s(),i():=a())] and
A3: for s being Element of Funcs(X(),INT) st P[s] holds P[f().(s,I()\;i(
)+=-1)] & P[f().(s, n() leq i())] and
A4: for s being Element of Funcs(X(),INT) st P[s] holds f().(s,I()).i()
= s.i() & f().(s,I()).n() = s.n() and
A5: n() <> i() & n() <> b() & i() <> b()
proof
set S = Funcs(X(),INT);
reconsider s1 = f().(s(),i():=a()) as Element of S;
set C = n() leq i();
reconsider s2 = f().(s1,C) as Element of S;
A6: P[s2] by A2,A3;
defpred Q[Element of S] means P[$1] & (a().s() >= s().n() implies $1.i()+1
>= s().n()) & $1.n() = s().n();
A7: s1.i() = a().s() by Th26;
then
A8: Q[s1] by A2,A5,Th26,XREAL_1:39;
A9: s2.i() = a().s() by A5,A7,Th35;
defpred R[Element of S] means $1.i() >= $1.n();
set T = S\(b(),0);
A10: f() complies_with_while_wrt T by AOFA_000:def 32;
set II = I()\;i()+=-1;
A11: f().(s(),F()) = f().(s1,while(C, II)) by A1,AOFA_000:def 29;
A12: s1.n() = s().n() by A5,Th26;
then
A13: s2.n() = s().n() by A5,Th35;
per cases;
suppose
A14: a().s() >= s().n();
deffunc F(Element of S) = In($1.i()+1-$1.n(),NAT);
defpred PR[Element of S] means P[$1] & R[$1];
A15: for s being Element of S st Q[s] & s in T & R[s] holds Q[f().(s,II)
qua Element of S]
proof
let s be Element of S;
assume that
A16: Q[s] and
s in T and
A17: R[s];
thus P[f().(s,II)] by A3,A16;
reconsider s99 = f().(s,I()) as Element of S;
reconsider s999 = f().(s99,i()+=-1) as Element of S;
A18: s999 = f().(s,II) by AOFA_000:def 29;
A19: s999.i() = s99.i()-1 by Th28;
s99.n() = s.n() by A4,A16;
hence thesis by A4,A5,A16,A17,A19,A18,Th28;
end;
A20: for s being Element of S st PR[s] holds (PR[f().(s,II\;C) qua Element
of S] iff f().(s,II\;C) in T) & F(f().(s,II\;C) qua Element of S) < F(s)
proof
let s be Element of S;
reconsider s9 = f().(s,I()) as Element of S;
reconsider s99 = f().(s9,i()+=-1) as Element of S;
reconsider s999 = f().(s99,C) as Element of S;
A21: f().(s,II\;C) = f().(f().(s,II),C) by AOFA_000:def 29;
A22: s99.n() = s9.n() by A5,Th28;
A23: s99.i() >= s99.n() implies s999.b() = 1 by Th35;
A24: s99.i() < s99.n() implies s999.b() = 0 by Th35;
assume
A25: PR[s];
then reconsider j = s.i()-s.n() as Element of NAT by INT_1:5;
A26: s999.i() = s99.i() by A5,Th35;
A27: s99 = f().(s,II) by AOFA_000:def 29;
then P[s99] by A3,A25;
hence
PR[f().(s,II\;C) qua Element of S] iff f().(s,II\;C) in T by A3,A5,A21
,A27,A26,A24,A23,Th2,Th35;
A28: s99.i() = s9.i()-1 by Th28;
A29: s9.n() = s.n() by A4,A25;
A30: s9.i() = s.i() by A4,A25;
s999.n() = s99.n() by A5,Th35;
then F(s999) = j by A26,A30,A29,A28,A22;
then F(s999)+1 = F(s);
hence thesis by A21,A27,NAT_1:13;
end;
A31: for s being Element of S st Q[s] holds Q[f().(s,C) qua Element of S]
& (f().(s,C) in T iff R[f().(s,C) qua Element of S])
proof
let s be Element of S;
A32: s.i() < s.n() implies f().(s,C).b() = 0 by Th35;
assume
A33: Q[s];
hence P[f().(s,C)] by A3;
A34: s.i() >= s.n() implies f().(s,C).b() = 1 by Th35;
f().(s,C).i() = s.i() by A5,Th35;
hence thesis by A5,A33,A32,A34,Th2,Th35;
end;
s2.b() = 1 by A7,A12,A14,Th35;
then
A35: f().(s1,C) in T iff PR[f().(s1,C) qua Element of S] by A2,A3,A5,A12,A9,A14
,Th35;
A36: f() iteration_terminates_for II\;C, f().(s1,C) from AOFA_000:sch 3(
A35,A20);
A37: Q[f().(s1,while(C,II)) qua Element of S] & not R[f().(s1,while(C,II))
qua Element of S] from AOFA_000:sch 5(A8,A36,A15,A31);
then (f().(s(),F())qua Element of S).i()+1 <= s().n()+1-1 by A11,INT_1:7;
then (f().(s(),F()) qua Element of S).i()+1 = s().n() by A11,A14,A37,
XXREAL_0:1;
hence thesis by A1,A14,A37,AOFA_000:def 29;
end;
suppose
A38: a().s() < s().n();
then s2.b() = 0 by A7,A12,Th35;
then s2 nin T by Th2;
hence thesis by A10,A9,A13,A11,A6,A38;
end;
end;
begin :: Termination in if-while algebras over integers
reserve b for (Element of X),
g for Euclidean ExecutionFunction of A, Funcs(X, INT), Funcs(X, INT)\(b,0);
theorem Th52:
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 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)
proof
let I be Element of A;
let i,n be Variable of g;
given d being Function such that
A1: d.b = 0 and
A2: d.n = 1 and
A3: d.i = 2;
set J = i+=1;
set C = i leq n;
set S = Funcs(X, INT);
set h = g;
assume
A4: for s holds g.(s,I).n = s.n & g.(s,I).i = s.i;
deffunc F(Element of S) = In($1.n+1-$1.i, NAT);
defpred R[Element of S] means $1.i <= $1.n;
set T = S\(b,0);
A5: i <> n by A2,A3;
A6: for s being Element of S st R[s] holds (R[h.(s,I\;J\;C) qua Element of
S] iff h.(s,I\;J\;C) in T) & F(h.(s,I\;J\;C) qua Element of S) < F(s)
proof
let s be Element of S;
set s1 = h.(s, I);
set q = h.(s, I\;J);
set q1 = h.(q, C);
A7: q = h.(s1, J) by AOFA_000:def 29;
s1.i = s.i by A4;
then q.i = s.i+1 by A7,Th28;
then
A8: q1.i = s.i+1 by A1,A3,Th35;
A9: q.i > q.n implies q1.b = 0 by Th35;
assume R[s];
then reconsider ni = s.n-s.i as Element of NAT by INT_1:3,XREAL_1:48;
A10: q1 = h.(s, I\;J\;C) by AOFA_000:def 29;
A11: q.i <= q.n implies q1.b = 1 by Th35;
q1.i = q.i by A1,A3,Th35;
hence
R[h.(s,I\;J\;C) qua Element of S] iff h.(s,I\;J\;C) in T by A1,A2,A9,A11
,A10,Th2,Th35;
A12: F(s) = ni+1;
s1.n = s.n by A4;
then q.n = s.n by A5,A7,Th28;
then q1.n = s.n by A1,A2,Th35;
then F(q1 qua Element of S) = ni by A8;
hence thesis by A10,A12,NAT_1:13;
end;
reconsider s1 = h.(s, C) as Element of S;
A13: s.i > s.n implies s1.b = 0 by Th35;
A14: s.i <= s.n implies s1.b = 1 by Th35;
s1.i = s.i by A1,A3,Th35;
then
A15: s1 in T iff R[s1] by A1,A2,A13,A14,Th2,Th35;
h iteration_terminates_for I\;J\;C, s1 from AOFA_000:sch 3(A15,A6 );
hence thesis;
end;
theorem Th53:
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 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 holds s in P implies g iteration_terminates_for I\; i+=1\; i
leq n, g.(s, i leq n)
proof
let P be set;
let I be Element of A;
let i,n be Variable of g;
given d being Function such that
A1: d.b = 0 and
A2: d.n = 1 and
A3: d.i = 2;
set J = i+=1;
set C = i leq n;
set S = Funcs(X, INT);
set h = g;
assume that
A4: for s 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 and
A5: s in P;
defpred P[Element of S] means $1 in P;
reconsider s1 = h.(s, C) as Element of S;
A6: P[s1] by A4,A5;
deffunc F(Element of S) = In($1.n+1-$1.i, NAT);
defpred R[Element of S] means $1.i <= $1.n;
set T = S\(b,0);
A7: i <> n by A2,A3;
A8: for s being Element of S st P[s] & s in T & R[s] holds P[h.(s,I\;J\;C)
qua Element of S] & (R[h.(s,I\;J\;C) qua Element of S] iff h.(s,I\;J\;C) in T)
& F(h.(s,I\;J\;C) qua Element of S) < F(s)
proof
let s be Element of S;
assume that
A9: P[s] and
s in T and
A10: R[s];
set q = h.(s, I\;J);
set s1 = h.(s, I);
set q1 = h.(q, C);
A11: q = h.(s1, J) by AOFA_000:def 29;
s1.i = s.i by A4,A9;
then q.i = s.i+1 by A11,Th28;
then
A12: q1.i = s.i+1 by A1,A3,Th35;
reconsider ni = s.n-s.i as Element of NAT by A10,INT_1:3,XREAL_1:48;
A13: F(s) = ni+1;
A14: q.i <= q.n implies q1.b = 1 by Th35;
A15: q1 = h.(s, I\;J\;C) by AOFA_000:def 29;
P[s1 qua Element of S] by A4,A9;
then P[q qua Element of S] by A4,A11;
hence P[h.(s,I\;J\;C) qua Element of S] by A4,A15;
A16: q.i > q.n implies q1.b = 0 by Th35;
q1.i = q.i by A1,A3,Th35;
hence
R[h.(s,I\;J\;C) qua Element of S] iff h.(s,I\;J\;C) in T by A1,A2,A16,A14
,A15,Th2,Th35;
s1.n = s.n by A4,A9;
then q.n = s.n by A7,A11,Th28;
then q1.n = s.n by A1,A2,Th35;
then F(q1 qua Element of S) = ni by A12;
hence thesis by A15,A13,NAT_1:13;
end;
A17: s.i > s.n implies s1.b = 0 by Th35;
A18: s.i <= s.n implies s1.b = 1 by Th35;
s1.i = s.i by A1,A3,Th35;
then
A19: s1 in T iff R[s1] by A1,A2,A17,A18,Th2,Th35;
h iteration_terminates_for I\;J\;C, s1 from AOFA_000:sch 4(A6,A19, A8);
hence thesis;
end;
theorem Th54:
for I being Element of A st I is_terminating_wrt g for i,n being
Variable of g st (ex d being Function st d.b = 0 & d.n = 1 & d.i = 2) & for s
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
proof
set S = Funcs(X, INT);
set T = Funcs(X, INT)\(b,0);
let I be Element of A such that
A1: I is_terminating_wrt g;
let i,n be Variable of g;
i+=1 is_terminating_wrt g by AOFA_000:104;
then
A2: I\; i+=1 is_terminating_wrt g by A1,AOFA_000:110;
set Q = while(i leq n, I\; i+=1);
given d being Function such that
A3: d.b = 0 and
A4: d.n = 1 and
A5: d.i = 2;
assume
A6: for s holds g.(s,I).n = s.n & g.(s,I).i = s.i;
let s;
A7: [s, i:=t] in TerminatingPrograms(A,S,T,g) by AOFA_000:def 36;
A8: i leq n is_terminating_wrt g by AOFA_000:104;
g iteration_terminates_for I\; i+=1\; i leq n, g.(g.(s, i:=t), i leq n)
by A3,A4,A5,A6,Th52;
then [g.(s, i:=t), Q] in TerminatingPrograms(A,S,T,g) by A8,A2,AOFA_000:114;
hence thesis by A7,AOFA_000:def 35;
end;
theorem
for P being set for I being Element of A st I is_terminating_wrt g, P
for i,n being Variable of g st (ex d being Function st d.b = 0 & d.n = 1 & d.i
= 2) & (for s 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
proof
set Z = Funcs(X, INT);
set T = Funcs(X, INT)\(b,0);
let S be set;
let I be Element of A;
assume
A1: I is_terminating_wrt g, S;
let i,n be Variable of g;
given d being Function such that
A2: d.b = 0 and
A3: d.n = 1 and
A4: d.i = 2;
set C = i leq n, J = I\; i+=1;
assume that
A5: for s st s in S holds g.(s,I).n = s.n & g.(s,I).i = s.i and
A6: S is_invariant_wrt i:=t, g and
A7: S is_invariant_wrt I, g and
A8: S is_invariant_wrt i leq n, g and
A9: S is_invariant_wrt i+=1, g;
let s;
assume s in S;
then
A10: g.(s, i:=t) in S by A6;
for s being Element of Z st s in S holds g.(s,I).n = s.n & g.(s,I).i =
s.i & g.(s, I) in S & g.(s, i leq n) in S & g.(s, i+=1) in S by A5,A7,A8,A9;
then
A11: g iteration_terminates_for J\; C, g.(g.(s, i:=t), C) by A2,A3,A4,A10,Th53;
set Q = while(C, J);
A12: C is_terminating_wrt g by AOFA_000:104;
A13: [s, i:=t] in TerminatingPrograms(A,Z,T,g) by AOFA_000:def 36;
S is_invariant_wrt J, g by A7,A9,AOFA_000:109;
then
A14: for s st s in S & g.(g.(s, J), C) in T holds g.(s,J) in S;
i+=1 is_terminating_wrt g, S by AOFA_000:107;
then [g.(s, i:=t), Q] in TerminatingPrograms(A,Z,T,g) by A1,A7,A8,A10,A11,A12
,A14,AOFA_000:111,116;
hence thesis by A13,AOFA_000:def 35;
end;
begin :: Examples
definition
let X,A,T,f,s;
let I be Element of A;
redefine func f.(s,I) -> Element of Funcs(X, INT); :: redefines . (BINOP_1, definition)
coherence
proof
f.(s,I) is Element of Funcs(X, INT);
hence thesis;
end;
end;
theorem
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
proof
set S = Funcs(X, INT);
set T = S\(b,0);
let n,s,i be Variable of g;
given d being Function such that
A1: d.n = 1 and
A2: d.s = 2 and
A3: d.i = 3 and
A4: d.b = 4;
A5: s <> n by A1,A2;
s <> i by A2,A3;
then
A6: for q be Element of S holds g.(q,s*=i).n = q.n & g.(q,s*=i).i = q.i by A5
,Th33;
A7: n <> b by A1,A4;
A8: b <> i by A3,A4;
let q be Element of S;
set t = .(2,A,g);
i <> n by A1,A3;
then ex d9 being Function st d9.b = 0 & d9.n = 1 & d9.i = 2 by A8,A7,Th1;
then for-do(i:=t, i leq n, i+=1, s*=i) is_terminating_wrt g by A6,Th54,
AOFA_000:104;
then
A9: [g.(q, s:=1) qua Element of S, for-do(i:=t, i leq n, i+=1, s*=i)] in
TerminatingPrograms(A,S,T,g);
[q,s:=1] in TerminatingPrograms(A,S,T,g) by AOFA_000:def 36;
hence thesis by A9,AOFA_000:def 35;
end;
theorem
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 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!
proof
set f = g;
let n,s,i be Variable of f;
given d being Function such that
A1: d.n = 1 and
A2: d.s = 2 and
A3: d.i = 3 and
A4: d.b = 4;
A5: n <> i & n <> b & i <> b by A1,A3,A4;
set S = Funcs(X,INT);
let q be Element of Funcs(X, INT);
reconsider q1 = f.(q, s:=1) as Element of S;
defpred P[Element of S] means
ex K being Nat st K = $1.i-1 & $1.s = K!;
reconsider a = .(2,A,f) as INT-Expression of A,g;
reconsider q2 = f.(q1, i:=2) as Element of S;
A6: q2.i = 2 by Th25;
A7: s <> i by A2,A3;
then q2.s = q1.s by Th25;
then
A8: P[f.(q1,i:=a)] by A6,Th25,NEWTON:13;
set I = s*=i;
A10: s <> b by A2,A4;
A11: for q being Element of Funcs(X,INT) st P[q] holds P[f.(q,I\;i+=1)] & P[
f.(q, i leq n)]
proof
let q be Element of Funcs(X,INT);
given Ki being Nat such that
A12: Ki = q.i-1 and
A13: q.s = Ki!;
reconsider q3 = f.(q,I) as Element of S;
reconsider q4 = f.(q3,i+=1) as Element of S;
A14: q3.s = q.s*q.i by Th33;
q4.s = q3.s by A7,Th28;
then
A15: q4.s = (Ki+1)! by A12,A13,A14,NEWTON:15;
A16: q4 = f.(q,I\;i+=1) by AOFA_000:def 29;
q4.i = q3.i+1 by Th28;
then Ki+1 = q4.i-1 by A7,A12,Th33;
hence P[f.(q,I\;i+=1) qua Element of S] by A16,A15;
reconsider q9 = f.(q, i leq n) as Element of S;
q9.i = q.i by A5,Th35;
hence thesis by A12,A13,A10,Th35;
end;
reconsider F = for-do(i:=a, i leq n, i+=1, I) as Element of A;
let N be Nat;
assume
A17: N = q.n;
A18: F = for-do(i:=a, i leq n, i+=1, I);
A19: s <> n by A1,A2;
A20: for q being Element of Funcs(X,INT) st P[q]
holds f.(q,I).i = q.i & f.(q,I).n = q.n by A19,A7,Th32;
A21: P[f.(q1,F)] & (a.q1 <= q1.n implies f.(q1,F).i = q1.n+1) &
(a.q1 > q1.n implies f.(q1,F).i = a.q1) & f.(q1,F).n = q1.n
from ForToIteration(A18,A8,A11,A20,A5);
consider K being Nat such that
A22: K = (f.(q1,F)).i-1 and
A23: (f.(q1,F)).s = K! by A21;
per cases;
suppose
A24: a.q1 <= q1.n;
thus f.(q, s:=1\;for-do(i:=2, i leq n, i+=1, s*=i)).s
= K! by A23,AOFA_000:def 29
.= N! by A17,A24,A21,A22,A19,Th25;
end;
suppose
A25: a.q1 > q1.n;
then 1+1 > N by A19,A17,Th25;
then
A26: 1 >= N by NAT_1:13;
thus f.(q, s:=1\;for-do(i:=2, i leq n, i+=1, s*=i)).s
= K! by A23,AOFA_000:def 29
.= N! by A25,A21,A22,A26,NAT_1:25,NEWTON:12,13;
end;
end;
theorem
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
proof
set S = Funcs(X, INT);
set T = S\(b,0);
let x,n,s,i be Variable of g;
given d being Function such that
A1: d.n = 1 and
A2: d.s = 2 and
A3: d.i = 3 and
A4: d.b = 4;
A5: s <> n by A1,A2;
s <> i by A2,A3;
then
A6: for q be Element of S holds g.(q,s*=x).n = q.n & g.(q,s*=x).i = q.i by A5
,Th33;
A7: n <> b by A1,A4;
A8: b <> i by A3,A4;
let q be Element of S;
set t = .(1,A,g);
i <> n by A1,A3;
then ex d9 being Function st d9.b = 0 & d9.n = 1 & d9.i = 2 by A8,A7,Th1;
then for-do(i:=t, i leq n, i+=1, s*=x) is_terminating_wrt g by A6,Th54,
AOFA_000:104;
then
A9: [g.(q, s:=1) qua Element of S, for-do(i:=t, i leq n, i+=1, s*=x)] in
TerminatingPrograms(A,S,T,g);
[q,s:=1] in TerminatingPrograms(A,S,T,g) by AOFA_000:def 36;
hence thesis by A9,AOFA_000:def 35;
end;
theorem
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 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
proof
set f = g;
let x,n,s,i be Variable of f;
given d being Function such that
A1: d.x = 0 and
A2: d.n = 1 and
A3: d.s = 2 and
A4: d.i = 3 and
A5: d.b = 4;
A6: n <> i & n <> b & i <> b by A2,A4,A5;
set S = Funcs(X,INT);
let q be Element of Funcs(X, INT);
reconsider q1 = f.(q, s:=1) as Element of S;
reconsider q2 = f.(q1, i:=1) as Element of S;
A7: s <> i by A3,A4;
then
A8: q2.s = q1.s by Th25;
defpred P[Element of S] means ex K being Nat st K = $1.i-1 & $1.s
= (q.x)|^K & $1.x = q.x;
set I = s*=x;
set q0 = q;
A9: (q.x)|^0 = 1 by NEWTON:4;
A10: s <> n by A2,A3;
then
A11: for q being Element of Funcs(X,INT) st P[q] holds f.(q,I).i = q.i & f.(
q,I).n = q.n by A7,Th32;
A12: s <> b by A3,A5;
A13: for q being Element of Funcs(X,INT) st P[q] holds P[f.(q,I\;i+=1)] & P[
f.(q, i leq n)]
proof
let q be Element of Funcs(X,INT);
given Ki being Nat such that
A14: Ki = q.i-1 and
A15: q.s = (q0.x)|^Ki and
A16: q.x = q0.x;
reconsider q3 = f.(q,I) as Element of S;
reconsider q4 = f.(q3,i+=1) as Element of S;
A17: q3.s = q.s*q.x by Th33;
q4.s = q3.s by A7,Th28;
then
A18: q4.s = (q0.x)|^(Ki+1) by A15,A16,A17,NEWTON:6;
A19: q4 = f.(q,I\;i+=1) by AOFA_000:def 29;
A20: q3.x = q.x by A1,A3,Th33;
q4.i = q3.i+1 by Th28;
then Ki+1 = q4.i-1 by A7,A14,Th33;
hence P[f.(q,I\;i+=1) qua Element of S] by A1,A4,A16,A19,A20,A18,Th28;
reconsider q9 = f.(q, i leq n) as Element of S;
A21: q9.s = q.s by A12,Th35;
A22: q9.i = q.i by A6,Th35;
q9.x = q.x by A1,A5,Th35;
hence thesis by A14,A15,A16,A21,A22;
end;
reconsider a = .(1,A,f) as INT-Expression of A,g;
reconsider F = for-do(i:=a, i leq n, i+=1, I) as Element of A;
A23: F = for-do(i:=a, i leq n, i+=1, I);
A24: q2.i = 1 by Th25;
A25: q2.x = q1. x by A1,A4,Th25;
A26: q1.s = 1 by Th25;
q1.x = q.x by A1,A3,Th25;
then
A27: P[f.(q1,i:=a)] by A26,A8,A24,A25,A9;
A28: P[f.(q1,F)] & (a.q1 <= q1.n implies f.(q1,F).i = q1.n+1) & (a.q1 > q1.n
implies f.(q1,F).i = a.q1) & f.(q1,F).n = q1.n from ForToIteration(A23,A27,A13,
A11,A6);
A30: q1.n = q.n by A10,Th25;
let N be Nat;
assume
A31: N = q.n;
A32: N = 0 or N >= 1 by NAT_1:25;
thus f.(q, s:=1\;for-do(i:=1, i leq n, i+=1, s*=x)).s = f.(q1, F).s by
AOFA_000:def 29
.= (q.x)|^N by A31,A30,A28,A32;
end;
theorem
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
proof
set S = Funcs(X, INT);
set T = S\(b,0);
let n,x,y,z,i be Variable of g;
given d being Function such that
A1: d.b = 0 and
A2: d.n = 1 and
A3: d.x = 2 and
A4: d.y = 3 and
A5: d.z = 4 and
A6: d.i = 5;
A7: i <> y by A4,A6;
A8: n <> z by A2,A5;
A9: n <> y by A2,A4;
A10: n <> x by A2,A3;
A11: i <> z by A5,A6;
set I = z:=x\;x:=y\;y+=z;
set I1 = z:=x, I2 = x:=y, I3 = y+=z;
A12: i <> x by A3,A6;
A13: for q be Element of S holds g.(q,I).n = q.n & g.(q,I).i = q.i
proof
let q be Element of S;
thus g.(q,I).n = g.(g.(q,I1\;I2),I3).n by AOFA_000:def 29
.= g.(q,I1\;I2).n by A9,Th30
.= g.(g.(q,I1),I2).n by AOFA_000:def 29
.= g.(q,I1).n by A10,Th27
.= q.n by A8,Th27;
thus g.(q,I).i = g.(g.(q,I1\;I2),I3).i by AOFA_000:def 29
.= g.(q,I1\;I2).i by A7,Th30
.= g.(g.(q,I1),I2).i by AOFA_000:def 29
.= g.(q,I1).i by A12,Th27
.= q.i by A11,Th27;
end;
let s;
set s2 = g.(s, x:=0\;y:=1);
i <> n by A2,A6;
then ex d9 being Function st d9.b = 0 & d9.n = 1 & d9.i = 2 by A1,A2,A6,Th1;
then for-do(i:=1, i leq n, i+=1, z:=x\;x:=y\;y+=z) is_terminating_wrt g by
A13,Th54,AOFA_000:104;
then
A14: [s2, for-do(i:=1, i leq n, i+=1, z:=x\;x:=y\;y+=z)] in
TerminatingPrograms(A,S,T,g);
[s, x:=0\;y:=1] in TerminatingPrograms(A,S,T,g) by AOFA_000:def 36;
hence thesis by A14,AOFA_000:def 35;
end;
theorem
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 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
proof
A1: (0 qua Element of NAT)+1 = 1;
set S = Funcs(X, INT);
let n,x,y,z,i be Variable of g;
given d being Function such that
A2: d.b = 0 and
A3: d.n = 1 and
A4: d.x = 2 and
A5: d.y = 3 and
A6: d.z = 4 and
A7: d.i = 5;
A8: n <> x by A3,A4;
A9: y <> z by A5,A6;
A10: x <> z by A4,A6;
A11: i <> z by A6,A7;
A12: n <> y by A3,A5;
let s be Element of Funcs(X, INT);
reconsider s1 = g.(s, x:=0) as Element of S;
reconsider s2 = g.(s1, y:=1) as Element of S;
reconsider s4 = g.(s2, i:=1) as Element of S;
A13: s4.i = 1 by Th25;
A14: i <> y by A5,A7;
then
A15: s4.y = s2.y by Th25;
set I = z:=x\;x:=y\;y+=z;
A16: s2.y = 1 by Th25;
A17: i <> x by A4,A7;
then
A18: s4.x = s2.x by Th25;
defpred P[Element of S] means ex N being Element of NAT st N = $1.i-1 & $1.x
= Fib N & $1.y = Fib(N+1);
reconsider a = .(1,A,g) as INT-Expression of A,g;
A19: s1.x = 0 by Th25;
A20: x <> y by A4,A5;
then s2.x = s1.x by Th25;
then
A21: P[g.(s2,i:=a)] by A19,A16,A15,A18,A13,A1,PRE_FF:1;
A22: n <> z by A3,A6;
A23: now
let s be Element of S;
reconsider s1 = g.(s,z:=x) as Element of S;
reconsider s2 = g.(s1,x:=y) as Element of S;
reconsider s3 = g.(s2,y+=z) as Element of S;
A24: g.(s,I) = g.(g.(s, z:=x\;x:=y), y+=z) by AOFA_000:def 29
.= s3 by AOFA_000:def 29;
A25: s1.z = s.x by Th27;
A26: s2.n = s1.n by A8,Th27;
A27: s1.i = s.i by A11,Th27;
A28: s2.z = s1.z by A10,Th27;
A29: s2.y = s1.y by A20,Th27;
A30: s2.i = s1.i by A17,Th27;
A31: s1.y = s.y by A9,Th27;
A32: s2.x = s1.y by Th27;
s1.n = s.n by A22,Th27;
hence
g.(s,I).i = s.i & g.(s,I).n = s.n & g.(s,I).x = s.y & g.(s,I).y = s.x
+s.y by A12,A14,A20,A31,A25,A27,A26,A32,A29,A28,A30,A24,Th30;
end;
A33: for s being Element of Funcs(X,INT) st P[s] holds P[g.(s,I\;i+=1)] & P[
g.(s, i leq n)]
proof
let s be Element of Funcs(X,INT);
given N being Element of NAT such that
A34: N = s.i-1 and
A35: s.x = Fib N and
A36: s.y = Fib(N+1);
reconsider s1 = g.(s,I) as Element of S;
reconsider s2 = g.(s1,i+=1) as Element of S;
A37: s1.x = s.y by A23;
A38: s2.i = s1.i+1 by Th28;
A39: s1.y = s.x+s.y by A23;
A40: s2.y = s1.y by A14,Th28;
thus P[g.(s,I\;i+=1) qua Element of S]
proof
take N+1;
g.(s,I\;i+=1) = s2 by AOFA_000:def 29;
hence thesis by A17,A23,A34,A35,A36,A37,A39,A40,A38,Th28,PRE_FF:1;
end;
take N;
thus thesis by A2,A4,A5,A7,A34,A35,A36,Th35;
end;
reconsider F = for-do(i:=a, i leq n, i+=1, I) as Element of A;
reconsider s3 = g.(s2, for-do(i:=1, i leq n, i+=1, z:=x\;x:=y\;y+=z)) as
Element of S;
let N be Element of NAT;
assume
A41: N = s.n;
A42: F = for-do(i:=a,i leq n,i+=1,I);
g.(s, x:=0\;y:=1) = s2 by AOFA_000:def 29;
then
A43: g.(s, x:=0\;y:=1\;F) = s3 by AOFA_000:def 29;
A44: 0 <= N & N <= 0 or N >= (0 qua Element of NAT)+1 by NAT_1:13;
A45: n <> i & n <> b & i <> b by A2,A3,A7;
A47: for s being Element of Funcs(X,INT) st P[s] holds g.(s,I).i = s.i & g.(
s,I).n = s.n by A23;
A48: P[g.(s2,F)] & (a.s2 <= s2.n implies g.(s2,F).i = s2.n+1) & (a.s2 > s2.n
implies g.(s2,F).i = a.s2) & g.(s2,F).n = s2.n from ForToIteration(A42,A21,A33,
A47,A45);
s2.n = s1.n by A12,Th25;
hence thesis by A41,A43,A8,A48,A44,Th25;
end;
Lm1: 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 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 st m = s.y & (s in Funcs(X, INT)\(b,0) iff m > 0) holds g
iteration_terminates_for z:=x\;z%=y\;x:=y\;y:=z\;y gt 0, s
proof
set h = g;
set S = Funcs(X, INT);
set T = S\(b,0);
let x,y,z be Variable of h;
given d being Function such that
A1: d.b = 0 and
A2: d.x = 1 and
A3: d.y = 2 and
A4: d.z = 3;
A5: z <> x by A2,A4;
let s be Element of Funcs(X, INT);
set I = z:=x\;z%=y\;x:=y\;y:=z;
A6: y <> z by A3,A4;
A7: x <> y by A2,A3;
A8: now
let s be Element of S;
reconsider s1 = h.(s, z:=x) as Element of S;
reconsider s2 = h.(s1, z%=y) as Element of S;
reconsider s3 = h.(s2, x:=y) as Element of S;
reconsider s4 = h.(s3, y:=z) as Element of S;
A9: h.(s, I) = h.(h.(s, z:=x\;z%=y\;x:=y), y:=z) by AOFA_000:def 29
.= h.(h.(h.(s, z:=x\;z%=y), x:=y), y:=z) by AOFA_000:def 29
.= s4 by AOFA_000:def 29;
A10: s1.z = s.x by Th27;
A11: s2.y = s1.y by A6,Th44;
A12: s2.z = s1.z mod s1.y by Th44;
A13: s3.z = s2.z by A5,Th27;
A14: s3.x = s2.y by Th27;
s1.y = s.y by A6,Th27;
hence h.(s, I).x = s.y & h.(s, I).y = s.x mod s.y by A7,A9,A10,A11,A12,A14
,A13,Th27;
end;
hence g.(s, I).x = s.y & h.(s, I).y = s.x mod s.y;
deffunc F(Element of S) = In($1.y, NAT);
defpred R[Element of S] means $1.y > 0;
set C = y gt 0;
A15: for s being Element of S st R[s] holds (R[h.(s,I\;C) qua Element of S]
iff h.(s,I\;C) in T) & F(h.(s,I\;C) qua Element of S) < F(s)
proof
let s be Element of S;
assume
A16: s.y > 0;
reconsider s9 = h.(s, I) as Element of S;
A17: s9.y = s.x mod s.y by A8;
then
A18: 0 <= s9.y by A16;
reconsider s99 = h.(s9, C) as Element of S;
A19: h.(s,I\;C) = s99 by AOFA_000:def 29;
A20: s9.y <= 0 implies s99.b = 0 by Th38;
s9.y > 0 implies s99.b = 1 by Th38;
hence R[h.(s,I\;C) qua Element of S] iff h.(s,I\;C) in T by A19,A20,Th2
,Th38;
s99.y = s9.y by A1,A3,Th38;
then
A21: F(s99) = s9.y by A18,INT_1:3,SUBSET_1:def 8;
A22: s9.y < s.y by A16,A17,NEWTON:65;
then F(s) = s.y by A18,INT_1:3,SUBSET_1:def 8;
hence thesis by A22,A21,AOFA_000:def 29;
end;
let n,m be Element of NAT;
assume that
A23: m = s.y;
assume s in T iff m > 0;
then
A24: s in T iff R[s] by A23;
h iteration_terminates_for I\;C, s from AOFA_000:sch 3(A24,A15);
hence thesis;
end;
theorem
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: s.x > s.y & s.y >= 0}
proof
set S = Funcs(X, INT);
set T = S\(b,0);
let x,y,z be Variable of g;
set P = {s: s.x > s.y & s.y >= 0};
given d being Function such that
A1: d.b = 0 and
A2: d.x = 1 and
A3: d.y = 2 and
A4: d.z = 3;
set C = y gt 0, I = z:=x\;z%=y\;x:=y\;y:=z;
A5: P is_invariant_wrt C,g
proof
let s;
set s1 = g.(s,C);
assume s in P;
then
A6: ex s9 st s9 = s & s9.x > s9.y & s9.y >= 0;
A7: s1.y = s.y by A1,A3,Th38;
s1.x = s.x by A1,A2,Th38;
hence thesis by A6,A7;
end;
A8: now
let s;
assume s in P;
then ex s9 st s9 = s & s9.x > s9.y & s9.y >= 0;
then reconsider m = s.y as Element of NAT by INT_1:3;
assume g.(g.(s,I),C) in T;
then g.(g.(s,I),C).b <> 0 by Th2;
then
A9: g.(s,I).y > 0 by Th38;
A10: g.(s,I).x = s.y by A1,A2,A3,A4,Lm1;
A11: g.(s,I).y = s.x mod s.y by A1,A2,A3,A4,Lm1;
then m <> 0 by A9;
then g.(s,I).x > g.(s,I).y by A11,A10,NEWTON:65;
hence g.(s,I) in P by A9;
end;
A12: now
let s;
set s1 = g.(s,C);
A13: s.y <= 0 implies s1.b = 0 by Th38;
assume g.(s,C) in P;
then ex s9 st s9 = g.(s,C) & s9.x > s9.y & s9.y >= 0;
then reconsider m = s1.y as Element of NAT by INT_1:3;
s.y > 0 implies s1.b = 1 by Th38;
then s1 in T iff m > 0 by A13,Th2,Th38;
hence g iteration_terminates_for I\;C, g.(s,C) by A1,A2,A3,A4,Lm1;
end;
C is_terminating_wrt g by AOFA_000:104;
hence thesis by A5,A8,A12,AOFA_000:107,118;
end;
theorem :: Correctness of Euclid algorithm
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 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
proof
set h = g;
set S = Funcs(X, INT);
set T = S\(b,0);
let x,y,z be Variable of h;
given d being Function such that
A1: d.b = 0 and
A2: d.x = 1 and
A3: d.y = 2 and
A4: d.z = 3;
set C = y gt 0;
set I = z:=x\;z%=y\;x:=y\;y:=z;
let s be Element of Funcs(X, INT);
reconsider fin = h.(s, while(C,I)) as Element of S;
defpred Q[Element of S] means fin.x divides $1.x & fin.x divides $1.y;
A5: for s being Element of S st Q[h.(s,C) qua Element of S] holds Q[s] by A1,A2
,A3,Th38;
A6: for s being Element of S st Q[h.(h.(s,C),I) qua Element of S] & h.(s,C)
in T holds Q[h.(s,C) qua Element of S]
proof
let s be Element of S;
assume
A7: Q[h.(h.(s,C),I) qua Element of S];
reconsider s1 = h.(s,C) as Element of S;
reconsider s2 = h.(s1,I) as Element of S;
A8: s.y <= 0 implies s1.b = 0 by Th38;
A9: s1.x = s.x by A1,A2,Th38;
A10: s2.y = s1.x mod s1.y by A1,A2,A3,A4,Lm1;
A11: s2.x = s1.y by A1,A2,A3,A4,Lm1;
A12: s1.y = s.y by A1,A3,Th38;
assume h.(s,C) in T;
then s.x = (s.x div s.y)*(s2.x)+s2.y*1 by A9,A12,A8,A11,A10,Th2,NEWTON:66;
hence thesis by A1,A2,A3,A4,A7,A9,Lm1,WSIERP_1:5;
end;
reconsider s1 = h.(s, C) as Element of S;
A13: s1.y = s.y by A1,A3,Th38;
A14: s.y <= 0 implies s1.b = 0 by Th38;
let n,m be Element of NAT;
defpred P[Element of S] means n gcd m divides $1.x & n gcd m divides $1.y &
$1.x > $1.y & $1.y >= 0;
defpred R[Element of S] means $1.y > 0;
assume that
A15: n = s.x and
A16: m = s.y and
A17: n > m;
s.y > 0 implies s1.b = 1 by Th38;
then s1 in T iff m > 0 by A16,A14,Th2;
then
A18: h iteration_terminates_for I\;C, h.(s,C) by A1,A2,A3,A4,A16,A13,Lm1;
A19: for s being Element of S st P[s] & s in T & R[s] holds P[h.(s,I)]
proof
let s be Element of S;
reconsider s99 = h.(s, I) as Element of S;
assume
A20: P[s];
then reconsider n9 = s.x, m9 = s.y as Element of NAT by INT_1:3;
assume that
s in T and
A21: R[s];
A22: s99.x = s.y by A1,A2,A3,A4,Lm1;
A23: s99.y = s.x mod s.y by A1,A2,A3,A4,Lm1;
n gcd m divides n9 mod m9 by A20,NAT_D:11;
hence thesis by A20,A21,A22,A23,NEWTON:65;
end;
A24: for s being Element of S st P[s] holds P[h.(s,C) qua Element of S] & (h
.(s,C) in T iff R[h.(s,C) qua Element of S])
proof
let s be Element of S;
assume
A25: P[s];
reconsider s9 = h.(s,C) as Element of S;
s9.y = s.y by A1,A3,Th38;
hence P[h.(s,C) qua Element of S] by A1,A2,A25,Th38;
A26: s.y <= 0 implies s9.b = 0 by Th38;
s.y > 0 implies s9.b = 1 by Th38;
hence thesis by A26,Th2,Th38;
end;
A27: P[s] by A15,A16,A17,NAT_D:def 5;
A28: P[h.(s,while(C,I)) qua Element of S] & not R[h.(s,while(C,I)) qua
Element of S] from AOFA_000:sch 5(A27,A18,A19,A24);
then fin.y = 0;
then
A29: Q[h.(s,while(C,I)) qua Element of S] by INT_2:12;
Q[s] from AOFA_000:sch 6(A29,A18,A6,A5);
then fin.x divides n gcd m by A15,A16,INT_2:22;
then fin.x = n gcd m or fin.x = -(n gcd m) by A28,INT_2:11;
hence thesis by A28;
end;
Lm2: 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 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 = |.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) iff m > 0) holds g
iteration_terminates_for z:=(.x-.y)\; if-then(z lt 0, z*=-1)\; x:=y\; y:=z\; y
gt 0, s
proof
set S = Funcs(X, INT);
set T = S\(b,0);
let x,y,z be Variable of g;
given d being Function such that
A1: d.b = 0 and
A2: d.x = 1 and
A3: d.y = 2 and
A4: d.z = 3;
A5: y <> z by A3,A4;
let s be Element of Funcs(X, INT);
set J = if-then(z lt 0, z*=-1);
A6: g complies_with_if_wrt T by AOFA_000:def 32;
A7: z <> x by A2,A4;
set I = z:=(.x-.y)\; J\; x:=y\; y:=z;
A8: x <> y by A2,A3;
A9: now
let s be Element of S;
set s1 = g.(s, z:=(.x-.y));
set s2 = g.(s1, z lt 0);
set q = g.(s1, J);
set qz = g.(s2, z*=-1);
A10: (s2.z)*(-1) = -(s2.z);
set s3 = g.(q, x:=y);
set s4 = g.(s3, y:=z);
A11: g.(s, I) = g.(g.(s, z:=(.x-.y)\; J\; x:=y), y:=z) by AOFA_000:def 29
.= g.(g.(g.(s, z:=(.x-.y)\; J), x:=y), y:=z) by AOFA_000:def 29
.= s4 by AOFA_000:def 29;
s2.b = 1 implies s2 in T;
then
A12: s2.b = 1 implies q = qz by A6;
A13: (.x).s = s.x by Th22;
A14: qz.y = s2.y by A5,Th31;
A15: (.y).s = s.y by Th22;
(.x-.y).s = ((.x).s)-((.y).s) by Def11;
then
A16: s1.z = (s.x)-(s.y) by A13,A15,Th26;
A17: s1.z < 0 implies s2.b = 1 by Th38;
A18: s2.z = s1.z by A1,A4,Th38;
A19: qz.z = (s2.z)*(-1) by Th31;
A20: s3.z = q.z by A7,Th27;
A21: s4.y = s3.z by Th27;
s2.b = 0 implies s2 nin T by Th2;
then
A22: s2.b = 0 implies q = s2 by A6,AOFA_000:80;
A23: s1.z >= 0 implies s2.b = 0 by Th38;
A24: s1.y = s.y by A5,Th26;
A25: s3.x = q.y by Th27;
s2.y = s1.y by A1,A3,Th38;
hence g.(s, I).x = s.y & g.(s, I).y = |.s.x-s.y.| by A8,A22,A12,A18,A17
,A23,A14,A19,A10,A11,A24,A16,A25,A20,A21,Th27,ABSVALUE:def 1;
end;
hence g.(s, I).x = s.y & g.(s, I).y = |.s.x-s.y.|;
deffunc F(Element of S) = IFEQ($1.y,0,0, IFEQ($1.x,0,2, IFEQ($1.x,$1.y,1, In
(max(2*$1.x,2*$1.y+1), NAT))));
defpred R[Element of S] means $1.x >= 0 & $1.y > 0;
set C = y gt 0;
A26: for s being Element of S st R[s] holds (R[g.(s,I\;C) qua Element of S]
iff g.(s,I\;C) in T) & F(g.(s,I\;C) qua Element of S) < F(s)
proof
let s be Element of S;
assume that
A27: s.x >= 0 and
A28: s.y > 0;
reconsider s9 = g.(s, I) as Element of S;
reconsider s99 = g.(s9, C) as Element of S;
A29: s9.y = |.s.x-s.y.| by A9;
then reconsider
nx = s.x, ny = s.y, nn = s99.y as Element of NAT by A1,A3,A27,A28,Th38,
INT_1:3;
A30: g.(s,I\;C) = s99 by AOFA_000:def 29;
A31: s99.x = s9.x by A1,A2,Th38;
A32: s9.y <= 0 implies s99.b = 0 by Th38;
A33: s9.y > 0 implies s99.b = 1 by Th38;
hence
R[g.(s,I\;C) qua Element of S] iff g.(s,I\;C) in T by A9,A28,A30,A31,A32
,Th2,Th38;
A34: s9.x = s.y by A9;
A35: F(s99) = IFEQ(nn,0,0, IFEQ(ny,0,2, IFEQ(ny,nn,1,max(2*ny,2*nn+1))))
by A31,A34;
2*ny+1 > 2*ny by NAT_1:13;
then
A36: max(2*nx,2*ny+1) > 2*ny by XXREAL_0:30;
A37: s99.y = s9.y by A1,A3,Th38;
A38: F(s) = IFEQ(ny,0,0, IFEQ(nx,0,2, IFEQ(nx,ny,1,max(2*nx,2*ny+1))))
.= IFEQ(nx,0,2, IFEQ(nx,ny,1,max(2*nx,2*ny+1))) by A28,FUNCOP_1:def 8;
per cases by XXREAL_0:1;
suppose
A39: nx = ny;
then
A40: IFEQ(nx,ny,1,max(2*nx,2*ny+1)) = 1 by FUNCOP_1:def 8;
A41: nn = 0 by A37,A29,A39,ABSVALUE:2;
F(s) = IFEQ(nx,ny,1,max(2*nx,2*ny+1)) by A28,A38,A39,FUNCOP_1:def 8;
hence thesis by A30,A40,A41,FUNCOP_1:def 8;
end;
suppose
A42: nx > ny;
then IFEQ(nx,ny,1,max(2*nx,2*ny+1)) = max(2*nx,2*ny+1) by FUNCOP_1:def 8;
then
A43: F(s) = max(2*nx,2*ny+1) by A38,A42,FUNCOP_1:def 8;
A44: nx-ny > 0 by A42,XREAL_1:50;
then
A45: F(s99) = IFEQ(ny,0,2, IFEQ(ny,nn,1,max(2*ny,2*nn+1))) by A37,A33,A32,A29
,A35,ABSVALUE:def 1,FUNCOP_1:def 8
.= IFEQ(ny,nn,1,max(2*ny,2*nn+1)) by A28,FUNCOP_1:def 8;
then
A46: ny = nn implies F(s99) = 1 by FUNCOP_1:def 8;
nn = nx-ny by A37,A29,A44,ABSVALUE:def 1;
then nn < nx by A28,XREAL_1:44;
then nn+1 <= nx by NAT_1:13;
then
A47: 2*(nn+1) <= 2*nx by XREAL_1:64;
A48: 1 <= 2*nn+1 by NAT_1:11;
A49: ny <> nn implies F(s99) = max(2*ny,2*nn+1) by A45,FUNCOP_1:def 8;
2*nn+2 = 2*nn+1+1;
then 2*nn+1 < 2*nx by A47,NAT_1:13;
then 2*nn+1 < F(s) by A43,XXREAL_0:30;
hence thesis by A30,A36,A43,A46,A49,A48,XXREAL_0:2,29;
end;
suppose
A50: nx < ny & nx > 0;
A51: -(nx-ny) = ny-nx;
A52: nx-ny < 0 by A50,XREAL_1:49;
then
A53: nn = -(nx-ny) by A37,A29,ABSVALUE:def 1;
then
A54: nn < ny by A50,A51,XREAL_1:44;
2*nn < 2*ny by A50,A53,A51,XREAL_1:44,68;
then 2*nn+1 < 2*ny+1 by XREAL_1:6;
then
A55: 2*nn+1 < max(2*nx,2*ny+1) by XXREAL_0:30;
nn > 0 by A37,A29,A52,A51,ABSVALUE:def 1;
then
A56: F(s99) = IFEQ(ny,0,2, IFEQ(ny,nn,1,max(2*ny,2*nn+1))) by A35,
FUNCOP_1:def 8
.= IFEQ(ny,nn,1,max(2*ny,2*nn+1)) by A28,FUNCOP_1:def 8
.= max(2*ny,2*nn+1) by A54,FUNCOP_1:def 8;
F(s) = IFEQ(nx,ny,1,max(2*nx,2*ny+1)) by A38,A50,FUNCOP_1:def 8
.= max(2*nx,2*ny+1) by A50,FUNCOP_1:def 8;
hence thesis by A30,A36,A55,A56,XXREAL_0:29;
end;
suppose
A57: nx = 0;
then
A58: F(s) = 2 by A38,FUNCOP_1:def 8;
A59: nn = -(nx-ny) by A28,A37,A29,A57,ABSVALUE:def 1
.= ny by A57;
then F(s99) = IFEQ(ny,0,2, IFEQ(ny,nn,1,max(2*ny,2*nn+1))) by A28,A35,
FUNCOP_1:def 8
.= IFEQ(ny,nn,1,max(2*ny,2*nn+1)) by A28,FUNCOP_1:def 8
.= 1 by A59,FUNCOP_1:def 8;
hence thesis by A30,A58;
end;
end;
let n,m be Element of NAT;
assume that
A60: n = s.x and
A61: m = s.y;
assume s in T iff m > 0;
then
A62: s in T iff R[s] by A60,A61;
g iteration_terminates_for I\;C, s from AOFA_000:sch 3(A62,A26);
hence thesis;
end;
theorem :: Termination of Euclid algorithm 2
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: s.x >= 0 & s.y >= 0}
proof
set S = Funcs(X, INT);
set T = S\(b,0);
let x,y,z be Variable of g;
set P = {s: s.x >= 0 & s.y >= 0};
given d being Function such that
A1: d.b = 0 and
A2: d.x = 1 and
A3: d.y = 2 and
A4: d.z = 3;
set C = y gt 0, I = z:=(.x-.y)\; if-then(z lt 0, z*=-1)\; x:=y\; y:=z;
A5: now
let s;
assume s in P;
then ex s9 st s9 = s & s9.x >= 0 & s9.y >= 0;
then reconsider m = s.y as Element of NAT by INT_1:3;
assume g.(g.(s,I),C) in T;
A6: g.(s,I).x = m by A1,A2,A3,A4,Lm2;
g.(s,I).y = |.s.x-s.y.| by A1,A2,A3,A4,Lm2;
hence g.(s,I) in P by A6;
end;
A7: now
let s;
set s1 = g.(s,C);
A8: s.y <= 0 implies s1.b = 0 by Th38;
assume g.(s,C) in P;
then ex s9 st s9 = g.(s,C) & s9.x >= 0 & s9.y >= 0;
then reconsider n = s1.x, m = s1.y as Element of NAT by INT_1:3;
A9: n = n;
s.y > 0 implies s1.b = 1 by Th38;
then s1 in T iff m > 0 by A8,Th2,Th38;
hence g iteration_terminates_for I\;C, g.(s,C) by A1,A2,A3,A4,A9,Lm2;
end;
A10: P is_invariant_wrt C,g
proof
let s;
set s1 = g.(s,C);
assume s in P;
then
A11: ex s9 st s9 = s & s9.x >= 0 & s9.y >= 0;
A12: s1.y = s.y by A1,A3,Th38;
s1.x = s.x by A1,A2,Th38;
hence thesis by A11,A12;
end;
C is_terminating_wrt g by AOFA_000:104;
hence thesis by A10,A5,A7,AOFA_000:107,118;
end;
theorem :: Euclid algorithm 2
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 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
proof
set h = g;
set S = Funcs(X, INT);
set T = S\(b,0);
A1: h complies_with_if_wrt T by AOFA_000:def 32;
let x,y,z be Variable of h;
given d being Function such that
A2: d.b = 0 and
A3: d.x = 1 and
A4: d.y = 2 and
A5: d.z = 3;
set C = y gt 0;
let s be Element of Funcs(X, INT);
A6: y <> z by A4,A5;
reconsider s1 = h.(s, C) as Element of S;
A7: s1.x = s.x by A2,A3,Th38;
A8: s1.y = s.y by A2,A4,Th38;
A9: s.y <= 0 implies s1.b = 0 by Th38;
defpred R[Element of S] means $1.x > 0 & $1.y > 0;
let n,m be Element of NAT;
defpred P[Element of S] means n gcd m divides $1.x & n gcd m divides $1.y &
$1.x > 0 & $1.y >= 0 & for c being Nat st c divides $1.x & c divides $1.y holds
c divides n gcd m;
set J = if-then(z lt 0, z*=-1);
set I = z:=(.x-.y)\; J\; x:=y\; y:=z;
assume that
A10: n = s.x and
A11: m = s.y and
A12: n > 0;
s.y > 0 implies s1.b = 1 by Th38;
then s1 in T iff R[s1] by A10,A12,A9,Th2,Th38;
then
A13: h iteration_terminates_for I\;C, h.(s,C) by A2,A3,A4,A5,A10,A11,A12,A7,A8
,Lm2;
A14: z <> x by A3,A5;
A15: x <> y by A3,A4;
A16: now
let s be Element of S;
set s1 = h.(s, z:=(.x-.y));
set s2 = h.(s1, z lt 0);
set q = h.(s1, J);
set qz = h.(s2, z*=-1);
A17: (s2.z)*(-1) = -(s2.z);
set s3 = h.(q, x:=y);
set s4 = h.(s3, y:=z);
A18: h.(s, I) = h.(h.(s, z:=(.x-.y)\; J\; x:=y), y:=z) by AOFA_000:def 29
.= h.(h.(h.(s, z:=(.x-.y)\; J), x:=y), y:=z) by AOFA_000:def 29
.= s4 by AOFA_000:def 29;
s2.b = 1 implies s2 in T;
then
A19: s2.b = 1 implies q = qz by A1;
A20: (.x).s = s.x by Th22;
A21: qz.y = s2.y by A6,Th31;
A22: (.y).s = s.y by Th22;
(.x-.y).s = ((.x).s)-((.y).s) by Def11;
then
A23: s1.z = (s.x)-(s.y) by A20,A22,Th26;
A24: s1.z < 0 implies s2.b = 1 by Th38;
A25: s2.z = s1.z by A2,A5,Th38;
A26: qz.z = (s2.z)*(-1) by Th31;
A27: s3.z = q.z by A14,Th27;
A28: s4.y = s3.z by Th27;
s2.b = 0 implies s2 nin T by Th2;
then
A29: s2.b = 0 implies q = s2 by A1,AOFA_000:80;
A30: s1.z >= 0 implies s2.b = 0 by Th38;
A31: s1.y = s.y by A6,Th26;
A32: s3.x = q.y by Th27;
s2.y = s1.y by A2,A4,Th38;
hence h.(s, I).x = s.y & h.(s, I).y = |.s.x-s.y.| by A15,A29,A19,A25,A24
,A30,A21,A26,A17,A18,A31,A23,A32,A27,A28,Th27,ABSVALUE:def 1;
end;
A33: for s being Element of S st P[s] & s in T & R[s] holds P[h.(s,I)]
proof
let s be Element of S;
reconsider s99 = h.(s, I) as Element of S;
A34: |.n gcd m.| = n gcd m by ABSVALUE:def 1;
A35: s99.y = |.s.x-s.y.| by A16;
assume
A36: P[s];
then reconsider n9 = s.x, m9 = s.y as Element of NAT by INT_1:3;
assume that
s in T and
A37: R[s];
n gcd m divides n9-m9 by A36,PREPOWER:94;
hence
n gcd m divides h.(s,I).x & n gcd m divides h.(s,I).y & h.(s,I).x > 0
& h.(s,I).y >= 0 by A16,A36,A37,A35,A34,INT_2:16;
let c be Nat;
reconsider c9 = c as Element of NAT by ORDINAL1:def 12;
assume that
A38: c divides h.(s,I).x and
A39: c divides h.(s,I).y;
A40: |.c.| = c by ABSVALUE:def 1;
A41: s99.x = s.y by A16;
c9 divides |.n9-m9.| by A16,A39;
then
A42: c divides n9-m9 by A40,INT_2:16;
c qua Integer divides m9 by A16,A38;
then c divides (n9-m9)+m9 by A42,WSIERP_1:4;
hence thesis by A36,A41,A38;
end;
A43: for s being Element of S st P[s] holds P[h.(s,C) qua Element of S] & (h
.(s,C) in T iff R[h.(s,C) qua Element of S])
proof
let s be Element of S;
assume
A44: P[s];
reconsider s9 = h.(s,C) as Element of S;
A45: s9.y = s.y by A2,A4,Th38;
s9.x = s.x by A2,A3,Th38;
hence P[h.(s,C) qua Element of S] by A44,A45;
A46: s.y <= 0 implies s9.b = 0 by Th38;
s.y > 0 implies s9.b = 1 by Th38;
hence thesis by A44,A46,Th2,Th38;
end;
reconsider fin = h.(s, while(C,I)) as Element of S;
A47: P[s] by A10,A11,A12,NAT_D:def 5;
A48: P[h.(s,while(C,I)) qua Element of S] & not R[h.(s,while(C,I)) qua
Element of S] from AOFA_000:sch 5(A47,A13,A33,A43);
then reconsider fn = fin.x as Element of NAT by INT_1:3;
A49: fn divides 0 by NAT_D:6;
fin.y = 0 by A48;
then fn divides n gcd m by A48,A49;
hence thesis by A48,NAT_D:5;
end;
theorem
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: s.m >= 0}
proof
set S = Funcs(X, INT);
set T = S\(b,0);
let x,y,m be Variable of g;
set P = {s: s.m >= 0};
given d being Function such that
A1: d.b = 0 and
A2: d.x = 1 and
A3: d.y = 2 and
A4: d.m = 3;
set C = m gt 0;
A5: y:=1 is_terminating_wrt g, P by AOFA_000:107;
deffunc F(Element of S) = In($1.m, NAT);
defpred R[Element of S] means $1.m > 0;
set I = if-then(m is_odd, y*=x);
set J = I\; m/=2\; x*=x;
A6: g complies_with_if_wrt T by AOFA_000:def 32;
A7: P is_invariant_wrt C,g
proof
let s;
assume s in P;
then
A8: ex s9 st s = s9 & s9.m >= 0;
g.(s, C).m = s.m by A1,A4,Th38;
hence g.(s, C) in P by A8;
end;
A9: for s st s in P & g.(g.(s,J),C) in T holds g.(s,J) in P
proof
let s such that
s in P;
assume g.(g.(s,J),C) in T;
then g.(s,J).m > 0 by Th40;
hence thesis;
end;
A10: m <> y by A3,A4;
A11: P is_invariant_wrt y:=1, g
proof
let s;
assume s in P;
then
A12: ex s9 st s = s9 & s9.m >= 0;
g.(s, y:=1).m = s.m by A10,Th25;
hence g.(s, y:=1) in P by A12;
end;
A13: m <> x by A2,A4;
A14: for s st g.(s,C) in P holds g iteration_terminates_for J\;C, g.(s,C)
proof
A15: for s being Element of S st R[s] holds (R[g.(s,J\;C)] iff g.(s,J\;C)
in T) & F(g.(s,J\;C)) < F(s)
proof
let s be Element of S such that
A16: s.m > 0;
A17: F(s) = s.m by A16,INT_1:3,SUBSET_1:def 8;
set q1 = g.(s,I);
set q0 = g.(s, m is_odd);
set sJ = g.(s,J);
set sC = g.(sJ,C);
A18: g.(s,J\;C) = sC by AOFA_000:def 29;
A19: sJ.m <= 0 implies sC.b = 0 by Th38;
sJ.m > 0 implies sC.b = 1 by Th38;
hence R[g.(s,J\;C)] iff g.(s,J\;C) in T by A19,A18,Th2,Th38;
set q2 = g.(q1,m/=2);
set q3 = g.(q2,x*=x);
A20: q1 = g.(q0, y*=x) or q1 = g.(q0, EmptyIns A) by A6;
q2 = g.(s,I\;m/=2) by AOFA_000:def 29;
then q3 = g.(s,J) by AOFA_000:def 29;
then
A21: sJ.m = q2.m by A13,Th33
.= (q1.m) div 2 by Th45
.= (q0.m) div 2 by A10,A20,Th33,AOFA_000:def 28
.= (s.m) div 2 by A1,A4,Th49;
A22: sC.m = sJ.m by A1,A4,Th38;
then sC.m in NAT by A16,A21,INT_1:3,61;
then F(sC) = sC.m by SUBSET_1:def 8;
hence thesis by A16,A22,A18,A21,A17,INT_1:56;
end;
let s0 be Element of S such that
g.(s0,C) in P;
set s1 = g.(s0,C);
A23: s0.m <= 0 implies s1.b = 0 by Th38;
s0.m > 0 implies s1.b = 1 by Th38;
then
A24: g.(s0,C) in T iff R[g.(s0,C)] by A23,Th2,Th38;
thus g iteration_terminates_for J\;C, g.(s0,C) from AOFA_000:sch 3(A24,A15
);
end;
J is_terminating_wrt g,P by AOFA_000:107;
then while(m gt 0, if-then(m is_odd, y*=x)\; m/=2\; x*=x )
is_terminating_wrt g, P by A7,A9,A14,AOFA_000:104,118;
hence thesis by A5,A11,AOFA_000:111;
end;
::$N Correctness of the algorithm of exponentiation by squaring
theorem
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 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
proof
set S = Funcs(X, INT);
set T = S\(b,0);
A1: g complies_with_if_wrt T by AOFA_000:def 32;
let x,y,m be Variable of g;
given d being Function such that
A2: d.b = 0 and
A3: d.x = 1 and
A4: d.y = 2 and
A5: d.m = 3;
defpred R[Element of S] means $1.m > 0;
set C = m gt 0;
let s be Element of Funcs(X, INT);
let n be Nat;
defpred P[Element of S] means (s.x)|^n = ($1.y)*(($1.x)to_power($1.m)) & $1.
m >= 0;
deffunc F(Element of S) = In($1.m, NAT);
set I = if-then(m is_odd, y*=x);
set J = I\; m/=2\; x*=x;
set s0 = g.(s, y:=1);
A6: m <> y by A4,A5;
then
A7: s0.m = s.m by Th25;
A8: for s being Element of S st P[s] holds P[g.(s,C)] & (g.(s,C) in T iff R
[g.(s,C)])
proof
let s be Element of S such that
A9: P[s];
set s1 = g.(s, C);
A10: s1.x = s.x by A2,A3,Th38;
s1.m = s.m by A2,A5,Th38;
hence P[g.(s,C)] by A2,A4,A9,A10,Th38;
A11: s.m <= 0 implies s1.b = 0 by Th38;
s.m > 0 implies s1.b = 1 by Th38;
hence thesis by A11,Th2,Th38;
end;
A12: s0.y = 1 by Th25;
set fs = g.(s0, while(C,J));
set s1 = g.(s0,C);
assume
A13: n = s.m;
A14: (fs.x) to_power 0 = 1 by POWER:24;
A15: m <> x by A3,A5;
A16: for s being Element of S st R[s] holds (R[g.(s,J\;C)] iff g.(s,J\;C) in
T) & F(g.(s,J\;C)) < F(s)
proof
let s be Element of S such that
A17: s.m > 0;
A18: F(s) = s.m by A17,INT_1:3,SUBSET_1:def 8;
set q1 = g.(s,I);
set q0 = g.(s, m is_odd);
set sJ = g.(s,J);
set sC = g.(sJ,C);
A19: g.(s,J\;C) = sC by AOFA_000:def 29;
A20: sJ.m <= 0 implies sC.b = 0 by Th38;
sJ.m > 0 implies sC.b = 1 by Th38;
hence R[g.(s,J\;C)] iff g.(s,J\;C) in T by A20,A19,Th2,Th38;
set q2 = g.(q1,m/=2);
set q3 = g.(q2,x*=x);
A21: q1 = g.(q0, y*=x) or q1 = g.(q0, EmptyIns A) by A1;
q2 = g.(s,I\;m/=2) by AOFA_000:def 29;
then q3 = g.(s,J) by AOFA_000:def 29;
then
A22: sJ.m = q2.m by A15,Th33
.= (q1.m) div 2 by Th45
.= (q0.m) div 2 by A6,A21,Th33,AOFA_000:def 28
.= (s.m) div 2 by A2,A5,Th49;
A23: sC.m = sJ.m by A2,A5,Th38;
then sC.m in NAT by A17,A22,INT_1:3,61;
then F(sC) = sC.m by SUBSET_1:def 8;
hence thesis by A17,A23,A19,A22,A18,INT_1:56;
end;
set q = s;
A24: x <> y by A3,A4;
A25: for s being Element of S st P[s] & s in T & R[s] holds P[g.(s,J)]
proof
let s be Element of S such that
A26: P[s] and
s in T and
R[s];
reconsider sm = s.m as Element of NAT by A26,INT_1:3;
s.m = ((s.m) div 2)*2+((s.m) mod 2) by NEWTON:66;
then
A27: (q.x)|^n = (s.y)*(((s.x)to_power((sm div 2)*2))*((s.x)to_power(sm mod
2))) by A26,FIB_NUM2:5
.= (s.y)*((s.x)to_power(sm mod 2))*((s.x)to_power((sm div 2)*2))
.= (s.y)*((s.x)to_power(sm mod 2))* (((s.x)to_power 2) to_power (sm
div 2)) by NEWTON:9
.= (s.y)*((s.x)to_power(sm mod 2))* (((s.x)*(s.x)) to_power (sm div 2)
) by NEWTON:81;
set q1 = g.(s,I);
set q0 = g.(s, m is_odd);
set sJ = g.(s,J);
set q2 = g.(q1,m/=2);
set q3 = g.(q2,x*=x);
A28: q1 = g.(q0, y*=x) or q1 = g.(q0, EmptyIns A) by A1;
A29: q2.x = q1.x by A15,Th45
.= q0.x by A24,A28,Th33,AOFA_000:def 28;
A30: q2.y = q1.y by A6,Th45;
A31: q0.y = s.y by A2,A4,Th49;
A32: q0.x = s.x by A2,A3,Th49;
q2 = g.(s,I\;m/=2) by AOFA_000:def 29;
then
A33: q3 = g.(s,J) by AOFA_000:def 29;
then
A34: sJ.y = q2.y by A24,Th33;
A35: sm div 2 = s.m div 2;
A36: now
A37: q0.b = (s.m) mod 2 by Th49;
per cases by A35,A37,NAT_D:12;
suppose
A38: q0.b = 0;
then q0 nin T by Th2;
then q1 = g.(q0, EmptyIns A) by A1;
then
A39: q1.y = q0.y by AOFA_000:def 28;
A40: (s.y)*1 = s.y;
(s.x)to_power 0 = 1 by POWER:24;
hence (s.y)*((s.x)to_power(sm mod 2)) = sJ.y by A34,A30,A31,A38,A39,A40
,Th49;
end;
suppose
A41: q0.b = 1;
then q0 in T;
then q1 = g.(q0, y*=x) by A1;
then
A42: q1.y = (q0.y)*(q0.x) by Th33;
(s.x)to_power 1 = s.x by POWER:25;
hence (s.y)*((s.x)to_power(sm mod 2)) = sJ.y by A32,A34,A30,A31,A41,A42
,Th49;
end;
end;
sJ.m = q2.m by A15,A33,Th33
.= (q1.m) div 2 by Th45
.= (q0.m) div 2 by A6,A28,Th33,AOFA_000:def 28
.= (s.m) div 2 by A2,A5,Th49;
hence thesis by A33,A29,A32,A36,A27,Th33;
end;
A43: s0.m <= 0 implies s1.b = 0 by Th38;
s0.m > 0 implies s1.b = 1 by Th38;
then
A44: g.(s0,C) in T iff R[g.(s0,C)] by A43,Th2,Th38;
A45: g iteration_terminates_for J\;C, g.(s0,C) from AOFA_000:sch 3(A44, A16);
s0.x = s.x by A24,Th25;
then
A46: P[s0] by A13,A7,A12,POWER:41;
A47: P[g.(s0,while(C,J))] & not R[g.(s0,while(C,J))] from AOFA_000:sch 5(A46
,A45,A25,A8);
then fs.m = 0;
hence thesis by A47,A14,AOFA_000:def 29;
end;