:: Mizar Analysis of Algorithms: Algorithms over Integers
:: by Grzegorz Bancerek
::
:: Received March 18, 2008
:: Copyright (c) 2008 Association of Mizar Users
environ
vocabularies AOFA_I00, AOFA_000, FUNCT_1, GROUP_1, FINSEQ_1, RELAT_1, FUNCT_2,
ORDINAL2, BOOLE, FUNCT_7, FUNCOP_1, FUNCT_4, ARYTM, AMI_3, TARSKI,
TREES_4, INT_1, QC_LANG1, MSUALG_3, FRAENKEL, ARYTM_1, FINSET_1,
CQC_LANG, CARD_4, NEWTON, AMI_2, VECTSP_1, ARYTM_3, FREEALG, CARD_1,
PRE_FF, NAT_1, ABSVALUE, SEQ_1, LANG1, SQUARE_1, EUCLMETR, SCMFSA6C,
ZF_LANG, SGRAPH1, MCART_1, REAL_3, POWER, CAT_1, MATRIX_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, PRE_TOPC, ENUMSET1, MCART_1,
ORDINAL1, MEMBERED, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
FUNCT_3, FINSET_1, CQC_LANG, LANG1, MSAFREE1, FINSEQ_1, REAL_3, SEQ_1,
SEQM_3, SEQ_4, BINOP_1, CARD_1, CARD_2, CARD_3, CARD_4, FRAENKEL, PROB_2,
FINSEQ_2, FINSEQOP, PBOOLE, PZFMISC1, PRE_FF, PRE_CIRC, FACIRC_1,
NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, POWER, TREES_1, TREES_2, TREES_3,
ABSVALUE, INT_1, INT_2, NAT_1, NAT_D, NEWTON, ABIAN, BINARITH, WSIERP_1,
VALUED_1, SUPINF_1, FUNCOP_1, FUNCT_4, FUNCT_7, CAT_2, MESFUNC1,
BORSUK_1, POLYNOM1, AMI_2, STRUCT_0, UNIALG_1, UNIALG_2, ALG_1, FREEALG,
COMPUT_1, TREES_4, DTCONSTR, MSUALG_1, MSAFREE, MSATERM, MSUALG_3,
PRALG_3, FINSEQ_4, AOFA_000;
constructors ORDINAL2, FINSEQ_1, UNIALG_1, PUA2MSS1, COMPUT_1, FUNCT_7,
BINOP_1, BINARITH, REAL_1, BORSUK_1, SUPINF_1, SUPINF_2, POLYNOM1,
CATALG_1, MSATERM, MSAFREE3, PROB_2, MSAFREE1, MSUALG_3, CQC_LANG,
FACIRC_1, CARD_4, AMI_2, FUNCT_3, MESFUNC1, PREPOWER, POWER, NAT_D,
NEWTON, ABIAN, VALUED_0, VALUED_1, NAT_1, SQUARE_1, ALG_1, FREEALG,
FINSEQ_4, FINSOP_1, ORDERS_1, PZFMISC1, PRE_FF, INT_2, SEQ_4, ABSVALUE,
REAL_3, FUNCT_5, FINSEQOP, WSIERP_1, ENUMSET1, PRE_CIRC, WELLORD2,
CLASSES1, CARD_2, UNIALG_2, CAT_2, PRALG_3, AOFA_000;
registrations ZFMISC_1, RELSET_1, FUNCT_1, FUNCOP_1, FINSEQ_2, FRAENKEL,
FUNCT_2, FINSEQ_1, UNIALG_1, COMPUT_1, NUMBERS, NAT_1, ORDINAL1,
STRUCT_0, PUA2MSS1, SUPINF_1, PBOOLE, MSUALG_1, INSTALG1, MSATERM,
MSAFREE1, MSAFREE3, MSUALG_2, PRALG_1, DTCONSTR, FREEALG, FUNCT_7, INT_1,
CARD_4, WAYBEL12, CARD_5, SUBSET_1, AFINSQ_1, CARD_1, CLASSES1, ORDERS_1,
CARD_3, VALUED_0, VALUED_1, MEMBERED, XREAL_0, REAL_3, TREES_4, XCMPLX_0,
XXREAL_0, XBOOLE_0, FINSET_1, POWER, TREES_1, PRE_CIRC, FACIRC_1,
RELAT_1, UNIALG_2, PRE_TOPC, AOFA_000, ABIAN;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions VALUED_0, XCMPLX_0, PZFMISC1, TREES_4, SUPINF_2, MEMBERED,
FINSEQ_2, CARD_2, TARSKI, XBOOLE_0, PUA2MSS1, SEQ_1, FINSEQ_4, FUNCT_1,
FUNCT_2, FREEALG, RELAT_1, FINSEQ_1, UNIALG_1, UNIALG_2, COMPUT_1,
BINOP_1, AOFA_000;
theorems XBOOLE_1, ZFMISC_1, RELAT_1, FUNCT_2, FUNCOP_1, CQC_LANG, 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, RFUNCT_1,
CARD_2, CARD_1, CARD_4, WELLORD2, FINSET_1, FUNCT_5, AOFA_000, MCART_1,
XXREAL_0, JORDAN12, POWER, POLYEQ_3, FIB_NUM2, ORDINAL3, POLYNOM1, NAT_D,
PREPOWER, VALUED_1;
schemes FUNCT_1, FUNCT_2, WELLORD2, XBOOLE_0, AOFA_000, TARSKI;
begin :: Preliminaries
theorem Lem3:
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
Z1: a <> b & b <> c & c <> a;
set fa = a.-->x;
set fb = b.-->y;
set fc = c.-->z;
take f = fa+*fb+*fc;
dom fc = {c} & dom fb = {b} & dom fa = {a} by CQC_LANG:5; then
Z2: a nin dom fc & a nin dom fb & b nin dom fc & b in dom fb & c in dom fc
by Z1,TARSKI:def 1;
thus f.a = (fa+*fb).a by Z2,FUNCT_4:12 .= fa.a by Z2,FUNCT_4:12
.= x by CQC_LANG:6;
thus f.b = (fa+*fb).b by Z2,FUNCT_4:12 .= fb.b by Z2,FUNCT_4:14
.= y by CQC_LANG:6;
thus f.c = fc.c by Z2,FUNCT_4:14 .= z by CQC_LANG:6;
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 set; 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 LemTS:
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:
ELEM:
not contradiction;
existence;
end;
notation
let f be real-yielding Function;
let x be real number;
synonym f*x for x(#)f;
end;
definition
let t1,t2 be integer-yielding Function;
func t1 div t2 -> integer-yielding Function means:
DEFdiv:
dom it = (dom t1) /\ (dom t2) & :: \ (t2"{0}) &
for s being set st s in dom it holds it.s = (t1.s) div (t2.s);
correctness
proof
deffunc F(set) = (t1.$1) div (t2.$1);
consider f being Function such that
A1: dom f = (dom t1) /\ (dom t2) &
for x being set st x in (dom t1) /\ (dom t2) holds f.x = F(x)
from FUNCT_1:sch 3;
f is integer-yielding
proof
let x be set;
assume x in dom f; then
f.x = F(x) by A1;
hence thesis;
end;
hence ex f being integer-yielding Function st dom f = (dom t1)/\(dom t2) &
for x being set st x in dom f holds f.x = F(x) by A1;
let f1,f2 be integer-yielding Function such that
A3: dom f1 = (dom t1) /\ dom t2 and
A4: for s being set st s in dom f1 holds f1.s = F(s) and
A5: dom f2 = (dom t1) /\ dom t2 and
A6: for s being set st s in dom f2 holds f2.s = F(s);
now
let s be set;
assume
A7: s in (dom t1) /\ dom t2;
hence f1.s = F(s) by A3,A4 .= f2.s by A5,A6,A7;
end;
hence thesis by A3,A5,FUNCT_1:9;
end;
func t1 mod t2 -> integer-yielding Function means:
DEFmod:
dom it = (dom t1) /\ (dom t2) & :: \ (t2"{0}) &
for s being set st s in dom it holds it.s = (t1.s) mod (t2.s);
correctness
proof
deffunc F(set) = (t1.$1) mod (t2.$1);
consider f being Function such that
A1: dom f = (dom t1) /\ (dom t2) &
for x being set st x in (dom t1) /\ (dom t2) holds f.x = F(x)
from FUNCT_1:sch 3;
f is integer-yielding
proof
let x be set;
assume x in dom f; then
f.x = F(x) by A1;
hence thesis;
end;
hence ex f being integer-yielding Function st dom f = (dom t1)/\(dom t2) &
for x being set st x in dom f holds f.x = F(x) by A1;
let f1,f2 be integer-yielding Function such that
A3: dom f1 = (dom t1) /\ dom t2 and
A4: for s being set st s in dom f1 holds f1.s = F(s) and
A5: dom f2 = (dom t1) /\ dom t2 and
A6: for s being set st s in dom f2 holds f2.s = F(s);
now
let s be set;
assume
A7: s in (dom t1) /\ dom t2;
hence f1.s = F(s) by A3,A4 .= f2.s by A5,A6,A7;
end;
hence thesis by A3,A5,FUNCT_1:9;
end;
func leq(t1,t2) -> integer-yielding Function means:
DEFleq:
dom it = (dom t1) /\ (dom t2) &
for s being set st s in dom it holds it.s = IFGT(t1.s,t2.s,0,1);
correctness
proof
deffunc F(set) = IFGT(t1.$1,t2.$1,0,1);
consider f being Function such that
A1: dom f = (dom t1) /\ (dom t2) &
for x being set st x in (dom t1) /\ (dom t2) holds f.x = F(x)
from FUNCT_1:sch 3;
f is integer-yielding
proof
let x be set;
assume x in dom f; then
f.x = F(x) by A1;
hence thesis;
end;
hence ex f being integer-yielding Function st dom f = (dom t1)/\(dom t2) &
for x being set st x in dom f holds f.x = F(x) by A1;
let f1,f2 be integer-yielding Function such that
A3: dom f1 = (dom t1) /\ dom t2 and
A4: for s being set st s in dom f1 holds f1.s = F(s) and
A5: dom f2 = (dom t1) /\ dom t2 and
A6: for s being set st s in dom f2 holds f2.s = F(s);
now
let s be set;
assume
A7: s in (dom t1) /\ dom t2;
hence f1.s = F(s) by A3,A4 .= f2.s by A5,A6,A7;
end;
hence thesis by A3,A5,FUNCT_1:9;
end;
func gt(t1,t2) -> integer-yielding Function means:
DEFgt:
dom it = (dom t1) /\ (dom t2) &
for s being set st s in dom it holds it.s = IFGT(t1.s,t2.s,1,0);
correctness
proof
deffunc F(set) = IFGT(t1.$1,t2.$1,1,0);
consider f being Function such that
A1: dom f = (dom t1) /\ (dom t2) &
for x being set st x in (dom t1) /\ (dom t2) holds f.x = F(x)
from FUNCT_1:sch 3;
f is integer-yielding
proof
let x be set;
assume x in dom f; then
f.x = F(x) by A1;
hence thesis;
end;
hence ex f being integer-yielding Function st dom f = (dom t1)/\(dom t2) &
for x being set st x in dom f holds f.x = F(x) by A1;
let f1,f2 be integer-yielding Function such that
A3: dom f1 = (dom t1) /\ dom t2 and
A4: for s being set st s in dom f1 holds f1.s = F(s) and
A5: dom f2 = (dom t1) /\ dom t2 and
A6: for s being set st s in dom f2 holds f2.s = F(s);
now
let s be set;
assume
A7: s in (dom t1) /\ dom t2;
hence f1.s = F(s) by A3,A4 .= f2.s by A5,A6,A7;
end;
hence thesis by A3,A5,FUNCT_1:9;
end;
func eq(t1,t2) -> integer-yielding Function means:
DEFeq:
dom it = (dom t1) /\ (dom t2) &
for s being set st s in dom it holds it.s = IFEQ(t1.s,t2.s,1,0);
correctness
proof
deffunc F(set) = IFEQ(t1.$1,t2.$1,1,0);
consider f being Function such that
A1: dom f = (dom t1) /\ (dom t2) &
for x being set st x in (dom t1) /\ (dom t2) holds f.x = F(x)
from FUNCT_1:sch 3;
f is integer-yielding
proof
let x be set;
assume x in dom f; then
f.x = F(x) by A1;
hence thesis;
end;
hence ex f being integer-yielding Function st dom f = (dom t1)/\(dom t2) &
for x being set st x in dom f holds f.x = F(x) by A1;
let f1,f2 be integer-yielding Function such that
A3: dom f1 = (dom t1) /\ dom t2 and
A4: for s being set st s in dom f1 holds f1.s = F(s) and
A5: dom f2 = (dom t1) /\ dom t2 and
A6: for s being set st s in dom f2 holds f2.s = F(s);
now
let s be set;
assume
A7: s in (dom t1) /\ dom t2;
hence f1.s = F(s) by A3,A4 .= f2.s by A5,A6,A7;
end;
hence thesis by A3,A5,FUNCT_1:9;
end;
end;
definition
let X be non empty set;
let f be Function of X, INT;
let x be integer number;
redefine
func f+x -> Function of X, INT means:
DEFplus2:
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) = dom f & dom f = X & dom ti = X by VALUED_1:def 2,FUNCT_2:def 1;
hence ti = f+x implies
for s being Element of X holds ti.s = f.s+x by VALUED_1:def 2;
assume for s being Element of X holds ti.s = f.s+x; then
for s being set st s in X holds ti.s = x+f.s;
hence ti = f+x by A1,VALUED_1:def 2;
end;
coherence
proof
x+f is Function of X, INT;
hence thesis;
end;
func f-x -> Function of X, INT means
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) = dom f & dom f = X & dom ti = X by VALUED_1:3,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
A2: for s being Element of X holds ti.s = f.s-x;
now let s be set; assume
A3: s in dom ti;
hence ti.s = f.s-x by A2 .= (f-x).s by A1,A3,VALUED_1:3;
end;
hence ti = f-x by A1,FUNCT_1:9;
end;
coherence
proof
thus f-x is Function of X, INT;
end;
func f*x -> Function of X, INT means:
DEFmult2:
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) = dom f & dom f = X & dom ti = X by VALUED_1:def 5,FUNCT_2:def 1;
hence ti = f*x implies
for s being Element of X holds ti.s = f.s*x by VALUED_1:def 5;
assume
for s being Element of X holds ti.s = f.s*x; then
for s being set st s in dom (f*x) holds ti.s = x*f.s by A1;
hence ti = f*x by A1,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;
coherence
proof
A1: rng f c= INT & rng g c= INT &
dom (f div g) = (dom f) /\ dom g & (dom f) /\ dom f = dom f &
dom f = X & dom g = X by DEFdiv,FUNCT_2:def 1;
rng (f div g) c= INT
proof
let y be set; assume y in rng (f div g); then
consider a being set such that
A2: a in dom (f div g) & y = (f div g).a by FUNCT_1:def 5;
f.a in rng f & g.a in rng g by A1,A2,FUNCT_1:12; then
reconsider i = f.a, j = g.a as Element of INT;
thus thesis by A2,INT_1:def 2;
end;
hence thesis by A1,FUNCT_2:4;
end;
func f mod g -> Function of X, INT;
coherence
proof
A1: rng f c= INT & rng g c= INT &
dom (f mod g) = (dom f) /\ dom g & (dom f) /\ dom f = dom f &
dom f = X & dom g = X by DEFmod,FUNCT_2:def 1;
rng (f mod g) c= INT
proof
let y be set; assume y in rng (f mod g); then
consider a being set such that
A2: a in dom (f mod g) & y = (f mod g).a by FUNCT_1:def 5;
f.a in rng f & g.a in rng g by A1,A2,FUNCT_1:12; then
reconsider i = f.a, j = g.a as Element of INT;
thus thesis by A2,INT_1:def 2;
end;
hence thesis by A1,FUNCT_2:4;
end;
func leq(f,g) -> Function of X, INT;
coherence
proof
A1: rng f c= INT & rng g c= INT &
dom leq(f,g) = (dom f) /\ dom g & (dom f) /\ dom f = dom f &
dom f = X & dom g = X by DEFleq,FUNCT_2:def 1;
rng leq(f,g) c= INT
proof
let y be set; assume y in rng leq(f,g); then
consider a being set such that
A2: a in dom leq(f,g) & y = leq(f,g).a by FUNCT_1:def 5;
f.a in rng f & g.a in rng g by A1,A2,FUNCT_1:12; then
reconsider i = f.a, j = g.a as Element of INT;
thus thesis by A2,INT_1:def 2;
end;
hence thesis by A1,FUNCT_2:4;
end;
func gt(f,g) -> Function of X, INT;
coherence
proof
A1: rng f c= INT & rng g c= INT &
dom gt(f,g) = (dom f) /\ dom g & (dom f) /\ dom f = dom f &
dom f = X & dom g = X by DEFgt,FUNCT_2:def 1;
rng gt(f,g) c= INT
proof
let y be set; assume y in rng gt(f,g); then
consider a being set such that
A2: a in dom gt(f,g) & y = gt(f,g).a by FUNCT_1:def 5;
f.a in rng f & g.a in rng g by A1,A2,FUNCT_1:12; then
reconsider i = f.a, j = g.a as Element of INT;
thus thesis by A2,INT_1:def 2;
end;
hence thesis by A1,FUNCT_2:4;
end;
func eq(f,g) -> Function of X, INT;
coherence
proof
A1: rng f c= INT & rng g c= INT &
dom eq(f,g) = (dom f) /\ dom g & (dom f) /\ dom f = dom f &
dom f = X & dom g = X by DEFeq,FUNCT_2:def 1;
rng eq(f,g) c= INT
proof
let y be set; assume y in rng eq(f,g); then
consider a being set such that
A2: a in dom eq(f,g) & y = eq(f,g).a by FUNCT_1:def 5;
f.a in rng f & g.a in rng g by A1,A2,FUNCT_1:12; then
reconsider i = f.a, j = g.a as Element of INT;
thus thesis by A2,INT_1:def 2;
end;
hence thesis by A1,FUNCT_2:4;
end;
end;
definition redefine
let X be non empty set;
let t1,t2 be Function of X, INT;
func t1-t2 -> Function of X, INT means:
DEFminus3:
for s being Element of X holds it.s = (t1.s)-(t2.s);
compatibility
proof
let ti be Function of X, INT;
A1: dom (t1-t2) = (dom t1)/\dom t2 & dom t1 = X & dom t2 = X & dom ti = X
by FUNCT_2:def 1,VALUED_1:12;
thus ti = t1-t2 implies
for s being Element of X holds ti.s = (t1.s)-(t2.s) by VALUED_1:15;
assume
A2: for s being Element of X holds ti.s = (t1.s)-(t2.s);
now let s be set; assume
A3: s in X;
hence ti.s = (t1.s)-(t2.s) by A2 .= (t1-t2).s by A3,VALUED_1:15;
end;
hence ti = t1-t2 by A1,FUNCT_1:9;
end;
coherence
proof
thus t1-t2 is Function of X, INT;
end;
func t1+t2 -> Function of X, INT means
for s being Element of X holds it.s = (t1.s)+(t2.s);
compatibility
proof
let ti be Function of X, INT;
A1: dom (t1+t2) = (dom t1)/\dom t2 & dom t1 = X & dom t2 = X & dom ti = X
by FUNCT_2:def 1,VALUED_1:def 1;
hence ti = t1+t2 implies
for s being Element of X holds ti.s = (t1.s)+(t2.s) by VALUED_1:def 1;
assume for s being Element of X holds ti.s = (t1.s)+(t2.s); then
for s being set st s in X holds ti.s = (t1.s)+(t2.s);
hence ti = t1+t2 by A1,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
consider a being Element of A;
{a} c= A & Card {a} = 1 by ZFMISC_1:37,CARD_1:50; then
A1: Card B <> 0 & 1 <=` Card A by CARD_1:27;
Card A = Card Card A & Card Card B = Card B; then
Card Funcs(A, B) = exp(Card B, Card A) by FUNCT_5:68; then
exp(Card B, 1) <=` Card Funcs(A, B) by A1,CARD_4:71; then
Card B <=` Card Funcs(A, B) & Card B is infinite
by CARD_2:40,CARD_4:1; then
Card Funcs(A, B) is infinite by FINSET_1:13;
hence thesis by CARD_4:1;
end;
end;
definition
let N be set;
let v be Function;
let f be Function;
func v**(f,N) -> Function means:
DSTAR:
(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
Y1: for y being set holds
y in Y1 iff ex h being Function st h in dom v & y in rng h and
A1: 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
B1: for g being Function st g in dom F1 holds F1.g = v.(g*f);
given Y2 being set such that
Y2: for y being set holds
y in Y2 iff ex h being Function st h in dom v & y in rng h and
A2: 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;
assume
B2: for g being Function st g in dom F2 holds F2.g = v.(g*f);
now let a be set;
a in Y1 iff ex h being Function st h in dom v & a in rng h by Y1;
hence a in Y1 iff a in Y2 by Y2;
end; then
Y3: Y1 = Y2 by TARSKI:2;
now
let a be set;
a in dom F1 iff a in Funcs(N,Y1) &
ex g being Function st a = g & g*f in dom v by A1;
hence a in dom F1 iff a in dom F2 by A2,Y3;
end; then
A3: dom F1 = dom F2 by TARSKI:2;
now
let a be set;
assume
A4: a in dom F1; then
consider g being Function such that
A5: a = g & g*f in dom v by A1;
thus F1.a = v.(g*f) by B1,A4,A5 .= F2.a by B2,A3,A4,A5;
end;
hence thesis by A3,FUNCT_1:9;
end;
existence
proof
defpred P[set,set] means
ex g being Function st $1 = g & $2 = rng g;
A0: for x,y,z being set st P[x,y] & P[x,z] holds y = z;
consider X being set such that
A1: for x being set holds x in X iff ex y being set st y in dom v & P[y,x]
from TARSKI:sch 1(A0);
set Y = union X;
defpred R[set] means ex g being Function st g = $1 & g*f in dom v;
consider D being set such that
A2: for x being set holds x in D iff x in Funcs(N,Y) & R[x]
from XBOOLE_0:sch 1;
defpred F[set,set] means ex g being Function st g = $1 & $2 = v.(g*f);
B1: for x,y1,y2 being set st x in D & F[x,y1] & F[x,y2] holds y1 = y2;
B2: for x being set st x in D ex y being set st F[x,y]
proof
let x be set; assume x in D; then
consider y being Function such that
B4: y = x & y*f in dom v by A2;
take v.(y*f);
thus F[x,v.(y*f)] by B4;
end;
consider F being Function such that
A3: dom F = D & for g being set st g in D holds F[g,F.g]
from FUNCT_1:sch 2(B1,B2);
take F;
hereby take Y;
hereby let y be set;
hereby assume y in Y; then
consider a being set such that
C2: y in a & a in X by TARSKI:def 4;
consider z being set such that
C3: z in dom v & P[z,a] by C2,A1;
thus ex h being Function st h in dom v & y in rng h by C2,C3;
end;
given h being Function such that
C1: h in dom v & y in rng h;
rng h in X by C1,A1;
hence y in Y by C1,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 A3,A2;
end;
let g be Function; assume g in dom F; then
F[g,F.g] by A3;
hence F.g = v.(g*f);
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);
coherence
proof
A0: dom v = Funcs(X,Y) & rng v c= Z by FUNCT_2:def 1;
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 DSTAR;
A3: Y0 = Y
proof
thus Y0 c= Y
proof let y be set; assume y in Y0; then
consider h being Function such that
B1: h in dom v & y in rng h by A1;
rng h c= Y by B1,FUNCT_2:169;
hence thesis by B1;
end;
let y be set; assume y in Y; then
reconsider y as Element of Y;
reconsider h = X-->y as Function of X,Y;
y in {y} & rng h = {y} & h in Funcs(X,Y)
by TARSKI:def 1,FUNCOP_1:14,FUNCT_2:11;
hence thesis by A0,A1;
end;
A4: dom (v**(f,N)) = Funcs(N,Y)
proof
thus dom (v**(f,N)) c= Funcs(N,Y)
proof
let a be set;
thus thesis by A2,A3;
end;
let a be set; assume
B2: a in Funcs(N,Y); then
reconsider g = a as Function of N,Y by FUNCT_2:121;
g*f in Funcs(X,Y) by FUNCT_2:11;
hence thesis by A0,A2,A3,B2;
end;
rng (v**(f,N)) c= Z
proof
let a be set; assume a in rng (v**(f,N)); then
consider g being set such that
B3: g in dom (v**(f,N)) & a = (v**(f,N)).g by FUNCT_1:def 5;
reconsider g as Element of Funcs(N,Y) by A4,B3;
reconsider gf = g*f as Element of Funcs(X,Y) by FUNCT_2:11;
a = v.gf by B3,DSTAR;
hence thesis;
end;
hence thesis by A4,FUNCT_2:def 2;
end;
end;
theorem LemR:
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
Z0: rng g c= dom f2;
dom (f1+*f2) = dom f1 \/ dom f2 by FUNCT_4:def 1; then
Z2: dom ((f1+*f2)*g) = dom g & dom (f2*g) = dom g by Z0,XBOOLE_1:10,RELAT_1:46;
now
let x be set; assume x in dom g; then
((f1+*f2)*g).x = (f1+*f2).(g.x) & (f2*g).x = f2.(g.x) & g.x in rng g
by FUNCT_1:12,23;
hence ((f1+*f2)*g).x = (f2*g).x by Z0,FUNCT_4:14;
end;
hence (f1+*f2)*g = f2*g by Z2,FUNCT_1:9;
end;
theorem LemQ:
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 such that
Z0: c is one-to-one;
let n be Element of I;
set f = N-->n, g = s*c";
Z1: dom (f+*g) = dom f \/ dom g by FUNCT_4:def 1;
Z2: dom g c= dom (c") & rng g c= rng s by RELAT_1:44,45;
Z3: dom f = N & rng f = {n} by FUNCOP_1:14,19;
dom (c") = rng c & rng c c= N by Z0,FUNCT_1:55; then
Z4: dom (f+*g) = N by Z1,Z2,Z3,XBOOLE_1:1,12;
rng g c= I by Z2,XBOOLE_1:1; then
rng (f+*g) c= rng f \/ rng g & rng f \/ rng g c= I
by XBOOLE_1:8,FUNCT_4:18;
hence (N-->n)+*(s*c") is Function of N,I by Z4,FUNCT_2:4,XBOOLE_1:1;
end;
theorem ThDS1:
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
Z0: dom v1 = dom v2 & dom v1 = Funcs(X,I);
reconsider rv1 = rng v1, rv2 = rng v2 as non empty set by Z0,RELAT_1:65;
reconsider Z = rv1\/rv2 as non empty set;
rng v1 c= Z & rng v2 c= Z by XBOOLE_1:7; then
reconsider f1 = v1, f2 = v2 as Element of Funcs(Funcs(X,I),Z)
by Z0,FUNCT_2:def 2;
let f be Function of X, N such that
Z1: f is one-to-one & v1**(f,N) = v2**(f,N);
02: dom (f1**(f,N)) = Funcs(N,I) & dom (f2**(f,N)) = Funcs(N,I)
by FUNCT_2:def 1;
now
let a be set; assume a in Funcs(X,I); then
reconsider h = a as Element of Funcs(X,I);
consider i being Element of I;
set g = (N-->i)+*(h*f");
g is Function of N,I by Z1,LemQ; then
03: g in Funcs(N,I) by FUNCT_2:11;
01: rng (f") = dom f & dom f = X & dom h = X
by Z1,FUNCT_1:55,FUNCT_2:def 1; then
dom (h*f") = dom (f") by RELAT_1:46 .= rng f by Z1,FUNCT_1:55; then
g*f = (h*f")*f by LemR .= h*(f"*f) by RELAT_1:55
.= h*id X by Z1,01,FUNCT_1:61 .= a by 01,RELAT_1:78; then
(v1**(f,N)).g = v1.a & (v2**(f,N)).g = v2.a by 02,03,DSTAR;
hence v1.a = v2.a by Z1;
end;
hence v1 = v2 by Z0,FUNCT_1:9;
end;
registration
let X be set;
cluster one-to-one onto Function of X, Card X;
existence
proof
X, Card X are_equipotent by CARD_1:def 5; then
consider f being Function such that
A1: f is one-to-one & dom f = X & rng f = Card X by WELLORD2:def 4;
reconsider f as Function of X,Card X by A1,FUNCT_2:4;
take f; thus f is one-to-one by A1;
thus rng f = Card X by A1;
end;
cluster one-to-one onto Function of Card X, X;
existence
proof
X, Card X are_equipotent by CARD_1:def 5; then
consider f being Function such that
A1: f is one-to-one & dom f = Card X & rng f = X by WELLORD2:def 4;
reconsider f as Function of Card X, X by A1,FUNCT_2:4;
take f; thus f is one-to-one by A1;
thus rng f = X by A1;
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 ThNum1:
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 = {} by CARD_2:59;
hence thesis by FUNCT_2:def 1,4,def 3;
end;
theorem ThNum2:
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 = {} by CARD_1:47;
hence thesis by FUNCT_2:def 1,4,def 3;
end;
theorem ThNum6:
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 & A = dom (f+*(x,f.y)) &
dom f = X & rng f = Card X by ThNum1,FUNCT_7:32;
A2: rng (f+*(x,f.y)+*(y,f.x)) = rng f
proof
f.y in rng f & f.x in rng f by A1; then
{f.y} c= rng f & {f.x} c= rng f by ZFMISC_1:37; then
A4: rng g c= rng (f+*(x,f.y)) \/ {f.x} & rng f \/ {f.y} = rng f &
rng f \/ {f.x} = rng f & rng (f+*(x,f.y)) c= rng f \/ {f.y}
by XBOOLE_1:12,POLYNOM1:6; then
rng (f+*(x,f.y)) \/ {f.x} c= rng f by XBOOLE_1:9;
hence rng g c= rng f by A4,XBOOLE_1:1;
let z be set; assume z in rng f; then
consider a being set such that
A6: a in dom f & z = f.a by FUNCT_1:def 5;
per cases;
suppose a <> x & a <> y; then
g.a = (f+*(x,f.y)).a & (f+*(x,f.y)).a = z by A6,FUNCT_7:34;
hence z in rng g by A1,A6,FUNCT_1:def 5;
end;
suppose a = x; then
g.y = z by A1,A6,FUNCT_7:33;
hence z in rng g by A1,FUNCT_1:def 5;
end;
suppose a = y; then
(x = y implies g.x = z) & (f+*(x,z)).x = z &
(x <> y implies g.x = (f+*(x,z)).x) by A1,A6,FUNCT_7:33,34;
hence z in rng g by A1,FUNCT_1:def 5;
end;
end;
f+*(x,f.y)+*(y,f.x) is one-to-one
proof
let a,b being set;
A3: (a = y implies g.a = f.x) &
(a <> y implies g.a = (f+*(x,f.y)).a) &
(a = x implies (f+*(x,f.y)).a = f.y) &
(a <> x implies (f+*(x,f.y)).a = f.a) by A1,FUNCT_7:33,34;
(b = y implies g.b = f.x) &
(b <> y implies g.b = (f+*(x,f.y)).b) &
(b = x implies (f+*(x,f.y)).b = f.y) &
(b <> x implies (f+*(x,f.y)).b = f.b) by A1,FUNCT_7:33,34;
hence thesis by A1,A3,FUNCT_1:def 8;
end;
hence thesis by A1,A2,ThNum1;
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;
consider f being Enumeration of X;
0 in Card X & dom f = X & rng f = Card X by ThNum1,ORDINAL3:10; then
consider y being set such that
A1: y in X & 0 = f.y by FUNCT_1:def 5;
reconsider y as Element of X by A1;
reconsider g = f+*(y,f.x)+*(x,0) as Enumeration of X by A1,ThNum6;
take g;
dom f = X by ThNum1; then
dom (f+*(y,f.x)) = X by FUNCT_7:32;
hence thesis by FUNCT_7:33;
end;
theorem ThNum4:
for X being non empty set, f being Denumeration of X
holds f.0 in X by FUNCT_2:7,ORDINAL3:10;
theorem ThNum5:
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_4:def 1,CARD_1:83;
hence thesis by ThNum1;
end;
definition
let X be set;
let f be Enumeration of X;
redefine func f" -> Denumeration of X;
coherence
proof
dom f = X & rng f = Card X & f is one-to-one by ThNum1; then
dom (f") = Card X & rng (f") = X & f" is one-to-one by FUNCT_1:55;
hence thesis by ThNum2;
end;
end;
definition
let X be set;
let f be Denumeration of X;
redefine func f" -> Enumeration of X;
coherence
proof
dom f = Card X & rng f = X & f is one-to-one by ThNum2; then
dom (f") = X & rng (f") = Card X & f" is one-to-one by FUNCT_1:55;
hence thesis by ThNum1;
end;
end;
LemP0:
for x being real number, n being Nat holds x to_power n = x |^ n
by POWER:46;
theorem LemP1:
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 n+m <> 0 by NAT_1:7; then
n+m > 0; then
0 to_power (n+m) = 0 & (0 to_power n = 0 or 0 to_power m = 0)
by A1,POWER:def 2;
hence thesis;
end;
suppose
n = 0 & m = 0; then
0 to_power (n+m) = 1 & 0 to_power n = 1 & 0 to_power m = 1
by POWER:def 2,POWER:29;
hence thesis;
end;
end;
theorem LemP2:
for x being real number
for n,m being Nat holds (x to_power n) to_power m = x to_power (n*m)
proof
let x be real number;
let n,m be Nat;
(x to_power n) to_power m = (x to_power n) |^ m &
x to_power n = x |^ n & x to_power (n*m) = x |^ (n*m) by LemP0;
hence thesis by NEWTON:14;
end;
LemP3: for x being real number holds x to_power 2 = x*x by NEWTON:100;
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:
IA:
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:
FA:
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
A: 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
A1: I is_assignment_wrt A,X,f by A;
consider v being (INT-Variable of X), t being INT-Expression of X
such that
A2: for s being Element of Funcs(X, INT) holds f.(s, I) = s+*(v.s,t.s)
by A1,IA;
take v,t,I;
thus thesis by A1,IA,A2;
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
A: 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
A1: I is_assignment_wrt A,X,f by A;
consider v being (INT-Variable of X), t being INT-Expression of X
such that
A2: for s being Element of Funcs(X, INT) holds f.(s, I) = s+*(v.s,t.s)
by A1,IA;
take t,v,I;
thus thesis by A1,A2,IA;
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;
coherence
proof
f.x in rng f by FUNCT_2:6;
hence thesis;
end;
end;
definition
let X be non empty set;
let x be Element of X;
func .x -> INT-Expression of X means:
::equals (commute id Funcs(X,INT)).x;
DEFvarexp1:
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 by FUNCT_2:113;
end;
end;
definition
let X be non empty set;
let v be INT-Variable of X;
func .v -> INT-Expression of X means:
DEFvarexp:
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 by FUNCT_2:113;
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 DEFvarexp .= s.x by FUNCOP_1:13;
end;
hence .x = .(^x) by DEFvarexp1;
end;
definition
let X be non empty set;
let i be integer number;
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:57;
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);
A1: .(0,X).s = 0 by FUNCOP_1:13;
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 by A1;
end;
hence t+ .(0,X) = t by FUNCT_2:113;
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 by FUNCOP_1:13 .= t.s;
end;
hence t(#).(1,X) = t by FUNCT_2:113;
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:
INT'iwa:
(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 number holds .(i,X) is INT-Expression of A,f) &
(for v being INT-Variable of A,f holds .v is INT-Expression of A,f) &
(for x being Element of X holds ^x is INT-Variable of A,f) &
(ex a being INT-Array of X st a|Card X is one-to-one &
for t being INT-Expression of A,f holds a*t is INT-Variable of A,f) &
(for t being INT-Expression of A,f holds
-t is INT-Expression of A,f) &
(for t1,t2 being INT-Expression of A,f holds
t1(#)t2 is INT-Expression of A,f &
t1+t2 is INT-Expression of A,f &
t1 div t2 is INT-Expression of A,f &
t1 mod t2 is INT-Expression of A,f &
leq(t1,t2) is INT-Expression of A,f &
gt(t1,t2) is INT-Expression of A,f);
end;
:: 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:
INT'iwa2:
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:
INTiwaEXEC:
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
set S = ECIW-signature, G = INT-ElemIns;
set A = FreeUnivAlgNSG(S,G);
reconsider b = 0 as Nat;
set Q = Funcs(NAT, INT), T = Q\(0,0);
AA: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
BB: Terminals DTConUA(S,G) = G by FREEALG:3;
defpred P[set,set] 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);
00: for x being set st x in [:Q,ElementaryInstructions A:]
ex y being set st y in Q & P[x,y]
proof
let x be set; assume x in [:Q,ElementaryInstructions A:]; then
consider s, I being set such that
00: s in Q & I in ElementaryInstructions A & x = [s,I] by ZFMISC_1:def 2;
consider a being Symbol of DTConUA(S,G) such that
01: I = root-tree a & a in Terminals DTConUA(S,G) by AA,00;
consider v,e being set such that
02: v in Funcs(Funcs(NAT, INT), NAT) & e in Funcs(Funcs(NAT, INT), INT) &
a = [v,e] by BB,01,ZFMISC_1:def 2;
reconsider s as Element of Q by 00;
reconsider v as Element of Funcs(Q, NAT) by 02;
reconsider e as Element of Funcs(Q, INT) by 02;
take y = s+*(v.s,e.s);
thus y in Q by FUNCT_2:11;
take s,v,e;
thus x = [s, root-tree [v,e]] & y = s+*(v.s,e.s) by 00,01,02;
end;
consider g being Function such that
01: dom g = [:Q,ElementaryInstructions A:] & rng g c= Q and
02: for x being set st x in [:Q,ElementaryInstructions A:] holds P[x,g.x]
from WELLORD2:sch 1(00);
reconsider g as Function of [:Q,ElementaryInstructions A:], Q
by 01,FUNCT_2:4;
reconsider i0 = 0 as Element of INT by INT_1:def 1;
reconsider q0 = NAT-->i0 as Element of Q by FUNCT_2:11;
consider f being ExecutionFunction of A, Q, T such that
A1: 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:106; then
I in ElementaryInstructions A by AA,BB; then
A2: [s,I] in [:Q,ElementaryInstructions A:] by ZFMISC_1:106; then
consider s' being (Element of Q), v' being (Element of Funcs(Q, NAT)),
e' being Element of Funcs(Q, INT) such that
A3: [s,I] = [s', root-tree [v',e']] & g.[s,I] = s'+*(v'.s',e'.s') by 02;
A4: s = s' & I = root-tree [v',e'] by A3,ZFMISC_1:33; then
[v,e] = [v',e'] by TREES_4:4; then
v = v' & e = e' by ZFMISC_1:33;
hence f.(s, root-tree [v,e]) = s+*(v.s,e.s) by A1,A2,A3,A4,FUNCT_1:72;
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
set S = ECIW-signature, G = INT-ElemIns X;
set A = FreeUnivAlgNSG(S,G);
reconsider b = 0 as Nat;
set Q = Funcs(X, INT), T = Q\(x,0);
AA: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
BB: Terminals DTConUA(S,G) = G by FREEALG:3;
defpred P[set,set] 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);
00: for x being set st x in [:Q,ElementaryInstructions A:]
ex y being set st y in Q & P[x,y]
proof
let x be set; assume x in [:Q,ElementaryInstructions A:]; then
consider s, I being set such that
00: s in Q & I in ElementaryInstructions A & x = [s,I] by ZFMISC_1:def 2;
consider a being Symbol of DTConUA(S,G) such that
01: I = root-tree a & a in Terminals DTConUA(S,G) by AA,00;
consider v,e being set such that
02: v in Funcs(Funcs(X, INT), X) & e in Funcs(Funcs(X, INT), INT) &
a = [v,e] by BB,01,ZFMISC_1:def 2;
reconsider s as Element of Q by 00;
reconsider v as Element of Funcs(Q, X) by 02;
reconsider e as Element of Funcs(Q, INT) by 02;
take y = s+*(v.s,e.s);
thus y in Q by FUNCT_2:11;
take s,v,e;
thus x = [s, root-tree [v,e]] & y = s+*(v.s,e.s) by 00,01,02;
end;
consider g being Function such that
01: dom g = [:Q,ElementaryInstructions A:] & rng g c= Q and
02: for x being set st x in [:Q,ElementaryInstructions A:] holds P[x,g.x]
from WELLORD2:sch 1(00);
reconsider g as Function of [:Q,ElementaryInstructions A:], Q
by 01,FUNCT_2:4;
reconsider i0 = 0 as Element of INT by INT_1:def 1;
reconsider q0 = X-->i0 as Element of Q by FUNCT_2:11;
consider f being ExecutionFunction of A, Q, T such that
A1: 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:106; then
I in ElementaryInstructions A by AA,BB; then
A2: [s,I] in [:Q,ElementaryInstructions A:] by ZFMISC_1:106; then
consider s' being (Element of Q), v' being (Element of Funcs(Q, X)),
e' being Element of Funcs(Q, INT) such that
A3: [s,I] = [s', root-tree [v',e']] & g.[s,I] = s'+*(v'.s',e'.s') by 02;
A4: s = s' & I = root-tree [v',e'] by A3,ZFMISC_1:33; then
[v,e] = [v',e'] by TREES_4:4; then
v = v' & e = e' by ZFMISC_1:33;
hence f.(s, root-tree [v,e]) = s+*(v.s,e.s) by A1,A2,A3,A4,FUNCT_1:72;
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
A: rng c c= NAT;
mode INT-Exec of c,T -> ExecutionFunction of
FreeUnivAlgNSG(ECIW-signature, INT-ElemIns), Funcs(X, INT), T means:
INTiwaEXECc:
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
set S = ECIW-signature, G = INT-ElemIns;
set A = FreeUnivAlgNSG(S,G);
set x = c".0;
set Q = Funcs(X, INT);
reconsider b = 0 as Nat;
reconsider i0 = 0 as Element of INT by INT_1:def 1;
reconsider q0 = X-->i0 as Element of Q by FUNCT_2:11;
dom c = X by ThNum1; then
reconsider c' = c as Function of X, NAT by A,FUNCT_2:4;
AA: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
BB: Terminals DTConUA(S,G) = G by FREEALG:3;
defpred P[set,set] 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)**(c',NAT),e**(c',NAT)]) or
ex v being (Element of Funcs(Q, X)), e being Element of Funcs(Q, INT) st
$1`2 = root-tree [(c*v)**(c',NAT),e**(c',NAT)] & $2 = s+*(v.s,e.s));
00: for x being set st x in [:Q,ElementaryInstructions A:]
ex y being set st y in Q & P[x,y]
proof
let x be set; assume x in [:Q,ElementaryInstructions A:]; then
consider s, I being set such that
00: s in Q & I in ElementaryInstructions A & x = [s,I] by ZFMISC_1:def 2;
05: x`1 = s & x`2 = I by 00,MCART_1:7;
consider a being Symbol of DTConUA(S,G) such that
01: I = root-tree a & a in Terminals DTConUA(S,G) by AA,00;
reconsider s as Element of Q by 00;
per cases;
suppose
ex v being (Element of Funcs(Q, X)), e being Element of Funcs(Q, INT)
st a = [(c*v)**(c',NAT),e**(c',NAT)]; then
consider v being (Element of Funcs(Q, X)),
e being Element of Funcs(Q, INT) such that
03: a = [(c*v)**(c',NAT),e**(c',NAT)];
take y = s+*(v.s,e.s);
thus y in Q by FUNCT_2:11;
thus thesis by 05,01,03;
end;
suppose
04: not ex v being (Element of Funcs(Q, X)),
e being Element of Funcs(Q, INT) st a = [(c*v)**(c',NAT),e**(c',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)**(c',NAT),e**(c',NAT)] by 04,05,01,TREES_4:4;
hence thesis by 05;
end;
end;
consider g being Function such that
01: dom g = [:Q,ElementaryInstructions A:] & rng g c= Q and
02: for x being set st x in [:Q,ElementaryInstructions A:] holds P[x,g.x]
from WELLORD2:sch 1(00);
reconsider g as Function of [:Q,ElementaryInstructions A:], Q
by 01,FUNCT_2:4;
consider f being ExecutionFunction of A, Q, T such that
A1: 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 = c'*vv as Element of Funcs(Funcs(X, INT), NAT)
by FUNCT_2:11;
set v0 = cv**(c',NAT), e0 = e**(c',NAT);
set I = root-tree [v0,e0];
[v0,e0] in G by ZFMISC_1:106; then
I in ElementaryInstructions A by AA,BB; then
A2: [s,I] in [:Q,ElementaryInstructions A:] by ZFMISC_1:106; then
A4: P[[s,I],g.[s,I]] & [s,I]`2 = I & [s,I]`1 = s by 02,MCART_1:7;
consider v' being (Element of Funcs(Q, X)),
e' being Element of Funcs(Q, INT) such that
A3: [s,I]`2 = root-tree [(c*v')**(c',NAT),e'**(c',NAT)] &
g.[s,I] = s+*(v'.s,e'.s) by A4;
A6: rng v c= X & rng v' c= X & dom c' = X & dom v' = Q & dom v = Q &
dom e = Q & dom e' = Q & dom cv = Q & dom (c'*v') = Q
by FUNCT_2:def 1;
[v0,e0] = [(c*v')**(c',NAT),e'**(c',NAT)] by A3,A4,TREES_4:4; then
v0 = (c*v')**(c',NAT) & e0 = e'**(c',NAT) by ZFMISC_1:33; then
A5: cv = c*v' & e = e' by A6,ThDS1;
v = v' by A5,A6,FUNCT_1:49;
hence f.(s, root-tree [(c*v)**(c,NAT),e**(c,NAT)]) = s+*(v.s,e.s)
by A1,A2,A3,A5,FUNCT_1:72;
end;
end;
theorem II1:
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
set X = NAT;
set S = ECIW-signature, G = INT-ElemIns;
set A = FreeUnivAlgNSG(S,G);
let f be INT-Exec;
let v be INT-Variable of NAT;
let t be INT-Expression of NAT;
reconsider v' = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:11;
reconsider t' = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:11;
AA: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
BB: Terminals DTConUA(S,G) = G by FREEALG:3;
CC: [v',t'] in G by ZFMISC_1:106; then
root-tree [v',t'] in ElementaryInstructions A by AA,BB; then
reconsider I = root-tree [v',t'] as Element of A;
take I; thus I in ElementaryInstructions A by AA,BB,CC;
thus for s being Element of Funcs(X, INT) holds f.(s, I) = s+*(v.s,t.s)
by INTiwaEXEC;
end;
theorem II2:
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 X = NAT;
set S = ECIW-signature, G = INT-ElemIns;
set A = FreeUnivAlgNSG(S,G);
let f be INT-Exec;
let v be INT-Variable of NAT;
consider t being INT-Expression of NAT;
AA: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
BB: Terminals DTConUA(S,G) = G by FREEALG:3;
reconsider v' = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:11;
reconsider t' = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:11;
CC: [v',t'] in G by ZFMISC_1:106; then
root-tree [v',t'] in ElementaryInstructions A by AA,BB; then
reconsider I = root-tree [v',t'] as Element of A;
hereby take I;
thus I is_assignment_wrt A,X,f
proof thus I in ElementaryInstructions A by AA,BB,CC;
take v,t;
thus thesis by INTiwaEXEC;
end;
end;
take t; thus v,t form_assignment_wrt f by II1;
end;
theorem II3:
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 X = NAT;
set S = ECIW-signature, G = INT-ElemIns;
set A = FreeUnivAlgNSG(S,G);
let f be INT-Exec;
consider v being INT-Variable of NAT;
let t be INT-Expression of NAT;
AA: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
BB: Terminals DTConUA(S,G) = G by FREEALG:3;
reconsider v' = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:11;
reconsider t' = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:11;
CC: [v',t'] in G by ZFMISC_1:106; then
root-tree [v',t'] in ElementaryInstructions A by AA,BB; then
reconsider I = root-tree [v',t'] as Element of A;
hereby take I;
thus I is_assignment_wrt A,X,f
proof thus I in ElementaryInstructions A by AA,BB,CC;
take v,t;
thus thesis by INTiwaEXEC;
end;
end;
take v; thus v,t form_assignment_wrt f by II1;
end;
registration
cluster -> Euclidean INT-Exec;
coherence
proof let f be INT-Exec;
set X = NAT;
set S = ECIW-signature, G = INT-ElemIns;
set A = FreeUnivAlgNSG(S,G);
set T = Funcs(X, INT)\(0,0);
thus for v being INT-Variable of A,f, t being INT-Expression of A,f
holds v,t form_assignment_wrt f by II1;
thus for i being integer number holds
.(i,X) is INT-Expression of A,f by II3;
thus for v being INT-Variable of A,f holds
.v is INT-Expression of A,f by II3;
thus for x being Element of X holds ^x is INT-Variable of A,f by II2;
set a = (INT --> 0)+*(id X);
{0} c= X by ZFMISC_1:37; then
dom (INT --> 0) = INT & rng (INT --> 0) = {0} &
dom id X = X & rng id X = X &
INT \/ X = INT & {0} \/ X = X
by NUMBERS:17,XBOOLE_1:12,RELAT_1:71,FUNCOP_1:14,19; then
dom a = INT & rng a c= NAT by FUNCT_4:def 1,18; then
reconsider a as INT-Array of X by FUNCT_2:4;
hereby take a;
Card X = X & dom id X = X by RELAT_1:71,CARD_1:84;
hence a|Card X is one-to-one by FUNCT_4:24;
thus for t being INT-Expression of A,f holds
a*t is INT-Variable of A,f by II2;
end;
thus thesis by II3;
end;
end;
theorem cII1:
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
let X be non empty countable set;
let T be Subset of Funcs(X, INT);
let c be Enumeration of X;
A0: rng c c= NAT & dom c = X by ThNum1,ThNum5; then
reconsider c' = c as Function of X,NAT by FUNCT_2:4;
set S = ECIW-signature, G = INT-ElemIns;
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 v' = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:11;
reconsider t' = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:11;
reconsider cv = c'*v as Element of Funcs(Funcs(X,INT),NAT) by FUNCT_2:11;
set v1 = cv**(c',NAT), t1 = t'**(c',NAT);
AA: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
BB: Terminals DTConUA(S,G) = G by FREEALG:3;
CC: [v1,t1] in G by ZFMISC_1:106; then
root-tree [v1,t1] in ElementaryInstructions A by AA,BB; 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*v')**(c,NAT),t'**(c,NAT)]) = s+*(v'.s,t'.s)
by A0,INTiwaEXECc;
hence thesis by AA,BB,CC;
end;
theorem cII2:
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
let X be non empty countable set;
let T be Subset of Funcs(X, INT);
let c be Enumeration of X;
A0: rng c c= NAT & dom c = X by ThNum1,ThNum5; then
reconsider c' = c as Function of X,NAT by FUNCT_2:4;
set S = ECIW-signature, G = INT-ElemIns;
set A = FreeUnivAlgNSG(S,G);
let f be INT-Exec of c,T;
let v be INT-Variable of X;
consider t being INT-Expression of X;
AA: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
BB: Terminals DTConUA(S,G) = G by FREEALG:3;
reconsider v' = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:11;
reconsider t' = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:11;
reconsider cv = c'*v as Element of Funcs(Funcs(X,INT),NAT) by FUNCT_2:11;
set v1 = cv**(c',NAT), t1 = t'**(c',NAT);
CC: [v1,t1] in G by ZFMISC_1:106; then
root-tree [v1,t1] in ElementaryInstructions A by AA,BB; 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 AA,BB,CC;
take v,t;
for s being Element of Funcs(X, INT)
holds f.(s, root-tree [(c*v')**(c,NAT),t'**(c,NAT)]) = s+*(v'.s,t'.s)
by A0,INTiwaEXECc;
hence thesis;
end;
end;
take t; thus v,t form_assignment_wrt f by cII1;
end;
theorem cII3:
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
let X be non empty countable set;
let T be Subset of Funcs(X, INT);
let c be Enumeration of X;
A0: rng c c= NAT & dom c = X by ThNum1,ThNum5; then
reconsider c' = c as Function of X,NAT by FUNCT_2:4;
set S = ECIW-signature, G = INT-ElemIns;
set A = FreeUnivAlgNSG(S,G);
let f be INT-Exec of c,T;
consider v being INT-Variable of X;
let t be INT-Expression of X;
AA: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
BB: Terminals DTConUA(S,G) = G by FREEALG:3;
reconsider v' = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:11;
reconsider t' = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:11;
reconsider cv = c'*v as Element of Funcs(Funcs(X,INT),NAT) by FUNCT_2:11;
set v1 = cv**(c',NAT), t1 = t'**(c',NAT);
CC: [v1,t1] in G by ZFMISC_1:106; then
root-tree [v1,t1] in ElementaryInstructions A by AA,BB; 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 AA,BB,CC;
take v,t;
for s being Element of Funcs(X, INT)
holds f.(s, root-tree [(c*v')**(c,NAT),t'**(c,NAT)]) = s+*(v'.s,t'.s)
by A0,INTiwaEXECc;
hence thesis;
end;
end;
take v; thus v,t form_assignment_wrt f by cII1;
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 INT-Exec of c,T;
coherence
proof let f be INT-Exec of c,T;
set S = ECIW-signature, G = INT-ElemIns;
set A = FreeUnivAlgNSG(S,G);
set x = c".0;
thus for v being INT-Variable of A,f, t being INT-Expression of A,f
holds v,t form_assignment_wrt f by cII1;
thus for i being integer number holds
.(i,X) is INT-Expression of A,f by cII3;
thus for v being INT-Variable of A,f holds
.v is INT-Expression of A,f by cII3;
thus for x being Element of X holds ^x is INT-Variable of A,f by cII2;
set a = (INT --> x)+*(c");
x in X & Card X = rng c & rng c c= NAT by ThNum1,ThNum4,ThNum5; then
{x} c= X & Card X c= INT by XBOOLE_1:1,ZFMISC_1:37,NUMBERS:17; then
dom (INT --> x) = INT & rng (INT --> x) = {x} &
dom (c") = Card X & rng (c") = X & {x} \/ X = X & INT \/ Card X = INT
by ThNum2,XBOOLE_1:12,FUNCOP_1:14,19; then
dom a = INT & rng a c= X by FUNCT_4:def 1,18; then
reconsider a as INT-Array of X by FUNCT_2:4;
hereby take a;
dom (c") = Card X by ThNum2;
hence a|Card X is one-to-one by FUNCT_4:24;
thus for t being INT-Expression of A,f holds
a*t is INT-Variable of A,f by cII2;
end;
thus thesis by cII3;
end;
end;
registration
cluster FreeUnivAlgNSG(ECIW-signature, INT-ElemIns) -> Euclidean;
coherence
proof
set A = FreeUnivAlgNSG(ECIW-signature, INT-ElemIns);
let X be non empty countable set, T be Subset of Funcs(X, INT);
consider c being Enumeration of X;
consider f being INT-Exec of c, T;
take f;
thus f is Euclidean;
end;
end;
registration
cluster Euclidean non degenerated preIfWhileAlgebra;
existence
proof
take A = 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 ExecutionFunction of A, Funcs(X, INT), T;
existence by INT'iwa2;
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 redefine
let A,X,T,f;
let t be INT-Expression of A,f;
func -t -> INT-Expression of A,f;
coherence by INT'iwa;
end;
definition redefine
let A,X,T,f;
let t be INT-Expression of A,f;
let i be integer number;
func t+i -> INT-Expression of A,f;
coherence
proof
.(i,X) is INT-Expression of A,f by INT'iwa; then
A1: t+.(i,X) is INT-Expression of A,f by INT'iwa;
A2: dom (t+.(i,X)) = Funcs(X,INT) & dom t = Funcs(X,INT) by FUNCT_2:def 1;
now
let a be set;
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 A2,VALUED_1:def 1
.= i+(t.a) by FUNCOP_1:13;
end;
hence thesis by A1,A2,VALUED_1:def 2;
end;
func t-i -> INT-Expression of A,f;
coherence
proof
.(i,X) is INT-Expression of A,f by INT'iwa; then
-.(i,X) is INT-Expression of A,f by INT'iwa; then
A1: t+-.(i,X) is INT-Expression of A,f by INT'iwa;
A2: dom (t+-.(i,X)) = Funcs(X,INT) & dom t = Funcs(X,INT) &
dom (t-i) = dom t & dom (-.(i,X)) = Funcs(X,INT)
by FUNCT_2:def 1,VALUED_1:3;
now
let a be set;
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 A2,VALUED_1:def 1
.= (t.s)+-(.(i,X).s) by VALUED_1:8
.= (t.s)-i by FUNCOP_1:13
.= (t-i).a by A2,VALUED_1:3;
end;
hence thesis by A1,A2,FUNCT_1:9;
end;
func t*i -> INT-Expression of A,f;
coherence
proof
.(i,X) is INT-Expression of A,f by INT'iwa; then
A1: t(#).(i,X) is INT-Expression of A,f by INT'iwa;
A2: dom (t(#).(i,X)) = Funcs(X,INT) & dom t = Funcs(X,INT) by FUNCT_2:def 1;
now
let a be set;
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 A2,VALUED_1:def 4
.= i*(t.a) by FUNCOP_1:13;
end;
hence thesis by A1,A2,VALUED_1:def 5;
end;
end;
definition redefine
let A,X,T,f;
let t1,t2 be INT-Expression of A,f;
func t1-t2 -> INT-Expression of A,f;
coherence
proof
-t2 is INT-Expression of A,f &
t1-t2 = t1+-t2 by RFUNCT_1:40;
hence thesis by INT'iwa;
end;
func t1+t2 -> INT-Expression of A,f;
coherence by INT'iwa;
func t1(#)t2 -> INT-Expression of A,f;
coherence by INT'iwa;
end;
definition redefine
let A,X,T,f;
let t1,t2 be INT-Expression of A,f;
func t1 div t2 -> INT-Expression of A,f means:
DEFdiv2:
for s being Element of Funcs(X, INT) holds it.s = t1.s div t2.s;
coherence by INT'iwa;
compatibility
proof
let ti be INT-Expression of A,f;
A1: dom (t1 div t2) = (dom t1)/\dom t2 & dom t1 = Funcs(X, INT) &
dom t2 = Funcs(X, INT) & dom ti = Funcs(X, INT) by DEFdiv,FUNCT_2:def 1;
hence ti = t1 div t2 implies
for s being Element of Funcs(X, INT) holds ti.s = t1.s div t2.s by DEFdiv;
assume
for s being Element of Funcs(X, INT) holds ti.s = t1.s div t2.s; then
for s being set st s in Funcs(X, INT) holds ti.s = t1.s div t2.s;
hence ti = t1 div t2 by A1,DEFdiv;
end;
func t1 mod t2 -> INT-Expression of A,f means:
DEFmod2:
for s being Element of Funcs(X, INT) holds it.s = t1.s mod t2.s;
coherence by INT'iwa;
compatibility
proof
let ti be INT-Expression of A,f;
A1: dom (t1 mod t2) = (dom t1)/\dom t2 & dom t1 = Funcs(X, INT) &
dom t2 = Funcs(X, INT) & dom ti = Funcs(X, INT) by DEFmod,FUNCT_2:def 1;
hence ti = t1 mod t2 implies
for s being Element of Funcs(X, INT) holds ti.s = t1.s mod t2.s by DEFmod;
assume
for s being Element of Funcs(X, INT) holds ti.s = t1.s mod t2.s; then
for s being set st s in Funcs(X, INT) holds ti.s = t1.s mod t2.s;
hence ti = t1 mod t2 by A1,DEFmod;
end;
func leq(t1,t2) -> INT-Expression of A,f means:
DEFleq2:
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;
A1: dom leq(t1,t2) = (dom t1)/\dom t2 & dom t1 = Funcs(X, INT) &
dom t2 = Funcs(X, INT) & dom ti = Funcs(X, INT) by DEFleq,FUNCT_2:def 1;
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 DEFleq;
assume
for s being Element of Funcs(X, INT) holds ti.s = IFGT(t1.s,t2.s,0,1); then
for s being set st s in Funcs(X, INT) holds ti.s = IFGT(t1.s,t2.s,0,1);
hence ti = leq(t1,t2) by A1,DEFleq;
end;
coherence by INT'iwa;
func gt(t1,t2) -> INT-Expression of A,f means:
DEFgt2:
for s being Element of Funcs(X, INT) holds it.s = IFGT(t1.s,t2.s,1,0);
coherence by INT'iwa;
compatibility
proof
let ti be INT-Expression of A,f;
A1: dom gt(t1,t2) = (dom t1)/\dom t2 & dom t1 = Funcs(X, INT) &
dom t2 = Funcs(X, INT) & dom ti = Funcs(X, INT) by DEFgt,FUNCT_2:def 1;
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 DEFgt;
assume
for s being Element of Funcs(X, INT) holds ti.s = IFGT(t1.s,t2.s,1,0); then
for s being set st s in Funcs(X, INT) holds ti.s = IFGT(t1.s,t2.s,1,0);
hence ti = gt(t1,t2) by A1,DEFgt;
end;
end;
definition redefine
let A,X,T,f;
let t1,t2 be INT-Expression of A,f;
func eq(t1,t2) -> INT-Expression of A,f means
for s being Element of Funcs(X, INT) holds it.s = IFEQ(t1.s,t2.s,1,0);
compatibility
proof
let ti be INT-Expression of A,f;
A1: dom eq(t1,t2) = (dom t1)/\dom t2 & dom t1 = Funcs(X, INT) &
dom t2 = Funcs(X, INT) & dom ti = Funcs(X, INT) by DEFeq,FUNCT_2:def 1;
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 DEFeq;
assume
for s being Element of Funcs(X, INT) holds ti.s = IFEQ(t1.s,t2.s,1,0); then
for s being set st s in Funcs(X, INT) holds ti.s = IFEQ(t1.s,t2.s,1,0);
hence ti = eq(t1,t2) by A1,DEFeq;
end;
coherence
proof
reconsider l1 = leq(t1,t2), l2 = leq(t2,t1) as INT-Expression of A,f;
A1: dom eq(t1,t2) = Funcs(X,INT) by FUNCT_2:def 1;
A2: dom (l1(#)l2) = Funcs(X,INT) by FUNCT_2:def 1;
now let a be set; assume a in Funcs(X,INT); then
reconsider s = a as Element of Funcs(X,INT);
A3: eq(t1,t2).s = IFEQ(t1.s,t2.s,1,0) by A1,DEFeq;
A4: l2.s = IFGT(t2.s,t1.s,0,1) & l1.s = IFGT(t1.s,t2.s,0,1) by DEFleq2;
A5: (l1(#)l2).s = (l1.s)*(l2.s) by A2,VALUED_1:def 4;
t1.s = t2.s or t1.s < t2.s or t2.s < t1.s by XXREAL_0:1; 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 A3,A4,FUNCOP_1:def 8,XXREAL_0:def 10;
hence eq(t1,t2).a = (l1(#)l2).a by A5;
end;
hence thesis by A1,A2,FUNCT_1:9;
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 INT'iwa;
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 INT'iwa;
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 ThE1:
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 DEFvarexp .= s.x by FUNCOP_1:13;
end;
definition
let A,X,T,f;
let i be integer number;
func .(i,A,f) -> INT-Expression of A,f equals .(i,X);
coherence by INT'iwa;
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 choose {I where I is Element of A:
I in ElementaryInstructions A &
for s being Element of Funcs(X, INT) holds f.(s,I) = s+*(v.s,t.s)};
coherence
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 INT'iwa; then
consider I0 being Element of A such that
A0: I0 in ElementaryInstructions A and
A1: for s being Element of Funcs(X, INT) holds f.(s,I0) = s+*(v.s,t.s) by FA;
A2: Y c= the carrier of A
proof let i be set;
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;
I0 in Y by A0,A1; then
choose Y in Y;
hence thesis by A2;
end;
end;
theorem Th99:
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;
v,t form_assignment_wrt f by INT'iwa; then
consider I0 being Element of A such that
A0: I0 in ElementaryInstructions A and
A1: for s being Element of Funcs(X, INT) holds f.(s,I0) = s+*(v.s,t.s) by FA;
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)};
I0 in Y by A0,A1; 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 Th99,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 number;
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 number;
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 number;
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 number;
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 number;
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, x,y,z for (Element of X),
s,s' 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,j,k for integer number;
theorem Th100:
f.(s, v:=t).(v.s) = t.s &
for z st z <> v.s holds f.(s, v:=t).z = s.z
proof
v,t form_assignment_wrt f by INT'iwa; then
consider I0 being Element of A such that
A0: I0 in ElementaryInstructions A and
A1: for s being Element of Funcs(X, INT) holds f.(s,I0) = s+*(v.s,t.s) by FA;
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)};
I0 in Y by A0,A1; then
v:=t in Y; then
consider I being Element of A such that
A2: v:=t = I and I in ElementaryInstructions A and
A3: for s being Element of Funcs(X, INT) holds f.(s,I) = s+*(v.s,t.s);
A4: f.(s, v:=t) = s+*(v.s,t.s) by A2,A3;
dom s = X by FUNCT_2:def 1;
hence thesis by A4,FUNCT_7:33,34;
end;
theorem Th011:
for x being Variable of f
for i being integer number 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 number;
x:=i = ^x:=.(i,A,f) & (^x).s = x & .(i,A,f).s = i by FUNCOP_1:13;
hence thesis by Th100;
end;
theorem Th111:
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:=t = ^x:=t & (^x).s = x by FUNCOP_1:13;
hence thesis by Th100;
end;
theorem Th211:
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;
x:=y = x:=.y & (.y).s = s.y by ThE1;
hence thesis by Th111;
end;
theorem Th012:
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;
x+=i = x:=(.x+i) & x:=(.x+i) = ^x:=(.x+i) & .x = .(^x) &
(^x).s = x & (.x+i).s = ((.x).s+i) &
.(^(x qua Element of X)).s = s.((^(x qua Element of X)).s)
by DEFvarexp,DEFplus2,FUNCOP_1:13;
hence thesis by Th100;
end;
theorem Th112:
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;
00: dom (.x+t) = Funcs(X, INT) by FUNCT_2:def 1;
x+=t = x:=(.x+t) & (^x).s = x & (.x+t).s = (.x).s+t.s & (.x).s = s.x
by 00,ThE1,FUNCOP_1:13,VALUED_1:def 1;
hence thesis by Th100;
end;
theorem Th212:
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;
x+=y = x+=.y & (.y).s = s.y by ThE1;
hence thesis by Th112;
end;
theorem Th013:
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;
x*=i = x:=(.x*i) & x:=(.x*i) = ^x:=(.x*i) & .x = .(^x) &
(^x).s = x & (.x*i).s = ((.x).s*i) &
.(^(x qua Element of X)).s = s.((^(x qua Element of X)).s)
by DEFvarexp,DEFmult2,FUNCOP_1:13;
hence thesis by Th100;
end;
theorem Th113:
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;
00: dom (.x(#)t) = Funcs(X, INT) by FUNCT_2:def 1;
x*=t = x:=(.x(#)t) & (^x).s = x & (.x(#)t).s = (.x).s*t.s & (.x).s = s.x
by 00,ThE1,FUNCOP_1:13,VALUED_1:def 4;
hence thesis by Th100;
end;
theorem Th213:
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;
01: dom (.x(#).y) = Funcs(X, INT) by FUNCT_2:def 1;
(^x).s = x by FUNCOP_1:13;
hence f.(s, x*=y).x = (.x(#).y).s by Th100
.= ((.x).s)*(.y.s) by 01,VALUED_1:def 4 .= (s.x)*(.y.s) by ThE1
.= (s.x)*(s.y) by ThE1;
thus thesis by Th111;
end;
theorem Th014:
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 number holds
(s.x <= i implies g.(s, x leq i).b = 1) &
(s.x > i implies g.(s, x leq i).b = 0) &
(s.x >= i implies g.(s, x geq i).b = 1) &
(s.x < i implies g.(s, x geq i).b = 0) &
for z 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);
let x be Variable of f;
let i be integer number;
reconsider b' = b as Variable of f by ELEM;
reconsider x' = x as Element of X;
set v = ^b';
set t = leq(.x,.(i,A,f));
04: (.(i,A,f)).s = i by FUNCOP_1:13;
(.x).s = s.((^x).s) & ^x = Funcs(X,INT) --> x by DEFvarexp; then
01: s.x = (.x).s & v.s = b by FUNCOP_1:13;
02: (.x).s <= i implies IFGT((.x).s,i,0,1) = 1 by XXREAL_0:def 10;
03: (.x).s > i implies IFGT((.x).s,i,0,1) = 0 by XXREAL_0:def 10;
05: (.x).s >= i implies IFGT(i,(.x).s,0,1) = 1 by XXREAL_0:def 10;
06: (.x).s < i implies IFGT(i,(.x).s,0,1) = 0 by XXREAL_0:def 10;
.x leq .(i,A,f) = v:=leq(.x,.(i,A,f)) &
leq(.x,.(i,A,f)).s = IFGT((.x).s,.(i,A,f).s,0,1) &
.x geq .(i,A,f) = v:=leq(.(i,A,f),.x) &
leq(.(i,A,f),.x).s = IFGT(.(i,A,f).s,(.x).s,0,1)
by DEFleq2;
hence thesis by 01,02,03,04,05,06,Th100;
end;
theorem Th114:
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);
let x,y be Variable of f;
reconsider b' = b as Variable of f by ELEM;
reconsider x' = x, y' = y as Element of X;
set v = ^b';
set t = leq(.x,.y);
(.x).s = s.((^x).s) & ^x = Funcs(X,INT) --> x &
(.y).s = s.((^y).s) & ^y = Funcs(X,INT) --> y by DEFvarexp; then
01: s.x = (.x).s & s.y = (.y).s & v.s = b by FUNCOP_1:13;
02: (.x).s <= .y.s implies IFGT((.x).s,(.y).s,0,1) = 1 by XXREAL_0:def 10;
03: (.x).s > .y.s implies IFGT((.x).s,(.y).s,0,1) = 0 by XXREAL_0:def 10;
.x leq .y = v:=leq(.x,.y) & leq(.x,.y).s = IFGT((.x).s,(.y).s,0,1)
by DEFleq2;
hence thesis by 01,02,03,Th100;
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 number 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 number;
g.(s, x leq i) in Funcs(X,INT)\(b,0) iff g.(s, x leq i).b <> 0 by LemTS;
hence (s.x <= i iff g.(s, x leq i) in Funcs(X,INT)\(b,0)) by Th014;
g.(s, x geq i) in Funcs(X,INT)\(b,0) iff g.(s, x geq i).b <> 0 by LemTS;
hence thesis by Th014;
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 LemTS;
hence (s.x <= s.y iff g.(s, x leq y) in Funcs(X,INT)\(b,0)) by Th114;
g.(s, x geq y) in Funcs(X,INT)\(b,0) iff g.(s, x geq y).b <> 0 by LemTS;
hence thesis by Th114;
end;
theorem Th015:
for b being Element of X
for g being Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0)
for x being Variable of g
for i being integer number holds
(s.x > i implies g.(s, x gt i).b = 1) &
(s.x <= i implies g.(s, x gt i).b = 0) &
(s.x < i implies g.(s, x lt i).b = 1) &
(s.x >= i implies g.(s, x lt i).b = 0) &
for z 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);
let x be Variable of f;
let i be integer number;
reconsider b' = b as Variable of f by ELEM;
reconsider x' = x as Element of X;
set v = ^b';
set t = gt(.x,.(i,A,f));
04: (.x).s = s.((^x).s) & ^x = Funcs(X,INT) --> x &
(.(i,A,f)).s = i by DEFvarexp,FUNCOP_1:13; then
01: s.x = (.x).s & v.s = b by FUNCOP_1:13;
02: (.x).s > i implies IFGT((.x).s,i,1,0) = 1 by XXREAL_0:def 10;
03: (.x).s <= i implies IFGT((.x).s,i,1,0) = 0 by XXREAL_0:def 10;
05: (.x).s < i implies IFGT(i,(.x).s,1,0) = 1 by XXREAL_0:def 10;
06: (.x).s >= i implies IFGT(i,(.x).s,1,0) = 0 by XXREAL_0:def 10;
.x gt .(i,A,f) = v:=gt(.x,.(i,A,f)) &
gt(.x,.(i,A,f)).s = IFGT((.x).s,(.(i,A,f)).s,1,0) &
.x lt .(i,A,f) = v:=gt(.(i,A,f),.x) &
gt(.(i,A,f),.x).s = IFGT((.(i,A,f)).s,(.x).s,1,0) by DEFgt2;
hence thesis by 01,02,03,04,05,06,Th100;
end;
theorem Th115:
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);
let x,y be Variable of f;
reconsider b' = b as Variable of f by ELEM;
reconsider x' = x, y' = y as Element of X;
set v = ^b';
set t = gt(.x,.y);
(.x).s = s.((^x).s) & ^x = Funcs(X,INT) --> x &
(.y).s = s.((^y).s) & ^y = Funcs(X,INT) --> y by DEFvarexp; then
01: s.x = (.x).s & s.y = (.y).s & v.s = b by FUNCOP_1:13;
02: (.x).s > .y.s implies IFGT((.x).s,(.y).s,1,0) = 1 by XXREAL_0:def 10;
03: (.x).s <= .y.s implies IFGT((.x).s,(.y).s,1,0) = 0 by XXREAL_0:def 10;
04: (.x).s < .y.s implies IFGT((.y).s,(.x).s,1,0) = 1 by XXREAL_0:def 10;
05: (.x).s >= .y.s implies IFGT((.y).s,(.x).s,1,0) = 0 by XXREAL_0:def 10;
.x gt .y = v:=gt(.x,.y) & gt(.x,.y).s = IFGT((.x).s,(.y).s,1,0) &
.x lt .y = v:=gt(.y,.x) & gt(.y,.x).s = IFGT((.y).s,(.x).s,1,0)
by DEFgt2;
hence thesis by 01,02,03,04,05,Th100;
end;
theorem Th015':
for b being Element of X
for g being Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0)
for x being Variable of g
for i being integer number holds
(s.x > i 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 number;
g.(s, x gt i) in Funcs(X,INT)\(b,0) iff g.(s, x gt i).b <> 0 by LemTS;
hence (s.x > i iff g.(s, x gt i) in Funcs(X,INT)\(b,0)) by Th015;
g.(s, x lt i) in Funcs(X,INT)\(b,0) iff g.(s, x lt i).b <> 0 by LemTS;
hence thesis by Th015;
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 LemTS;
hence (s.x > s.y iff g.(s, x gt y) in Funcs(X,INT)\(b,0)) by Th115;
g.(s, x lt y) in Funcs(X,INT)\(b,0) iff g.(s, x lt y).b <> 0 by LemTS;
hence thesis by Th115;
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;
x%=i = ^x:=(.x mod .(i,A,f)) & .(i,A,f).s = i & .x = .(^x) &
(^x).s = x & (.x mod .(i,A,f)).s = (.x).s mod (.(i,A,f).s) &
.(^(x qua Element of X)).s = s.((^(x qua Element of X)).s)
by DEFvarexp,DEFmod2,FUNCOP_1:13;
hence thesis by Th100;
end;
theorem Th116:
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;
x%=t = x:=(.x mod t) & (^x).s = x & (.x mod t).s = (.x).s mod t.s &
(.x).s = s.x by ThE1,DEFmod2,FUNCOP_1:13;
hence thesis by Th100;
end;
theorem Th216:
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;
x%=y = x%=.y & (.y).s = s.y by ThE1;
hence thesis by Th116;
end;
theorem Th017:
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;
x/=i = ^x:=(.x div .(i,A,f)) & .(i,A,f).s = i & .x = .(^x) &
(^x).s = x & (.x div .(i,A,f)).s = (.x).s div (.(i,A,f).s) &
.(^(x qua Element of X)).s = s.((^(x qua Element of X)).s)
by DEFvarexp,DEFdiv2,FUNCOP_1:13;
hence thesis by Th100;
end;
theorem Th117:
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;
x/=t = x:=(.x div t) & (^x).s = x & (.x div t).s = (.x).s div t.s &
(.x).s = s.x by ThE1,DEFdiv2,FUNCOP_1:13;
hence thesis by Th100;
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;
x/=y = x/=.y & (.y).s = s.y by ThE1;
hence thesis by Th117;
end;
theorem Th118:
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);
reconsider y = b as Variable of f by ELEM;
let t be INT-Expression of A,f;
.(2,A,f).s = 2 & dom(t+1) = Funcs(X,INT) by FUNCT_2:def 1,FUNCOP_1:13; then
t is_odd = y:=(t mod .(2,A,f)) & (t mod .(2,A,f)).s = (t.s) mod 2 &
t is_even = y:=((t+1) mod .(2,A,f)) & (t+1).s = 1+(t.s) &
((t+1) mod .(2,A,f)).s = ((t+1).s) mod 2 by DEFmod2,VALUED_1:def 2;
hence thesis by Th111;
end;
theorem Th218:
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 is_odd = .x is_odd & (.x).s = s.x by ThE1;
hence thesis by Th118;
end;
LemMod:
for i,j being integer number holds
(i is even iff j is even) iff i+j is even
proof
let i,j be integer number;
i is even or i is odd; then
consider i0 being even Integer, i1 being odd Integer such that
A: i = i0 or i = i1;
j is even or j is odd; then
consider j0 being even Integer, j1 being odd Integer such that
B: j = j0 or j = j1;
i0+j0 is even & i0+j1 is odd & i1+j0 is odd & i1+j1 is even;
hence thesis by A,B;
end;
theorem Th318:
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;
01: f.(s, t is_odd).b = (t.s) mod 2 & f.(s, t is_even).b = (t.s+1) mod 2
by Th118;
02: (t.s) mod 2 = 0 or (t.s) mod 2 = 1 by PRE_FF:6;
03: t.s = ((t.s) div 2)*2 + ((t.s) mod 2) by INT_1:86;
04: ((t.s) div 2)*2 is even & ((t.s) div 2)*2 + 1 is odd;
thus (t.s is odd iff f.(s, t is_odd) in Funcs(X,INT)\(b,0))
by 01, 02, 03, 04, LemTS;
02: (t.s+1) mod 2 = 0 or (t.s+1) mod 2 = 1 by PRE_FF:6;
03: t.s+1 = ((t.s+1) div 2)*2 + ((t.s+1) mod 2) by INT_1:86;
thus thesis by 01, 02, 03, JORDAN12:3, LemMod, LemTS;
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 is_odd = .x is_odd & (.x).s = s.x by ThE1;
hence thesis by Th318;
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
F: F() = for-do(i():=a(), i() leq n(), i()+=1, I()) and
A: P[g().(s(),i():=a())] and
B: 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
C: 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
D: n() <> i() & n() <> b() & i() <> b()
proof
set S = Funcs(X(),INT);
set T = S\(b(),0);
set C = i() leq n();
set II = I()\;i()+=1;
Z0: g() is complying_with_catenation & g() complies_with_while_wrt T
by AOFA_000:def 32;
reconsider s1 = g().(s(),i():=a()) as Element of S;
reconsider s2 = g().(s1,C) as Element of S;
S1: s1.i() = a().s() & s1.n() = s().n() by D,Th111; then
S2: s2.i() = a().s() & s2.n() = s().n() by D,Th114;
Sn: g().(s(),F()) = g().(s1,while(C, II)) by F,AOFA_000:def 29;
defpred R[Element of S] means $1.i() <= $1.n();
defpred Q[Element of S] means P[$1] &
(a().s() <= s().n() implies $1.i()-1 <= s().n()) &
$1.n() = s().n();
a().s()-1 < a().s() by XREAL_1:46; then
A1: Q[s1] by A,S1,XXREAL_0:2;
A2: P[s2] by B,A;
per cases;
suppose
C1: a().s() <= s().n(); then
B': s2.b() = 1 by S1,Th114;
defpred PR[Element of S] means P[$1] & R[$1];
BB: g().(s1,C) in T iff PR[g().(s1,C) qua Element of S] by A,B,C1,S2,B';
deffunc F(Element of S) = In($1.n()+1-$1.i(),NAT);
Ct: 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; assume
00: PR[s];
reconsider s' = g().(s,I()) as Element of S;
reconsider s'' = g().(s',i()+=1) as Element of S;
reconsider s''' = g().(s'',C) as Element of S;
01: g().(s,II\;C) = g().(g().(s,II),C) & s'' = g().(s,II)
by AOFA_000:def 29;
02: s'''.i() = s''.i() & s'''.n() = s''.n() &
(s''.i() > s''.n() implies s'''.b() = 0) &
(s''.i() <= s''.n() implies s'''.b() = 1) by D,Th114;
03: s'.i() = s.i() & s'.n() = s.n() by C,00;
04: s''.i() = s'.i()+1 & s''.n() = s'.n() & P[s''] by 00,01,B,D,Th012;
hence (PR[g().(s,II\;C) qua Element of S] iff g().(s,II\;C) in T)
by 01,02,B,LemTS;
reconsider j = s.n()-s.i() as Element of NAT by 00,INT_1:18;
F(s''') = j by 02,03,04,FUNCT_7:def 1; then
F(s''')+1 = F(s) by FUNCT_7:def 1;
hence F(g().(s,II\;C) qua Element of S) < F(s) by 01,NAT_1:13;
end;
C': g() iteration_terminates_for II\;C, g().(s1,C)
from AOFA_000:sch 3(BB,Ct);
D': 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
01: Q[s] & s in T & R[s];
thus P[g().(s,II)] by B,01;
reconsider s' = g().(s,I()) as Element of S;
reconsider s'' = g().(s',i()+=1) as Element of S;
03: s'.i() = s.i() & s'.n() = s.n() &
s''.i() = s'.i()+1 & s''.n() = s'.n() by 01,C,D,Th012;
s'' = g().(s,II) by AOFA_000:def 29;
hence thesis by 01,03;
end;
E': 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; assume
01: Q[s];
hence P[g().(s,C)] by B;
g().(s,C).i() = s.i() & g().(s,C).n() = s.n() &
(s.i() > s.n() implies g().(s,C).b() = 0) &
(s.i() <= s.n() implies g().(s,C).b() = 1) by D,Th114;
hence thesis by 01,LemTS;
end;
F': 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(A1,C',D',E'); then
(g().(s(),F()) qua Element of S).i() >= s().n()+1 by Sn,INT_1:20; then
(g().(s(),F()) qua Element of S).i()-1 >= s().n()+1-1 by XREAL_1:15; then
(g().(s(),F()) qua Element of S).i()-1 = s().n() by C1,Sn,F',XXREAL_0:1;
hence thesis by C1,F,F',AOFA_000:def 29;
end;
suppose
C2: a().s() > s().n(); then
s2.b() = 0 by S1,Th114; then
s2 nin T by LemTS;
hence thesis by A2,C2,S2,Sn,Z0,AOFA_000:def 31;
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
F: F() = for-do(i():=a(),.n() leq .i(),i()+=-1,I()) and
A: P[f().(s(),i():=a())] and
B: 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
C: 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
D: n() <> i() & n() <> b() & i() <> b()
proof
set S = Funcs(X(),INT);
set T = S\(b(),0);
set C = n() leq i();
set II = I()\;i()+=-1;
Z0: f() is complying_with_catenation & f() complies_with_while_wrt T
by AOFA_000:def 32;
reconsider s1 = f().(s(),i():=a()) as Element of S;
reconsider s2 = f().(s1,C) as Element of S;
S1: s1.i() = a().s() & s1.n() = s().n() by D,Th111; then
S2: s2.i() = a().s() & s2.n() = s().n() by D,Th114;
Sn: f().(s(),F()) = f().(s1,while(C, II)) by F,AOFA_000:def 29;
defpred R[Element of S] means $1.i() >= $1.n();
defpred Q[Element of S] means P[$1] &
(a().s() >= s().n() implies $1.i()+1 >= s().n()) &
$1.n() = s().n();
A1: Q[s1] by A,S1,XREAL_1:41;
A2: P[s2] by B,A;
per cases;
suppose
C1: a().s() >= s().n(); then
B': s2.b() = 1 by S1,Th114;
defpred PR[Element of S] means P[$1] & R[$1];
BB: f().(s1,C) in T iff PR[f().(s1,C) qua Element of S] by B',A,B,C1,S2;
deffunc F(Element of S) = In($1.i()+1-$1.n(),NAT);
Ct: 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; assume
00: PR[s];
reconsider s' = f().(s,I()) as Element of S;
reconsider s'' = f().(s',i()+=-1) as Element of S;
reconsider s''' = f().(s'',C) as Element of S;
01: f().(s,II\;C) = f().(f().(s,II),C) & s'' = f().(s,II)
by AOFA_000:def 29;
02: s'''.i() = s''.i() & s'''.n() = s''.n() &
(s''.i() < s''.n() implies s'''.b() = 0) &
(s''.i() >= s''.n() implies s'''.b() = 1) by D,Th114;
03: s'.i() = s.i() & s'.n() = s.n() by C,00;
04: s''.i() = s'.i()-1 & s''.n() = s'.n() & P[s''] by 00,01,B,D,Th012;
hence (PR[f().(s,II\;C) qua Element of S] iff f().(s,II\;C) in T)
by 01,02,B,LemTS;
reconsider j = s.i()-s.n() as Element of NAT by 00,INT_1:18;
F(s''') = j by 02,03,04,FUNCT_7:def 1; then
F(s''')+1 = F(s) by FUNCT_7:def 1;
hence F(f().(s,II\;C) qua Element of S) < F(s) by 01,NAT_1:13;
end;
C': f() iteration_terminates_for II\;C, f().(s1,C)
from AOFA_000:sch 3(BB,Ct);
D': 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
01: Q[s] & s in T & R[s];
thus P[f().(s,II)] by 01,B;
reconsider s'' = f().(s,I()) as Element of S;
reconsider s''' = f().(s'',i()+=-1) as Element of S;
03: s''.i() = s.i() & s''.n() = s.n() &
s'''.i() = s''.i()-1 & s'''.n() = s''.n() by 01,C,D,Th012;
s''' = f().(s,II) by AOFA_000:def 29;
hence thesis by 01,03;
end;
E': 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; assume
01: Q[s];
hence P[f().(s,C)] by B;
f().(s,C).i() = s.i() & f().(s,C).n() = s.n() &
(s.i() < s.n() implies f().(s,C).b() = 0) &
(s.i() >= s.n() implies f().(s,C).b() = 1) by D,Th114;
hence thesis by 01,LemTS;
end;
F': 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(A1,C',D',E'); then
(f().(s(),F())qua Element of S).i()+1 <= s().n()+1-1 by Sn,INT_1:20; then
(f().(s(),F()) qua Element of S).i()+1 = s().n() by C1,Sn,F',XXREAL_0:1;
hence thesis by C1,F',F,AOFA_000:def 29;
end;
suppose
C2: a().s() < s().n(); then
s2.b() = 0 by S1,Th114; then
s2 nin T by LemTS;
hence thesis by A2,C2,S2,Sn,Z0,AOFA_000:def 31;
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 ThT1:
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
A0: d.b = 0 & d.n = 1 & d.i = 2;
D1: b <> i & b <> n & i <> n by A0;
assume
00: for s holds g.(s,I).n = s.n & g.(s,I).i = s.i;
set h = g;
set S = Funcs(X, INT);
set T = S\(b,0);
set C = i leq n;
set J = i+=1;
reconsider s1 = h.(s, C) as Element of S;
defpred R[Element of S] means $1.i <= $1.n;
deffunc F(Element of S) = In($1.n+1-$1.i, NAT);
(s.i > s.n implies s1.b = 0) & (s.i > s.n or s.i <= s.n) & s1.i = s.i &
s1.n = s.n & (s.i <= s.n implies s1.b = 1) by A0,Th114; then
AB: s1 in T iff R[s1] by LemTS;
C: 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; assume
R[s]; then
reconsider ni = s.n-s.i as Element of NAT by INT_1:16,XREAL_1:50;
set s1 = h.(s, I);
set q = h.(s, I\;J);
set q1 = h.(q, C);
01: (q.i > q.n implies q1.b = 0) & (q.i > q.n or q.i <= q.n) & q1.i = q.i &
q1.n = q.n & (q.i <= q.n implies q1.b = 1) by A0,Th114;
02: q = h.(s1, J) & q1 = h.(s, I\;J\;C) by AOFA_000:def 29;
hence R[h.(s,I\;J\;C) qua Element of S] iff h.(s,I\;J\;C) in T
by 01,LemTS;
s1.i = s.i & s1.n = s.n by 00; then
q.i = s.i+1 & q.n = s.n by 02,D1,Th012; then
q1.i = s.i+1 & q1.n = s.n by A0,Th114; then
F(q1 qua Element of S) = ni & F(s) = ni+1 by FUNCT_7:def 1;
hence F(h.(s,I\;J\;C) qua Element of S) < F(s) by 02,NAT_1:13;
end;
h iteration_terminates_for I\;J\;C, s1 from AOFA_000:sch 3(AB,C);
hence thesis;
end;
theorem ThT12:
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
D0: d.b = 0 & d.n = 1 & d.i = 2;
D1: b <> i & b <> n & i <> n by D0;
assume that
00: 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
A0: s in P;
set h = g;
set S = Funcs(X, INT);
set T = S\(b,0);
set C = i leq n;
set J = i+=1;
reconsider s1 = h.(s, C) as Element of S;
defpred P[Element of S] means $1 in P;
defpred R[Element of S] means $1.i <= $1.n;
deffunc F(Element of S) = In($1.n+1-$1.i, NAT);
AA: P[s1] by A0,00;
(s.i > s.n implies s1.b = 0) & (s.i > s.n or s.i <= s.n) & s1.i = s.i &
s1.n = s.n & (s.i <= s.n implies s1.b = 1) by D0,Th114; then
AB: s1 in T iff R[s1] by LemTS;
C: 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
01: P[s] & s in T & R[s]; then
reconsider ni = s.n-s.i as Element of NAT by INT_1:16,XREAL_1:50;
set s1 = h.(s, I);
set q = h.(s, I\;J);
set q1 = h.(q, C);
03: (q.i > q.n implies q1.b = 0) & (q.i > q.n or q.i <= q.n) & q1.i = q.i &
q1.n = q.n & (q.i <= q.n implies q1.b = 1) by D0,Th114;
02: q = h.(s1, J) & q1 = h.(s, I\;J\;C) by AOFA_000:def 29;
P[s1 qua Element of S] by 01,00; then
P[q qua Element of S] by 00,02;
hence P[h.(s,I\;J\;C) qua Element of S] by 00,02;
thus R[h.(s,I\;J\;C) qua Element of S] iff h.(s,I\;J\;C) in T
by 02,03,LemTS;
s1.i = s.i & s1.n = s.n by 01,00; then
q.i = s.i+1 & q.n = s.n by 02,D1,Th012; then
q1.i = s.i+1 & q1.n = s.n by D0,Th114; then
F(q1 qua Element of S) = ni & F(s) = ni+1 by FUNCT_7:def 1;
hence F(h.(s,I\;J\;C) qua Element of S) < F(s) by 02,NAT_1:13;
end;
h iteration_terminates_for I\;J\;C, s1 from AOFA_000:sch 4(AA,AB,C);
hence thesis;
end;
theorem ThT4:
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
A0: I is_terminating_wrt g;
let i,n be Variable of g;
given d being Function such that
00: d.b = 0 & d.n = 1 & d.i = 2;
assume
01: for s holds g.(s,I).n = s.n & g.(s,I).i = s.i;
let s;
set P = for-do(i:=t, i leq n, i+=1, I);
02: g iteration_terminates_for I\; i+=1\; i leq n, g.(g.(s, i:=t), i leq n)
by 00,01,ThT1;
set Q = while(i leq n, I\; i+=1);
04: i+=1 is_terminating_wrt g & i leq n is_terminating_wrt g
by AOFA_000:104; then
I\; i+=1 is_terminating_wrt g by A0,AOFA_000:110; then
03: [g.(s, i:=t), Q] in TerminatingPrograms(A,S,T,g) by 02,04,AOFA_000:114;
P = i:=t\; Q & [s, i:=t] in TerminatingPrograms(A,S,T,g)
by AOFA_000:def 36;
hence [s, P] in TerminatingPrograms(A,S,T,g) by 03,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
00: I is_terminating_wrt g, S;
let i,n be Variable of g;
given d being Function such that
01: d.b = 0 & d.n = 1 & d.i = 2;
assume that
02: for s st s in S holds g.(s,I).n = s.n & g.(s,I).i = s.i and
04: S is_invariant_wrt i:=t, g & S is_invariant_wrt I, g &
S is_invariant_wrt i leq n, g & S is_invariant_wrt i+=1, g;
let s; assume
s in S; then
03: g.(s, i:=t) in S by 04,AOFA_000:def 39;
set P = for-do(i:=t, i leq n, i+=1, I);
set C = i leq n, J = I\; i+=1;
set Q = while(C, J);
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 02,04,AOFA_000:def 39; then
06: g iteration_terminates_for J\; C, g.(g.(s, i:=t), C) by 01,03,ThT12;
07: i+=1 is_terminating_wrt g, S & C is_terminating_wrt g
by AOFA_000:104,107; then
09: S is_invariant_wrt J, g & J is_terminating_wrt g, S
by 00,04,AOFA_000:109,111; then
for s st s in S & g.(g.(s, J), C) in T holds g.(s,J) in S
by AOFA_000:def 39; then
08: [g.(s, i:=t), Q] in TerminatingPrograms(A,Z,T,g)
by 03,04,06,07,09,AOFA_000:116;
P = i:=t\; Q & [s, i:=t] in TerminatingPrograms(A,Z,T,g)
by AOFA_000:def 36;
hence [s, P] in TerminatingPrograms(A,Z,T,g) by 08,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);
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
00: d.n = 1 & d.s = 2 & d.i = 3 & d.b = 4;
D1: s <> i & s <> n & i <> n & b <> i & n <> b by 00;
set t = .(2,A,g);
let q be Element of S;
01: s*=i is_terminating_wrt g by AOFA_000:104;
02: [q,s:=1] in TerminatingPrograms(A,S,T,g) by AOFA_000:def 36;
03: for q be Element of S holds g.(q,s*=i).n = q.n & g.(q,s*=i).i = q.i
by D1,Th213;
ex d' being Function st d'.b = 0 & d'.n = 1 & d'.i = 2 by D1,Lem3; then
for-do(i:=t, i leq n, i+=1, s*=i) is_terminating_wrt g by 01,03,ThT4; then
[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) by AOFA_000:def 37;
hence thesis by 02,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 natural number 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
A0: d.n = 1 & d.s = 2 & d.i = 3 & d.b = 4;
let q be Element of Funcs(X, INT);
let N be natural number;
assume
A1: N = q.n;
set S = Funcs(X,INT);
set T = S\(b,0);
reconsider q1 = f.(q, s:=1) as Element of S;
reconsider q2 = f.(q1, i:=2) as Element of S;
set I = s*=i;
reconsider a = .(2,A,f) as INT-Expression of A,g;
reconsider F = for-do(i:=a, i leq n, i+=1, I) as Element of A;
defpred P[Element of S] means
ex K being natural number st K = $1.i-1 & $1.s = K!;
F: F = for-do(i:=a, i leq n, i+=1, I);
A2: s <> n & s <> i & s <> b by A0;
D: n <> i & n <> b & i <> b by A0;
Q1: q1.n = q.n & q1.s = 1 & q.n+1-1 = q.n by A2,Th011;
Q2: q2.n = q1.n & q2.s = q1.s & q2.i = 2 & 2-1 = 1 by A2,D,Th011;
A: P[f.(q1,i:=a)] by Q1,Q2,NEWTON:19;
C: 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 A2,Th113;
B: 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 natural number such that
A3: Ki = q.i-1 & q.s = Ki!;
reconsider q3 = f.(q,I) as Element of S;
reconsider q4 = f.(q3,i+=1) as Element of S;
reconsider q' = f.(q, i leq n) as Element of S;
A4: q4 = f.(q,I\;i+=1) by AOFA_000:def 29;
q3.i = q.i & q3.s = q.s*q.i & q4.s = q3.s & q.i+1-1 = q.i &
q.i-1+1 = q.i & q4.i = q3.i+1
by A2,Th012,Th213; then
Ki+1 = q4.i-1 & q4.s = (Ki+1)! by A3,NEWTON:21;
hence P[f.(q,I\;i+=1) qua Element of S] by A4;
q'.s = q.s & q'.i = q.i by A2,D,Th114;
hence P[f.(q, i leq n) qua Element of S] by A3;
end;
E: 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(F,A,B,C,D);
M: a.q1 = 2 by FUNCOP_1:13;
thus f.(q, s:=1\;for-do(i:=2, i leq n, i+=1, s*=i)).s
= f.(q1, F).s by AOFA_000:def 29
.= N! by M,A1,Q1,E,NAT_1:27,NEWTON:18,19;
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
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
00: d.x = 0 & d.n = 1 & d.s = 2 & d.i = 3 & d.b = 4;
D1: s <> i & s <> n & i <> n & b <> i & n <> b by 00;
set t = .(1,A,g);
let q be Element of S;
01: s*=x is_terminating_wrt g by AOFA_000:104;
02: [q,s:=1] in TerminatingPrograms(A,S,T,g) by AOFA_000:def 36;
03: for q be Element of S holds g.(q,s*=x).n = q.n & g.(q,s*=x).i = q.i
by D1,Th213;
ex d' being Function st d'.b = 0 & d'.n = 1 & d'.i = 2 by D1,Lem3; then
for-do(i:=t, i leq n, i+=1, s*=x) is_terminating_wrt g by 01,03,ThT4; then
[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) by AOFA_000:def 37;
hence thesis by 02,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 natural number st N = q.n
holds g.(q, s:=1\;for-do(i:=1, i leq n, i+=1, s*=x)).s = (q.x)|^N
proof set f = g;
let x,n,s,i be Variable of f;
given d being Function such that
A0: d.x = 0 & d.n = 1 & d.s = 2 & d.i = 3 & d.b = 4;
let q be Element of Funcs(X, INT);
let N be natural number;
assume
A1: N = q.n;
set S = Funcs(X,INT);
set T = S\(b,0);
set q0 = q;
reconsider q1 = f.(q, s:=1) as Element of S;
reconsider q2 = f.(q1, i:=1) as Element of S;
set I = s*=x;
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;
defpred P[Element of S] means
ex K being natural number st K = $1.i-1 & $1.s = (q.x)|^K & $1.x = q.x;
F: F = for-do(i:=a, i leq n, i+=1, I);
A2: i <> x & b <> x & s <> x & s <> n & s <> i & s <> b by A0;
D: n <> i & n <> b & i <> b by A0;
Q1: q1.n = q.n & q1.s = 1 & q.n+1-1 = q.n & q1.x = q.x by A2,Th011;
Q2: q2.n = q1.n & q2.s = q1.s & q2.i = 1 & q2.x = q1. x & 1-1 = 0
by A2,D,Th011;
(q.x)|^0 = 1 by NEWTON:9; then
A: P[f.(q1,i:=a)] by Q1,Q2;
C: 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 A2,Th113;
B: 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 natural number such that
A3: Ki = q.i-1 & q.s = (q0.x)|^Ki & q.x = q0.x;
reconsider q3 = f.(q,I) as Element of S;
reconsider q4 = f.(q3,i+=1) as Element of S;
reconsider q' = f.(q, i leq n) as Element of S;
A4: q4 = f.(q,I\;i+=1) by AOFA_000:def 29;
A5: q3.i = q.i & q3.s = q.s*q.x & q4.s = q3.s & q.i+1-1 = q.i &
q3.x = q.x & q4.x = q3.x & q.i-1+1 = q.i & q4.i = q3.i+1
by A2,Th012,Th213; then
Ki+1 = q4.i-1 & q4.s = (q0.x)|^(Ki+1) by A3,NEWTON:11;
hence P[f.(q,I\;i+=1) qua Element of S] by A3,A4,A5;
q'.s = q.s & q'.i = q.i & q'.x = q.x by A2,D,Th114;
hence P[f.(q, i leq n) qua Element of S] by A3;
end;
E: 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(F,A,B,C,D);
N: N = 0 or N >= 1 by NAT_1:26;
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 A1,Q1,E,N,FUNCOP_1:13;
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
00: d.b = 0 & d.n = 1 & d.x = 2 & d.y = 3 & d.z = 4 & d.i = 5;
D1: i <> n & b <> i & n <> b by 00;
D2: i <> x & i <> y & i <> z & n <> x & n <> y & n <> z by 00;
let s;
set s2 = g.(s, x:=0\;y:=1);
set I1 = z:=x, I2 = x:=y, I3 = y+=z;
set I = z:=x\;x:=y\;y+=z;
01: I is_terminating_wrt g by AOFA_000:104;
02: [s, x:=0\;y:=1] in TerminatingPrograms(A,S,T,g) by AOFA_000:def 36;
03: 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 D2,Th212
.= g.(g.(q,I1),I2).n by AOFA_000:def 29
.= g.(q,I1).n by D2,Th211
.= q.n by D2,Th211;
thus g.(q,I).i
= g.(g.(q,I1\;I2),I3).i by AOFA_000:def 29
.= g.(q,I1\;I2).i by D2,Th212
.= g.(g.(q,I1),I2).i by AOFA_000:def 29
.= g.(q,I1).i by D2,Th211
.= q.i by D2,Th211;
end;
ex d' being Function st d'.b = 0 & d'.n = 1 & d'.i = 2 by D1,Lem3; then
for-do(i:=1, i leq n, i+=1, z:=x\;x:=y\;y+=z) is_terminating_wrt g
by 01,03,ThT4; then
[s2, for-do(i:=1, i leq n, i+=1, z:=x\;x:=y\;y+=z)] in
TerminatingPrograms(A,S,T,g) by AOFA_000:def 37;
hence [s,x:=0\;y:=1\;for-do(i:=1, i leq n, i+=1, z:=x\;x:=y\;y+=z)]
in TerminatingPrograms(A,S,T,g) by 02,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
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
A0: d.b = 0 & d.n = 1 & d.x = 2 & d.y = 3 & d.z = 4 & d.i = 5;
let s be Element of Funcs(X, INT);
let N be Element of NAT;
assume
A1: N = s.n;
reconsider s1 = g.(s, x:=0) as Element of S;
reconsider s2 = g.(s1, y:=1) as Element of S;
reconsider s3 = g.(s2, for-do(i:=1, i leq n, i+=1, z:=x\;x:=y\;y+=z))
as Element of S;
reconsider s4 = g.(s2, i:=1) as Element of S;
set I = z:=x\;x:=y\;y+=z;
reconsider a = .(1,A,g) as INT-Expression of A,g;
reconsider F = for-do(i:=a, i leq n, i+=1, I) as Element of A;
g.(s, x:=0\;y:=1) = s2 by AOFA_000:def 29; then
S0: g.(s, x:=0\;y:=1\;F) = s3 by AOFA_000:def 29;
D0: n <> x & i <> x & n <> y & i <> y & x <> y & i <> n & n <> z & i <> z &
x <> z & y <> z by A0; then
S1: s1.n = s.n & s1.x = 0 by Th011;
S2: s2.n = s1.n & s2.y = 1 & s2.x = s1.x by D0,Th011;
S3: s4.n = s2.n & s4.y = s2.y & s4.x = s2.x & s4.i = 1 by D0,Th011;
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);
F: F = for-do(i:=a,i leq n,i+=1,I);
1-1 = 0 & (0 qua Element of NAT)+1 = 1; then
A: P[g.(s2,i:=a)] by S1,S2,S3,PRE_FF:1;
Si: 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;
R1: s1.n = s.n & s1.x = s.x & s1.y = s.y & s1.z = s.x & s1.i = s.i
by D0,Th211;
R2: s2.n = s1.n & s2.x = s1.y & s2.y = s1.y & s2.z = s1.z & s2.i = s1.i
by D0,Th211;
R4: g.(s,I) = g.(g.(s, z:=x\;x:=y), y+=z) by AOFA_000:def 29
.= s3 by AOFA_000:def 29;
thus 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 R1,R2,D0,R4,Th212;
end;
B: 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
Q0: N = s.i-1 & s.x = Fib N & s.y = Fib(N+1);
reconsider s1 = g.(s,I) as Element of S;
reconsider s2 = g.(s1,i+=1) as Element of S;
Q1: s1.x = s.y & s1.y = s.x+s.y & s1.i = s.i by Si;
Q2: s2.x = s1.x & s2.y = s1.y & s2.i = s1.i+1 by D0,Th012;
thus P[g.(s,I\;i+=1) qua Element of S]
proof take N1 = N+1;
g.(s,I\;i+=1) = s2 & N1-1 = N by AOFA_000:def 29;
hence thesis by Q0,Q1,Q2,PRE_FF:1;
end;
take N;
thus thesis by Q0,A0,Th114;
end;
C: 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 Si;
D: n <> i & n <> b & i <> b by A0;
E: 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(F,A,B,C,D);
E2: 0 <= N & N <= 0 or N >= (0 qua Element of NAT)+1 by NAT_1:13;
a.s2 = 1 by FUNCOP_1:13;
hence thesis by A1,S0,D0,Th011,S2,E,E2,XXREAL_0:1;
end;
LemEAterm:
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 n = s.x & m = s.y & n > m &
(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
A0: d.b = 0 & d.x = 1 & d.y = 2 & d.z = 3;
D1: x <> y & y <> z & z <> x by A0;
set I = z:=x\;z%=y\;x:=y\;y:=z;
set C = y gt 0;
IT: 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;
00: 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;
01: s1.x = s.x & s1.y = s.y & s1.z = s.x by D1,Th211;
02: s2.x = s1.x & s2.y = s1.y & s2.z = s1.z mod s1.y by D1,Th216;
03: s3.x = s2.y & s3.y = s2.y & s3.z = s2.z by D1,Th211;
thus h.(s, I).x = s.y & h.(s, I).y = s.x mod s.y by 00,01,02,03,D1,Th211;
end;
let s be Element of Funcs(X, INT);
thus g.(s, I).x = s.y & h.(s, I).y = s.x mod s.y by IT;
let n,m be Element of NAT; assume
A1: n = s.x & m = s.y & n > m;
reconsider s1 = h.(s, C) as Element of S;
reconsider fin = h.(s, while(C,I)) as Element of S;
defpred R[Element of S] means $1.y > 0;
deffunc F(Element of S) = In($1.y, NAT);
defpred P[Element of S] means
n hcf m divides $1.x & n hcf m divides $1.y & $1.x > $1.y & $1.y >= 0;
defpred Q[Element of S] means
fin.x divides $1.x & fin.x divides $1.y;
assume s in T iff m > 0; then
AB: s in T iff R[s] by A1;
C: 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
00: s.y > 0;
reconsider s' = h.(s, I) as Element of S;
reconsider s'' = h.(s', C) as Element of S;
01: h.(s,I\;C) = s'' by AOFA_000:def 29;
02: s''.x = s'.x & s''.y = s'.y & (s'.y > 0 implies s''.b = 1) &
(s'.y <= 0 implies s''.b = 0) by A0,Th015;
hence (R[h.(s,I\;C) qua Element of S] iff h.(s,I\;C) in T) by 01,LemTS;
s'.y = s.x mod s.y by IT; then
03: 0 <= s'.y & s'.y < s.y by 00,NEWTON:78,79; then
F(s'') = s'.y & F(s) = s.y by 02,FUNCT_7:def 1,INT_1:16;
hence F(h.(s,I\;C) qua Element of S) < F(s) by 03,AOFA_000:def 29;
end;
h iteration_terminates_for I\;C, s from AOFA_000:sch 3(AB,C);
hence h iteration_terminates_for I\;C, s;
end;
theorem :: Termination 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
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
00: d.b = 0 & d.x = 1 & d.y = 2 & d.z = 3;
set C = y gt 0, I = z:=x\;z%=y\;x:=y\;y:=z;
01: P is_invariant_wrt C,g
proof
let s; assume s in P; then
A0: ex s' st s' = s & s'.x > s'.y & s'.y >= 0;
set s1 = g.(s,C);
s1.x = s.x & s1.y = s.y by 00,Th015;
hence thesis by A0;
end;
02: C is_terminating_wrt g & I is_terminating_wrt g,P by AOFA_000:104,107;
03: now
let s; assume s in P; then
ex s' st s' = s & s'.x > s'.y & s'.y >= 0; then
reconsider n = s.x, m = s.y as Element of NAT by INT_1:16;
assume g.(g.(s,I),C) in T; then
A2: g.(g.(s,I),C).b <> 0 & g.(s,I).y = s.x mod s.y & g.(s,I).x = s.y
by 00,LemTS,LemEAterm; then
A1: g.(s,I).y > 0 by Th015; then
m <> 0 by A2,INT_1:def 8; then
m > 0; then
g.(s,I).x > g.(s,I).y by A2,NEWTON:79;
hence g.(s,I) in P by A1;
end;
now let s; set s1 = g.(s,C);
assume g.(s,C) in P; then
A0: ex s' st s' = g.(s,C) & s'.x > s'.y & s'.y >= 0; then
reconsider n = s1.x, m = s1.y as Element of NAT by INT_1:16;
s1.x = s.x & s1.y = s.y & (s.y > 0 implies s1.b = 1) &
(s.y <= 0 implies s1.b = 0) by 00,Th015; then
n > m & (s1 in T iff m > 0) by A0,LemTS;
hence g iteration_terminates_for I\;C, g.(s,C) by 00,LemEAterm;
end;
hence while(y gt 0, z:=x\;z%=y\;x:=y\;y:=z) is_terminating_wrt g, P
by 01,02,03,AOFA_000: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 hcf 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
A0: d.b = 0 & d.x = 1 & d.y = 2 & d.z = 3;
let s be Element of Funcs(X, INT);
let n,m be Element of NAT; assume
A1: n = s.x & m = s.y & n > m;
set I = z:=x\;z%=y\;x:=y\;y:=z;
set C = y gt 0;
reconsider s1 = h.(s, C) as Element of S;
reconsider fin = h.(s, while(C,I)) as Element of S;
S1: s1.x = s.x & s1.y = s.y & (s.y > 0 implies s1.b = 1) &
(s.y <= 0 implies s1.b = 0) by A0,Th015;
defpred R[Element of S] means $1.y > 0;
deffunc F(Element of S) = In($1.y, NAT);
defpred P[Element of S] means
n hcf m divides $1.x & n hcf m divides $1.y & $1.x > $1.y & $1.y >= 0;
defpred Q[Element of S] means
fin.x divides $1.x & fin.x divides $1.y;
AB: s1 in T iff m > 0 by A1,S1,LemTS;
s1.x = s.x & s1.y = s.y by A0,Th015; then
II: h iteration_terminates_for I\;C, h.(s,C) by AB,A0,A1,LemEAterm;
IA: P[s] by A1,NAT_D:def 5;
ID: 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; assume
00: P[s];
reconsider n' = s.x, m' = s.y as Element of NAT by 00,INT_1:16;
assume
01: s in T & R[s];
reconsider s'' = h.(s, I) as Element of S;
04: s''.x = s.y & s''.y = s.x mod s.y by A0,LemEAterm;
n hcf m divides n' mod m' & s.x mod s.y = n' mod m'
by 00,NAT_D:11;
hence P[h.(s,I)] by 01,00,04,NEWTON:79;
end;
IE: 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
01: P[s];
reconsider s' = h.(s,C) as Element of S;
02: s'.x = s.x & s'.y = s.y & (s.y > 0 implies s'.b = 1) &
(s.y <= 0 implies s'.b = 0) by A0,Th015;
hence P[h.(s,C) qua Element of S] by 01;
thus thesis by 02,LemTS;
end;
08: 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(IA,II,ID,IE); then
n hcf m divides fin.x & fin.x > fin.y & fin.y = 0; then
cA: Q[h.(s,while(C,I)) qua Element of S] by INT_2:16;
cD: 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
00: Q[h.(h.(s,C),I) qua Element of S];
assume
01: h.(s,C) in T;
reconsider s1 = h.(s,C) as Element of S;
reconsider s2 = h.(s1,I) as Element of S;
02: s1.x = s.x & s1.y = s.y & (s.y > 0 implies s1.b = 1) &
(s.y <= 0 implies s1.b = 0) by A0,Th015;
03: s2.x = s1.y & s2.y = s1.x mod s1.y by A0,LemEAterm;
s.x = (s.x div s.y)*(s2.x)+s2.y*1 by 01,02,03,LemTS,NEWTON:80;
hence Q[h.(s,C) qua Element of S] by 00,02,A0,LemEAterm,WSIERP_1:10;
end;
cE: for s being Element of S st Q[h.(s,C) qua Element of S] holds Q[s]
by A0,Th015;
Q[s] from AOFA_000:sch 6(cA,II,cD,cE); then
fin.x divides n hcf m by A1,INT_2:33; then
fin.x = n hcf m or fin.x = -(n hcf m) by 08,INT_2:15;
hence h.(s, while(y gt 0, z:=x\;z%=y\;x:=y\;y:=z)).x = n hcf m by 08;
end;
LemEA2term:
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 = abs(s.x-s.y) &
for n,m being Element of NAT st n = s.x & m = s.y &
(s in Funcs(X, INT)\(b,0) 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
A0: d.b = 0 & d.x = 1 & d.y = 2 & d.z = 3;
D1: x <> y & y <> z & z <> x by A0;
Z0: g complies_with_if_wrt T & g complies_with_while_wrt T by AOFA_000:def 32;
set J = if-then(z lt 0, z*=-1);
set I = z:=(.x-.y)\; J\; x:=y\; y:=z;
set C = y gt 0;
IT: 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);
(s2.b = 0 implies s2 nin T) & (s2.b = 1 implies s2 in T) by LemTS; then
Q5: (s2.b = 0 implies q = s2) & (s2.b = 1 implies q = qz)
by Z0,AOFA_000:def 30,80;
02: s2.x = s1.x & s2.y = s1.y & s2.z = s1.z by A0,Th015;
04: (s1.z < 0 implies s2.b = 1) & (s1.z >= 0 implies s2.b = 0)
by Th015;
05: qz.x = s2.x & qz.y = s2.y & qz.z = (s2.z)*(-1) & (s2.z)*(-1) = -(s2.z)
by D1,Th013;
set s3 = g.(q, x:=y);
set s4 = g.(s3, y:=z);
00: 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;
(.x-.y).s = ((.x).s)-((.y).s) & (.x).s = s.x & (.y).s = s.y
by ThE1,DEFminus3; then
01: s1.x = s.x & s1.y = s.y & s1.z = (s.x)-(s.y) by D1,Th111;
03: s3.x = q.y & s3.y = q.y & s3.z = q.z by D1,Th211;
s4.x = s3.x & s4.y = s3.z by D1,Th211;
hence g.(s, I).x = s.y & g.(s, I).y = abs(s.x-s.y)
by 00,01,02,03,04,05,Q5,ABSVALUE:def 1;
end;
let s be Element of Funcs(X, INT);
thus g.(s, I).x = s.y & g.(s, I).y = abs(s.x-s.y) by IT;
let n,m be Element of NAT; assume
A1: n = s.x & m = s.y;
reconsider s1 = g.(s, C) as Element of S;
reconsider fin = g.(s, while(C,I)) as Element of S;
defpred R[Element of S] means $1.x >= 0 & $1.y > 0;
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 P[Element of S] means
n hcf m divides $1.x & n hcf 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 hcf m;
assume s in T iff m > 0; then
AB: s in T iff R[s] by A1;
C: 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
00: s.x >= 0 & s.y > 0;
reconsider s' = g.(s, I) as Element of S;
reconsider s'' = g.(s', C) as Element of S;
01: g.(s,I\;C) = s'' by AOFA_000:def 29;
02: s''.x = s'.x & s''.y = s'.y & (s'.y > 0 implies s''.b = 1) &
(s'.y <= 0 implies s''.b = 0) by A0,Th015;
04: s'.y = abs(s.x-s.y) & s'.x = s.y by IT;
thus R[g.(s,I\;C) qua Element of S] iff g.(s,I\;C) in T
by 00,01,02,LemTS,IT;
reconsider nx = s.x, ny = s.y, nn = s''.y as Element of NAT
by 00,04,A0,Th015,INT_1:16;
(max(2*ny,2*nn+1) = 2*ny or max(2*ny,2*nn+1) = 2*nn+1)
by XXREAL_0:16; then
03: F(s'') = IFEQ(nn,0,0, IFEQ(ny,0,2, IFEQ(ny,nn,1,max(2*ny,2*nn+1))))
by 02,04,FUNCT_7:def 1;
(max(2*nx,2*ny+1) = 2*nx or max(2*nx,2*ny+1) = 2*ny+1)
by XXREAL_0:16; then
03': F(s) = IFEQ(ny,0,0, IFEQ(nx,0,2, IFEQ(nx,ny,1,max(2*nx,2*ny+1))))
by FUNCT_7:def 1
.= IFEQ(nx,0,2, IFEQ(nx,ny,1,max(2*nx,2*ny+1))) by 00,FUNCOP_1:def 8;
2*ny+1 > 2*ny by NAT_1:13; then
05: max(2*nx,2*ny+1) > 2*ny by XXREAL_0:30;
per cases by XXREAL_0:1;
suppose
07: nx = ny; then
06: nx-ny = 0 & F(s) = IFEQ(nx,ny,1,max(2*nx,2*ny+1)) &
IFEQ(nx,ny,1,max(2*nx,2*ny+1)) = 1
by 00,03',FUNCOP_1:def 8;
nn = 0 by 02,04,07,ABSVALUE:7;
hence F(g.(s,I\;C) qua Element of S) < F(s) by 01,06,FUNCOP_1:def 8;
end;
suppose nx > ny; then
06: nx-ny > 0 & nx > 0 & IFEQ(nx,ny,1,max(2*nx,2*ny+1)) = max(2*nx,2*ny+1)
by XREAL_1:52,FUNCOP_1:def 8; then
07: nn = nx-ny & F(s) = max(2*nx,2*ny+1)
by 03',FUNCOP_1:def 8; then
F(s'') = IFEQ(ny,0,2, IFEQ(ny,nn,1,max(2*ny,2*nn+1)))
by 03,06,FUNCOP_1:def 8
.= IFEQ(ny,nn,1,max(2*ny,2*nn+1)) by 00,FUNCOP_1:def 8; then
08: (ny = nn implies F(s'') = 1) &
(ny <> nn implies F(s'') = max(2*ny,2*nn+1)) by FUNCOP_1:def 8;
nn < nx by 00,07,XREAL_1:46; then
nn+1 <= nx by NAT_1:13; then
2*(nn+1) <= 2*nx & 2*(nn+1) = 2*nn+2*1 & 2*nn+2 = 2*nn+1+1
by XREAL_1:66; then
2*nn+1 < 2*nx by NAT_1:13; then
1 <= 2*nn+1 & 2*nn+1 < F(s) by 07,XXREAL_0:30,NAT_1:11;
hence F(g.(s,I\;C) qua Element of S) < F(s)
by 01,08,05,07,XXREAL_0:29,2;
end;
suppose
0A: nx < ny & nx > 0; then
nx-ny < 0 by XREAL_1:51; then
nn = -(nx-ny) & -(nx-ny) = ny-nx
by 04,02,ABSVALUE:def 1; then
0D: nn < ny & nn > 0 by 0A,XREAL_1:46,52; then
2*nn < 2*ny by XREAL_1:70; then
2*nn+1 < 2*ny+1 by XREAL_1:8; then
0B: 2*nn+1 < max(2*nx,2*ny+1) by XXREAL_0:30;
0C: F(s) = IFEQ(nx,ny,1,max(2*nx,2*ny+1)) by 03',0A,FUNCOP_1:def 8
.= max(2*nx,2*ny+1) by 0A,FUNCOP_1:def 8;
F(s'') = IFEQ(ny,0,2, IFEQ(ny,nn,1,max(2*ny,2*nn+1)))
by 03,0D,FUNCOP_1:def 8
.= IFEQ(ny,nn,1,max(2*ny,2*nn+1)) by 00,FUNCOP_1:def 8
.= max(2*ny,2*nn+1) by 0D,FUNCOP_1:def 8;
hence F(g.(s,I\;C) qua Element of S) < F(s) by 01,05,0B,0C,XXREAL_0:29;
end;
suppose
09: nx = 0; then
0A: F(s) = 2 by 03',FUNCOP_1:def 8;
nx-ny < 0 by 00,09,XREAL_1:51; then
0B: nn = -(nx-ny) by 04,02,ABSVALUE:def 1 .= ny by 09; then
F(s'') = IFEQ(ny,0,2, IFEQ(ny,nn,1,max(2*ny,2*nn+1)))
by 00,03,FUNCOP_1:def 8
.= IFEQ(ny,nn,1,max(2*ny,2*nn+1)) by 00,FUNCOP_1:def 8
.= 1 by 0B,FUNCOP_1:def 8;
hence F(g.(s,I\;C) qua Element of S) < F(s) by 01,0A;
end;
end;
g iteration_terminates_for I\;C, s from AOFA_000:sch 3(AB,C);
hence g iteration_terminates_for I\;C, s;
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
00: d.b = 0 & d.x = 1 & d.y = 2 & d.z = 3;
set C = y gt 0, I = z:=(.x-.y)\; if-then(z lt 0, z*=-1)\; x:=y\; y:=z;
01: P is_invariant_wrt C,g
proof
let s; assume s in P; then
A0: ex s' st s' = s & s'.x >= 0 & s'.y >= 0;
set s1 = g.(s,C);
s1.x = s.x & s1.y = s.y by 00,Th015;
hence thesis by A0;
end;
02: C is_terminating_wrt g & I is_terminating_wrt g,P by AOFA_000:104,107;
03: now
let s; assume s in P; then
ex s' st s' = s & s'.x >= 0 & s'.y >= 0; then
reconsider n = s.x, m = s.y as Element of NAT by INT_1:16;
assume g.(g.(s,I),C) in T; then
g.(g.(s,I),C).b <> 0 & g.(s,I).y = abs(s.x-s.y) & g.(s,I).x = m
by 00,LemTS,LemEA2term;
hence g.(s,I) in P;
end;
now let s; set s1 = g.(s,C);
assume g.(s,C) in P; then
ex s' st s' = g.(s,C) & s'.x >= 0 & s'.y >= 0; then
reconsider n = s1.x, m = s1.y as Element of NAT by INT_1:16;
s1.x = s.x & s1.y = s.y & (s.y > 0 implies s1.b = 1) &
(s.y <= 0 implies s1.b = 0) by 00,Th015; then
(s1 in T iff m > 0) & n = n by LemTS;
hence g iteration_terminates_for I\;C, g.(s,C) by 00,LemEA2term;
end;
hence while(y gt 0, z:=(.x-.y)\; if-then(z lt 0, z*=-1)\; x:=y\; y:=z)
is_terminating_wrt g, P by 01,02,03,AOFA_000: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 hcf m
proof set h = g;
set S = Funcs(X, INT);
set T = S\(b,0);
Z0: h complies_with_if_wrt T & h complies_with_while_wrt T by AOFA_000:def 32;
let x,y,z be Variable of h;
given d being Function such that
A0: d.b = 0 & d.x = 1 & d.y = 2 & d.z = 3;
let s be Element of Funcs(X, INT);
let n,m be Element of NAT; assume
A1: n = s.x & m = s.y & n > 0;
set J = if-then(z lt 0, z*=-1);
set I = z:=(.x-.y)\; J\; x:=y\; y:=z;
set C = y gt 0;
reconsider s1 = h.(s, C) as Element of S;
reconsider fin = h.(s, while(C,I)) as Element of S;
D1: x <> y & y <> z & z <> x by A0;
S1: s1.x = s.x & s1.y = s.y & (s.y > 0 implies s1.b = 1) &
(s.y <= 0 implies s1.b = 0) by A0,Th015;
defpred R[Element of S] means $1.x > 0 & $1.y > 0;
deffunc F(Element of S) = In(max(2*$1.x,2*$1.y+1), NAT);
defpred P[Element of S] means
n hcf m divides $1.x & n hcf 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 hcf m;
AB: s1 in T iff R[s1] by A1,S1,LemTS;
IT: 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);
(s2.b = 0 implies s2 nin T) & (s2.b = 1 implies s2 in T) by LemTS; then
Q5: (s2.b = 0 implies q = s2) & (s2.b = 1 implies q = qz)
by Z0,AOFA_000:def 30,80;
02: s2.x = s1.x & s2.y = s1.y & s2.z = s1.z by A0,Th015;
04: (s1.z < 0 implies s2.b = 1) & (s1.z >= 0 implies s2.b = 0)
by Th015;
05: qz.x = s2.x & qz.y = s2.y & qz.z = (s2.z)*(-1) & (s2.z)*(-1) = -(s2.z)
by D1,Th013;
set s3 = h.(q, x:=y);
set s4 = h.(s3, y:=z);
00: 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;
(.x-.y).s = ((.x).s)-((.y).s) & (.x).s = s.x & (.y).s = s.y
by ThE1,DEFminus3; then
01: s1.x = s.x & s1.y = s.y & s1.z = (s.x)-(s.y) by D1,Th111;
03: s3.x = q.y & s3.y = q.y & s3.z = q.z by D1,Th211;
s4.x = s3.x & s4.y = s3.z by D1,Th211;
hence h.(s, I).x = s.y & h.(s, I).y = abs(s.x-s.y)
by 00,01,02,03,04,05,Q5,ABSVALUE:def 1;
end;
II: h iteration_terminates_for I\;C, h.(s,C) by AB,A0,A1,S1,LemEA2term;
IA: P[s] by A1,NAT_D:def 5;
ID: 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; assume
00: P[s];
reconsider n' = s.x, m' = s.y as Element of NAT by 00,INT_1:16;
assume
01: s in T & R[s];
reconsider s'' = h.(s, I) as Element of S;
04: s''.x = s.y & s''.y = abs(s.x-s.y) by IT;
n hcf m divides n'-m' & abs(n hcf m) = n hcf m
by 00,PREPOWER:108,ABSVALUE:def 1;
hence n hcf m divides h.(s,I).x & n hcf m divides h.(s,I).y &
h.(s,I).x > 0 & h.(s,I).y >= 0 by 01,00,04,INT_2:21;
let c be Nat; reconsider c' = c as Element of NAT by ORDINAL1:def 13;
assume
05: c divides h.(s,I).x & c divides h.(s,I).y;
c' divides m' & c' divides abs(n'-m') & abs c = c
by 05,IT,ABSVALUE:def 1; then
c qua Integer divides m' & c divides n'-m' by INT_2:21; then
c divides (n'-m')+m' & (n'-m')+m' = n' by WSIERP_1:9;
hence c divides n hcf m by 00,04,05;
end;
IE: 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
01: P[s];
reconsider s' = h.(s,C) as Element of S;
02: s'.x = s.x & s'.y = s.y & (s.y > 0 implies s'.b = 1) &
(s.y <= 0 implies s'.b = 0) by A0,Th015;
hence P[h.(s,C) qua Element of S] by 01;
thus thesis by 01,02,LemTS;
end;
K: 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(IA,II,ID,IE); then
reconsider fn = fin.x as Element of NAT by INT_1:16;
now
thus n hcf m divides fn by K;
fn divides 0 & fin.y = 0 by K,NAT_D:6;
hence fn divides n hcf m by K;
end;
hence h.(s, while(y gt 0, I)).x = n hcf m by 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
A0: d.b = 0 & d.x = 1 & d.y = 2 & d.m = 3;
D0: m <> x & m <> y & x <> y & b <> x & b <> y & b <> m by A0;
A1: y:=1 is_terminating_wrt g, P by AOFA_000:107;
A2: P is_invariant_wrt y:=1, g
proof let s;
assume s in P; then
B1: ex s' st s = s' & s'.m >= 0;
g.(s, y:=1).m = s.m by D0,Th011;
hence g.(s, y:=1) in P by B1;
end;
set C = m gt 0;
set I = if-then(m is_odd, y*=x);
set J = I\; m/=2\; x*=x;
A3: C is_terminating_wrt g by AOFA_000:104;
A4: J is_terminating_wrt g,P by AOFA_000:107;
A5: P is_invariant_wrt C,g
proof let s;
assume s in P; then
B1: ex s' st s = s' & s'.m >= 0;
g.(s, C).m = s.m by A0,Th015;
hence g.(s, C) in P by B1;
end;
A6: 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 Th015';
hence g.(s,J) in P;
end;
defpred R[Element of S] means $1.m > 0;
deffunc F(Element of S) = In($1.m, NAT);
Z0: g complies_with_while_wrt T & g complies_with_if_wrt T by AOFA_000:def 32;
for s st g.(s,C) in P holds g iteration_terminates_for J\;C, g.(s,C)
proof let s0 be Element of S such that g.(s0,C) in P;
set s1 = g.(s0,C);
A4: s1.x = s0.x & s1.m = s0.m & s1.y = s0.y &
(s0.m > 0 implies s1.b = 1) & (s0.m <= 0 implies s1.b = 0) by A0,Th015;
B0: g.(s0,C) in T iff R[g.(s0,C)] by A4,LemTS;
B1: 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
00: s.m > 0;
set sJ = g.(s,J);
set sC = g.(sJ,C);
01: (sJ.m > 0 implies sC.b = 1) & (sJ.m <= 0 implies sC.b = 0) &
sC.m = sJ.m & g.(s,J\;C) = sC by A0,Th015,AOFA_000:def 29;
hence R[g.(s,J\;C)] iff g.(s,J\;C) in T by LemTS;
set q0 = g.(s, m is_odd);
set q1 = g.(s,I);
set q2 = g.(q1,m/=2);
set q3 = g.(q2,x*=x);
q0 in T or q0 nin T; then
03: q1 = g.(q0, y*=x) or q1 = g.(q0, EmptyIns A) by Z0,AOFA_000:def 30;
q2 = g.(s,I\;m/=2) by AOFA_000:def 29; then
q3 = g.(s,J) by AOFA_000:def 29; then
02: sJ.m = q2.m by D0,Th213 .= (q1.m) div 2 by Th017
.= (q0.m) div 2 by D0,03,Th213,AOFA_000:def 28
.= (s.m) div 2 by A0,Th218; then
sC.m in NAT & s.m in NAT by 00,01,INT_1:16,88; then
F(s) = s.m & F(sC) = sC.m by FUNCT_7:def 1;
hence F(g.(s,J\;C)) < F(s) by 00,01,02,INT_1:83;
end;
thus g iteration_terminates_for J\;C, g.(s0,C)
from AOFA_000:sch 3(B0,B1);
end; then
while(m gt 0,
if-then(m is_odd, y*=x)\; m/=2\; x*=x
) is_terminating_wrt g, P by A3,A4,A5,A6,AOFA_000:118;
hence 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} by A1,A2,AOFA_000:111;
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
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);
Z0: g complies_with_while_wrt T & 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
A0: d.b = 0 & d.x = 1 & d.y = 2 & d.m = 3;
D0: m <> x & m <> y & x <> y & b <> x & b <> y & b <> m by A0;
let s be Element of Funcs(X, INT);
set q = s;
let n be Nat;
assume
A1: n = s.m;
set C = m gt 0;
set I = if-then(m is_odd, y*=x);
set J = I\; m/=2\; x*=x;
set s0 = g.(s, y:=1);
set s1 = g.(s0,C);
set fs = g.(s0, while(C,J));
A3: s0.x = s.x & s0.m = s.m & s0.y = 1 by D0,Th011;
A4: s1.x = s0.x & s1.m = s0.m & s1.y = s0.y &
(s0.m > 0 implies s1.b = 1) & (s0.m <= 0 implies s1.b = 0) by A0,Th015;
defpred P[Element of S] means
(s.x)|^n = ($1.y)*(($1.x)to_power($1.m)) & $1.m >= 0;
defpred R[Element of S] means $1.m > 0;
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
(n = 0 or n > 0) & (n > 0 implies 0 to_power n = 0) & 0 to_power 0 = 1 &
(s.x = 0 or s.x <> 0) by POWER:def 2,29; then
A: P[s0] by A1,A3,POLYEQ_3:50,NEWTON:9,POWER:46;
deffunc F(Element of S) = In($1.m, NAT);
B0: g.(s0,C) in T iff R[g.(s0,C)] by A4,LemTS;
B1: 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
00: s.m > 0;
set sJ = g.(s,J);
set sC = g.(sJ,C);
01: (sJ.m > 0 implies sC.b = 1) & (sJ.m <= 0 implies sC.b = 0) &
sC.m = sJ.m & g.(s,J\;C) = sC by A0,Th015,AOFA_000:def 29;
hence R[g.(s,J\;C)] iff g.(s,J\;C) in T by LemTS;
set q0 = g.(s, m is_odd);
set q1 = g.(s,I);
set q2 = g.(q1,m/=2);
set q3 = g.(q2,x*=x);
q0 in T or q0 nin T; then
03: q1 = g.(q0, y*=x) or q1 = g.(q0, EmptyIns A) by Z0,AOFA_000:def 30;
q2 = g.(s,I\;m/=2) by AOFA_000:def 29; then
q3 = g.(s,J) by AOFA_000:def 29; then
02: sJ.m = q2.m by D0,Th213 .= (q1.m) div 2 by Th017
.= (q0.m) div 2 by D0,03,Th213,AOFA_000:def 28
.= (s.m) div 2 by A0,Th218; then
sC.m in NAT & s.m in NAT by 00,01,INT_1:16,88; then
F(s) = s.m & F(sC) = sC.m by FUNCT_7:def 1;
hence F(g.(s,J\;C)) < F(s) by 00,01,02,INT_1:83;
end;
B: g iteration_terminates_for J\;C, g.(s0,C) from AOFA_000:sch 3(B0,B1);
C: 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
00: P[s] & s in T & R[s];
reconsider sm = s.m as Element of NAT by 00,INT_1:16;
set sJ = g.(s,J);
set q0 = g.(s, m is_odd);
set q1 = g.(s,I);
set q2 = g.(q1,m/=2);
set q3 = g.(q2,x*=x);
q0 in T or q0 nin T; then
03: q1 = g.(q0, y*=x) or q1 = g.(q0, EmptyIns A) by Z0,AOFA_000:def 30;
q2 = g.(s,I\;m/=2) by AOFA_000:def 29; then
07: q3 = g.(s,J) by AOFA_000:def 29; then
02: sJ.m = q2.m by D0,Th213 .= (q1.m) div 2 by Th017
.= (q0.m) div 2 by D0,03,Th213,AOFA_000:def 28
.= (s.m) div 2 by A0,Th218;
q2.x = q1.x by D0,Th017 .= q0.x by D0,03,Th213,AOFA_000:def 28; then
06: sJ.x = (q0.x)*(q0.x) & q0.x = s.x by A0,Th218,07,Th213;
08: sJ.y = q2.y & q2.y = q1.y & q0.y = s.y by 07,D0,Th213,Th017,Th218;
04: sm div 2 = s.m div 2 & sm mod 2 = s.m mod 2;
09: now
I1: q0.b = (s.m) mod 2 by Th218;
per cases by 04,I1,NAT_D:12;
suppose
I2: q0.b = 0; then
q0 nin T by LemTS; then
q1 = g.(q0, EmptyIns A) by Z0,AOFA_000:def 30; then
q1.y = q0.y & (s.x)to_power 0 = 1 & (s.y)*1 = s.y
by AOFA_000:def 28,POWER:29;
hence (s.y)*((s.x)to_power(sm mod 2)) = sJ.y by I2,08,Th218;
end;
suppose
I3: q0.b = 1; then
q0 in T; then
q1 = g.(q0, y*=x) by Z0,AOFA_000:def 30; then
q1.y = (q0.y)*(q0.x) & (s.x)to_power 1 = s.x
by Th213,POWER:30;
hence (s.y)*((s.x)to_power(sm mod 2)) = sJ.y by I3,08,06,Th218;
end;
end;
05: s.x = 0 or s.x is non empty;
s.m = ((s.m) div 2)*2+((s.m) mod 2) by NEWTON:80; then
(q.x)|^n
= (s.y)*(((s.x)to_power((sm div 2)*2))*((s.x)to_power(sm mod 2)))
by 00,05,LemP1,FIB_NUM2:7
.= (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 LemP2
.= (s.y)*((s.x)to_power(sm mod 2))*
(((s.x)*(s.x)) to_power (sm div 2)) by LemP3;
hence P[g.(s,J)] by 02,06,09;
end;
D: 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
00: P[s];
set s1 = g.(s, C);
s1.m = s.m & s1.x = s.x & s1.y = s.y by A0,Th015;
hence P[g.(s,C)] by 00;
(s.m > 0 implies s1.b = 1) & (s.m > 0 or s.m <= 0) &
(s.m <= 0 implies s1.b = 0) by Th015;
hence thesis by Th015,LemTS;
end;
E: P[g.(s0,while(C,J))] & not R[g.(s0,while(C,J))]
from AOFA_000:sch 5(A,B,C,D); then
fs.m = 0 & (fs.x) to_power 0 = 1 by POWER:29;
hence g.(s, y:=1\; while(m gt 0, J)).y = (s.x)|^n by E,AOFA_000:def 29;
end;