:: Mizar Analysis of Algorithms: Algorithms over Integers
::  by Grzegorz Bancerek
::
:: Received March 18, 2008
:: Copyright (c) 2008-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, FUNCT_1, FUNCOP_1, RELAT_1, AOFA_000, FUNCT_4, XBOOLE_0,
      SUBSET_1, TARSKI, ZFMISC_1, FUNCT_2, ZF_LANG, VALUED_0, XREAL_0,
      ORDINAL1, VALUED_1, INT_1, XXREAL_0, CARD_1, ARYTM_3, ARYTM_1, FINSET_1,
      ORDINAL2, MEMBER_1, CARD_3, NAT_1, POWER, ORDINAL4, EUCLMETR, FREEALG,
      TREES_4, LANG1, MCART_1, STRUCT_0, GRAPHSP, ABIAN, FUNCT_7, REALSET1,
      NEWTON, PRE_FF, INT_2, COMPLEX1, AOFA_I00;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, MCART_1, ORDINAL1,
      RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSET_1, LANG1, BINOP_1,
      CARD_1, CARD_2, CARD_3, VALUED_0, PRE_FF, NUMBERS, XCMPLX_0, XXREAL_0,
      XREAL_0, POWER, INT_1, INT_2, NAT_1, NAT_D, NEWTON, ABIAN, FUNCOP_1,
      FUNCT_4, FUNCT_7, STRUCT_0, FREEALG, TREES_4, AOFA_000, VALUED_1;
 constructors REAL_1, BORSUK_1, PREPOWER, POWER, NAT_D, NEWTON, ABIAN,
      SQUARE_1, PRE_FF, WSIERP_1, WELLORD2, CARD_2, CAT_2, AOFA_000, XTUPLE_0;
 registrations RELSET_1, FUNCT_1, FUNCOP_1, FUNCT_2, NUMBERS, NAT_1, STRUCT_0,
      FREEALG, INT_1, CARD_5, CARD_1, CARD_3, VALUED_0, VALUED_1, MEMBERED,
      XREAL_0, XCMPLX_0, XXREAL_0, XBOOLE_0, FINSET_1, POWER, AOFA_000, ABIAN,
      XTUPLE_0;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
 definitions XCMPLX_0, CARD_2, TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2,
      FREEALG, BINOP_1, AOFA_000, FUNCOP_1, VALUED_1, XTUPLE_0;
 theorems XBOOLE_1, ZFMISC_1, RELAT_1, FUNCT_2, FUNCOP_1, TARSKI, NEWTON,
      XREAL_1, INT_1, FUNCT_7, NAT_1, ORDINAL1, FUNCT_4, FREEALG, PRE_FF,
      INT_2, ABSVALUE, WSIERP_1, TREES_4, NUMBERS, FUNCT_1, CARD_2, CARD_1,
      WELLORD2, FUNCT_5, AOFA_000, MCART_1, XXREAL_0, POWER, FIB_NUM2,
      ORDINAL3, NAT_D, PREPOWER, VALUED_1, CARD_3, XTUPLE_0;
 schemes FUNCT_1, FUNCT_2, XBOOLE_0, AOFA_000, TARSKI, CLASSES1;

begin :: Preliminaries

theorem Th1:
  for x,y,z,a,b,c being set st a <> b & b <> c & c <> a ex f being
  Function st f.a = x & f.b = y & f.c = z
proof
  let x,y,z,a,b,c be set such that
A1: a <> b and
A2: b <> c and
A3: c <> a;
  set fb = b.-->y;
A4: dom fb = {b} by FUNCOP_1:13;
A5: a nin dom fb by A1,TARSKI:def 1;
A6: b in dom fb by A4,TARSKI:def 1;
  set fc = c.-->z;
  set fa = a.-->x;
  take f = fa+*fb+*fc;
A7: dom fc = {c} by FUNCOP_1:13;
  a nin dom fc by A3,TARSKI:def 1;
  hence f.a = (fa+*fb).a by FUNCT_4:11
    .= fa.a by A5,FUNCT_4:11
    .= x by FUNCOP_1:72;
  b nin dom fc by A2,TARSKI:def 1;
  hence f.b = (fa+*fb).b by FUNCT_4:11
    .= fb.b by A6,FUNCT_4:13
    .= y by FUNCOP_1:72;
  c in dom fc by A7,TARSKI:def 1;
  hence f.c = fc.c by FUNCT_4:13
    .= z by FUNCOP_1:72;
end;

definition
  let F be non empty functional set;
  let x be set;
  let f be set;
  func F\(x,f) -> Subset of F equals
  {g where g is Element of F: g.x <> f};
  coherence
  proof
    set X = {g where g is Element of F: g.x <> f};
    X c= F
    proof
      let a be 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 Th2:
  for F being non empty functional set, x,y be set, g being Element
  of F holds g in F\(x,y) iff g.x <> y
proof
  let F be non empty functional set;
  let x,y be set;
  let g be Element of F;
  g in F\(x,y) iff ex f being Element of F st g = f & f.x <> y;
  hence thesis;
end;

definition
  let X be set;
  let Y,Z be set;
  let f be Function of [:Funcs(X,INT),Y:],Z;
  mode Variable of f -> Element of X means
    : Def2:
    not contradiction;
  existence;
end;

notation
  let f be real-valued Function;
  let x be real number;
  synonym f*x for x(#)f;
end;

definition
  let t1,t2 be INT-valued Function;
  func t1 div t2 -> INT-valued Function means
  : Def3:
  dom it = (dom t1) /\ (dom t2) &
  for s being 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 INT-valued
    proof
      let y be set;
      assume y in rng f;
      then consider x being set such that
A2:   x in dom f and
A3:   f.x = y by FUNCT_1:def 3;
      f.x = F(x) by A1,A2;
      hence thesis by A3,INT_1:def 2;
    end;
    hence ex f being INT-valued Function st dom f = (dom t1)/\(dom t2) &
    for x being set st x in dom f holds f.x = F(x) by A1;
    let f1,f2 be INT-valued Function such that
A4: dom f1 = (dom t1) /\ dom t2 and
A5: for s being set st s in dom f1 holds f1.s = F(s) and
A6: dom f2 = (dom t1) /\ dom t2 and
A7: for s being set st s in dom f2 holds f2.s = F(s);
    now
      let s be set;
      assume
A8:   s in (dom t1) /\ dom t2;
      hence f1.s = F(s) by A4,A5
        .= f2.s by A6,A7,A8;
    end;
    hence thesis by A4,A6,FUNCT_1:2;
  end;
  func t1 mod t2 -> INT-valued Function means
  : Def4:
  dom it = (dom t1) /\ (dom t2) &
  for s being set st s in dom it holds it.s = (t1.s) mod (t2.s);
  correctness
  proof
    deffunc F(set) = (t1.$1) mod (t2.$1);
    consider f being Function such that
A9: 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 INT-valued
    proof
      let y be set;
      assume y in rng f;
      then consider x being set such that
A10:   x in dom f and
A11:   f.x = y by FUNCT_1:def 3;
      f.x = F(x) by A9,A10;
      hence thesis by A11,INT_1:def 2;
    end;
    hence ex f being INT-valued Function st dom f = (dom t1)/\(dom t2) &
    for x being set st x in dom f holds f.x = F(x) by A9;
    let f1,f2 be INT-valued Function such that
A12: dom f1 = (dom t1) /\ dom t2 and
A13: for s being set st s in dom f1 holds f1.s = F(s) and
A14: dom f2 = (dom t1) /\ dom t2 and
A15: for s being set st s in dom f2 holds f2.s = F(s);
    now
      let s be set;
      assume
A16:  s in (dom t1) /\ dom t2;
      hence f1.s = F(s) by A12,A13
        .= f2.s by A14,A15,A16;
    end;
    hence thesis by A12,A14,FUNCT_1:2;
  end;
  func leq(t1,t2) -> INT-valued Function means
  : Def5:
  dom it = (dom t1) /\ (dom t2) &
  for s being set st s in dom it holds it.s = IFGT(t1.s,t2.s,0,1);
  correctness
  proof
    deffunc F(set) = IFGT(t1.$1,t2.$1,0,1);
    consider f being Function such that
A17: 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 INT-valued
    proof
      let y be set;
      assume y in rng f;
      then consider x being set such that
A18:   x in dom f and
A19:   f.x = y by FUNCT_1:def 3;
      f.x = F(x) by A17,A18;
      hence thesis by A19,INT_1:def 2;
    end;
    hence ex f being INT-valued Function st dom f = (dom t1)/\(dom t2) &
    for x being set st x in dom f holds f.x = F(x) by A17;
    let f1,f2 be INT-valued Function such that
A20: dom f1 = (dom t1) /\ dom t2 and
A21: for s being set st s in dom f1 holds f1.s = F(s) and
A22: dom f2 = (dom t1) /\ dom t2 and
A23: for s being set st s in dom f2 holds f2.s = F(s);
    now
      let s be set;
      assume
A24:  s in (dom t1) /\ dom t2;
      hence f1.s = F(s) by A20,A21
        .= f2.s by A22,A23,A24;
    end;
    hence thesis by A20,A22,FUNCT_1:2;
  end;
  func gt(t1,t2) -> INT-valued Function means
  : Def6:
  dom it = (dom t1) /\ (dom t2) &
  for s being set st s in dom it holds it.s = IFGT(t1.s,t2.s,1,0);
  correctness
  proof
    deffunc F(set) = IFGT(t1.$1,t2.$1,1,0);
    consider f being Function such that
A25: 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 INT-valued
    proof
      let y be set;
      assume y in rng f;
      then consider x being set such that
A26:   x in dom f and
A27:   f.x = y by FUNCT_1:def 3;
      f.x = F(x) by A25,A26;
      hence thesis by A27,INT_1:def 2;
    end;
    hence ex f being INT-valued Function st dom f = (dom t1)/\(dom t2) &
    for x being set st x in dom f holds f.x = F(x) by A25;
    let f1,f2 be INT-valued Function such that
A28: dom f1 = (dom t1) /\ dom t2 and
A29: for s being set st s in dom f1 holds f1.s = F(s) and
A30: dom f2 = (dom t1) /\ dom t2 and
A31: for s being set st s in dom f2 holds f2.s = F(s);
    now
      let s be set;
      assume
A32:  s in (dom t1) /\ dom t2;
      hence f1.s = F(s) by A28,A29
        .= f2.s by A30,A31,A32;
    end;
    hence thesis by A28,A30,FUNCT_1:2;
  end;
  func eq(t1,t2) -> INT-valued Function means
  : Def7:
  dom it = (dom t1) /\ (dom t2) &
  for s being set st s in dom it holds it.s = IFEQ(t1.s,t2.s,1,0);
  correctness
  proof
    deffunc F(set) = IFEQ(t1.$1,t2.$1,1,0);
    consider f being Function such that
A33: 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 INT-valued
    proof
      let y be set;
      assume y in rng f;
      then consider x being set such that
A34:   x in dom f and
A35:   f.x = y by FUNCT_1:def 3;
      f.x = F(x) by A33,A34;
      hence thesis by A35,INT_1:def 2;
    end;
    hence ex f being INT-valued Function st dom f = (dom t1)/\(dom t2) &
    for x being set st x in dom f holds f.x = F(x) by A33;
    let f1,f2 be INT-valued Function such that
A36: dom f1 = (dom t1) /\ dom t2 and
A37: for s being set st s in dom f1 holds f1.s = F(s) and
A38: dom f2 = (dom t1) /\ dom t2 and
A39: for s being set st s in dom f2 holds f2.s = F(s);
    now
      let s be set;
      assume
A40:  s in (dom t1) /\ dom t2;
      hence f1.s = F(s) by A36,A37
        .= f2.s by A38,A39,A40;
    end;
    hence thesis by A36,A38,FUNCT_1:2;
  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
  : Def8:
  for s being Element of X holds it.s = f.s+x;
  compatibility
  proof
    let ti be Function of X, INT;
A1: dom f = X by FUNCT_2:def 1;
    dom (f+x) = dom f by VALUED_1:def 2;
    hence ti = f+x implies for s being Element of X holds ti.s = f.s+x by A1,
VALUED_1:def 2;
A2: dom ti = X by FUNCT_2:def 1;
    assume for s being Element of X holds ti.s = f.s+x;
    then for s being set st s in X holds ti.s = x+f.s;
    hence thesis by A1,A2,VALUED_1:def 2;
  end;
  coherence
  proof
    x+f is Function of X, INT;
    hence thesis;
  end;
  redefine func f-x -> Function of X, INT means
  for s being Element of X holds it.s = f .s-x;
  compatibility
  proof
    let ti be Function of X, INT;
A3: dom ti = X by FUNCT_2:def 1;
A4: dom f = X by FUNCT_2:def 1;
    hence ti = f-x implies for s being Element of X holds ti.s = f.s-x by
VALUED_1:3;
    assume
A5: for s being Element of X holds ti.s = f.s-x;
A6: now
      let s be set;
      assume
A7:   s in dom ti;
      hence ti.s = f.s-x by A5
        .= (f-x).s by A4,A7,VALUED_1:3;
    end;
    dom (f-x) = dom f by VALUED_1:3;
    hence ti = f-x by A4,A3,A6,FUNCT_1:2;
  end;
  coherence
  proof
    thus f-x is Function of X, INT;
  end;
  redefine func f*x -> Function of X, INT means
  : Def10:
  for s being Element of X holds it.s = f.s*x;
  compatibility
  proof
    let ti be Function of X, INT;
A8: dom (f*x) = dom f by VALUED_1:def 5;
A9: dom f = X by FUNCT_2:def 1;
    hence ti = f*x implies for s being Element of X holds ti.s = f.s*x by A8,
VALUED_1:def 5;
A10: dom ti = X by FUNCT_2:def 1;
    assume for s being Element of X holds ti.s = f.s*x;
    then for s being set st s in dom (f*x) holds ti.s = x*f.s;
    hence thesis by A8,A9,A10,VALUED_1:def 5;
  end;
  coherence
  proof
    x(#)f is Function of X, INT;
    hence thesis;
  end;
end;

definition
  let X be set;
  let f,g be Function of X, INT;
  redefine func f div g -> Function of X, INT;
  coherence
  proof
A1: dom g = X by FUNCT_2:def 1;
A2: dom (f div g) = (dom f) /\ dom g by Def3;
A3: dom f = X by FUNCT_2:def 1;
    rng (f div g) c= INT;
    hence thesis by A2,A3,A1,FUNCT_2:2;
  end;
  redefine func f mod g -> Function of X, INT;
  coherence
  proof
A4: dom g = X by FUNCT_2:def 1;
A5: dom (f mod g) = (dom f) /\ dom g by Def4;
A6: dom f = X by FUNCT_2:def 1;
    rng (f mod g) c= INT;
    hence thesis by A5,A6,A4,FUNCT_2:2;
  end;
  redefine func leq(f,g) -> Function of X, INT;
  coherence
  proof
A7: dom g = X by FUNCT_2:def 1;
A8: dom leq(f,g) = (dom f) /\ dom g by Def5;
A9: dom f = X by FUNCT_2:def 1;
    rng leq(f,g) c= INT;
    hence thesis by A8,A9,A7,FUNCT_2:2;
  end;
  redefine func gt(f,g) -> Function of X, INT;
  coherence
  proof
A10: dom g = X by FUNCT_2:def 1;
A11: dom gt(f,g) = (dom f) /\ dom g by Def6;
A12: dom f = X by FUNCT_2:def 1;
    rng gt(f,g) c= INT;
    hence thesis by A11,A12,A10,FUNCT_2:2;
  end;
  redefine func eq(f,g) -> Function of X, INT;
  coherence
  proof
A13: dom g = X by FUNCT_2:def 1;
A14: dom eq(f,g) = (dom f) /\ dom g by Def7;
A15: dom f = X by FUNCT_2:def 1;
    rng eq(f,g) c= INT;
    hence thesis by A14,A15,A13,FUNCT_2:2;
  end;
end;

definition
  let X be non empty set;
  let t1,t2 be Function of X, INT;
  redefine func t1-t2 -> Function of X, INT means
  : Def11:
  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 = X by FUNCT_2:def 1;
    thus ti = t1-t2 implies for s being Element of X holds ti.s = (t1.s)-(t2.s
    ) by VALUED_1:15;
A2: dom ti = X by FUNCT_2:def 1;
    assume
A3: for s being Element of X holds ti.s = (t1.s)-(t2.s);
A4: now
      let s be set;
      assume
A5:   s in X;
      hence ti.s = (t1.s)-(t2.s) by A3
        .= (t1-t2).s by A5,VALUED_1:15;
    end;
A6: dom t2 = X by FUNCT_2:def 1;
    dom (t1-t2) = (dom t1)/\dom t2 by VALUED_1:12;
    hence ti = t1-t2 by A1,A6,A2,A4,FUNCT_1:2;
  end;
  coherence
  proof
    thus t1-t2 is Function of X, INT;
  end;
  redefine 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;
A7: dom t1 = X by FUNCT_2:def 1;
A8: dom t2 = X by FUNCT_2:def 1;
A9: dom (t1+t2) = (dom t1)/\dom t2 by VALUED_1:def 1;
    hence
    ti = t1+t2 implies for s being Element of X holds ti.s = (t1.s)+(t2.s
    ) by A7,A8,VALUED_1:def 1;
A10: dom ti = X by FUNCT_2:def 1;
    assume for s being Element of X holds ti.s = (t1.s)+(t2.s);
    then for s being set st s in X holds ti.s = (t1.s)+(t2.s);
    hence ti = t1+t2 by A9,A7,A8,A10,VALUED_1:def 1;
  end;
  coherence
  proof
    thus t1+t2 is Function of X, INT;
  end;
end;

registration
  let A be non empty set;
  let B be infinite set;
  cluster Funcs(A, B) -> infinite;
  coherence
  proof
A1: card card B = card B;
    card A = card card A;
    then
A2: card Funcs(A, B) = exp(card B, card A) by A1,FUNCT_5:61;
    set a = the Element of A;
A3: card {a} = 1 by CARD_1:30;
    {a} c= A by ZFMISC_1:31;
    then 1 c= card A by A3,CARD_1:11;
    then exp(card B, 1) c= card Funcs(A, B) by A2,CARD_2:93;
    hence thesis by CARD_2:27;
  end;
end;

definition
  let N be set;
  let v be Function;
  let f be Function;
  func v**(f,N) -> Function means
  : Def13:
  (ex Y being set st (for y being set
holds y in Y iff ex h being Function st h in dom v & y in rng h) & for a being
set holds a in dom it iff a in Funcs(N,Y) & ex g being Function st a = g & g*f
  in dom v) & for g being Function st g in dom it holds it.g = v.(g*f);
  uniqueness
  proof
    let F1,F2 be Function;
    given Y1 being set such that
A1: for y being set holds y in Y1 iff ex h being Function st h in dom
    v & y in rng h and
A2: for a being set holds a in dom F1 iff a in Funcs(N,Y1) & ex g
    being Function st a = g & g*f in dom v;
    assume
A3: for g being Function st g in dom F1 holds F1.g = v.(g*f);
    given Y2 being set such that
A4: for y being set holds y in Y2 iff ex h being Function st h in dom
    v & y in rng h and
A5: for a being set holds a in dom F2 iff a in Funcs(N,Y2) & ex g
    being Function st a = g & g*f in dom v;
    now
      let a be set;
      a in Y1 iff ex h being Function st h in dom v & a in rng h by A1;
      hence a in Y1 iff a in Y2 by A4;
    end;
    then
A6: Y1 = Y2 by TARSKI:1;
    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 A2;
      hence a in dom F1 iff a in dom F2 by A5,A6;
    end;
    then
A7: dom F1 = dom F2 by TARSKI:1;
    assume
A8: for g being Function st g in dom F2 holds F2.g = v.(g*f);
    now
      let a be set;
      assume
A9:   a in dom F1;
      then consider g being Function such that
A10:  a = g and
      g*f in dom v by A2;
      thus F1.a = v.(g*f) by A3,A9,A10
        .= F2.a by A8,A7,A9,A10;
    end;
    hence thesis by A7,FUNCT_1:2;
  end;
  existence
  proof
    defpred F[set,set] means ex g being Function st g = $1 & $2 = v.(g*f);
    defpred R[set] means ex g being Function st g = $1 & g*f in dom v;
    defpred P[set,set] means ex g being Function st $1 = g & $2 = rng g;
A11: for x,y,z being set st P[x,y] & P[x,z] holds y = z;
    consider X being set such that
A12: 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(A11);
    set Y = union X;
    consider D being set such that
A13: for x being set holds x in D iff x in Funcs(N,Y) & R[x] from
    XBOOLE_0:sch 1;
A14: 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
A15:  y = x and
      y*f in dom v by A13;
      take v.(y*f);
      thus thesis by A15;
    end;
    consider F being Function such that
A16: dom F = D & for g being set st g in D holds F[g,F.g] from
    CLASSES1:sch 1(A14);
    take F;
    hereby
      take Y;
      hereby
        let y be set;
        hereby
          assume y in Y;
          then consider a being set such that
A17:      y in a and
A18:      a in X by TARSKI:def 4;
          ex z being set st z in dom v & P[z,a] by A12,A18;
          hence ex h being Function st h in dom v & y in rng h by A17;
        end;
        given h being Function such that
A19:    h in dom v and
A20:    y in rng h;
        rng h in X by A12,A19;
        hence y in Y by A20,TARSKI:def 4;
      end;
      let a be set;
      thus a in dom F iff a in Funcs(N,Y) & ex g being Function st a = g & g*f
      in dom v by A13,A16;
    end;
    let g be Function;
    assume g in dom F;
    then F[g,F.g] by A16;
    hence thesis;
  end;
end;

definition
  let X,Y,Z,N be non empty set;
  let v be Element of Funcs(Funcs(X,Y), Z);
  let f be Function of X,N;
  redefine func v**(f,N) -> Element of Funcs(Funcs(N,Y),Z);
  coherence
  proof
    consider Y0 being set such that
A1: for y being set holds y in Y0 iff ex h being Function st h in dom
    v & y in rng h and
A2: for a being set holds a in dom (v**(f,N)) iff a in Funcs(N,Y0) &
    ex g being Function st a = g & g*f in dom v by Def13;
A3: dom v = Funcs(X,Y) by FUNCT_2:def 1;
A4: Y0 = Y
    proof
      thus Y0 c= Y
      proof
        let y be set;
        assume y in Y0;
        then consider h being Function such that
A5:     h in dom v and
A6:     y in rng h by A1;
        rng h c= Y by A5,FUNCT_2:92;
        hence thesis by A6;
      end;
      let y be set;
      assume y in Y;
      then reconsider y as Element of Y;
      reconsider h = X-->y as Function of X,Y;
A7:   rng h = {y} by FUNCOP_1:8;
A8:   h in Funcs(X,Y) by FUNCT_2:8;
      y in {y} by TARSKI:def 1;
      hence thesis by A3,A1,A7,A8;
    end;
A9: dom (v**(f,N)) = Funcs(N,Y)
    proof
      thus dom (v**(f,N)) c= Funcs(N,Y)
      proof
        let a be set;
        thus thesis by A2,A4;
      end;
      let a be set;
      assume
A10:  a in Funcs(N,Y);
      then reconsider g = a as Function of N,Y by FUNCT_2:66;
      g*f in Funcs(X,Y) by FUNCT_2:8;
      hence thesis by A3,A2,A4,A10;
    end;
    rng (v**(f,N)) c= Z
    proof
      let a be set;
      assume a in rng (v**(f,N));
      then consider g being set such that
A11:  g in dom (v**(f,N)) and
A12:  a = (v**(f,N)).g by FUNCT_1:def 3;
      reconsider g as Element of Funcs(N,Y) by A9,A11;
      reconsider gf = g*f as Element of Funcs(X,Y) by FUNCT_2:8;
      a = v.gf by A11,A12,Def13;
      hence thesis;
    end;
    hence thesis by A9,FUNCT_2:def 2;
  end;
end;

theorem Th3:
  for f1,f2,g being Function st rng g c= dom f2 holds (f1+*f2)*g = f2*g
proof
  let f1,f2,g be Function;
  assume
A1: rng g c= dom f2;
A2: now
    let x be set;
    assume
A3: x in dom g;
    then
A4: (f2*g).x = f2.(g.x) by FUNCT_1:13;
A5: g.x in rng g by A3,FUNCT_1:3;
    ((f1+*f2)*g).x = (f1+*f2).(g.x) by A3,FUNCT_1:13;
    hence ((f1+*f2)*g).x = (f2*g).x by A1,A4,A5,FUNCT_4:13;
  end;
  dom (f1+*f2) = dom f1 \/ dom f2 by FUNCT_4:def 1;
  then
A6: dom ((f1+*f2)*g) = dom g by A1,RELAT_1:27,XBOOLE_1:10;
  dom (f2*g) = dom g by A1,RELAT_1:27;
  hence thesis by A6,A2,FUNCT_1:2;
end;

theorem Th4:
  for X,N,I being non empty set for s being Function of X,I for c
being Function of X,N st c is one-to-one for n being Element of I holds (N-->n)
  +*(s*c") is Function of N,I
proof
  let X,N,I be non empty set;
  let s be Function of X,I;
  let c be Function of X,N;
  assume c is one-to-one;
  then
A1: dom (c") = rng c by FUNCT_1:33;
  let n be Element of I;
  set f = N-->n, g = s*c";
A2: dom g c= dom (c") by RELAT_1:25;
  rng g c= rng s by RELAT_1:26;
  then rng g c= I by XBOOLE_1:1;
  then
A3: rng f \/ rng g c= I by XBOOLE_1:8;
A4: dom f = N by FUNCOP_1:13;
A5: rng (f+*g) c= rng f \/ rng g by FUNCT_4:17;
  dom (f+*g) = dom f \/ dom g by FUNCT_4:def 1;
  then dom (f+*g) = N by A2,A4,A1,XBOOLE_1:1,12;
  hence thesis by A5,A3,FUNCT_2:2,XBOOLE_1:1;
end;

theorem Th5:
  for N,X,I being non empty set for v1,v2 being Function st dom v1
= dom v2 & dom v1 = Funcs(X,I) for f being Function of X, N st f is one-to-one
  & v1**(f,N) = v2**(f,N) holds v1 = v2
proof
  let N,X,I be non empty set;
  let v1,v2 be Function such that
A1: dom v1 = dom v2 and
A2: dom v1 = Funcs(X,I);
  reconsider rv1 = rng v1, rv2 = rng v2 as non empty set by A1,A2,RELAT_1:42;
  reconsider Z = rv1\/rv2 as non empty set;
A3: rng v2 c= Z by XBOOLE_1:7;
  rng v1 c= Z by XBOOLE_1:7;
  then reconsider f1 = v1, f2 = v2 as Element of Funcs(Funcs(X,I),Z) by A1,A2
,A3,FUNCT_2:def 2;
  let f be Function of X, N such that
A4: f is one-to-one and
A5: v1**(f,N) = v2**(f,N);
A6: dom (f2**(f,N)) = Funcs(N,I) by FUNCT_2:def 1;
A7: dom (f1**(f,N)) = Funcs(N,I) by FUNCT_2:def 1;
  now
    set i = the Element of I;
    let a be set;
A8: dom f = X by FUNCT_2:def 1;
    assume a in Funcs(X,I);
    then reconsider h = a as Element of Funcs(X,I);
    set g = (N-->i)+*(h*f");
A9: dom h = X by FUNCT_2:def 1;
    rng (f") = dom f by A4,FUNCT_1:33;
    then dom (h*f") = dom (f") by A9,RELAT_1:27
      .= rng f by A4,FUNCT_1:33;
    then
A10: g*f = (h*f")*f by Th3
      .= h*(f"*f) by RELAT_1:36
      .= h*id X by A4,A8,FUNCT_1:39
      .= a by A9,RELAT_1:52;
    g is Function of N,I by A4,Th4;
    then
A11: g in Funcs(N,I) by FUNCT_2:8;
    then (v1**(f,N)).g = v1.a by A7,A10,Def13;
    hence v1.a = v2.a by A5,A6,A11,A10,Def13;
  end;
  hence thesis by A1,A2,FUNCT_1:2;
end;

registration
  let X be set;
  cluster one-to-one onto for Function of X, card X;
  existence
  proof
    X, card X are_equipotent by CARD_1:def 2;
    then consider f being Function such that
A1: f is one-to-one and
A2: dom f = X and
A3: rng f = card X by WELLORD2:def 4;
    reconsider f as Function of X,card X by A2,A3,FUNCT_2:2;
    take f;
    thus f is one-to-one by A1;
    thus rng f = card X by A3;
  end;
  cluster one-to-one onto for Function of card X, X;
  existence
  proof
    X, card X are_equipotent by CARD_1:def 2;
    then consider f being Function such that
A4: f is one-to-one and
A5: dom f = card X and
A6: rng f = X by WELLORD2:def 4;
    reconsider f as Function of card X, X by A5,A6,FUNCT_2:2;
    take f;
    thus f is one-to-one by A4;
    thus rng f = X by A6;
  end;
end;

definition
  let X be set;
  mode Enumeration of X is one-to-one onto Function of X, card X;
  mode Denumeration of X is one-to-one onto Function of card X, X;
end;

theorem Th6:
  for X being set, f being Function holds f is Enumeration of X iff
  dom f = X & rng f = card X & f is one-to-one
proof
  let X be set, f be Function;
  card X = {} implies X = {};
  hence thesis by FUNCT_2:2,def 1,def 3;
end;

theorem Th7:
  for X being set, f being Function holds f is Denumeration of X
  iff dom f = card X & rng f = X & f is one-to-one
proof
  let X be set, f be Function;
  X = {} implies card X = {};
  hence thesis by FUNCT_2:2,def 1,def 3;
end;

theorem Th8:
  for X being non empty set, x,y being Element of X for f being
  Enumeration of X holds f+*(x,f.y)+*(y,f.x) is Enumeration of X
proof
  let X be non empty set, x,y be Element of X;
  let f be Enumeration of X;
  set g = f+*(x,f.y)+*(y,f.x);
  set A = dom g;
A1: dom (f+*(x,f.y)) = dom f by FUNCT_7:30;
A2: A = dom (f+*(x,f.y)) by FUNCT_7:30;
A3: dom f = X by Th6;
A4: rng f = card X by Th6;
A5: rng (f+*(x,f.y)+*(y,f.x)) = rng f
  proof
    {f.x} c= rng f by A4,ZFMISC_1:31;
    then
A6: rng f \/ {f.x} = rng f by XBOOLE_1:12;
A7: rng g c= rng (f+*(x,f.y)) \/ {f.x} by FUNCT_7:100;
    {f.y} c= rng f by A4,ZFMISC_1:31;
    then rng f \/ {f.y} = rng f by XBOOLE_1:12;
    then rng (f+*(x,f.y)) \/ {f.x} c= rng f by A6,FUNCT_7:100,XBOOLE_1:9;
    hence rng g c= rng f by A7,XBOOLE_1:1;
    let z be set;
    assume z in rng f;
    then consider a being set such that
A8: a in dom f and
A9: z = f.a by FUNCT_1:def 3;
    per cases;
    suppose
A10:  a <> x & a <> y;
      then
A11:  g.a = (f+*(x,f.y)).a by FUNCT_7:32;
      (f+*(x,f.y)).a = z by A9,A10,FUNCT_7:32;
      hence thesis by A1,A2,A8,A11,FUNCT_1:def 3;
    end;
    suppose
      a = x;
      then g.y = z by A1,A3,A9,FUNCT_7:31;
      hence thesis by A1,A2,A3,FUNCT_1:def 3;
    end;
    suppose
A12:  a = y;
      then
A13:  x <> y implies g.x = (f+*(x,z)).x by A9,FUNCT_7:32;
A14:  (f+*(x,z)).x = z by A3,FUNCT_7:31;
      x = y implies g.x = z by A1,A3,A9,A12,FUNCT_7:31;
      hence thesis by A1,A2,A3,A14,A13,FUNCT_1:def 3;
    end;
  end;
  f+*(x,f.y)+*(y,f.x) is one-to-one
  proof
    let a,b being set;
A15: a <> y implies g.a = (f+*(x,f.y)).a by FUNCT_7:32;
A16: a <> x implies (f+*(x,f.y)).a = f.a by FUNCT_7:32;
A17: b = y implies g.b = f.x by A1,A3,FUNCT_7:31;
A18: b <> y implies g.b = (f+*(x,f.y)).b by FUNCT_7:32;
A19: b = x implies (f+*(x,f.y)).b = f.y by A3,FUNCT_7:31;
A20: a = x implies (f+*(x,f.y)).a = f.y by A3,FUNCT_7:31;
A21: b <> x implies (f+*(x,f.y)).b = f.b by FUNCT_7:32;
    a = y implies g.a = f.x by A1,A3,FUNCT_7:31;
    hence thesis by A2,A3,A15,A20,A16,A17,A18,A19,A21,FUNCT_1:def 4;
  end;
  hence thesis by A1,A2,A3,A4,A5,Th6;
end;

theorem
  for X being non empty set, x being Element of X ex f being Enumeration
  of X st f.x = 0
proof
  let X be non empty set, x be Element of X;
  set f = the Enumeration of X;
A1: 0 in card X by ORDINAL3:8;
A2: rng f = card X by Th6;
  dom f = X by Th6;
  then consider y being set such that
A3: y in X and
A4: 0 = f.y by A1,A2,FUNCT_1:def 3;
  reconsider y as Element of X by A3;
  reconsider g = f+*(y,f.x)+*(x,0) as Enumeration of X by A4,Th8;
  take g;
  dom f = X by Th6;
  then dom (f+*(y,f.x)) = X by FUNCT_7:30;
  hence thesis by FUNCT_7:31;
end;

theorem
  for X being non empty set, f being Denumeration of X holds f.0 in X by
FUNCT_2:5,ORDINAL3:8;

theorem Th11:
  for X being countable set, f being Enumeration of X holds rng f c= NAT
proof
  let X be countable set, f be Enumeration of X;
  card X c= NAT by CARD_3:def 14;
  hence thesis by Th6;
end;

definition
  let X be set;
  let f be Enumeration of X;
  redefine func f" -> Denumeration of X;
  coherence
  proof
    rng f = card X by Th6;
    then
A1: dom (f") = card X by FUNCT_1:33;
    dom f = X by Th6;
    then rng (f") = X by FUNCT_1:33;
    hence thesis by A1,Th7;
  end;
end;

definition
  let X be set;
  let f be Denumeration of X;
  redefine func f" -> Enumeration of X;
  coherence
  proof
    rng f = X by Th7;
    then
A1: dom (f") = X by FUNCT_1:33;
    dom f = card X by Th7;
    then rng (f") = card X by FUNCT_1:33;
    hence thesis by A1,Th6;
  end;
end;

theorem
  for n,m being Nat holds 0 to_power (n+m) = (0 to_power n)*(0 to_power m)
proof
  let n,m be Nat;
  per cases;
  suppose
A1: n > 0 or m > 0;
    then 0 to_power n = 0 or 0 to_power m = 0 by POWER:def 2;
    hence thesis by A1,POWER:def 2;
  end;
  suppose
A2: n = 0 & m = 0;
    then 0 to_power (n+m) = 1 by POWER:24;
    hence thesis by A2;
  end;
end;

theorem
  for x being real number for n,m being Nat holds (x to_power n)
  to_power m = x to_power (n*m) by NEWTON:9;

begin :: If-while algebra over integers

definition
  let X be non empty set;
  mode INT-Variable of X is Function of Funcs(X, INT), X;
  mode INT-Expression of X is Function of Funcs(X, INT), INT;
  mode INT-Array of X is Function of INT, X;
end;

reserve A for preIfWhileAlgebra;

definition
  let A;
  let I be Element of A;
  let X be non empty set;
  let T be Subset of Funcs(X, INT);
  let f be ExecutionFunction of A, Funcs(X, INT), T;
  pred I is_assignment_wrt A,X,f means
  : Def14:
  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
  : Def15:
  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
B1: 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 B1;
    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,Def14;
    take v,t,I;
    thus thesis by A1,A2,Def14;
  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
B1: 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 B1;
    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,Def14;
    take t,v,I;
    thus thesis by A1,A2,Def14;
  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:4;
    hence thesis;
  end;
end;

definition
  let X be non empty set;
  let x be Element of X;
  func .x -> INT-Expression of X means
  : Def18:
  for s being Element of Funcs(X, INT) holds it.s = s.x;
  correctness
  proof
    deffunc F(Element of Funcs(X,INT)) = $1.x;
    thus ex f being Function of Funcs(X, INT), INT st for x being Element of
    Funcs(X, INT) holds f.x = F(x) from FUNCT_2:sch 4;
    let f1,f2 be INT-Expression of X such that
A1: for s being Element of Funcs(X, INT) holds f1.s = s.x and
A2: for s being Element of Funcs(X, INT) holds f2.s = s.x;
    now
      let s be Element of Funcs(X, INT);
      thus f1.s = s.x by A1
        .= f2.s by A2;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

definition
  let X be non empty set;
  let v be INT-Variable of X;
  func .v -> INT-Expression of X means
  : Def19:
  for s being Element of Funcs(X, INT) holds it.s = s.(v.s);
  correctness
  proof
    deffunc F(Element of Funcs(X,INT)) = $1.(v.$1);
    thus ex f being Function of Funcs(X, INT), INT st for x being Element of
    Funcs(X, INT) holds f.x = F(x) from FUNCT_2:sch 4;
    let f1,f2 be INT-Expression of X such that
A1: for s being Element of Funcs(X, INT) holds f1.s = s.(v.s) and
A2: for s being Element of Funcs(X, INT) holds f2.s = s.(v.s);
    now
      let s be Element of Funcs(X, INT);
      thus f1.s = s.(v.s) by A1
        .= f2.s by A2;
    end;
    hence thesis by FUNCT_2:63;
  end;
end;

definition
  let X be non empty set;
  let x be Element of X;
  func ^x -> INT-Variable of X equals
  Funcs(X, INT) --> x;
  correctness;
end;

theorem
  for X being non empty set for x being Element of X holds .x = .(^x)
proof
  let X be non empty set;
  let x be Element of X;
  for s being Element of Funcs(X, INT) holds .(^x).s = s.x
  proof
    let s be Element of Funcs(X, INT);
    thus .(^x).s = s.((^x).s) by Def19
      .= s.x by FUNCOP_1:7;
  end;
  hence thesis by Def18;
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:45;
  end;
end;

theorem
  for X being non empty set, t being INT-Expression of X holds t+ .(0,X)
  = t & t(#).(1,X) = t
proof
  let X be non empty set;
  let t be INT-Expression of X;
  now
    let s be Element of Funcs(X,INT);
A1: .(0,X).s = 0 by FUNCOP_1:7;
    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:63;
  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:7
      .= t.s;
  end;
  hence thesis by FUNCT_2:63;
end;

:: The word "Euclidean" is chosen in following definition
:: to suggest that Euclid algoritm could be annotated
:: in quite natural way (all needed expressions are allowed).

definition
  let A;
  let X be non empty set;
  let T be Subset of Funcs(X, INT);
  let f be ExecutionFunction of A, Funcs(X, INT), T;
  attr f is Euclidean means
  : Def22:
  (for v being INT-Variable of A,f, t being
  INT-Expression of A,f holds v,t form_assignment_wrt f) & (for i being integer
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
  : Def23:
  for X being non empty countable set, T
being Subset of Funcs(X, INT) ex f being ExecutionFunction of A, Funcs(X, INT),
  T st f is Euclidean;
end;

definition
  func INT-ElemIns -> infinite disjoint_with_NAT set equals
  [:Funcs(Funcs(NAT, INT), NAT), Funcs(Funcs(NAT, INT), INT):];
  coherence;
end;

definition
  mode INT-Exec -> ExecutionFunction of FreeUnivAlgNSG(ECIW-signature,
    INT-ElemIns), Funcs(NAT, INT), Funcs(NAT,INT)\(0,0) means
    : Def25:
    for s being
Element of Funcs(NAT, INT) for v being Element of Funcs(Funcs(NAT, INT), NAT)
for e being Element of Funcs(Funcs(NAT, INT), INT) holds it.(s, root-tree [v,e]
    ) = s+*(v.s,e.s);
  existence
  proof
    reconsider i0 = 0 as Element of INT by INT_1:def 1;
    set Q = Funcs(NAT, INT), T = Q\(0,0);
    set S = ECIW-signature, G = INT-ElemIns;
    set A = FreeUnivAlgNSG(S,G);
A1: Terminals DTConUA(S,G) = G by FREEALG:3;
    reconsider q0 = NAT-->i0 as Element of Q by FUNCT_2:8;
    defpred P[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);
A2: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
A3: 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
A4:   s in Q and
A5:   I in ElementaryInstructions A and
A6:   x = [s,I] by ZFMISC_1:def 2;
      reconsider s as Element of Q by A4;
      consider a being Symbol of DTConUA(S,G) such that
A7:   I = root-tree a and
A8:   a in Terminals DTConUA(S,G) by A2,A5;
      consider v,e being set such that
A9:   v in Funcs(Funcs(NAT, INT), NAT) and
A10:  e in Funcs(Funcs(NAT, INT), INT) and
A11:  a = [v,e] by A1,A8,ZFMISC_1:def 2;
      reconsider e as Element of Funcs(Q, INT) by A10;
      reconsider v as Element of Funcs(Q, NAT) by A9;
      take y = s+*(v.s,e.s);
      thus y in Q by FUNCT_2:8;
      take s,v,e;
      thus x = [s, root-tree [v,e]] & y = s+*(v.s,e.s) by A6,A7,A11;
    end;
    consider g being Function such that
A12: dom g = [:Q,ElementaryInstructions A:] & rng g c= Q and
A13: for x being set st x in [:Q,ElementaryInstructions A:] holds P[x,
    g.x] from FUNCT_1:sch 5(A3);
    reconsider g as Function of [:Q,ElementaryInstructions A:], Q by A12,
FUNCT_2:2;
    consider f being ExecutionFunction of A, Q, T such that
A14: f|[:Q,ElementaryInstructions A:] = g and
    for s being Element of Q for C,I being Element of A st not f
iteration_terminates_for I\;C, f.(s,C) holds f.(s, while(C,I)) = q0 by
AOFA_000:91;
    take f;
    let s be Element of Funcs(NAT, INT);
    let v be Element of Funcs(Funcs(NAT, INT), NAT);
    let e be Element of Funcs(Funcs(NAT, INT), INT);
    set I = root-tree [v,e];
    [v,e] in G by ZFMISC_1:87;
    then I in ElementaryInstructions A by A2,A1;
    then
A15: [s,I] in [:Q,ElementaryInstructions A:] by ZFMISC_1:87;
    then consider
    s9 being (Element of Q), v9 being (Element of Funcs(Q, NAT)), e9
    being Element of Funcs(Q, INT) such that
A16: [s,I] = [s9, root-tree [v9,e9]] and
A17: g.[s,I] = s9+*(v9.s9,e9.s9) by A13;
    I = root-tree [v9,e9] by A16,XTUPLE_0:1;
    then
A18: [v,e] = [v9,e9] by TREES_4:4;
    then
A19: v = v9 by XTUPLE_0:1;
A20: e = e9 by A18,XTUPLE_0:1;
    s = s9 by A16,XTUPLE_0:1;
    hence thesis by A14,A15,A17,A19,A20,FUNCT_1:49;
  end;
end;

definition
  let X be non empty set;
  func INT-ElemIns X -> infinite disjoint_with_NAT set equals
  [:Funcs(Funcs(X,
  INT), X), Funcs(Funcs(X, INT), INT):];
  coherence;
end;

definition
  let X be non empty set;
  let x be Element of X;
  mode INT-Exec of x -> ExecutionFunction of FreeUnivAlgNSG(ECIW-signature,
    INT-ElemIns X), Funcs(X, INT), Funcs(X,INT)\(x,0) means
    for s being Element of
    Funcs(X, INT) for v being Element of Funcs(Funcs(X, INT), X) for e being
Element of Funcs(Funcs(X, INT), INT) holds it.(s, root-tree [v,e]) = s+*(v.s,e.
    s);
  existence
  proof
    reconsider i0 = 0 as Element of INT by INT_1:def 1;
    set Q = Funcs(X, INT), T = Q\(x,0);
    set S = ECIW-signature, G = INT-ElemIns X;
    set A = FreeUnivAlgNSG(S,G);
A1: Terminals DTConUA(S,G) = G by FREEALG:3;
    reconsider q0 = X-->i0 as Element of Q by FUNCT_2:8;
    defpred P[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);
A2: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
A3: 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
A4:   s in Q and
A5:   I in ElementaryInstructions A and
A6:   x = [s,I] by ZFMISC_1:def 2;
      reconsider s as Element of Q by A4;
      consider a being Symbol of DTConUA(S,G) such that
A7:   I = root-tree a and
A8:   a in Terminals DTConUA(S,G) by A2,A5;
      consider v,e being set such that
A9:   v in Funcs(Funcs(X, INT), X) and
A10:  e in Funcs(Funcs(X, INT), INT) and
A11:  a = [v,e] by A1,A8,ZFMISC_1:def 2;
      reconsider e as Element of Funcs(Q, INT) by A10;
      reconsider v as Element of Funcs(Q, X) by A9;
      take y = s+*(v.s,e.s);
      thus y in Q by FUNCT_2:8;
      take s,v,e;
      thus x = [s, root-tree [v,e]] & y = s+*(v.s,e.s) by A6,A7,A11;
    end;
    consider g being Function such that
A12: dom g = [:Q,ElementaryInstructions A:] & rng g c= Q and
A13: for x being set st x in [:Q,ElementaryInstructions A:] holds P[x,
    g.x] from FUNCT_1:sch 5(A3);
    reconsider g as Function of [:Q,ElementaryInstructions A:], Q by A12,
FUNCT_2:2;
    consider f being ExecutionFunction of A, Q, T such that
A14: f|[:Q,ElementaryInstructions A:] = g and
    for s being Element of Q for C,I being Element of A st not f
iteration_terminates_for I\;C, f.(s,C) holds f.(s, while(C,I)) = q0 by
AOFA_000:91;
    take f;
    let s be Element of Funcs(X, INT);
    let v be Element of Funcs(Funcs(X, INT), X);
    let e be Element of Funcs(Funcs(X, INT), INT);
    set I = root-tree [v,e];
    [v,e] in G by ZFMISC_1:87;
    then I in ElementaryInstructions A by A2,A1;
    then
A15: [s,I] in [:Q,ElementaryInstructions A:] by ZFMISC_1:87;
    then consider
    s9 being (Element of Q), v9 being (Element of Funcs(Q, X)), e9
    being Element of Funcs(Q, INT) such that
A16: [s,I] = [s9, root-tree [v9,e9]] and
A17: g.[s,I] = s9+*(v9.s9,e9.s9) by A13;
    I = root-tree [v9,e9] by A16,XTUPLE_0:1;
    then
A18: [v,e] = [v9,e9] by TREES_4:4;
    then
A19: v = v9 by XTUPLE_0:1;
A20: e = e9 by A18,XTUPLE_0:1;
    s = s9 by A16,XTUPLE_0:1;
    hence thesis by A14,A15,A17,A19,A20,FUNCT_1:49;
  end;
end;

definition
  let X be non empty set;
  let T be Subset of Funcs(X, INT);
  let c be Enumeration of X such that
A1: rng c c= NAT;
  mode INT-Exec of c,T -> ExecutionFunction of FreeUnivAlgNSG(ECIW-signature,
    INT-ElemIns), Funcs(X, INT), T means
    : Def28:
    for s being Element of Funcs(X,
    INT) for v being Element of Funcs(Funcs(X, INT), X) for e being Element of
Funcs(Funcs(X, INT), INT) holds it.(s, root-tree [(c*v)**(c,NAT),e**(c,NAT)]) =
    s+*(v.s,e.s);
  existence
  proof
    dom c = X by Th6;
    then reconsider c9 = c as Function of X, NAT by A1,FUNCT_2:2;
    reconsider i0 = 0 as Element of INT by INT_1:def 1;
    set Q = Funcs(X, INT);
    set S = ECIW-signature, G = INT-ElemIns;
    set A = FreeUnivAlgNSG(S,G);
    reconsider q0 = X-->i0 as Element of Q by FUNCT_2:8;
A1: 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)**(c9,NAT),e**(c9,NAT)]) or ex v being (Element of Funcs
(Q, X)), e being Element of Funcs(Q, INT) st $1`2 = root-tree [(c*v)**(c9,NAT),
    e**(c9,NAT)] & $2 = s+*(v.s,e.s));
A2: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
A3: 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
A4:   s in Q and
A5:   I in ElementaryInstructions A and
A6:   x = [s,I] by ZFMISC_1:def 2;
A7:   x`1 = s by A6,MCART_1:7;
      reconsider s as Element of Q by A4;
A8:   x`2 = I by A6,MCART_1:7;
      consider a being Symbol of DTConUA(S,G) such that
A9:  I = root-tree a and
      a in Terminals DTConUA(S,G) by A2,A5;
      per cases;
      suppose
        ex v being (Element of Funcs(Q, X)), e being Element of Funcs
        (Q, INT) st a = [(c*v)**(c9,NAT),e**(c9,NAT)];
        then consider
        v being (Element of Funcs(Q, X)), e being Element of Funcs(Q,
        INT) such that
A10:    a = [(c*v)**(c9,NAT),e**(c9,NAT)];
        take y = s+*(v.s,e.s);
        thus y in Q by FUNCT_2:8;
        thus thesis by A7,A8,A9,A10;
      end;
      suppose
A11:    not ex v being (Element of Funcs(Q, X)), e being Element of
        Funcs(Q, INT) st a = [(c*v)**(c9,NAT),e**(c9,NAT)];
        take y = s;
        thus y in Q;
        not ex v being (Element of Funcs(Q, X)), e being Element of Funcs
(Q, INT) st x`2 = root-tree [(c*v)**(c9,NAT),e**(c9,NAT)] by A8,A9,A11,
TREES_4:4;
        hence thesis by A7;
      end;
    end;
    consider g being Function such that
A12: dom g = [:Q,ElementaryInstructions A:] & rng g c= Q and
A13: for x being set st x in [:Q,ElementaryInstructions A:] holds P[x,
    g.x] from FUNCT_1:sch 5(A3);
    reconsider g as Function of [:Q,ElementaryInstructions A:], Q by A12,
FUNCT_2:2;
    consider f being ExecutionFunction of A, Q, T such that
A14: f|[:Q,ElementaryInstructions A:] = g and
    for s being Element of Q for C,I being Element of A st not f
iteration_terminates_for I\;C, f.(s,C) holds f.(s, while(C,I)) = q0 by
AOFA_000:91;
    take f;
    let s be Element of Funcs(X, INT);
    let v be Element of Funcs(Funcs(X, INT), X);
    let e be Element of Funcs(Funcs(X, INT), INT);
    reconsider vv = v as Function of Funcs(X, INT), X;
    reconsider cv = c9*vv as Element of Funcs(Funcs(X, INT), NAT) by FUNCT_2:8
;
    set v0 = cv**(c9,NAT), e0 = e**(c9,NAT);
    set I = root-tree [v0,e0];
    [v0,e0] in G by ZFMISC_1:87;
    then I in ElementaryInstructions A by A2,A1;
    then
A15: [s,I] in [:Q,ElementaryInstructions A:] by ZFMISC_1:87;
    then P[[s,I],g.[s,I]] by A13;
    then consider
    v9 being (Element of Funcs(Q, X)), e9 being Element of Funcs(Q,
    INT) such that
A16: [s,I]`2 = root-tree [(c*v9)**(c9,NAT),e9**(c9,NAT)] and
A17: g.[s,I] = s+*(v9.s,e9.s);
A18: dom (c9*v9) = Q by FUNCT_2:def 1;
A19: dom e = Q by FUNCT_2:def 1;
A20: dom v = Q by FUNCT_2:def 1;
A21: dom cv = Q by FUNCT_2:def 1;
A22: dom c9 = X by FUNCT_2:def 1;
A23: rng v c= X;
A24: dom e9 = Q by FUNCT_2:def 1;
A25: dom v9 = Q by FUNCT_2:def 1;
A26: [v0,e0] = [(c*v9)**(c9,NAT),e9**(c9,NAT)] by A16,TREES_4:4;
    then v0 = (c*v9)**(c9,NAT) by XTUPLE_0:1;
    then
A27: cv = c*v9 by A21,A18,Th5;
    e0 = e9**(c9,NAT) by A26,XTUPLE_0:1;
    then
A28: e = e9 by A19,A24,Th5;
    rng v9 c= X;
    then v = v9 by A23,A22,A25,A20,A27,FUNCT_1:27;
    hence thesis by A14,A15,A17,A28,FUNCT_1:49;
  end;
end;

theorem Th16:
  for f being INT-Exec for v being INT-Variable of NAT for t being
  INT-Expression of NAT holds v,t form_assignment_wrt f
proof
  let f be INT-Exec;
  set S = ECIW-signature, G = INT-ElemIns;
  set X = NAT;
  set A = FreeUnivAlgNSG(S,G);
  let v be INT-Variable of NAT;
  let t be INT-Expression of NAT;
  reconsider v9 = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:8;
  reconsider t9 = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:8;
A1: Terminals DTConUA(S,G) = G by FREEALG:3;
A2: [v9,t9] in G by ZFMISC_1:87;
A3: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
  then root-tree [v9,t9] in ElementaryInstructions A by A1,A2;
  then reconsider I = root-tree [v9,t9] as Element of A;
  take I;
  thus I in ElementaryInstructions A by A3,A1,A2;
  thus thesis by Def25;
end;

theorem Th17:
  for f being INT-Exec for v being INT-Variable of NAT holds v is
  INT-Variable of FreeUnivAlgNSG(ECIW-signature, INT-ElemIns), f
proof
  set t = the INT-Expression of NAT;
  let f be INT-Exec;
  set S = ECIW-signature, G = INT-ElemIns;
  set X = NAT;
  set A = FreeUnivAlgNSG(S,G);
  let v be INT-Variable of NAT;
A1: Terminals DTConUA(S,G) = G by FREEALG:3;
  reconsider t9 = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:8;
  reconsider v9 = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:8;
A2: [v9,t9] in G by ZFMISC_1:87;
A3: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
  then root-tree [v9,t9] in ElementaryInstructions A by A1,A2;
  then reconsider I = root-tree [v9,t9] as Element of A;
  hereby
    take I;
    thus I is_assignment_wrt A,X,f
    proof
      thus I in ElementaryInstructions A by A3,A1,A2;
      take v,t;
      thus thesis by Def25;
    end;
  end;
  take t;
  thus thesis by Th16;
end;

theorem Th18:
  for f being INT-Exec for t being INT-Expression of NAT holds t
  is INT-Expression of FreeUnivAlgNSG(ECIW-signature, INT-ElemIns), f
proof
  set v = the INT-Variable of NAT;
  let f be INT-Exec;
  set S = ECIW-signature, G = INT-ElemIns;
  set X = NAT;
  set A = FreeUnivAlgNSG(S,G);
  let t be INT-Expression of NAT;
A1: Terminals DTConUA(S,G) = G by FREEALG:3;
  reconsider t9 = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:8;
  reconsider v9 = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:8;
A2: [v9,t9] in G by ZFMISC_1:87;
A3: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
  then root-tree [v9,t9] in ElementaryInstructions A by A1,A2;
  then reconsider I = root-tree [v9,t9] as Element of A;
  hereby
    take I;
    thus I is_assignment_wrt A,X,f
    proof
      thus I in ElementaryInstructions A by A3,A1,A2;
      take v,t;
      thus thesis by Def25;
    end;
  end;
  take v;
  thus thesis by Th16;
end;

registration
  cluster -> Euclidean for INT-Exec;
  coherence
  proof
    set X = NAT;
    set a = (INT --> 0)+*(id X);
A1: dom id X = X by RELAT_1:45;
A2: INT \/ X = INT by NUMBERS:17,XBOOLE_1:12;
    dom (INT --> 0) = INT by FUNCOP_1:13;
    then
A3: dom a = INT by A1,A2,FUNCT_4:def 1;
A4: rng id X = X by RELAT_1:45;
    {0} c= X by ZFMISC_1:31;
    then
A5: {0} \/ X = X by XBOOLE_1:12;
    rng (INT --> 0) = {0} by FUNCOP_1:8;
    then rng a c= NAT by A4,A5,FUNCT_4:17;
    then reconsider a as INT-Array of X by A3,FUNCT_2:2;
    let f be INT-Exec;
    set S = ECIW-signature, G = INT-ElemIns;
    set A = FreeUnivAlgNSG(S,G);
    thus for v being INT-Variable of A,f, t being INT-Expression of A,f holds
    v,t form_assignment_wrt f by Th16;
    thus for i being integer number holds .(i,X) is INT-Expression of A,f by
Th18;
    thus for v being INT-Variable of A,f holds .v is INT-Expression of A,f by
Th18;
    thus for x being Element of X holds ^x is INT-Variable of A,f by Th17;
    hereby
      take a;
      dom id X = X by RELAT_1:45;
      hence a|card X is one-to-one by CARD_1:47,FUNCT_4:23;
      thus for t being INT-Expression of A,f holds a*t is INT-Variable of A,f
      by Th17;
    end;
    thus thesis by Th18;
  end;
end;

theorem Th19:
  for X being non empty countable set for T being Subset of Funcs(
  X, INT) for c being Enumeration of X for f being INT-Exec of c,T for v being
INT-Variable of X for t being INT-Expression of X holds v,t form_assignment_wrt
  f
proof
  set S = ECIW-signature, G = INT-ElemIns;
  let X be non empty countable set;
  let T be Subset of Funcs(X, INT);
  let c be Enumeration of X;
  set A = FreeUnivAlgNSG(S,G);
  let f be INT-Exec of c,T;
  let v be INT-Variable of X;
  let t be INT-Expression of X;
  reconsider v9 = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:8;
  reconsider t9 = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:8;
A1: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
A2: rng c c= NAT by Th11;
  dom c = X by Th6;
  then reconsider c9 = c as Function of X,NAT by A2,FUNCT_2:2;
  reconsider cv = c9*v as Element of Funcs(Funcs(X,INT),NAT) by FUNCT_2:8;
  set v1 = cv**(c9,NAT), t1 = t9**(c9,NAT);
A3: Terminals DTConUA(S,G) = G by FREEALG:3;
A4: [v1,t1] in G by ZFMISC_1:87;
  then root-tree [v1,t1] in ElementaryInstructions A by A1,A3;
  then reconsider I = root-tree [v1,t1] as Element of A;
  take I;
  for s being Element of Funcs(X, INT) holds f.(s, root-tree [(c*v9)**(c,
  NAT),t9**(c,NAT)]) = s+*(v9.s,t9.s) by A2,Def28;
  hence thesis by A1,A3,A4;
end;

theorem Th20:
  for X being non empty countable set for T being Subset of Funcs(
  X, INT) for c being Enumeration of X for f being INT-Exec of c,T for v being
  INT-Variable of X holds v is INT-Variable of FreeUnivAlgNSG(ECIW-signature,
  INT-ElemIns), f
proof
  set S = ECIW-signature, G = INT-ElemIns;
  let X be non empty countable set;
  let T be Subset of Funcs(X, INT);
  let c be Enumeration of X;
  set A = FreeUnivAlgNSG(S,G);
  let f be INT-Exec of c,T;
  let v be INT-Variable of X;
  set t = the INT-Expression of X;
A1: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
A2: rng c c= NAT by Th11;
  dom c = X by Th6;
  then reconsider c9 = c as Function of X,NAT by A2,FUNCT_2:2;
  reconsider cv = c9*v as Element of Funcs(Funcs(X,INT),NAT) by FUNCT_2:8;
  reconsider v9 = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:8;
  reconsider t9 = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:8;
A3: Terminals DTConUA(S,G) = G by FREEALG:3;
  set v1 = cv**(c9,NAT), t1 = t9**(c9,NAT);
A4: [v1,t1] in G by ZFMISC_1:87;
  then root-tree [v1,t1] in ElementaryInstructions A by A1,A3;
  then reconsider I = root-tree [v1,t1] as Element of A;
  hereby
    take I;
    thus I is_assignment_wrt A,X,f
    proof
      thus I in ElementaryInstructions A by A1,A3,A4;
      take v,t;
      for s being Element of Funcs(X, INT) holds f.(s, root-tree [(c*v9)**
      (c,NAT),t9**(c,NAT)]) = s+*(v9.s,t9.s) by A2,Def28;
      hence thesis;
    end;
  end;
  take t;
  thus thesis by Th19;
end;

theorem Th21:
  for X being non empty countable set for T being Subset of Funcs(
  X, INT) for c being Enumeration of X for f being INT-Exec of c,T for t being
INT-Expression of X holds t is INT-Expression of FreeUnivAlgNSG(ECIW-signature,
  INT-ElemIns), f
proof
  set S = ECIW-signature, G = INT-ElemIns;
  let X be non empty countable set;
  let T be Subset of Funcs(X, INT);
  let c be Enumeration of X;
  set A = FreeUnivAlgNSG(S,G);
  let f be INT-Exec of c,T;
  set v = the INT-Variable of X;
  let t be INT-Expression of X;
A1: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
A2: rng c c= NAT by Th11;
  dom c = X by Th6;
  then reconsider c9 = c as Function of X,NAT by A2,FUNCT_2:2;
  reconsider cv = c9*v as Element of Funcs(Funcs(X,INT),NAT) by FUNCT_2:8;
  reconsider v9 = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:8;
  reconsider t9 = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:8;
A3: Terminals DTConUA(S,G) = G by FREEALG:3;
  set v1 = cv**(c9,NAT), t1 = t9**(c9,NAT);
A4: [v1,t1] in G by ZFMISC_1:87;
  then root-tree [v1,t1] in ElementaryInstructions A by A1,A3;
  then reconsider I = root-tree [v1,t1] as Element of A;
  hereby
    take I;
    thus I is_assignment_wrt A,X,f
    proof
      thus I in ElementaryInstructions A by A1,A3,A4;
      take v,t;
      for s being Element of Funcs(X, INT) holds f.(s, root-tree [(c*v9)**
      (c,NAT),t9**(c,NAT)]) = s+*(v9.s,t9.s) by A2,Def28;
      hence thesis;
    end;
  end;
  take v;
  thus thesis by Th19;
end;

registration
  let X be countable non empty set;
  let T be Subset of Funcs(X, INT);
  let c be Enumeration of X;
  cluster -> Euclidean for INT-Exec of c,T;
  coherence
  proof
A1: rng c c= NAT by Th11;
    card X = rng c by Th6;
    then
A2: INT \/ card X = INT by A1,NUMBERS:17,XBOOLE_1:1,12;
    set x = c".0;
    set a = (INT --> x)+*(c");
A3: dom (INT --> x) = INT by FUNCOP_1:13;
A4: rng (INT --> x) = {x} by FUNCOP_1:8;
    x in X by FUNCT_2:5,ORDINAL3:8;
    then {x} c= X by ZFMISC_1:31;
    then
A5: {x} \/ X = X by XBOOLE_1:12;
    rng (c") = X by Th7;
    then
A6: rng a c= X by A4,A5,FUNCT_4:17;
    dom (c") = card X by Th7;
    then dom a = INT by A3,A2,FUNCT_4:def 1;
    then reconsider a as INT-Array of X by A6,FUNCT_2:2;
    let f be INT-Exec of c,T;
    set S = ECIW-signature, G = INT-ElemIns;
    set A = FreeUnivAlgNSG(S,G);
    thus for v being INT-Variable of A,f, t being INT-Expression of A,f holds
    v,t form_assignment_wrt f by Th19;
    thus for i being integer number holds .(i,X) is INT-Expression of A,f by
Th21;
    thus for v being INT-Variable of A,f holds .v is INT-Expression of A,f by
Th21;
    thus for x being Element of X holds ^x is INT-Variable of A,f by Th20;
    hereby
      take a;
      dom (c") = card X by Th7;
      hence a|card X is one-to-one by FUNCT_4:23;
      thus for t being INT-Expression of A,f holds a*t is INT-Variable of A,f
      by Th20;
    end;
    thus thesis by Th21;
  end;
end;

registration
  cluster FreeUnivAlgNSG(ECIW-signature, INT-ElemIns) -> Euclidean;
  coherence
  proof
    let X be non empty countable set, T be Subset of Funcs(X, INT);
    set c = the Enumeration of X;
    set f = the INT-Exec of c, T;
    take f;
    thus thesis;
  end;
end;

registration
  cluster Euclidean non degenerated for preIfWhileAlgebra;
  existence
  proof
    take FreeUnivAlgNSG(ECIW-signature, INT-ElemIns);
    thus thesis;
  end;
end;

registration
  let A be Euclidean preIfWhileAlgebra;
  let X be non empty countable set;
  let T be Subset of Funcs(X, INT);
  cluster Euclidean for ExecutionFunction of A, Funcs(X, INT), T;
  existence by Def23;
end;

:: Arithmetic of Expressions

reserve A for Euclidean preIfWhileAlgebra;
reserve X for non empty countable set;
reserve T for Subset of Funcs(X, INT);
reserve f for Euclidean ExecutionFunction of A, Funcs(X, INT), T;

definition
  let A,X,T,f;
  let t be INT-Expression of A,f;
  redefine func -t -> INT-Expression of A,f;
  coherence by Def22;
end;

definition
  let A,X,T,f;
  let t be INT-Expression of A,f;
  let i be integer number;
  redefine func t+i -> INT-Expression of A,f;
  coherence
  proof
A1: dom (t+.(i,X)) = Funcs(X,INT) by FUNCT_2:def 1;
A2: 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 A1,VALUED_1:def 1
        .= i+(t.a) by FUNCOP_1:7;
    end;
    .(i,X) is INT-Expression of A,f by Def22;
    then
A3: t+.(i,X) is INT-Expression of A,f by Def22;
    dom t = Funcs(X,INT) by FUNCT_2:def 1;
    hence thesis by A3,A1,A2,VALUED_1:def 2;
  end;
  redefine func t-i -> INT-Expression of A,f;
  coherence
  proof
    .(i,X) is INT-Expression of A,f by Def22;
    then -.(i,X) is INT-Expression of A,f by Def22;
    then
A4: t+-.(i,X) is INT-Expression of A,f by Def22;
A5: dom t = Funcs(X,INT) by FUNCT_2:def 1;
A6: dom (t+-.(i,X)) = Funcs(X,INT) by FUNCT_2:def 1;
A7: now
      let a be 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 A6,VALUED_1:def 1
        .= (t.s)+-(.(i,X).s) by VALUED_1:8
        .= (t.s)-i by FUNCOP_1:7
        .= (t-i).a by A5,VALUED_1:3;
    end;
    dom (t-i) = dom t by VALUED_1:3;
    hence thesis by A4,A6,A5,A7,FUNCT_1:2;
  end;
  redefine func t*i -> INT-Expression of A,f;
  coherence
  proof
A8: dom (t(#).(i,X)) = Funcs(X,INT) by FUNCT_2:def 1;
A9: 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 A8,VALUED_1:def 4
        .= i*(t.a) by FUNCOP_1:7;
    end;
    .(i,X) is INT-Expression of A,f by Def22;
    then
A10: t(#).(i,X) is INT-Expression of A,f by Def22;
    dom t = Funcs(X,INT) by FUNCT_2:def 1;
    hence thesis by A10,A8,A9,VALUED_1:def 5;
  end;
end;

definition
  let A,X,T,f;
  let t1,t2 be INT-Expression of A,f;
  redefine func t1-t2 -> INT-Expression of A,f;
  coherence
  proof
    -t2 is INT-Expression of A,f;
    hence thesis by Def22;
  end;
  redefine func t1+t2 -> INT-Expression of A,f;
  coherence by Def22;
  redefine func t1(#)t2 -> INT-Expression of A,f;
  coherence by Def22;
end;

definition
  let A,X,T,f;
  let t1,t2 be INT-Expression of A,f;
  redefine func t1 div t2 -> INT-Expression of A,f means
  : Def29:
  for s being Element of Funcs(X, INT) holds it.s = t1.s div t2.s;
  coherence by Def22;
  compatibility
  proof
    let ti be INT-Expression of A,f;
A1: dom t1 = Funcs(X, INT) by FUNCT_2:def 1;
A2: dom t2 = Funcs(X, INT) by FUNCT_2:def 1;
A3: dom (t1 div t2) = (dom t1)/\dom t2 by Def3;
    hence
    ti = t1 div t2 implies for s being Element of Funcs(X, INT) holds ti.
    s = t1.s div t2.s by A1,A2,Def3;
A4: dom ti = Funcs(X, INT) by FUNCT_2:def 1;
    assume for s being Element of Funcs(X, INT) holds ti.s = t1.s div t2.s;
    then for s being set st s in Funcs(X, INT) holds ti.s = t1.s div t2.s;
    hence ti = t1 div t2 by A3,A1,A2,A4,Def3;
  end;
  redefine func t1 mod t2 -> INT-Expression of A,f means
  : Def30:
  for s being Element of Funcs(X, INT) holds it.s = t1.s mod t2.s;
  coherence by Def22;
  compatibility
  proof
    let ti be INT-Expression of A,f;
A5: dom t1 = Funcs(X, INT) by FUNCT_2:def 1;
A6: dom t2 = Funcs(X, INT) by FUNCT_2:def 1;
A7: dom (t1 mod t2) = (dom t1)/\dom t2 by Def4;
    hence
    ti = t1 mod t2 implies for s being Element of Funcs(X, INT) holds ti.
    s = t1.s mod t2.s by A5,A6,Def4;
A8: dom ti = Funcs(X, INT) by FUNCT_2:def 1;
    assume for s being Element of Funcs(X, INT) holds ti.s = t1.s mod t2.s;
    then for s being set st s in Funcs(X, INT) holds ti.s = t1.s mod t2.s;
    hence ti = t1 mod t2 by A7,A5,A6,A8,Def4;
  end;
  redefine func leq(t1,t2) -> INT-Expression of A,f means
  : Def31:
  for s being Element of Funcs(X, INT) holds it.s = IFGT(t1.s,t2.s,0,1);
  compatibility
  proof
    let ti be INT-Expression of A,f;
A9: dom t1 = Funcs(X, INT) by FUNCT_2:def 1;
A10: dom t2 = Funcs(X, INT) by FUNCT_2:def 1;
A11: dom leq(t1,t2) = (dom t1)/\dom t2 by Def5;
    hence
    ti = leq(t1,t2) implies for s being Element of Funcs(X, INT) holds ti
    .s = IFGT(t1.s,t2.s,0,1) by A9,A10,Def5;
A12: dom ti = Funcs(X, INT) by FUNCT_2:def 1;
    assume
    for s being Element of Funcs(X, INT) holds ti.s = IFGT(t1.s,t2.s, 0,1);
    then
    for s being set st s in Funcs(X, INT) holds ti.s = IFGT(t1.s,t2.s,0,1 );
    hence ti = leq(t1,t2) by A11,A9,A10,A12,Def5;
  end;
  coherence by Def22;
  redefine func gt(t1,t2) -> INT-Expression of A,f means
  : Def32:
  for s being Element of Funcs(X, INT) holds it.s = IFGT(t1.s,t2.s,1,0);
  coherence by Def22;
  compatibility
  proof
    let ti be INT-Expression of A,f;
A13: dom t1 = Funcs(X, INT) by FUNCT_2:def 1;
A14: dom t2 = Funcs(X, INT) by FUNCT_2:def 1;
A15: dom gt(t1,t2) = (dom t1)/\dom t2 by Def6;
    hence
    ti = gt(t1,t2) implies for s being Element of Funcs(X, INT) holds ti.
    s = IFGT(t1.s,t2.s,1,0) by A13,A14,Def6;
A16: dom ti = Funcs(X, INT) by FUNCT_2:def 1;
    assume
    for s being Element of Funcs(X, INT) holds ti.s = IFGT(t1.s,t2.s, 1,0);
    then
    for s being set st s in Funcs(X, INT) holds ti.s = IFGT(t1.s,t2.s,1,0 );
    hence ti = gt(t1,t2) by A15,A13,A14,A16,Def6;
  end;
end;

definition
  let A,X,T,f;
  let t1,t2 be INT-Expression of A,f;
  redefine func eq(t1,t2) -> INT-Expression of A,f means
  for s being Element of Funcs(X , INT) holds it.s = IFEQ(t1.s,t2.s,1,0);
  compatibility
  proof
    let ti be INT-Expression of A,f;
A1: dom t1 = Funcs(X, INT) by FUNCT_2:def 1;
A2: dom t2 = Funcs(X, INT) by FUNCT_2:def 1;
A3: dom eq(t1,t2) = (dom t1)/\dom t2 by Def7;
    hence
    ti = eq(t1,t2) implies for s being Element of Funcs(X, INT) holds ti.
    s = IFEQ(t1.s,t2.s,1,0) by A1,A2,Def7;
A4: dom ti = Funcs(X, INT) by FUNCT_2:def 1;
    assume
    for s being Element of Funcs(X, INT) holds ti.s = IFEQ(t1.s,t2.s,1 ,0);
    then
    for s being set st s in Funcs(X, INT) holds ti.s = IFEQ(t1.s,t2.s,1,0);
    hence ti = eq(t1,t2) by A3,A1,A2,A4,Def7;
  end;
  coherence
  proof
    reconsider l1 = leq(t1,t2), l2 = leq(t2,t1) as INT-Expression of A,f;
A5: dom (l1(#)l2) = Funcs(X,INT) by FUNCT_2:def 1;
A6: dom eq(t1,t2) = Funcs(X,INT) by FUNCT_2:def 1;
    now
      let a be set;
      assume a in Funcs(X,INT);
      then reconsider s = a as Element of Funcs(X,INT);
A7:   t1.s = t2.s or t1.s < t2.s or t2.s < t1.s by XXREAL_0:1;
A8:   l2.s = IFGT(t2.s,t1.s,0,1) by Def31;
A9:   (l1(#)l2).s = (l1.s)*(l2.s) by A5,VALUED_1:def 4;
A10:  l1.s = IFGT(t1.s,t2.s,0,1) by Def31;
      eq(t1,t2).s = IFEQ(t1.s,t2.s,1,0) by A6,Def7;
      then
      eq(t1,t2).s = 1 & l1.s = 1 & l2.s = 1 or eq(t1,t2).s = 0 & l1.s = 0
      & l2.s = 1 or eq(t1,t2).s = 0 & l1.s = 1 & l2.s = 0 by A8,A10,A7,
FUNCOP_1:def 8,XXREAL_0:def 11;
      hence eq(t1,t2).a = (l1(#)l2).a by A9;
    end;
    hence thesis by A6,A5,FUNCT_1:2;
  end;
end;

definition
  let A,X,T,f;
  let v be INT-Variable of A,f;
  func .v -> INT-Expression of A,f equals
  .v;
  coherence by Def22;
end;

definition
  let A,X,T,f;
  let x be Element of X;
  func x^(A,f) -> INT-Variable of A,f equals
  ^x;
  coherence by Def22;
end;

notation
  let A,X,T,f;
  let x be Variable of f;
  synonym ^x for x^(A,f);
end;

definition
  let A,X,T,f;
  let x be Variable of f;
  func .x -> INT-Expression of A,f equals
  .(^x);
  coherence;
end;

theorem Th22:
  for x being Variable of f for s being Element of Funcs(X, INT)
  holds (.x).s = s.x
proof
  let x be Variable of f;
  let s be Element of Funcs(X, INT);
  thus (.x).s = s.((x^(A,f)).s) by Def19
    .= s.x by FUNCOP_1:7;
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 Def22;
end;

definition :: "choose" function may cause some problems in further development.
  let A,X,T,f;
  let v be INT-Variable of A,f;
  let t be INT-Expression of A,f;
  func v:=t -> Element of A equals
  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)};
A1: 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;
    v,t form_assignment_wrt f by Def22;
    then consider I0 being Element of A such that
A2: I0 in ElementaryInstructions A and
A3: for s being Element of Funcs(X, INT) holds f.(s,I0) = s+*(v.s,t.s)
    by Def15;
    I0 in Y by A2,A3;
    then choose Y in Y;
    hence thesis by A1;
  end;
end;

theorem Th23:
  for v being INT-Variable of A,f for t being INT-Expression of A,
  f holds v:=t in ElementaryInstructions A
proof
  let v be INT-Variable of A,f;
  let t be INT-Expression of A,f;
  set Y = {I where I is Element of A: I in ElementaryInstructions A & for s
  being Element of Funcs(X, INT) holds f.(s,I) = s+*(v.s,t.s)};
  v,t form_assignment_wrt f by Def22;
  then consider I0 being Element of A such that
A1: I0 in ElementaryInstructions A and
A2: for s being Element of Funcs(X, INT) holds f.(s,I0) = s+*(v.s,t.s)
  by Def15;
  I0 in Y by A1,A2;
  then v:=t in Y;
  then ex I being Element of A st v:=t = I & I in ElementaryInstructions A &
  for s being Element of Funcs(X, INT) holds f.(s,I) = s+*(v.s,t.s);
  hence thesis;
end;

registration
  let A,X,T,f;
  let v be INT-Variable of A,f;
  let t be INT-Expression of A,f;
  cluster v:=t -> absolutely-terminating;
  coherence by Th23,AOFA_000:95;
end;

definition
  let A,X,T,f;
  let v be INT-Variable of A,f;
  let t be INT-Expression of A,f;
  func v+=t -> absolutely-terminating Element of A equals
  v:=(.v+t);
  coherence;
  func v*=t -> absolutely-terminating Element of A equals
  v:=(.v(#)t);
  coherence;
end;

definition
  let A,X,T,f;
  let x be Element of X;
  let t be INT-Expression of A,f;
  func x:=t -> absolutely-terminating Element of A equals
  x^(A,f):=t;
  correctness;
end;

definition
  let A,X,T,f;
  let x be Element of X;
  let y be Variable of f;
  func x:=y -> absolutely-terminating Element of A equals
  x:=.y;
  correctness;
end;

definition
  let A,X,T,f;
  let x be Element of X;
  let v be INT-Variable of A,f;
  func x:=v -> absolutely-terminating Element of A equals
  x:=.v;
  correctness;
end;

definition
  let A,X,T,f;
  let v,w be INT-Variable of A,f;
  func v:=w -> absolutely-terminating Element of A equals
  v:=.w;
  correctness;
end;

definition
  let A,X,T,f;
  let x be Variable of f;
  let i be integer 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,
   z for (Element of X),
  s,s9 for (Element of Funcs(X, INT)),
  T for Subset of Funcs(X, INT),
  f for Euclidean ExecutionFunction of A, Funcs(X, INT), T,
  v for INT-Variable of A,f,
  t for INT-Expression of A,f;
reserve i for integer number;

theorem Th24:
  f.(s, v:=t).(v.s) = t.s & for z st z <> v.s holds f.(s, v:=t).z = s.z
proof
  set Y = {I where I is Element of A: I in ElementaryInstructions A & for s
  being Element of Funcs(X, INT) holds f.(s,I) = s+*(v.s,t.s)};
  v,t form_assignment_wrt f by Def22;
  then consider I0 being Element of A such that
A1: I0 in ElementaryInstructions A and
A2: for s being Element of Funcs(X, INT) holds f.(s,I0) = s+*(v.s,t.s)
  by Def15;
  I0 in Y by A1,A2;
  then v:=t in Y;
  then
  ex I being Element of A st v:=t = I & I in ElementaryInstructions A &
  for s being Element of Funcs(X, INT) holds f.(s,I) = s+*(v.s,t.s);
  then
A3: f.(s, v:=t) = s+*(v.s,t.s);
  dom s = X by FUNCT_2:def 1;
  hence thesis by A3,FUNCT_7:31,32;
end;

theorem Th25:
  for x being Variable of f for i being integer 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;
A1: .(i,A,f).s = i by FUNCOP_1:7;
  (^x).s = x by FUNCOP_1:7;
  hence thesis by A1,Th24;
end;

theorem Th26:
  for x being Variable of f for t being INT-Expression of A,f
  holds f.(s, x:=t).x = t.s & for z st z <> x holds f.(s, x:=t).z = s.z
proof
  let x be Variable of f;
  let t be INT-Expression of A,f;
  (^x).s = x by FUNCOP_1:7;
  hence thesis by Th24;
end;

theorem Th27:
  for x,y being Variable of f holds f.(s, x:=y).x = s.y & for z st
  z <> x holds f.(s, x:=y).z = s.z
proof
  let x,y be Variable of f;
  (.y).s = s.y by Th22;
  hence thesis by Th26;
end;

theorem Th28:
  for x being Variable of f holds f.(s, x+=i).x = s.x+i & for z st
  z <> x holds f.(s, x+=i).z = s.z
proof
  let x be Variable of f;
A1: (^x).s = x by FUNCOP_1:7;
A2: .(^(x qua Element of X)).s = s.((^(x qua Element of X)).s) by Def19;
  (.x+i).s = ((.x).s+i) by Def8;
  hence thesis by A1,A2,Th24;
end;

theorem Th29:
  for x being Variable of f for t being INT-Expression of A,f
  holds f.(s, x+=t).x = s.x+t.s & for z st z <> x holds f.(s, x+=t).z = s.z
proof
  let x be Variable of f;
  let t be INT-Expression of A,f;
A1: (^x).s = x by FUNCOP_1:7;
  dom (.x+t) = Funcs(X, INT) by FUNCT_2:def 1;
  then
A2: (.x+t).s = (.x).s+t.s by VALUED_1:def 1;
  (.x).s = s.x by Th22;
  hence thesis by A1,A2,Th24;
end;

theorem Th30:
  for x,y being Variable of f holds f.(s, x+=y).x = s.x+s.y & for
  z st z <> x holds f.(s, x+=y).z = s.z
proof
  let x,y be Variable of f;
  (.y).s = s.y by Th22;
  hence thesis by Th29;
end;

theorem Th31:
  for x being Variable of f holds f.(s, x*=i).x = s.x*i & for z st
  z <> x holds f.(s, x*=i).z = s.z
proof
  let x be Variable of f;
A1: (^x).s = x by FUNCOP_1:7;
A2: .(^(x qua Element of X)).s = s.((^(x qua Element of X)).s) by Def19;
  (.x*i).s = ((.x).s*i) by Def10;
  hence thesis by A1,A2,Th24;
end;

theorem Th32:
  for x being Variable of f for t being INT-Expression of A,f
  holds f.(s, x*=t).x = s.x*t.s & for z st z <> x holds f.(s, x*=t).z = s.z
proof
  let x be Variable of f;
  let t be INT-Expression of A,f;
A1: (^x).s = x by FUNCOP_1:7;
  dom (.x(#)t) = Funcs(X, INT) by FUNCT_2:def 1;
  then
A2: (.x(#)t).s = (.x).s*t.s by VALUED_1:def 4;
  (.x).s = s.x by Th22;
  hence thesis by A1,A2,Th24;
end;

theorem Th33:
  for x,y being Variable of f holds f.(s, x*=y).x = s.x*s.y & for
  z st z <> x holds f.(s, x*=y).z = s.z
proof
  let x,y be Variable of f;
A1: dom (.x(#).y) = Funcs(X, INT) by FUNCT_2:def 1;
  (^x).s = x by FUNCOP_1:7;
  hence f.(s, x*=y).x = (.x(#).y).s by Th24
    .= ((.x).s)*(.y.s) by A1,VALUED_1:def 4
    .= (s.x)*(.y.s) by Th22
    .= (s.x)*(s.y) by Th22;
  thus thesis by Th26;
end;

theorem Th34:
  for b being Element of X for g being Euclidean ExecutionFunction
  of A,Funcs(X,INT), Funcs(X,INT)\(b,0) for x being Variable of g holds for i
  being integer 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);
  reconsider b9 = b as Variable of f by Def2;
  let x be Variable of f;
  let i be integer number;
  set v = ^b9;
A1: (.(i,A,f)).s = i by FUNCOP_1:7;
A2: v.s = b by FUNCOP_1:7;
A3: (.x).s < i implies IFGT(i,(.x).s,0,1) = 0 by XXREAL_0:def 11;
A4: (.x).s >= i implies IFGT(i,(.x).s,0,1) = 1 by XXREAL_0:def 11;
A5: leq(.(i,A,f),.x).s = IFGT(.(i,A,f).s,(.x).s,0,1) by Def31;
A6: (.x).s > i implies IFGT((.x).s,i,0,1) = 0 by XXREAL_0:def 11;
A7: leq(.x,.(i,A,f)).s = IFGT((.x).s,.(i,A,f).s,0,1) by Def31;
A8: (.x).s <= i implies IFGT((.x).s,i,0,1) = 1 by XXREAL_0:def 11;
  (.x).s = s.((^x).s) by Def19;
  hence thesis by A1,A2,A8,A6,A4,A3,A7,A5,Th24,FUNCOP_1:7;
end;

theorem Th35:
  for b being Element of X for g being Euclidean ExecutionFunction
of A,Funcs(X,INT), Funcs(X,INT)\(b,0) for x,y being Variable of g holds (s.x <=
s.y implies g.(s, x leq y).b = 1) & (s.x > s.y implies g.(s, x leq y).b = 0) &
  for z st z <> b holds g.(s, x leq y).z = s.z
proof
  let b be Element of X;
  let f be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
  reconsider b9 = b as Variable of f by Def2;
  let x,y be Variable of f;
  set v = ^b9;
A1: v.s = b by FUNCOP_1:7;
A2: (.x).s <= .y.s implies IFGT((.x).s,(.y).s,0,1) = 1 by XXREAL_0:def 11;
  (.x).s = s.((^x).s) by Def19;
  then
A3: s.x = (.x).s by FUNCOP_1:7;
A4: (.x).s > .y.s implies IFGT((.x).s,(.y).s,0,1) = 0 by XXREAL_0:def 11;
A5: leq(.x,.y).s = IFGT((.x).s,(.y).s,0,1) by Def31;
  (.y).s = s.((^y).s) by Def19;
  hence thesis by A3,A1,A2,A4,A5,Th24,FUNCOP_1:7;
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 Th2;
  hence s.x <= i iff g.(s, x leq i) in Funcs(X,INT)\(b,0) by Th34;
  g.(s, x geq i) in Funcs(X,INT)\(b,0) iff g.(s, x geq i).b <> 0 by Th2;
  hence thesis by Th34;
end;

theorem
  for b being Element of X for g being Euclidean ExecutionFunction of A,
Funcs(X,INT), Funcs(X,INT)\(b,0) for x,y being Variable of g holds (s.x <= s.y
  iff g.(s, x leq y) in Funcs(X,INT)\(b,0)) & (s.x >= s.y iff g.(s, x geq y) in
  Funcs(X,INT)\(b,0))
proof
  let b be Element of X;
  let g be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
  let x,y be Variable of g;
  g.(s, x leq y) in Funcs(X,INT)\(b,0) iff g.(s, x leq y).b <> 0 by Th2;
  hence s.x <= s.y iff g.(s, x leq y) in Funcs(X,INT)\(b,0) by Th35;
  g.(s, x geq y) in Funcs(X,INT)\(b,0) iff g.(s, x geq y).b <> 0 by Th2;
  hence thesis by Th35;
end;

theorem Th38:
  for b being Element of X for g being Euclidean ExecutionFunction
  of A,Funcs(X,INT), Funcs(X,INT)\(b,0) for x being Variable of g for i being
integer 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);
  reconsider b9 = b as Variable of f by Def2;
  let x be Variable of f;
  let i be integer number;
  set v = ^b9;
A1: (.(i,A,f)).s = i by FUNCOP_1:7;
A2: v.s = b by FUNCOP_1:7;
A3: (.x).s >= i implies IFGT(i,(.x).s,1,0) = 0 by XXREAL_0:def 11;
A4: (.x).s < i implies IFGT(i,(.x).s,1,0) = 1 by XXREAL_0:def 11;
A5: gt(.(i,A,f),.x).s = IFGT((.(i,A,f)).s,(.x).s,1,0) by Def32;
A6: (.x).s <= i implies IFGT((.x).s,i,1,0) = 0 by XXREAL_0:def 11;
A7: gt(.x,.(i,A,f)).s = IFGT((.x).s,(.(i,A,f)).s,1,0) by Def32;
A8: (.x).s > i implies IFGT((.x).s,i,1,0) = 1 by XXREAL_0:def 11;
  (.x).s = s.((^x).s) by Def19;
  hence thesis by A1,A2,A8,A6,A4,A3,A7,A5,Th24,FUNCOP_1:7;
end;

theorem Th39:
  for b being Element of X for g being Euclidean ExecutionFunction
of A,Funcs(X,INT), Funcs(X,INT)\(b,0) for x,y being Variable of g holds (s.x >
s.y implies g.(s, x gt y).b = 1) & (s.x <= s.y implies g.(s, x gt y).b = 0) & (
s.x < s.y implies g.(s, x lt y).b = 1) & (s.x >= s.y implies g.(s, x lt y).b =
  0) & for z st z <> b holds g.(s, x gt y).z = s.z & g.(s, x lt y).z = s.z
proof
  let b be Element of X;
  let f be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
  reconsider b9 = b as Variable of f by Def2;
  let x,y be Variable of f;
  set v = ^b9;
A1: v.s = b by FUNCOP_1:7;
A2: (.x).s > .y.s implies IFGT((.x).s,(.y).s,1,0) = 1 by XXREAL_0:def 11;
A3: gt(.x,.y).s = IFGT((.x).s,(.y).s,1,0) by Def32;
A4: (.x).s < .y.s implies IFGT((.y).s,(.x).s,1,0) = 1 by XXREAL_0:def 11;
  (.x).s = s.((^x).s) by Def19;
  then
A5: s.x = (.x).s by FUNCOP_1:7;
A6: (.x).s <= .y.s implies IFGT((.x).s,(.y).s,1,0) = 0 by XXREAL_0:def 11;
A7: gt(.y,.x).s = IFGT((.y).s,(.x).s,1,0) by Def32;
A8: (.x).s >= .y.s implies IFGT((.y).s,(.x).s,1,0) = 0 by XXREAL_0:def 11;
  (.y).s = s.((^y).s) by Def19;
  hence thesis by A5,A1,A2,A6,A4,A8,A3,A7,Th24,FUNCOP_1:7;
end;

theorem Th40:
  for b being Element of X for g being Euclidean ExecutionFunction
  of A,Funcs(X,INT), Funcs(X,INT)\(b,0) for x being Variable of g for i being
integer 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 Th2;
  hence s.x > i iff g.(s, x gt i) in Funcs(X,INT)\(b,0) by Th38;
  g.(s, x lt i) in Funcs(X,INT)\(b,0) iff g.(s, x lt i).b <> 0 by Th2;
  hence thesis by Th38;
end;

theorem
  for b being Element of X for g being Euclidean ExecutionFunction of A,
  Funcs(X,INT), Funcs(X,INT)\(b,0) for x,y being Variable of g holds (s.x > s.y
  iff g.(s, x gt y) in Funcs(X,INT)\(b,0)) & (s.x < s.y iff g.(s, x lt y) in
  Funcs(X,INT)\(b,0))
proof
  let b be Element of X;
  let g be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
  let x,y be Variable of g;
  g.(s, x gt y) in Funcs(X,INT)\(b,0) iff g.(s, x gt y).b <> 0 by Th2;
  hence s.x > s.y iff g.(s, x gt y) in Funcs(X,INT)\(b,0) by Th39;
  g.(s, x lt y) in Funcs(X,INT)\(b,0) iff g.(s, x lt y).b <> 0 by Th2;
  hence thesis by Th39;
end;

theorem
  for x being Variable of f holds f.(s, x%=i).x = s.x mod i & for z st z
  <> x holds f.(s, x%=i).z = s.z
proof
  let x be Variable of f;
A1: .(i,A,f).s = i by FUNCOP_1:7;
A2: (^x).s = x by FUNCOP_1:7;
A3: .(^(x qua Element of X)).s = s.((^(x qua Element of X)).s) by Def19;
  (.x mod .(i,A,f)).s = (.x).s mod (.(i,A,f).s) by Def30;
  hence thesis by A1,A2,A3,Th24;
end;

theorem Th43:
  for x being Variable of f for t being INT-Expression of A,f
  holds f.(s, x%=t).x = s.x mod t.s & for z st z <> x holds f.(s, x%=t).z = s.z
proof
  let x be Variable of f;
  let t be INT-Expression of A,f;
A1: (^x).s = x by FUNCOP_1:7;
A2: (.x).s = s.x by Th22;
  (.x mod t).s = (.x).s mod t.s by Def30;
  hence thesis by A1,A2,Th24;
end;

theorem Th44:
  for x,y being Variable of f holds f.(s, x%=y).x = s.x mod s.y &
  for z st z <> x holds f.(s, x%=y).z = s.z
proof
  let x,y be Variable of f;
A1: x%=y = x%=.y;
  (.y).s = s.y by Th22;
  hence thesis by A1,Th43;
end;

theorem Th45:
  for x being Variable of f holds f.(s, x/=i).x = s.x div i & for
  z st z <> x holds f.(s, x/=i).z = s.z
proof
  let x be Variable of f;
A1: .(i,A,f).s = i by FUNCOP_1:7;
A2: (^x).s = x by FUNCOP_1:7;
A3: .(^(x qua Element of X)).s = s.((^(x qua Element of X)).s) by Def19;
  (.x div .(i,A,f)).s = (.x).s div (.(i,A,f).s) by Def29;
  hence thesis by A1,A2,A3,Th24;
end;

theorem Th46:
  for x being Variable of f for t being INT-Expression of A,f
  holds f.(s, x/=t).x = s.x div t.s & for z st z <> x holds f.(s, x/=t).z = s.z
proof
  let x be Variable of f;
  let t be INT-Expression of A,f;
A1: (^x).s = x by FUNCOP_1:7;
A2: (.x).s = s.x by Th22;
  (.x div t).s = (.x).s div t.s by Def29;
  hence thesis by A1,A2,Th24;
end;

theorem
  for x,y being Variable of f holds f.(s, x/=y).x = s.x div s.y & for z
  st z <> x holds f.(s, x/=y).z = s.z
proof
  let x,y be Variable of f;
A1: x/=y = x/=.y;
  (.y).s = s.y by Th22;
  hence thesis by A1,Th46;
end;

theorem Th48:
  for b being Element of X for g being Euclidean ExecutionFunction
of A,Funcs(X,INT), Funcs(X,INT)\(b,0) for t being INT-Expression of A,g holds g
.(s, t is_odd).b = (t.s) mod 2 & g.(s, t is_even).b = (t.s+1) mod 2 & for z st
  z <> b holds g.(s, t is_odd).z = s.z & g.(s, t is_even).z = s.z
proof
  let b be Element of X;
  let f be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
  let t be INT-Expression of A,f;
  reconsider y = b as Variable of f by Def2;
A1: t is_odd = y:=(t mod .(2,A,f));
  dom(t+1) = Funcs(X,INT) by FUNCT_2:def 1;
  then
A2: (t+1).s = 1+(t.s) by VALUED_1:def 2;
A3: .(2,A,f).s = 2 by FUNCOP_1:7;
  then
A4: ((t+1) mod .(2,A,f)).s = ((t+1).s) mod 2 by Def30;
  (t mod .(2,A,f)).s = (t.s) mod 2 by A3,Def30;
  hence thesis by A1,A2,A4,Th26;
end;

theorem Th49:
  for b being Element of X for g being Euclidean ExecutionFunction
  of A,Funcs(X,INT), Funcs(X,INT)\(b,0) for x being Variable of g holds g.(s, x
  is_odd).b = s.x mod 2 & g.(s, x is_even).b = (s.x+1) mod 2 & for z st z <> b
  holds g.(s, x is_odd).z = s.z
proof
  let b be Element of X;
  let f be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
  let x be Variable of f;
  (.x).s = s.x by Th22;
  hence thesis by Th48;
end;

theorem Th50:
  for b being Element of X for g being Euclidean ExecutionFunction
of A,Funcs(X,INT), Funcs(X,INT)\(b,0) for t being INT-Expression of A,g holds (
t.s is odd iff g.(s, t is_odd) in Funcs(X,INT)\(b,0)) & (t.s is even iff g.(s,
  t is_even) in Funcs(X,INT)\(b,0))
proof
  let b be Element of X;
  let f be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
  let t be INT-Expression of A,f;
A1: (t.s) mod 2 = 0 or (t.s) mod 2 = 1 by PRE_FF:6;
A2: t.s = ((t.s) div 2)*2 + ((t.s) mod 2) by INT_1:59;
  f.(s, t is_odd).b = (t.s) mod 2 by Th48;
  hence t.s is odd iff f.(s, t is_odd) in Funcs(X,INT)\(b,0) by A1,A2,Th2;
A3: (t.s+1) mod 2 = 0 or (t.s+1) mod 2 = 1 by PRE_FF:6;
A4: t.s+1 = ((t.s+1) div 2)*2 + ((t.s+1) mod 2) by INT_1:59;
  f.(s, t is_even).b = (t.s+1) mod 2 by Th48;
  hence thesis by A3,A4,Th2;
end;

theorem
  for b being Element of X for g being Euclidean ExecutionFunction of A,
  Funcs(X,INT), Funcs(X,INT)\(b,0) for x being Variable of g holds (s.x is odd
iff g.(s, x is_odd) in Funcs(X,INT)\(b,0)) & (s.x is even iff g.(s, x is_even)
  in Funcs(X,INT)\(b,0))
proof
  let b be Element of X;
  let f be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
  let x be Variable of f;
  (.x).s = s.x by Th22;
  hence thesis by Th50;
end;

scheme
  ForToIteration {A() -> Euclidean preIfWhileAlgebra, X() -> countable non
empty set, b() -> (Element of X()), I,F() -> (Element of A()), g() -> Euclidean
  ExecutionFunction of A(), Funcs(X(),INT), Funcs(X(),INT)\(b(),0), i,n() -> (
Variable of g()), s() -> (Element of Funcs(X(),INT)), a() -> INT-Expression of
A(),g(), P[set] }: P[g().(s(),F())] & (a().s() <= s().n() implies g().(s(),F())
.i() = s().n()+1) & (a().s() > s().n() implies g().(s(),F()).i() = a().s()) & g
  ().(s(),F()).n() = s().n()
provided
A1: F() = for-do(i():=a(), i() leq n(), i()+=1, I()) and
A2: P[g().(s(),i():=a())] and
A3: for s being Element of Funcs(X(),INT) st P[s] holds P[g().(s,I()\;i(
)+=1)] & P[g().(s, i() leq n())] and
A4: for s being Element of Funcs(X(),INT) st P[s] holds g().(s,I()).i()
= s.i() & g().(s,I()).n() = s.n() and
A5: n() <> i() & n() <> b() & i() <> b()
proof
  set C = i() leq n();
  set S = Funcs(X(),INT);
  reconsider s1 = g().(s(),i():=a()) as Element of S;
  reconsider s2 = g().(s1,C) as Element of S;
A6: P[s2] by A2,A3;
  defpred Q[Element of S] means P[$1] & (a().s() <= s().n() implies $1.i()-1
  <= s().n()) & $1.n() = s().n();
A7: s1.i() = a().s() by Th26;
  then
A8: s2.i() = a().s() by A5,Th35;
  defpred R[Element of S] means $1.i() <= $1.n();
  set T = S\(b(),0);
A9: g() complies_with_while_wrt T by AOFA_000:def 32;
  set II = I()\;i()+=1;
A10: g().(s(),F()) = g().(s1,while(C, II)) by A1,AOFA_000:def 29;
  a().s()-1 < a().s() by XREAL_1:44;
  then
A11: Q[s1] by A2,A5,A7,Th26,XXREAL_0:2;
A12: s1.n() = s().n() by A5,Th26;
  then
A13: s2.n() = s().n() by A5,Th35;
  per cases;
  suppose
A14: a().s() <= s().n();
    deffunc F(Element of S) = In($1.n()+1-$1.i(),NAT);
    defpred PR[Element of S] means P[$1] & R[$1];
A15: for s being Element of S st Q[s] & s in T & R[s] holds Q[g().(s,II)
    qua Element of S]
    proof
      let s be Element of S;
      assume that
A16:  Q[s] and
      s in T and
A17:  R[s];
      thus P[g().(s,II)] by A3,A16;
      reconsider s9 = g().(s,I()) as Element of S;
      reconsider s99 = g().(s9,i()+=1) as Element of S;
A18:  s99 = g().(s,II) by AOFA_000:def 29;
A19:  s99.i() = s9.i()+1 by Th28;
      s9.n() = s.n() by A4,A16;
      hence thesis by A4,A5,A16,A17,A19,A18,Th28;
    end;
A20: for s being Element of S st PR[s] holds (PR[g().(s,II\;C) qua Element
    of S] iff g().(s,II\;C) in T) & F(g().(s,II\;C) qua Element of S) < F(s)
    proof
      let s be Element of S;
      reconsider s9 = g().(s,I()) as Element of S;
      reconsider s99 = g().(s9,i()+=1) as Element of S;
      reconsider s999 = g().(s99,C) as Element of S;
A21:  g().(s,II\;C) = g().(g().(s,II),C) by AOFA_000:def 29;
A22:  s99.n() = s9.n() by A5,Th28;
A23:  s99.i() <= s99.n() implies s999.b() = 1 by Th35;
A24:  s99.i() > s99.n() implies s999.b() = 0 by Th35;
      assume
A25:  PR[s];
      then reconsider j = s.n()-s.i() as Element of NAT by INT_1:5;
A26:  s999.i() = s99.i() by A5,Th35;
A27:  s99 = g().(s,II) by AOFA_000:def 29;
      then P[s99] by A3,A25;
      hence
      PR[g().(s,II\;C) qua Element of S] iff g().(s,II\;C) in T by A3,A5,A21
,A27,A26,A24,A23,Th2,Th35;
A28:  s99.i() = s9.i()+1 by Th28;
A29:  s9.n() = s.n() by A4,A25;
A30:  s9.i() = s.i() by A4,A25;
      s999.n() = s99.n() by A5,Th35;
      then F(s999) = j by A26,A30,A29,A28,A22,FUNCT_7:def 1;
      then F(s999)+1 = F(s) by FUNCT_7:def 1;
      hence thesis by A21,A27,NAT_1:13;
    end;
A31: for s being Element of S st Q[s] holds Q[g().(s,C) qua Element of S]
    & (g().(s,C) in T iff R[g().(s,C) qua Element of S])
    proof
      let s be Element of S;
A32:  s.i() > s.n() implies g().(s,C).b() = 0 by Th35;
      assume
A33:  Q[s];
      hence P[g().(s,C)] by A3;
A34:  s.i() <= s.n() implies g().(s,C).b() = 1 by Th35;
      g().(s,C).i() = s.i() by A5,Th35;
      hence thesis by A5,A33,A32,A34,Th2,Th35;
    end;
    s2.b() = 1 by A7,A12,A14,Th35;
    then
A35: g().(s1,C) in T iff PR[g().(s1,C) qua Element of S] by A2,A3,A5,A12,A8,A14
,Th35;
A36: g() iteration_terminates_for II\;C, g().(s1,C) from AOFA_000:sch 3(
    A35,A20);
A37: Q[g().(s1,while(C,II)) qua Element of S] & not R[g().(s1,while(C,II))
    qua Element of S] from AOFA_000:sch 5(A11,A36,A15,A31);
    then (g().(s(),F()) qua Element of S).i() >= s().n()+1 by A10,INT_1:7;
    then (g().(s(),F()) qua Element of S).i()-1 >= s().n()+1-1 by XREAL_1:13;
    then (g().(s(),F()) qua Element of S).i()-1 = s().n() by A10,A14,A37,
XXREAL_0:1;
    hence thesis by A1,A14,A37,AOFA_000:def 29;
  end;
  suppose
A38: a().s() > s().n();
    then s2.b() = 0 by A7,A12,Th35;
    then s2 nin T by Th2;
    hence thesis by A9,A8,A13,A10,A6,A38,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
A1: F() = for-do(i():=a(),.n() leq .i(),i()+=-1,I()) and
A2: P[f().(s(),i():=a())] and
A3: for s being Element of Funcs(X(),INT) st P[s] holds P[f().(s,I()\;i(
)+=-1)] & P[f().(s, n() leq i())] and
A4: for s being Element of Funcs(X(),INT) st P[s] holds f().(s,I()).i()
= s.i() & f().(s,I()).n() = s.n() and
A5: n() <> i() & n() <> b() & i() <> b()
proof
  set S = Funcs(X(),INT);
  reconsider s1 = f().(s(),i():=a()) as Element of S;
  set C = n() leq i();
  reconsider s2 = f().(s1,C) as Element of S;
A6: P[s2] by A2,A3;
  defpred Q[Element of S] means P[$1] & (a().s() >= s().n() implies $1.i()+1
  >= s().n()) & $1.n() = s().n();
A7: s1.i() = a().s() by Th26;
  then
A8: Q[s1] by A2,A5,Th26,XREAL_1:39;
A9: s2.i() = a().s() by A5,A7,Th35;
  defpred R[Element of S] means $1.i() >= $1.n();
  set T = S\(b(),0);
A10: f() complies_with_while_wrt T by AOFA_000:def 32;
  set II = I()\;i()+=-1;
A11: f().(s(),F()) = f().(s1,while(C, II)) by A1,AOFA_000:def 29;
A12: s1.n() = s().n() by A5,Th26;
  then
A13: s2.n() = s().n() by A5,Th35;
  per cases;
  suppose
A14: a().s() >= s().n();
    deffunc F(Element of S) = In($1.i()+1-$1.n(),NAT);
    defpred PR[Element of S] means P[$1] & R[$1];
A15: for s being Element of S st Q[s] & s in T & R[s] holds Q[f().(s,II)
    qua Element of S]
    proof
      let s be Element of S;
      assume that
A16:  Q[s] and
      s in T and
A17:  R[s];
      thus P[f().(s,II)] by A3,A16;
      reconsider s99 = f().(s,I()) as Element of S;
      reconsider s999 = f().(s99,i()+=-1) as Element of S;
A18:  s999 = f().(s,II) by AOFA_000:def 29;
A19:  s999.i() = s99.i()-1 by Th28;
      s99.n() = s.n() by A4,A16;
      hence thesis by A4,A5,A16,A17,A19,A18,Th28;
    end;
A20: for s being Element of S st PR[s] holds (PR[f().(s,II\;C) qua Element
    of S] iff f().(s,II\;C) in T) & F(f().(s,II\;C) qua Element of S) < F(s)
    proof
      let s be Element of S;
      reconsider s9 = f().(s,I()) as Element of S;
      reconsider s99 = f().(s9,i()+=-1) as Element of S;
      reconsider s999 = f().(s99,C) as Element of S;
A21:  f().(s,II\;C) = f().(f().(s,II),C) by AOFA_000:def 29;
A22:  s99.n() = s9.n() by A5,Th28;
A23:  s99.i() >= s99.n() implies s999.b() = 1 by Th35;
A24:  s99.i() < s99.n() implies s999.b() = 0 by Th35;
      assume
A25:  PR[s];
      then reconsider j = s.i()-s.n() as Element of NAT by INT_1:5;
A26:  s999.i() = s99.i() by A5,Th35;
A27:  s99 = f().(s,II) by AOFA_000:def 29;
      then P[s99] by A3,A25;
      hence
      PR[f().(s,II\;C) qua Element of S] iff f().(s,II\;C) in T by A3,A5,A21
,A27,A26,A24,A23,Th2,Th35;
A28:  s99.i() = s9.i()-1 by Th28;
A29:  s9.n() = s.n() by A4,A25;
A30:  s9.i() = s.i() by A4,A25;
      s999.n() = s99.n() by A5,Th35;
      then F(s999) = j by A26,A30,A29,A28,A22,FUNCT_7:def 1;
      then F(s999)+1 = F(s) by FUNCT_7:def 1;
      hence thesis by A21,A27,NAT_1:13;
    end;
A31: for s being Element of S st Q[s] holds Q[f().(s,C) qua Element of S]
    & (f().(s,C) in T iff R[f().(s,C) qua Element of S])
    proof
      let s be Element of S;
A32:  s.i() < s.n() implies f().(s,C).b() = 0 by Th35;
      assume
A33:  Q[s];
      hence P[f().(s,C)] by A3;
A34:  s.i() >= s.n() implies f().(s,C).b() = 1 by Th35;
      f().(s,C).i() = s.i() by A5,Th35;
      hence thesis by A5,A33,A32,A34,Th2,Th35;
    end;
    s2.b() = 1 by A7,A12,A14,Th35;
    then
A35: f().(s1,C) in T iff PR[f().(s1,C) qua Element of S] by A2,A3,A5,A12,A9,A14
,Th35;
A36: f() iteration_terminates_for II\;C, f().(s1,C) from AOFA_000:sch 3(
    A35,A20);
A37: Q[f().(s1,while(C,II)) qua Element of S] & not R[f().(s1,while(C,II))
    qua Element of S] from AOFA_000:sch 5(A8,A36,A15,A31);
    then (f().(s(),F())qua Element of S).i()+1 <= s().n()+1-1 by A11,INT_1:7;
    then (f().(s(),F()) qua Element of S).i()+1 = s().n() by A11,A14,A37,
XXREAL_0:1;
    hence thesis by A1,A14,A37,AOFA_000:def 29;
  end;
  suppose
A38: a().s() < s().n();
    then s2.b() = 0 by A7,A12,Th35;
    then s2 nin T by Th2;
    hence thesis by A10,A9,A13,A11,A6,A38,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 Th52:
  for I being Element of A for i,n being Variable of g st (ex d
being Function st d.b = 0 & d.n = 1 & d.i = 2) & for s holds g.(s,I).n = s.n &
  g.(s,I).i = s.i holds g iteration_terminates_for I\; i+=1\; i leq n, g.(s, i
  leq n)
proof
  let I be Element of A;
  let i,n be Variable of g;
  given d being Function such that
A1: d.b = 0 and
A2: d.n = 1 and
A3: d.i = 2;
  set J = i+=1;
  set C = i leq n;
  set S = Funcs(X, INT);
  set h = g;
  assume
A4: for s holds g.(s,I).n = s.n & g.(s,I).i = s.i;
  deffunc F(Element of S) = In($1.n+1-$1.i, NAT);
  defpred R[Element of S] means $1.i <= $1.n;
  set T = S\(b,0);
A5: i <> n by A2,A3;
A6: for s being Element of S st R[s] holds (R[h.(s,I\;J\;C) qua Element of
  S] iff h.(s,I\;J\;C) in T) & F(h.(s,I\;J\;C) qua Element of S) < F(s)
  proof
    let s be Element of S;
    set s1 = h.(s, I);
    set q = h.(s, I\;J);
    set q1 = h.(q, C);
A7: q = h.(s1, J) by AOFA_000:def 29;
    s1.i = s.i by A4;
    then q.i = s.i+1 by A7,Th28;
    then
A8: q1.i = s.i+1 by A1,A3,Th35;
A9: q.i > q.n implies q1.b = 0 by Th35;
    assume R[s];
    then reconsider ni = s.n-s.i as Element of NAT by INT_1:3,XREAL_1:48;
A10: q1 = h.(s, I\;J\;C) by AOFA_000:def 29;
A11: q.i <= q.n implies q1.b = 1 by Th35;
    q1.i = q.i by A1,A3,Th35;
    hence
    R[h.(s,I\;J\;C) qua Element of S] iff h.(s,I\;J\;C) in T by A1,A2,A9,A11
,A10,Th2,Th35;
A12: F(s) = ni+1 by FUNCT_7:def 1;
    s1.n = s.n by A4;
    then q.n = s.n by A5,A7,Th28;
    then q1.n = s.n by A1,A2,Th35;
    then F(q1 qua Element of S) = ni by A8,FUNCT_7:def 1;
    hence thesis by A10,A12,NAT_1:13;
  end;
  reconsider s1 = h.(s, C) as Element of S;
A13: s.i > s.n implies s1.b = 0 by Th35;
A14: s.i <= s.n implies s1.b = 1 by Th35;
  s1.i = s.i by A1,A3,Th35;
  then
A15: s1 in T iff R[s1] by A1,A2,A13,A14,Th2,Th35;
  h iteration_terminates_for I\;J\;C, s1 from AOFA_000:sch 3(A15,A6 );
  hence thesis;
end;

theorem Th53:
  for P being set for I being Element of A for i,n being Variable
of g st (ex d being Function st d.b = 0 & d.n = 1 & d.i = 2) & for s st s in P
holds g.(s,I).n = s.n & g.(s,I).i = s.i & g.(s, I) in P & g.(s, i leq n) in P &
  g.(s, i+=1) in P holds s in P implies g iteration_terminates_for I\; i+=1\; i
  leq n, g.(s, i leq n)
proof
  let P be set;
  let I be Element of A;
  let i,n be Variable of g;
  given d being Function such that
A1: d.b = 0 and
A2: d.n = 1 and
A3: d.i = 2;
  set J = i+=1;
  set C = i leq n;
  set S = Funcs(X, INT);
  set h = g;
  assume that
A4: for s st s in P holds g.(s,I).n = s.n & g.(s,I).i = s.i & g.(s, I)
  in P & g.(s, i leq n) in P & g.(s, i+=1) in P and
A5: s in P;
  defpred P[Element of S] means $1 in P;
  reconsider s1 = h.(s, C) as Element of S;
A6: P[s1] by A4,A5;
  deffunc F(Element of S) = In($1.n+1-$1.i, NAT);
  defpred R[Element of S] means $1.i <= $1.n;
  set T = S\(b,0);
A7: i <> n by A2,A3;
A8: for s being Element of S st P[s] & s in T & R[s] holds P[h.(s,I\;J\;C)
qua Element of S] & (R[h.(s,I\;J\;C) qua Element of S] iff h.(s,I\;J\;C) in T)
  & F(h.(s,I\;J\;C) qua Element of S) < F(s)
  proof
    let s be Element of S;
    assume that
A9: P[s] and
    s in T and
A10: R[s];
    set q = h.(s, I\;J);
    set s1 = h.(s, I);
    set q1 = h.(q, C);
A11: q = h.(s1, J) by AOFA_000:def 29;
    s1.i = s.i by A4,A9;
    then q.i = s.i+1 by A11,Th28;
    then
A12: q1.i = s.i+1 by A1,A3,Th35;
    reconsider ni = s.n-s.i as Element of NAT by A10,INT_1:3,XREAL_1:48;
A13: F(s) = ni+1 by FUNCT_7:def 1;
A14: q.i <= q.n implies q1.b = 1 by Th35;
A15: q1 = h.(s, I\;J\;C) by AOFA_000:def 29;
    P[s1 qua Element of S] by A4,A9;
    then P[q qua Element of S] by A4,A11;
    hence P[h.(s,I\;J\;C) qua Element of S] by A4,A15;
A16: q.i > q.n implies q1.b = 0 by Th35;
    q1.i = q.i by A1,A3,Th35;
    hence
    R[h.(s,I\;J\;C) qua Element of S] iff h.(s,I\;J\;C) in T by A1,A2,A16,A14
,A15,Th2,Th35;
    s1.n = s.n by A4,A9;
    then q.n = s.n by A7,A11,Th28;
    then q1.n = s.n by A1,A2,Th35;
    then F(q1 qua Element of S) = ni by A12,FUNCT_7:def 1;
    hence thesis by A15,A13,NAT_1:13;
  end;
A17: s.i > s.n implies s1.b = 0 by Th35;
A18: s.i <= s.n implies s1.b = 1 by Th35;
  s1.i = s.i by A1,A3,Th35;
  then
A19: s1 in T iff R[s1] by A1,A2,A17,A18,Th2,Th35;
  h iteration_terminates_for I\;J\;C, s1 from AOFA_000:sch 4(A6,A19, A8);
  hence thesis;
end;

theorem Th54:
  for I being Element of A st I is_terminating_wrt g for i,n being
  Variable of g st (ex d being Function st d.b = 0 & d.n = 1 & d.i = 2) & for s
  holds g.(s,I).n = s.n & g.(s,I).i = s.i holds for-do(i:=t, i leq n, i+=1, I)
  is_terminating_wrt g
proof
  set S = Funcs(X, INT);
  set T = Funcs(X, INT)\(b,0);
  let I be Element of A such that
A1: I is_terminating_wrt g;
  let i,n be Variable of g;
  i+=1 is_terminating_wrt g by AOFA_000:104;
  then
A2: I\; i+=1 is_terminating_wrt g by A1,AOFA_000:110;
  set Q = while(i leq n, I\; i+=1);
  given d being Function such that
A3: d.b = 0 and
A4: d.n = 1 and
A5: d.i = 2;
  assume
A6: for s holds g.(s,I).n = s.n & g.(s,I).i = s.i;
  let s;
A7: [s, i:=t] in TerminatingPrograms(A,S,T,g) by AOFA_000:def 36;
A8: i leq n is_terminating_wrt g by AOFA_000:104;
  g iteration_terminates_for I\; i+=1\; i leq n, g.(g.(s, i:=t), i leq n)
  by A3,A4,A5,A6,Th52;
  then [g.(s, i:=t), Q] in TerminatingPrograms(A,S,T,g) by A8,A2,AOFA_000:114;
  hence thesis by A7,AOFA_000:def 35;
end;

theorem
  for P being set for I being Element of A st I is_terminating_wrt g, P
for i,n being Variable of g st (ex d being Function st d.b = 0 & d.n = 1 & d.i
  = 2) & (for s st s in P holds g.(s,I).n = s.n & g.(s,I).i = s.i) & P
is_invariant_wrt i:=t, g & P is_invariant_wrt I, g & P is_invariant_wrt i leq n
  , g & P is_invariant_wrt i+=1, g holds for-do(i:=t, i leq n, i+=1, I)
  is_terminating_wrt g, P
proof
  set Z = Funcs(X, INT);
  set T = Funcs(X, INT)\(b,0);
  let S be set;
  let I be Element of A;
  assume
A1: I is_terminating_wrt g, S;
  let i,n be Variable of g;
  given d being Function such that
A2: d.b = 0 and
A3: d.n = 1 and
A4: d.i = 2;
  set C = i leq n, J = I\; i+=1;
  assume that
A5: for s st s in S holds g.(s,I).n = s.n & g.(s,I).i = s.i and
A6: S is_invariant_wrt i:=t, g and
A7: S is_invariant_wrt I, g and
A8: S is_invariant_wrt i leq n, g and
A9: S is_invariant_wrt i+=1, g;
  let s;
  assume s in S;
  then
A10: g.(s, i:=t) in S by A6,AOFA_000:def 39;
  for s being Element of Z st s in S holds g.(s,I).n = s.n & g.(s,I).i =
  s.i & g.(s, I) in S & g.(s, i leq n) in S & g.(s, i+=1) in S by A5,A7,A8,A9,
AOFA_000:def 39;
  then
A11: g iteration_terminates_for J\; C, g.(g.(s, i:=t), C) by A2,A3,A4,A10,Th53;
  set Q = while(C, J);
A12: C is_terminating_wrt g by AOFA_000:104;
A13: [s, i:=t] in TerminatingPrograms(A,Z,T,g) by AOFA_000:def 36;
  S is_invariant_wrt J, g by A7,A9,AOFA_000:109;
  then
A14: for s st s in S & g.(g.(s, J), C) in T holds g.(s,J) in S by
AOFA_000:def 39;
  i+=1 is_terminating_wrt g, S by AOFA_000:107;
  then [g.(s, i:=t), Q] in TerminatingPrograms(A,Z,T,g) by A1,A7,A8,A10,A11,A12
,A14,AOFA_000:111,116;
  hence thesis by A13,AOFA_000:def 35;
end;

begin :: Examples

definition
  let X,A,T,f,s;
  let I be Element of A;
  redefine func f.(s,I) -> Element of Funcs(X, INT);
  coherence
  proof
    f.(s,I) is Element of Funcs(X, INT);
    hence thesis;
  end;
end;

theorem
  for n,s,i being Variable of g st ex d being Function st d.n = 1 & d.s
  = 2 & d.i = 3 & d.b = 4 holds s:=1\;for-do(i:=2, i leq n, i+=1, s*=i)
  is_terminating_wrt g
proof
  set S = Funcs(X, INT);
  set T = S\(b,0);
  let n,s,i be Variable of g;
  given d being Function such that
A1: d.n = 1 and
A2: d.s = 2 and
A3: d.i = 3 and
A4: d.b = 4;
A5: s <> n by A1,A2;
  s <> i by A2,A3;
  then
A6: for q be Element of S holds g.(q,s*=i).n = q.n & g.(q,s*=i).i = q.i by A5
,Th33;
A7: n <> b by A1,A4;
A8: b <> i by A3,A4;
  let q be Element of S;
  set t = .(2,A,g);
  i <> n by A1,A3;
  then ex d9 being Function st d9.b = 0 & d9.n = 1 & d9.i = 2 by A8,A7,Th1;
  then for-do(i:=t, i leq n, i+=1, s*=i) is_terminating_wrt g by A6,Th54,
AOFA_000:104;
  then
A9: [g.(q, s:=1) qua Element of S, for-do(i:=t, i leq n, i+=1, s*=i)] in
  TerminatingPrograms(A,S,T,g) by AOFA_000:def 37;
  [q,s:=1] in TerminatingPrograms(A,S,T,g) by AOFA_000:def 36;
  hence thesis by A9,AOFA_000:def 35;
end;

theorem
  for n,s,i being Variable of g st ex d being Function st d.n = 1 & d.s
  = 2 & d.i = 3 & d.b = 4 for q being Element of Funcs(X, INT) for N being
Nat st N = q.n holds g.(q, s:=1\;for-do(i:=2, i leq n, i+=1, s*=i)).
  s = N!
proof
  set f = g;
  let n,s,i be Variable of f;
  given d being Function such that
A1: d.n = 1 and
A2: d.s = 2 and
A3: d.i = 3 and
A4: d.b = 4;
A5: n <> i & n <> b & i <> b by A1,A3,A4;
  set S = Funcs(X,INT);
  let q be Element of Funcs(X, INT);
  reconsider q1 = f.(q, s:=1) as Element of S;
  defpred P[Element of S] means ex K being Nat st K = $1.i-1 & $1.s
  = K!;
  reconsider a = .(2,A,f) as INT-Expression of A,g;
  reconsider q2 = f.(q1, i:=2) as Element of S;
A6: q2.i = 2 by Th25;
A7: s <> i by A2,A3;
  then q2.s = q1.s by Th25;
  then
A8: P[f.(q1,i:=a)] by A6,Th25,NEWTON:13;
  set I = s*=i;
A9: a.q1 = 2 by FUNCOP_1:7;
A10: s <> b by A2,A4;
A11: for q being Element of Funcs(X,INT) st P[q] holds P[f.(q,I\;i+=1)] & P[
  f.(q, i leq n)]
  proof
    let q be Element of Funcs(X,INT);
    given Ki being Nat such that
A12: Ki = q.i-1 and
A13: q.s = Ki!;
    reconsider q3 = f.(q,I) as Element of S;
    reconsider q4 = f.(q3,i+=1) as Element of S;
A14: q3.s = q.s*q.i by Th33;
    q4.s = q3.s by A7,Th28;
    then
A15: q4.s = (Ki+1)! by A12,A13,A14,NEWTON:15;
A16: q4 = f.(q,I\;i+=1) by AOFA_000:def 29;
    q4.i = q3.i+1 by Th28;
    then Ki+1 = q4.i-1 by A7,A12,Th33;
    hence P[f.(q,I\;i+=1) qua Element of S] by A16,A15;
    reconsider q9 = f.(q, i leq n) as Element of S;
A17: q9.i = q.i by A5,Th35;
    q9.s = q.s by A10,Th35;
    hence thesis by A12,A13,A17;
  end;
  reconsider F = for-do(i:=a, i leq n, i+=1, I) as Element of A;
  let N be Nat;
  assume
A18: N = q.n;
A19: F = for-do(i:=a, i leq n, i+=1, I);
A20: s <> n by A1,A2;
  then
A21: q1.n = q.n by Th25;
A22: 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 A20,A7,Th32;
A23: 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(A19,A8,A11,
  A22,A5);
  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 A18,A21,A23,A9,NAT_1:26,NEWTON:12,13;
end;

theorem
  for x,n,s,i being Variable of g st ex d being Function st d.n = 1 & d.
  s = 2 & d.i = 3 & d.b = 4 holds s:=1\;for-do(i:=1, i leq n, i+=1, s*=x)
  is_terminating_wrt g
proof
  set S = Funcs(X, INT);
  set T = S\(b,0);
  let x,n,s,i be Variable of g;
  given d being Function such that
A1: d.n = 1 and
A2: d.s = 2 and
A3: d.i = 3 and
A4: d.b = 4;
A5: s <> n by A1,A2;
  s <> i by A2,A3;
  then
A6: for q be Element of S holds g.(q,s*=x).n = q.n & g.(q,s*=x).i = q.i by A5
,Th33;
A7: n <> b by A1,A4;
A8: b <> i by A3,A4;
  let q be Element of S;
  set t = .(1,A,g);
  i <> n by A1,A3;
  then ex d9 being Function st d9.b = 0 & d9.n = 1 & d9.i = 2 by A8,A7,Th1;
  then for-do(i:=t, i leq n, i+=1, s*=x) is_terminating_wrt g by A6,Th54,
AOFA_000:104;
  then
A9: [g.(q, s:=1) qua Element of S, for-do(i:=t, i leq n, i+=1, s*=x)] in
  TerminatingPrograms(A,S,T,g) by AOFA_000:def 37;
  [q,s:=1] in TerminatingPrograms(A,S,T,g) by AOFA_000:def 36;
  hence thesis by A9,AOFA_000:def 35;
end;

theorem
  for x,n,s,i being Variable of g st ex d being Function st d.x = 0 & d.
n = 1 & d.s = 2 & d.i = 3 & d.b = 4 for q being Element of Funcs(X, INT) for N
being Nat st N = q.n holds g.(q, s:=1\;for-do(i:=1, i leq n, i+=1, s
  *=x)).s = (q.x)|^N
proof
  set f = g;
  let x,n,s,i be Variable of f;
  given d being Function such that
A1: d.x = 0 and
A2: d.n = 1 and
A3: d.s = 2 and
A4: d.i = 3 and
A5: d.b = 4;
A6: n <> i & n <> b & i <> b by A2,A4,A5;
  set S = Funcs(X,INT);
  let q be Element of Funcs(X, INT);
  reconsider q1 = f.(q, s:=1) as Element of S;
  reconsider q2 = f.(q1, i:=1) as Element of S;
A7: s <> i by A3,A4;
  then
A8: q2.s = q1.s by Th25;
  defpred P[Element of S] means ex K being Nat st K = $1.i-1 & $1.s
  = (q.x)|^K & $1.x = q.x;
  set I = s*=x;
  set q0 = q;
A9: (q.x)|^0 = 1 by NEWTON:4;
A10: s <> n by A2,A3;
  then
A11: for q being Element of Funcs(X,INT) st P[q] holds f.(q,I).i = q.i & f.(
  q,I).n = q.n by A7,Th32;
A12: s <> b by A3,A5;
A13: for q being Element of Funcs(X,INT) st P[q] holds P[f.(q,I\;i+=1)] & P[
  f.(q, i leq n)]
  proof
    let q be Element of Funcs(X,INT);
    given Ki being Nat such that
A14: Ki = q.i-1 and
A15: q.s = (q0.x)|^Ki and
A16: q.x = q0.x;
    reconsider q3 = f.(q,I) as Element of S;
    reconsider q4 = f.(q3,i+=1) as Element of S;
A17: q3.s = q.s*q.x by Th33;
    q4.s = q3.s by A7,Th28;
    then
A18: q4.s = (q0.x)|^(Ki+1) by A15,A16,A17,NEWTON:6;
A19: q4 = f.(q,I\;i+=1) by AOFA_000:def 29;
A20: q3.x = q.x by A1,A3,Th33;
    q4.i = q3.i+1 by Th28;
    then Ki+1 = q4.i-1 by A7,A14,Th33;
    hence P[f.(q,I\;i+=1) qua Element of S] by A1,A4,A16,A19,A20,A18,Th28;
    reconsider q9 = f.(q, i leq n) as Element of S;
A21: q9.s = q.s by A12,Th35;
A22: q9.i = q.i by A6,Th35;
    q9.x = q.x by A1,A5,Th35;
    hence thesis by A14,A15,A16,A21,A22;
  end;
  reconsider a = .(1,A,f) as INT-Expression of A,g;
  reconsider F = for-do(i:=a, i leq n, i+=1, I) as Element of A;
A23: F = for-do(i:=a, i leq n, i+=1, I);
A24: q2.i = 1 by Th25;
A25: q2.x = q1. x by A1,A4,Th25;
A26: q1.s = 1 by Th25;
  q1.x = q.x by A1,A3,Th25;
  then
A27: P[f.(q1,i:=a)] by A26,A8,A24,A25,A9;
A28: P[f.(q1,F)] & (a.q1 <= q1.n implies f.(q1,F).i = q1.n+1) & (a.q1 > q1.n
implies f.(q1,F).i = a.q1) & f.(q1,F).n = q1.n from ForToIteration(A23,A27,A13,
  A11,A6);
A29: q.n+1-1 = q.n;
A30: q1.n = q.n by A10,Th25;
  let N be Nat;
  assume
A31: N = q.n;
A32: N = 0 or N >= 1 by NAT_1:25;
  thus f.(q, s:=1\;for-do(i:=1, i leq n, i+=1, s*=x)).s = f.(q1, F).s by
AOFA_000:def 29
    .= (q.x)|^N by A31,A30,A29,A28,A32,FUNCOP_1:7;
end;

theorem
  for n,x,y,z,i being Variable of g st ex d being Function st d.b = 0 &
d.n = 1 & d.x = 2 & d.y = 3 & d.z = 4 & d.i = 5 holds x:=0\;y:=1\;for-do(i:=1,
  i leq n, i+=1, z:=x\;x:=y\;y+=z) is_terminating_wrt g
proof
  set S = Funcs(X, INT);
  set T = S\(b,0);
  let n,x,y,z,i be Variable of g;
  given d being Function such that
A1: d.b = 0 and
A2: d.n = 1 and
A3: d.x = 2 and
A4: d.y = 3 and
A5: d.z = 4 and
A6: d.i = 5;
A7: i <> y by A4,A6;
A8: n <> z by A2,A5;
A9: n <> y by A2,A4;
A10: n <> x by A2,A3;
A11: i <> z by A5,A6;
  set I = z:=x\;x:=y\;y+=z;
  set I1 = z:=x, I2 = x:=y, I3 = y+=z;
A12: i <> x by A3,A6;
A13: for q be Element of S holds g.(q,I).n = q.n & g.(q,I).i = q.i
  proof
    let q be Element of S;
    thus g.(q,I).n = g.(g.(q,I1\;I2),I3).n by AOFA_000:def 29
      .= g.(q,I1\;I2).n by A9,Th30
      .= g.(g.(q,I1),I2).n by AOFA_000:def 29
      .= g.(q,I1).n by A10,Th27
      .= q.n by A8,Th27;
    thus g.(q,I).i = g.(g.(q,I1\;I2),I3).i by AOFA_000:def 29
      .= g.(q,I1\;I2).i by A7,Th30
      .= g.(g.(q,I1),I2).i by AOFA_000:def 29
      .= g.(q,I1).i by A12,Th27
      .= q.i by A11,Th27;
  end;
  let s;
  set s2 = g.(s, x:=0\;y:=1);
  i <> n by A2,A6;
  then ex d9 being Function st d9.b = 0 & d9.n = 1 & d9.i = 2 by A1,A2,A6,Th1;
  then for-do(i:=1, i leq n, i+=1, z:=x\;x:=y\;y+=z) is_terminating_wrt g by
A13,Th54,AOFA_000:104;
  then
A14: [s2, for-do(i:=1, i leq n, i+=1, z:=x\;x:=y\;y+=z)] in
  TerminatingPrograms(A,S,T,g) by AOFA_000:def 37;
  [s, x:=0\;y:=1] in TerminatingPrograms(A,S,T,g) by AOFA_000:def 36;
  hence thesis by A14,AOFA_000:def 35;
end;

theorem
  for n,x,y,z,i being Variable of g st ex d being Function st d.b = 0 &
d.n = 1 & d.x = 2 & d.y = 3 & d.z = 4 & d.i = 5 for s being Element of Funcs(X,
INT) for N being Element of NAT st N = s.n holds g.(s, x:=0\;y:=1\;for-do(i:=1,
  i leq n, i+=1, z:=x\;x:=y\;y+=z)).x = Fib N
proof
A1: (0 qua Element of NAT)+1 = 1;
  set S = Funcs(X, INT);
  let n,x,y,z,i be Variable of g;
  given d being Function such that
A2: d.b = 0 and
A3: d.n = 1 and
A4: d.x = 2 and
A5: d.y = 3 and
A6: d.z = 4 and
A7: d.i = 5;
A8: n <> x by A3,A4;
A9: y <> z by A5,A6;
A10: x <> z by A4,A6;
A11: i <> z by A6,A7;
A12: n <> y by A3,A5;
  let s be Element of Funcs(X, INT);
  reconsider s1 = g.(s, x:=0) as Element of S;
  reconsider s2 = g.(s1, y:=1) as Element of S;
  reconsider s4 = g.(s2, i:=1) as Element of S;
A13: s4.i = 1 by Th25;
A14: i <> y by A5,A7;
  then
A15: s4.y = s2.y by Th25;
  set I = z:=x\;x:=y\;y+=z;
A16: s2.y = 1 by Th25;
A17: i <> x by A4,A7;
  then
A18: s4.x = s2.x by Th25;
  defpred P[Element of S] means ex N being Element of NAT st N = $1.i-1 & $1.x
  = Fib N & $1.y = Fib(N+1);
  reconsider a = .(1,A,g) as INT-Expression of A,g;
A19: s1.x = 0 by Th25;
A20: x <> y by A4,A5;
  then s2.x = s1.x by Th25;
  then
A21: P[g.(s2,i:=a)] by A19,A16,A15,A18,A13,A1,PRE_FF:1;
A22: n <> z by A3,A6;
A23: now
    let s be Element of S;
    reconsider s1 = g.(s,z:=x) as Element of S;
    reconsider s2 = g.(s1,x:=y) as Element of S;
    reconsider s3 = g.(s2,y+=z) as Element of S;
A24: g.(s,I) = g.(g.(s, z:=x\;x:=y), y+=z) by AOFA_000:def 29
      .= s3 by AOFA_000:def 29;
A25: s1.z = s.x by Th27;
A26: s2.n = s1.n by A8,Th27;
A27: s1.i = s.i by A11,Th27;
A28: s2.z = s1.z by A10,Th27;
A29: s2.y = s1.y by A20,Th27;
A30: s2.i = s1.i by A17,Th27;
A31: s1.y = s.y by A9,Th27;
A32: s2.x = s1.y by Th27;
    s1.n = s.n by A22,Th27;
    hence
    g.(s,I).i = s.i & g.(s,I).n = s.n & g.(s,I).x = s.y & g.(s,I).y = s.x
    +s.y by A12,A14,A20,A31,A25,A27,A26,A32,A29,A28,A30,A24,Th30;
  end;
A33: for s being Element of Funcs(X,INT) st P[s] holds P[g.(s,I\;i+=1)] & P[
  g.(s, i leq n)]
  proof
    let s be Element of Funcs(X,INT);
    given N being Element of NAT such that
A34: N = s.i-1 and
A35: s.x = Fib N and
A36: s.y = Fib(N+1);
    reconsider s1 = g.(s,I) as Element of S;
    reconsider s2 = g.(s1,i+=1) as Element of S;
A37: s1.x = s.y by A23;
A38: s2.i = s1.i+1 by Th28;
A39: s1.y = s.x+s.y by A23;
A40: s2.y = s1.y by A14,Th28;
    thus P[g.(s,I\;i+=1) qua Element of S]
    proof
      take N+1;
      g.(s,I\;i+=1) = s2 by AOFA_000:def 29;
      hence thesis by A17,A23,A34,A35,A36,A37,A39,A40,A38,Th28,PRE_FF:1;
    end;
    take N;
    thus thesis by A2,A4,A5,A7,A34,A35,A36,Th35;
  end;
  reconsider F = for-do(i:=a, i leq n, i+=1, I) as Element of A;
  reconsider s3 = g.(s2, for-do(i:=1, i leq n, i+=1, z:=x\;x:=y\;y+=z)) as
  Element of S;
  let N be Element of NAT;
  assume
A41: N = s.n;
A42: F = for-do(i:=a,i leq n,i+=1,I);
  g.(s, x:=0\;y:=1) = s2 by AOFA_000:def 29;
  then
A43: g.(s, x:=0\;y:=1\;F) = s3 by AOFA_000:def 29;
A44: 0 <= N & N <= 0 or N >= (0 qua Element of NAT)+1 by NAT_1:13;
A45: n <> i & n <> b & i <> b by A2,A3,A7;
A46: a.s2 = 1 by FUNCOP_1:7;
A47: for s being Element of Funcs(X,INT) st P[s] holds g.(s,I).i = s.i & g.(
  s,I).n = s.n by A23;
A48: P[g.(s2,F)] & (a.s2 <= s2.n implies g.(s2,F).i = s2.n+1) & (a.s2 > s2.n
implies g.(s2,F).i = a.s2) & g.(s2,F).n = s2.n from ForToIteration(A42,A21,A33,
  A47,A45);
  s2.n = s1.n by A12,Th25;
  hence thesis by A41,A43,A8,A48,A44,A46,Th25;
end;

Lm1: for x,y,z being Variable of g st ex d being Function st d.b = 0 & d.x = 1
& d.y = 2 & d.z = 3 for s being Element of Funcs(X, INT) holds g.(s, z:=x\;z%=y
\;x:=y\;y:=z).x = s.y & g.(s, z:=x\;z%=y\;x:=y\;y:=z).y = s.x mod s.y & for n,m
being Element of NAT st m = s.y & (s in Funcs(X, INT)\(b,0) iff m > 0) holds g
iteration_terminates_for z:=x\;z%=y\;x:=y\;y:=z\;y gt 0, s
proof
  set h = g;
  set S = Funcs(X, INT);
  set T = S\(b,0);
  let x,y,z be Variable of h;
  given d being Function such that
A1: d.b = 0 and
A2: d.x = 1 and
A3: d.y = 2 and
A4: d.z = 3;
A5: z <> x by A2,A4;
  let s be Element of Funcs(X, INT);
  set I = z:=x\;z%=y\;x:=y\;y:=z;
A6: y <> z by A3,A4;
A7: x <> y by A2,A3;
A8: now
    let s be Element of S;
    reconsider s1 = h.(s, z:=x) as Element of S;
    reconsider s2 = h.(s1, z%=y) as Element of S;
    reconsider s3 = h.(s2, x:=y) as Element of S;
    reconsider s4 = h.(s3, y:=z) as Element of S;
A9: h.(s, I) = h.(h.(s, z:=x\;z%=y\;x:=y), y:=z) by AOFA_000:def 29
      .= h.(h.(h.(s, z:=x\;z%=y), x:=y), y:=z) by AOFA_000:def 29
      .= s4 by AOFA_000:def 29;
A10: s1.z = s.x by Th27;
A11: s2.y = s1.y by A6,Th44;
A12: s2.z = s1.z mod s1.y by Th44;
A13: s3.z = s2.z by A5,Th27;
A14: s3.x = s2.y by Th27;
    s1.y = s.y by A6,Th27;
    hence h.(s, I).x = s.y & h.(s, I).y = s.x mod s.y by A7,A9,A10,A11,A12,A14
,A13,Th27;
  end;
  hence g.(s, I).x = s.y & h.(s, I).y = s.x mod s.y;
  deffunc F(Element of S) = In($1.y, NAT);
  defpred R[Element of S] means $1.y > 0;
  set C = y gt 0;
A15: for s being Element of S st R[s] holds (R[h.(s,I\;C) qua Element of S]
  iff h.(s,I\;C) in T) & F(h.(s,I\;C) qua Element of S) < F(s)
  proof
    let s be Element of S;
    assume
A16: s.y > 0;
    reconsider s9 = h.(s, I) as Element of S;
A17: s9.y = s.x mod s.y by A8;
    then
A18: 0 <= s9.y by A16,NEWTON:64;
    reconsider s99 = h.(s9, C) as Element of S;
A19: h.(s,I\;C) = s99 by AOFA_000:def 29;
A20: s9.y <= 0 implies s99.b = 0 by Th38;
    s9.y > 0 implies s99.b = 1 by Th38;
    hence R[h.(s,I\;C) qua Element of S] iff h.(s,I\;C) in T by A19,A20,Th2
,Th38;
    s99.y = s9.y by A1,A3,Th38;
    then
A21: F(s99) = s9.y by A18,FUNCT_7:def 1,INT_1:3;
A22: s9.y < s.y by A16,A17,NEWTON:65;
    then F(s) = s.y by A18,FUNCT_7:def 1,INT_1:3;
    hence thesis by A22,A21,AOFA_000:def 29;
  end;
  let n,m be Element of NAT;
  assume that
A23: m = s.y;
  assume s in T iff m > 0;
  then
A24: s in T iff R[s] by A23;
  h iteration_terminates_for I\;C, s from AOFA_000:sch 3(A24,A15);
  hence thesis;
end;

theorem
  for x,y,z being Variable of g st ex d being Function st d.b = 0 & d.x
  = 1 & d.y = 2 & d.z = 3 holds while(y gt 0, z:=x\;z%=y\;x:=y\;y:=z)
  is_terminating_wrt g, {s: s.x > s.y & s.y >= 0}
proof
  set S = Funcs(X, INT);
  set T = S\(b,0);
  let x,y,z be Variable of g;
  set P = {s: s.x > s.y & s.y >= 0};
  given d being Function such that
A1: d.b = 0 and
A2: d.x = 1 and
A3: d.y = 2 and
A4: d.z = 3;
  set C = y gt 0, I = z:=x\;z%=y\;x:=y\;y:=z;
A5: P is_invariant_wrt C,g
  proof
    let s;
    set s1 = g.(s,C);
    assume s in P;
    then
A6: ex s9 st s9 = s & s9.x > s9.y & s9.y >= 0;
A7: s1.y = s.y by A1,A3,Th38;
    s1.x = s.x by A1,A2,Th38;
    hence thesis by A6,A7;
  end;
A8: now
    let s;
    assume s in P;
    then ex s9 st s9 = s & s9.x > s9.y & s9.y >= 0;
    then reconsider m = s.y as Element of NAT by INT_1:3;
    assume g.(g.(s,I),C) in T;
    then g.(g.(s,I),C).b <> 0 by Th2;
    then
A9: g.(s,I).y > 0 by Th38;
A10: g.(s,I).x = s.y by A1,A2,A3,A4,Lm1;
A11: g.(s,I).y = s.x mod s.y by A1,A2,A3,A4,Lm1;
    then m <> 0 by A9,INT_1:def 10;
    then g.(s,I).x > g.(s,I).y by A11,A10,NEWTON:65;
    hence g.(s,I) in P by A9;
  end;
A12: now
    let s;
    set s1 = g.(s,C);
A13: s.y <= 0 implies s1.b = 0 by Th38;
    assume g.(s,C) in P;
    then ex s9 st s9 = g.(s,C) & s9.x > s9.y & s9.y >= 0;
    then reconsider m = s1.y as Element of NAT by INT_1:3;
    s.y > 0 implies s1.b = 1 by Th38;
    then s1 in T iff m > 0 by A13,Th2,Th38;
    hence g iteration_terminates_for I\;C, g.(s,C) by A1,A2,A3,A4,Lm1;
  end;
  C is_terminating_wrt g by AOFA_000:104;
  hence thesis by A5,A8,A12,AOFA_000:107,118;
end;

theorem :: Correctness of Euclid algorithm
  for x,y,z being Variable of g st ex d being Function st d.b = 0 & d.x
  = 1 & d.y = 2 & d.z = 3 for s being Element of Funcs(X, INT) for n,m being
Element of NAT st n = s.x & m = s.y & n > m holds g.(s, while(y gt 0, z:=x\;z%=
  y\;x:=y\;y:=z)).x = n gcd m
proof
  set h = g;
  set S = Funcs(X, INT);
  set T = S\(b,0);
  let x,y,z be Variable of h;
  given d being Function such that
A1: d.b = 0 and
A2: d.x = 1 and
A3: d.y = 2 and
A4: d.z = 3;
  set C = y gt 0;
  set I = z:=x\;z%=y\;x:=y\;y:=z;
  let s be Element of Funcs(X, INT);
  reconsider fin = h.(s, while(C,I)) as Element of S;
  defpred Q[Element of S] means fin.x divides $1.x & fin.x divides $1.y;
A5: for s being Element of S st Q[h.(s,C) qua Element of S] holds Q[s] by A1,A2
,A3,Th38;
A6: for s being Element of S st Q[h.(h.(s,C),I) qua Element of S] & h.(s,C)
  in T holds Q[h.(s,C) qua Element of S]
  proof
    let s be Element of S;
    assume
A7: Q[h.(h.(s,C),I) qua Element of S];
    reconsider s1 = h.(s,C) as Element of S;
    reconsider s2 = h.(s1,I) as Element of S;
A8: s.y <= 0 implies s1.b = 0 by Th38;
A9: s1.x = s.x by A1,A2,Th38;
A10: s2.y = s1.x mod s1.y by A1,A2,A3,A4,Lm1;
A11: s2.x = s1.y by A1,A2,A3,A4,Lm1;
A12: s1.y = s.y by A1,A3,Th38;
    assume h.(s,C) in T;
    then s.x = (s.x div s.y)*(s2.x)+s2.y*1 by A9,A12,A8,A11,A10,Th2,NEWTON:66;
    hence thesis by A1,A2,A3,A4,A7,A9,Lm1,WSIERP_1:5;
  end;
  reconsider s1 = h.(s, C) as Element of S;
A13: s1.y = s.y by A1,A3,Th38;
A14: s.y <= 0 implies s1.b = 0 by Th38;
  let n,m be Element of NAT;
  defpred P[Element of S] means n gcd m divides $1.x & n gcd m divides $1.y &
  $1.x > $1.y & $1.y >= 0;
  defpred R[Element of S] means $1.y > 0;
  assume that
A15: n = s.x and
A16: m = s.y and
A17: n > m;
  s.y > 0 implies s1.b = 1 by Th38;
  then s1 in T iff m > 0 by A16,A14,Th2;
  then
A18: h iteration_terminates_for I\;C, h.(s,C) by A1,A2,A3,A4,A16,A13,Lm1;
A19: for s being Element of S st P[s] & s in T & R[s] holds P[h.(s,I)]
  proof
    let s be Element of S;
    reconsider s99 = h.(s, I) as Element of S;
    assume
A20: P[s];
    then reconsider n9 = s.x, m9 = s.y as Element of NAT by INT_1:3;
    assume that
    s in T and
A21: R[s];
A22: s99.x = s.y by A1,A2,A3,A4,Lm1;
A23: s99.y = s.x mod s.y by A1,A2,A3,A4,Lm1;
    n gcd m divides n9 mod m9 by A20,NAT_D:11;
    hence thesis by A20,A21,A22,A23,NEWTON:65;
  end;
A24: for s being Element of S st P[s] holds P[h.(s,C) qua Element of S] & (h
  .(s,C) in T iff R[h.(s,C) qua Element of S])
  proof
    let s be Element of S;
    assume
A25: P[s];
    reconsider s9 = h.(s,C) as Element of S;
    s9.y = s.y by A1,A3,Th38;
    hence P[h.(s,C) qua Element of S] by A1,A2,A25,Th38;
A26: s.y <= 0 implies s9.b = 0 by Th38;
    s.y > 0 implies s9.b = 1 by Th38;
    hence thesis by A26,Th2,Th38;
  end;
A27: P[s] by A15,A16,A17,NAT_D:def 5;
A28: P[h.(s,while(C,I)) qua Element of S] & not R[h.(s,while(C,I)) qua
  Element of S] from AOFA_000:sch 5(A27,A18,A19,A24);
  then fin.y = 0;
  then
A29: Q[h.(s,while(C,I)) qua Element of S] by INT_2:12;
  Q[s] from AOFA_000:sch 6(A29,A18,A6,A5);
  then fin.x divides n gcd m by A15,A16,INT_2:22;
  then fin.x = n gcd m or fin.x = -(n gcd m) by A28,INT_2:11;
  hence thesis by A28;
end;

Lm2: for x,y,z being Variable of g st ex d being Function st d.b = 0 & d.x = 1
& d.y = 2 & d.z = 3 for s being Element of Funcs(X, INT) holds g.(s, z:=(.x-.y)
\; if-then(z lt 0, z*=-1)\; x:=y\; y:=z).x = s.y & g.(s, z:=(.x-.y)\; if-then(z
lt 0, z*=-1)\; x:=y\; y:=z).y = 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
A1: d.b = 0 and
A2: d.x = 1 and
A3: d.y = 2 and
A4: d.z = 3;
A5: y <> z by A3,A4;
  let s be Element of Funcs(X, INT);
  set J = if-then(z lt 0, z*=-1);
A6: g complies_with_if_wrt T by AOFA_000:def 32;
A7: z <> x by A2,A4;
  set I = z:=(.x-.y)\; J\; x:=y\; y:=z;
A8: x <> y by A2,A3;
A9: now
    let s be Element of S;
    set s1 = g.(s, z:=(.x-.y));
    set s2 = g.(s1, z lt 0);
    set q = g.(s1, J);
    set qz = g.(s2, z*=-1);
A10: (s2.z)*(-1) = -(s2.z);
    set s3 = g.(q, x:=y);
    set s4 = g.(s3, y:=z);
A11: g.(s, I) = g.(g.(s, z:=(.x-.y)\; J\; x:=y), y:=z) by AOFA_000:def 29
      .= g.(g.(g.(s, z:=(.x-.y)\; J), x:=y), y:=z) by AOFA_000:def 29
      .= s4 by AOFA_000:def 29;
    s2.b = 1 implies s2 in T;
    then
A12: s2.b = 1 implies q = qz by A6,AOFA_000:def 30;
A13: (.x).s = s.x by Th22;
A14: qz.y = s2.y by A5,Th31;
A15: (.y).s = s.y by Th22;
    (.x-.y).s = ((.x).s)-((.y).s) by Def11;
    then
A16: s1.z = (s.x)-(s.y) by A13,A15,Th26;
A17: s1.z < 0 implies s2.b = 1 by Th38;
A18: s2.z = s1.z by A1,A4,Th38;
A19: qz.z = (s2.z)*(-1) by Th31;
A20: s3.z = q.z by A7,Th27;
A21: s4.y = s3.z by Th27;
    s2.b = 0 implies s2 nin T by Th2;
    then
A22: s2.b = 0 implies q = s2 by A6,AOFA_000:80;
A23: s1.z >= 0 implies s2.b = 0 by Th38;
A24: s1.y = s.y by A5,Th26;
A25: s3.x = q.y by Th27;
    s2.y = s1.y by A1,A3,Th38;
    hence g.(s, I).x = s.y & g.(s, I).y = abs(s.x-s.y) by A8,A22,A12,A18,A17
,A23,A14,A19,A10,A11,A24,A16,A25,A20,A21,Th27,ABSVALUE:def 1;
  end;
  hence g.(s, I).x = s.y & g.(s, I).y = abs(s.x-s.y);
  deffunc F(Element of S) = IFEQ($1.y,0,0, IFEQ($1.x,0,2, IFEQ($1.x,$1.y,1, In
  (max(2*$1.x,2*$1.y+1), NAT))));
  defpred R[Element of S] means $1.x >= 0 & $1.y > 0;
  set C = y gt 0;
A26: for s being Element of S st R[s] holds (R[g.(s,I\;C) qua Element of S]
  iff g.(s,I\;C) in T) & F(g.(s,I\;C) qua Element of S) < F(s)
  proof
    let s be Element of S;
    assume that
A27: s.x >= 0 and
A28: s.y > 0;
    reconsider s9 = g.(s, I) as Element of S;
    reconsider s99 = g.(s9, C) as Element of S;
A29: s9.y = abs(s.x-s.y) by A9;
    then reconsider
    nx = s.x, ny = s.y, nn = s99.y as Element of NAT by A1,A3,A27,A28,Th38,
INT_1:3;
A30: g.(s,I\;C) = s99 by AOFA_000:def 29;
A31: s99.x = s9.x by A1,A2,Th38;
A32: s9.y <= 0 implies s99.b = 0 by Th38;
A33: s9.y > 0 implies s99.b = 1 by Th38;
    hence
    R[g.(s,I\;C) qua Element of S] iff g.(s,I\;C) in T by A9,A28,A30,A31,A32
,Th2,Th38;
A34: s9.x = s.y by A9;
A35: F(s99) = IFEQ(nn,0,0, IFEQ(ny,0,2, IFEQ(ny,nn,1,max(2*ny,2*nn+1))))
    by A31,A34,FUNCT_7:def 1;
    2*ny+1 > 2*ny by NAT_1:13;
    then
A36: max(2*nx,2*ny+1) > 2*ny by XXREAL_0:30;
A37: s99.y = s9.y by A1,A3,Th38;
A38: F(s) = IFEQ(ny,0,0, IFEQ(nx,0,2, IFEQ(nx,ny,1,max(2*nx,2*ny+1)))) by
FUNCT_7:def 1
      .= IFEQ(nx,0,2, IFEQ(nx,ny,1,max(2*nx,2*ny+1))) by A28,FUNCOP_1:def 8;
    per cases by XXREAL_0:1;
    suppose
A39:  nx = ny;
      then
A40:  IFEQ(nx,ny,1,max(2*nx,2*ny+1)) = 1 by FUNCOP_1:def 8;
A41:  nn = 0 by A37,A29,A39,ABSVALUE:2;
      F(s) = IFEQ(nx,ny,1,max(2*nx,2*ny+1)) by A28,A38,A39,FUNCOP_1:def 8;
      hence thesis by A30,A40,A41,FUNCOP_1:def 8;
    end;
    suppose
A42:  nx > ny;
      then IFEQ(nx,ny,1,max(2*nx,2*ny+1)) = max(2*nx,2*ny+1) by FUNCOP_1:def 8;
      then
A43:  F(s) = max(2*nx,2*ny+1) by A38,A42,FUNCOP_1:def 8;
A44:  nx-ny > 0 by A42,XREAL_1:50;
      then
A45:  F(s99) = IFEQ(ny,0,2, IFEQ(ny,nn,1,max(2*ny,2*nn+1))) by A37,A33,A32,A29
,A35,ABSVALUE:def 1,FUNCOP_1:def 8
        .= IFEQ(ny,nn,1,max(2*ny,2*nn+1)) by A28,FUNCOP_1:def 8;
      then
A46:  ny = nn implies F(s99) = 1 by FUNCOP_1:def 8;
      nn = nx-ny by A37,A29,A44,ABSVALUE:def 1;
      then nn < nx by A28,XREAL_1:44;
      then nn+1 <= nx by NAT_1:13;
      then
A47:  2*(nn+1) <= 2*nx by XREAL_1:64;
A48:  1 <= 2*nn+1 by NAT_1:11;
A49:  ny <> nn implies F(s99) = max(2*ny,2*nn+1) by A45,FUNCOP_1:def 8;
      2*nn+2 = 2*nn+1+1;
      then 2*nn+1 < 2*nx by A47,NAT_1:13;
      then 2*nn+1 < F(s) by A43,XXREAL_0:30;
      hence thesis by A30,A36,A43,A46,A49,A48,XXREAL_0:2,29;
    end;
    suppose
A50:  nx < ny & nx > 0;
A51:  -(nx-ny) = ny-nx;
A52:  nx-ny < 0 by A50,XREAL_1:49;
      then
A53:  nn = -(nx-ny) by A37,A29,ABSVALUE:def 1;
      then
A54:  nn < ny by A50,A51,XREAL_1:44;
      2*nn < 2*ny by A50,A53,A51,XREAL_1:44,68;
      then 2*nn+1 < 2*ny+1 by XREAL_1:6;
      then
A55:  2*nn+1 < max(2*nx,2*ny+1) by XXREAL_0:30;
      nn > 0 by A37,A29,A52,A51,ABSVALUE:def 1;
      then
A56:  F(s99) = IFEQ(ny,0,2, IFEQ(ny,nn,1,max(2*ny,2*nn+1))) by A35,
FUNCOP_1:def 8
        .= IFEQ(ny,nn,1,max(2*ny,2*nn+1)) by A28,FUNCOP_1:def 8
        .= max(2*ny,2*nn+1) by A54,FUNCOP_1:def 8;
      F(s) = IFEQ(nx,ny,1,max(2*nx,2*ny+1)) by A38,A50,FUNCOP_1:def 8
        .= max(2*nx,2*ny+1) by A50,FUNCOP_1:def 8;
      hence thesis by A30,A36,A55,A56,XXREAL_0:29;
    end;
    suppose
A57:  nx = 0;
      then
A58:  F(s) = 2 by A38,FUNCOP_1:def 8;
A59:  nn = -(nx-ny) by A28,A37,A29,A57,ABSVALUE:def 1
        .= ny by A57;
      then F(s99) = IFEQ(ny,0,2, IFEQ(ny,nn,1,max(2*ny,2*nn+1))) by A28,A35,
FUNCOP_1:def 8
        .= IFEQ(ny,nn,1,max(2*ny,2*nn+1)) by A28,FUNCOP_1:def 8
        .= 1 by A59,FUNCOP_1:def 8;
      hence thesis by A30,A58;
    end;
  end;
  let n,m be Element of NAT;
  assume that
A60: n = s.x and
A61: m = s.y;
  assume s in T iff m > 0;
  then
A62: s in T iff R[s] by A60,A61;
  g iteration_terminates_for I\;C, s from AOFA_000:sch 3(A62,A26);
  hence thesis;
end;

theorem :: Termination of Euclid algorithm 2
  for x,y,z being Variable of g st ex d being Function st d.b = 0 & d.x
= 1 & d.y = 2 & d.z = 3 holds while(y gt 0, z:=(.x-.y)\; if-then(z lt 0, z*=-1)
  \; x:=y\; y:=z) is_terminating_wrt g, {s: s.x >= 0 & s.y >= 0}
proof
  set S = Funcs(X, INT);
  set T = S\(b,0);
  let x,y,z be Variable of g;
  set P = {s: s.x >= 0 & s.y >= 0};
  given d being Function such that
A1: d.b = 0 and
A2: d.x = 1 and
A3: d.y = 2 and
A4: d.z = 3;
  set C = y gt 0, I = z:=(.x-.y)\; if-then(z lt 0, z*=-1)\; x:=y\; y:=z;
A5: now
    let s;
    assume s in P;
    then ex s9 st s9 = s & s9.x >= 0 & s9.y >= 0;
    then reconsider m = s.y as Element of NAT by INT_1:3;
    assume g.(g.(s,I),C) in T;
A6: g.(s,I).x = m by A1,A2,A3,A4,Lm2;
    g.(s,I).y = abs(s.x-s.y) by A1,A2,A3,A4,Lm2;
    hence g.(s,I) in P by A6;
  end;
A7: now
    let s;
    set s1 = g.(s,C);
A8: s.y <= 0 implies s1.b = 0 by Th38;
    assume g.(s,C) in P;
    then ex s9 st s9 = g.(s,C) & s9.x >= 0 & s9.y >= 0;
    then reconsider n = s1.x, m = s1.y as Element of NAT by INT_1:3;
A9: n = n;
    s.y > 0 implies s1.b = 1 by Th38;
    then s1 in T iff m > 0 by A8,Th2,Th38;
    hence g iteration_terminates_for I\;C, g.(s,C) by A1,A2,A3,A4,A9,Lm2;
  end;
A10: P is_invariant_wrt C,g
  proof
    let s;
    set s1 = g.(s,C);
    assume s in P;
    then
A11: ex s9 st s9 = s & s9.x >= 0 & s9.y >= 0;
A12: s1.y = s.y by A1,A3,Th38;
    s1.x = s.x by A1,A2,Th38;
    hence thesis by A11,A12;
  end;
  C is_terminating_wrt g by AOFA_000:104;
  hence thesis by A10,A5,A7,AOFA_000:107,118;
end;

theorem :: Euclid algorithm 2
  for x,y,z being Variable of g st ex d being Function st d.b = 0 & d.x
  = 1 & d.y = 2 & d.z = 3 for s being Element of Funcs(X, INT) for n,m being
Element of NAT st n = s.x & m = s.y & n > 0 holds g.(s, while(y gt 0, z:=(.x-.y
  )\; if-then(z lt 0, z*=-1)\; x:=y\; y:=z ) ).x = n gcd m
proof
  set h = g;
  set S = Funcs(X, INT);
  set T = S\(b,0);
A1: h complies_with_if_wrt T by AOFA_000:def 32;
  let x,y,z be Variable of h;
  given d being Function such that
A2: d.b = 0 and
A3: d.x = 1 and
A4: d.y = 2 and
A5: d.z = 3;
  set C = y gt 0;
  let s be Element of Funcs(X, INT);
A6: y <> z by A4,A5;
  reconsider s1 = h.(s, C) as Element of S;
A7: s1.x = s.x by A2,A3,Th38;
A8: s1.y = s.y by A2,A4,Th38;
A9: s.y <= 0 implies s1.b = 0 by Th38;
  defpred R[Element of S] means $1.x > 0 & $1.y > 0;
  let n,m be Element of NAT;
  defpred P[Element of S] means n gcd m divides $1.x & n gcd m divides $1.y &
$1.x > 0 & $1.y >= 0 & for c being Nat st c divides $1.x & c divides $1.y holds
  c divides n gcd m;
  set J = if-then(z lt 0, z*=-1);
  set I = z:=(.x-.y)\; J\; x:=y\; y:=z;
  assume that
A10: n = s.x and
A11: m = s.y and
A12: n > 0;
  s.y > 0 implies s1.b = 1 by Th38;
  then s1 in T iff R[s1] by A10,A12,A9,Th2,Th38;
  then
A13: h iteration_terminates_for I\;C, h.(s,C) by A2,A3,A4,A5,A10,A11,A12,A7,A8
,Lm2;
A14: z <> x by A3,A5;
A15: x <> y by A3,A4;
A16: now
    let s be Element of S;
    set s1 = h.(s, z:=(.x-.y));
    set s2 = h.(s1, z lt 0);
    set q = h.(s1, J);
    set qz = h.(s2, z*=-1);
A17: (s2.z)*(-1) = -(s2.z);
    set s3 = h.(q, x:=y);
    set s4 = h.(s3, y:=z);
A18: h.(s, I) = h.(h.(s, z:=(.x-.y)\; J\; x:=y), y:=z) by AOFA_000:def 29
      .= h.(h.(h.(s, z:=(.x-.y)\; J), x:=y), y:=z) by AOFA_000:def 29
      .= s4 by AOFA_000:def 29;
    s2.b = 1 implies s2 in T;
    then
A19: s2.b = 1 implies q = qz by A1,AOFA_000:def 30;
A20: (.x).s = s.x by Th22;
A21: qz.y = s2.y by A6,Th31;
A22: (.y).s = s.y by Th22;
    (.x-.y).s = ((.x).s)-((.y).s) by Def11;
    then
A23: s1.z = (s.x)-(s.y) by A20,A22,Th26;
A24: s1.z < 0 implies s2.b = 1 by Th38;
A25: s2.z = s1.z by A2,A5,Th38;
A26: qz.z = (s2.z)*(-1) by Th31;
A27: s3.z = q.z by A14,Th27;
A28: s4.y = s3.z by Th27;
    s2.b = 0 implies s2 nin T by Th2;
    then
A29: s2.b = 0 implies q = s2 by A1,AOFA_000:80;
A30: s1.z >= 0 implies s2.b = 0 by Th38;
A31: s1.y = s.y by A6,Th26;
A32: s3.x = q.y by Th27;
    s2.y = s1.y by A2,A4,Th38;
    hence h.(s, I).x = s.y & h.(s, I).y = abs(s.x-s.y) by A15,A29,A19,A25,A24
,A30,A21,A26,A17,A18,A31,A23,A32,A27,A28,Th27,ABSVALUE:def 1;
  end;
A33: for s being Element of S st P[s] & s in T & R[s] holds P[h.(s,I)]
  proof
    let s be Element of S;
    reconsider s99 = h.(s, I) as Element of S;
A34: abs(n gcd m) = n gcd m by ABSVALUE:def 1;
A35: s99.y = abs(s.x-s.y) by A16;
    assume
A36: P[s];
    then reconsider n9 = s.x, m9 = s.y as Element of NAT by INT_1:3;
    assume that
    s in T and
A37: R[s];
    n gcd m divides n9-m9 by A36,PREPOWER:94;
    hence
    n gcd m divides h.(s,I).x & n gcd m divides h.(s,I).y & h.(s,I).x > 0
    & h.(s,I).y >= 0 by A16,A36,A37,A35,A34,INT_2:16;
    let c be Nat;
    reconsider c9 = c as Element of NAT by ORDINAL1:def 12;
    assume that
A38: c divides h.(s,I).x and
A39: c divides h.(s,I).y;
A40: abs c = c by ABSVALUE:def 1;
A41: s99.x = s.y by A16;
    c9 divides abs(n9-m9) by A16,A39;
    then
A42: c divides n9-m9 by A40,INT_2:16;
    c qua Integer divides m9 by A16,A38;
    then c divides (n9-m9)+m9 by A42,WSIERP_1:4;
    hence thesis by A36,A41,A38;
  end;
A43: for s being Element of S st P[s] holds P[h.(s,C) qua Element of S] & (h
  .(s,C) in T iff R[h.(s,C) qua Element of S])
  proof
    let s be Element of S;
    assume
A44: P[s];
    reconsider s9 = h.(s,C) as Element of S;
A45: s9.y = s.y by A2,A4,Th38;
    s9.x = s.x by A2,A3,Th38;
    hence P[h.(s,C) qua Element of S] by A44,A45;
A46: s.y <= 0 implies s9.b = 0 by Th38;
    s.y > 0 implies s9.b = 1 by Th38;
    hence thesis by A44,A46,Th2,Th38;
  end;
  reconsider fin = h.(s, while(C,I)) as Element of S;
A47: P[s] by A10,A11,A12,NAT_D:def 5;
A48: P[h.(s,while(C,I)) qua Element of S] & not R[h.(s,while(C,I)) qua
  Element of S] from AOFA_000:sch 5(A47,A13,A33,A43);
  then reconsider fn = fin.x as Element of NAT by INT_1:3;
A49: fn divides 0 by NAT_D:6;
  fin.y = 0 by A48;
  then fn divides n gcd m by A48,A49;
  hence thesis by A48,NAT_D:5;
end;

theorem
  for x,y,m being Variable of g st ex d being Function st d.b = 0 & d.x
= 1 & d.y = 2 & d.m = 3 holds y:=1\; while(m gt 0, if-then(m is_odd, y*=x)\; m
  /=2\; x*=x ) is_terminating_wrt g, {s: s.m >= 0}
proof
  set S = Funcs(X, INT);
  set T = S\(b,0);
  let x,y,m be Variable of g;
  set P = {s: s.m >= 0};
  given d being Function such that
A1: d.b = 0 and
A2: d.x = 1 and
A3: d.y = 2 and
A4: d.m = 3;
  set C = m gt 0;
A5: y:=1 is_terminating_wrt g, P by AOFA_000:107;
  deffunc F(Element of S) = In($1.m, NAT);
  defpred R[Element of S] means $1.m > 0;
  set I = if-then(m is_odd, y*=x);
  set J = I\; m/=2\; x*=x;
A6: g complies_with_if_wrt T by AOFA_000:def 32;
A7: P is_invariant_wrt C,g
  proof
    let s;
    assume s in P;
    then
A8: ex s9 st s = s9 & s9.m >= 0;
    g.(s, C).m = s.m by A1,A4,Th38;
    hence g.(s, C) in P by A8;
  end;
A9: for s st s in P & g.(g.(s,J),C) in T holds g.(s,J) in P
  proof
    let s such that
    s in P;
    assume g.(g.(s,J),C) in T;
    then g.(s,J).m > 0 by Th40;
    hence thesis;
  end;
A10: m <> y by A3,A4;
A11: P is_invariant_wrt y:=1, g
  proof
    let s;
    assume s in P;
    then
A12: ex s9 st s = s9 & s9.m >= 0;
    g.(s, y:=1).m = s.m by A10,Th25;
    hence g.(s, y:=1) in P by A12;
  end;
A13: m <> x by A2,A4;
A14: for s st g.(s,C) in P holds g iteration_terminates_for J\;C, g.(s,C)
  proof
A15: for s being Element of S st R[s] holds (R[g.(s,J\;C)] iff g.(s,J\;C)
    in T) & F(g.(s,J\;C)) < F(s)
    proof
      let s be Element of S such that
A16:  s.m > 0;
A17:  F(s) = s.m by A16,FUNCT_7:def 1,INT_1:3;
      set q1 = g.(s,I);
      set q0 = g.(s, m is_odd);
      set sJ = g.(s,J);
      set sC = g.(sJ,C);
A18:  g.(s,J\;C) = sC by AOFA_000:def 29;
A19:  sJ.m <= 0 implies sC.b = 0 by Th38;
      sJ.m > 0 implies sC.b = 1 by Th38;
      hence R[g.(s,J\;C)] iff g.(s,J\;C) in T by A19,A18,Th2,Th38;
      set q2 = g.(q1,m/=2);
      set q3 = g.(q2,x*=x);
A20:  q1 = g.(q0, y*=x) or q1 = g.(q0, EmptyIns A) by A6,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
A21:  sJ.m = q2.m by A13,Th33
        .= (q1.m) div 2 by Th45
        .= (q0.m) div 2 by A10,A20,Th33,AOFA_000:def 28
        .= (s.m) div 2 by A1,A4,Th49;
A22:  sC.m = sJ.m by A1,A4,Th38;
      then sC.m in NAT by A16,A21,INT_1:3,61;
      then F(sC) = sC.m by FUNCT_7:def 1;
      hence thesis by A16,A22,A18,A21,A17,INT_1:56;
    end;
    let s0 be Element of S such that
    g.(s0,C) in P;
    set s1 = g.(s0,C);
A23: s0.m <= 0 implies s1.b = 0 by Th38;
    s0.m > 0 implies s1.b = 1 by Th38;
    then
A24: g.(s0,C) in T iff R[g.(s0,C)] by A23,Th2,Th38;
    thus g iteration_terminates_for J\;C, g.(s0,C) from AOFA_000:sch 3(A24,A15
    );
  end;
  J is_terminating_wrt g,P by AOFA_000:107;
  then while(m gt 0, if-then(m is_odd, y*=x)\; m/=2\; x*=x )
  is_terminating_wrt g, P by A7,A9,A14,AOFA_000:104,118;
  hence thesis by A5,A11,AOFA_000:111;
end;

::$N Correctness of the algorithm of exponentiation by squaring
theorem
  for x,y,m being Variable of g st ex d being Function st d.b = 0 & d.x
= 1 & d.y = 2 & d.m = 3 for s being Element of Funcs(X, INT) for n being Nat st
n = s.m holds g.(s, y:=1\; while(m gt 0, if-then(m is_odd, y*=x)\; m/=2\; x*=x
  ) ).y = (s.x)|^n
proof
  set S = Funcs(X, INT);
  set T = S\(b,0);
A1: g complies_with_if_wrt T by AOFA_000:def 32;
  let x,y,m be Variable of g;
  given d being Function such that
A2: d.b = 0 and
A3: d.x = 1 and
A4: d.y = 2 and
A5: d.m = 3;
  defpred R[Element of S] means $1.m > 0;
  set C = m gt 0;
  let s be Element of Funcs(X, INT);
  let n be Nat;
  defpred P[Element of S] means (s.x)|^n = ($1.y)*(($1.x)to_power($1.m)) & $1.
  m >= 0;
  deffunc F(Element of S) = In($1.m, NAT);
  set I = if-then(m is_odd, y*=x);
  set J = I\; m/=2\; x*=x;
  set s0 = g.(s, y:=1);
A6: m <> y by A4,A5;
  then
A7: s0.m = s.m by Th25;
A8: for s being Element of S st P[s] holds P[g.(s,C)] & (g.(s,C) in T iff R
  [g.(s,C)])
  proof
    let s be Element of S such that
A9: P[s];
    set s1 = g.(s, C);
A10: s1.x = s.x by A2,A3,Th38;
    s1.m = s.m by A2,A5,Th38;
    hence P[g.(s,C)] by A2,A4,A9,A10,Th38;
A11: s.m <= 0 implies s1.b = 0 by Th38;
    s.m > 0 implies s1.b = 1 by Th38;
    hence thesis by A11,Th2,Th38;
  end;
A12: s0.y = 1 by Th25;
  set fs = g.(s0, while(C,J));
  set s1 = g.(s0,C);
  assume
A13: n = s.m;
A14: (fs.x) to_power 0 = 1 by POWER:24;
A15: m <> x by A3,A5;
A16: for s being Element of S st R[s] holds (R[g.(s,J\;C)] iff g.(s,J\;C) in
  T) & F(g.(s,J\;C)) < F(s)
  proof
    let s be Element of S such that
A17: s.m > 0;
A18: F(s) = s.m by A17,FUNCT_7:def 1,INT_1:3;
    set q1 = g.(s,I);
    set q0 = g.(s, m is_odd);
    set sJ = g.(s,J);
    set sC = g.(sJ,C);
A19: g.(s,J\;C) = sC by AOFA_000:def 29;
A20: sJ.m <= 0 implies sC.b = 0 by Th38;
    sJ.m > 0 implies sC.b = 1 by Th38;
    hence R[g.(s,J\;C)] iff g.(s,J\;C) in T by A20,A19,Th2,Th38;
    set q2 = g.(q1,m/=2);
    set q3 = g.(q2,x*=x);
A21: q1 = g.(q0, y*=x) or q1 = g.(q0, EmptyIns A) by A1,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
A22: sJ.m = q2.m by A15,Th33
      .= (q1.m) div 2 by Th45
      .= (q0.m) div 2 by A6,A21,Th33,AOFA_000:def 28
      .= (s.m) div 2 by A2,A5,Th49;
A23: sC.m = sJ.m by A2,A5,Th38;
    then sC.m in NAT by A17,A22,INT_1:3,61;
    then F(sC) = sC.m by FUNCT_7:def 1;
    hence thesis by A17,A23,A19,A22,A18,INT_1:56;
  end;
  set q = s;
A24: x <> y by A3,A4;
A25: for s being Element of S st P[s] & s in T & R[s] holds P[g.(s,J)]
  proof
    let s be Element of S such that
A26: P[s] and
    s in T and
    R[s];
    reconsider sm = s.m as Element of NAT by A26,INT_1:3;
    s.m = ((s.m) div 2)*2+((s.m) mod 2) by NEWTON:66;
    then
A27: (q.x)|^n = (s.y)*(((s.x)to_power((sm div 2)*2))*((s.x)to_power(sm mod
    2))) by A26,FIB_NUM2:5
      .= (s.y)*((s.x)to_power(sm mod 2))*((s.x)to_power((sm div 2)*2))
      .= (s.y)*((s.x)to_power(sm mod 2))* (((s.x)to_power 2) to_power (sm
    div 2)) by NEWTON:9
      .= (s.y)*((s.x)to_power(sm mod 2))* (((s.x)*(s.x)) to_power (sm div 2)
    ) by NEWTON:81;
    set q1 = g.(s,I);
    set q0 = g.(s, m is_odd);
    set sJ = g.(s,J);
    set q2 = g.(q1,m/=2);
    set q3 = g.(q2,x*=x);
A28: q1 = g.(q0, y*=x) or q1 = g.(q0, EmptyIns A) by A1,AOFA_000:def 30;
A29: q2.x = q1.x by A15,Th45
      .= q0.x by A24,A28,Th33,AOFA_000:def 28;
A30: q2.y = q1.y by A6,Th45;
A31: q0.y = s.y by A2,A4,Th49;
A32: q0.x = s.x by A2,A3,Th49;
    q2 = g.(s,I\;m/=2) by AOFA_000:def 29;
    then
A33: q3 = g.(s,J) by AOFA_000:def 29;
    then
A34: sJ.y = q2.y by A24,Th33;
A35: sm div 2 = s.m div 2;
A36: now
A37:  q0.b = (s.m) mod 2 by Th49;
      per cases by A35,A37,NAT_D:12;
      suppose
A38:    q0.b = 0;
        then q0 nin T by Th2;
        then q1 = g.(q0, EmptyIns A) by A1,AOFA_000:def 30;
        then
A39:    q1.y = q0.y by AOFA_000:def 28;
A40:    (s.y)*1 = s.y;
        (s.x)to_power 0 = 1 by POWER:24;
        hence (s.y)*((s.x)to_power(sm mod 2)) = sJ.y by A34,A30,A31,A38,A39,A40
,Th49;
      end;
      suppose
A41:    q0.b = 1;
        then q0 in T;
        then q1 = g.(q0, y*=x) by A1,AOFA_000:def 30;
        then
A42:    q1.y = (q0.y)*(q0.x) by Th33;
        (s.x)to_power 1 = s.x by POWER:25;
        hence (s.y)*((s.x)to_power(sm mod 2)) = sJ.y by A32,A34,A30,A31,A41,A42
,Th49;
      end;
    end;
    sJ.m = q2.m by A15,A33,Th33
      .= (q1.m) div 2 by Th45
      .= (q0.m) div 2 by A6,A28,Th33,AOFA_000:def 28
      .= (s.m) div 2 by A2,A5,Th49;
    hence thesis by A33,A29,A32,A36,A27,Th33;
  end;
A43: s0.m <= 0 implies s1.b = 0 by Th38;
  s0.m > 0 implies s1.b = 1 by Th38;
  then
A44: g.(s0,C) in T iff R[g.(s0,C)] by A43,Th2,Th38;
A45: g iteration_terminates_for J\;C, g.(s0,C) from AOFA_000:sch 3(A44, A16);
  s0.x = s.x by A24,Th25;
  then
A46: P[s0] by A13,A7,A12,POWER:41;
A47: P[g.(s0,while(C,J))] & not R[g.(s0,while(C,J))] from AOFA_000:sch 5(A46
  ,A45,A25,A8);
  then fs.m = 0;
  hence thesis by A47,A14,AOFA_000:def 29;
end;