:: Mizar Analysis of Algorithms: Algorithms over Integers
::  by Grzegorz Bancerek
:: 
:: Received March 18, 2008
:: Copyright (c) 2008 Association of Mizar Users

environ

 vocabularies AOFA_I00, AOFA_000, FUNCT_1, GROUP_1, FINSEQ_1, RELAT_1, FUNCT_2,
      ORDINAL2, BOOLE, FUNCT_7, FUNCOP_1, FUNCT_4, ARYTM, AMI_3, TARSKI,
      TREES_4, INT_1, QC_LANG1, MSUALG_3, FRAENKEL, ARYTM_1, FINSET_1,
      CQC_LANG, CARD_4, NEWTON, AMI_2, VECTSP_1, ARYTM_3, FREEALG, CARD_1,
      PRE_FF, NAT_1, ABSVALUE, SEQ_1, LANG1, SQUARE_1, EUCLMETR, SCMFSA6C,
      ZF_LANG, SGRAPH1, MCART_1, REAL_3, POWER, CAT_1, MATRIX_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, PRE_TOPC, ENUMSET1, MCART_1,
      ORDINAL1, MEMBERED, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2,
      FUNCT_3, FINSET_1, CQC_LANG, LANG1, MSAFREE1, FINSEQ_1, REAL_3, SEQ_1,
      SEQM_3, SEQ_4, BINOP_1, CARD_1, CARD_2, CARD_3, CARD_4, FRAENKEL, PROB_2,
      FINSEQ_2, FINSEQOP, PBOOLE, PZFMISC1, PRE_FF, PRE_CIRC, FACIRC_1,
      NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, POWER, TREES_1, TREES_2, TREES_3,
      ABSVALUE, INT_1, INT_2, NAT_1, NAT_D, NEWTON, ABIAN, BINARITH, WSIERP_1,
      VALUED_1, SUPINF_1, FUNCOP_1, FUNCT_4, FUNCT_7, CAT_2, MESFUNC1,
      BORSUK_1, POLYNOM1, AMI_2, STRUCT_0, UNIALG_1, UNIALG_2, ALG_1, FREEALG,
      COMPUT_1, TREES_4, DTCONSTR, MSUALG_1, MSAFREE, MSATERM, MSUALG_3,
      PRALG_3, FINSEQ_4, AOFA_000;
 constructors ORDINAL2, FINSEQ_1, UNIALG_1, PUA2MSS1, COMPUT_1, FUNCT_7,
      BINOP_1, BINARITH, REAL_1, BORSUK_1, SUPINF_1, SUPINF_2, POLYNOM1,
      CATALG_1, MSATERM, MSAFREE3, PROB_2, MSAFREE1, MSUALG_3, CQC_LANG,
      FACIRC_1, CARD_4, AMI_2, FUNCT_3, MESFUNC1, PREPOWER, POWER, NAT_D,
      NEWTON, ABIAN, VALUED_0, VALUED_1, NAT_1, SQUARE_1, ALG_1, FREEALG,
      FINSEQ_4, FINSOP_1, ORDERS_1, PZFMISC1, PRE_FF, INT_2, SEQ_4, ABSVALUE,
      REAL_3, FUNCT_5, FINSEQOP, WSIERP_1, ENUMSET1, PRE_CIRC, WELLORD2,
      CLASSES1, CARD_2, UNIALG_2, CAT_2, PRALG_3, AOFA_000;
 registrations ZFMISC_1, RELSET_1, FUNCT_1, FUNCOP_1, FINSEQ_2, FRAENKEL,
      FUNCT_2, FINSEQ_1, UNIALG_1, COMPUT_1, NUMBERS, NAT_1, ORDINAL1,
      STRUCT_0, PUA2MSS1, SUPINF_1, PBOOLE, MSUALG_1, INSTALG1, MSATERM,
      MSAFREE1, MSAFREE3, MSUALG_2, PRALG_1, DTCONSTR, FREEALG, FUNCT_7, INT_1,
      CARD_4, WAYBEL12, CARD_5, SUBSET_1, AFINSQ_1, CARD_1, CLASSES1, ORDERS_1,
      CARD_3, VALUED_0, VALUED_1, MEMBERED, XREAL_0, REAL_3, TREES_4, XCMPLX_0,
      XXREAL_0, XBOOLE_0, FINSET_1, POWER, TREES_1, PRE_CIRC, FACIRC_1,
      RELAT_1, UNIALG_2, PRE_TOPC, AOFA_000, ABIAN;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
 definitions VALUED_0, XCMPLX_0, PZFMISC1, TREES_4, SUPINF_2, MEMBERED,
      FINSEQ_2, CARD_2, TARSKI, XBOOLE_0, PUA2MSS1, SEQ_1, FINSEQ_4, FUNCT_1,
      FUNCT_2, FREEALG, RELAT_1, FINSEQ_1, UNIALG_1, UNIALG_2, COMPUT_1,
      BINOP_1, AOFA_000;
 theorems XBOOLE_1, ZFMISC_1, RELAT_1, FUNCT_2, FUNCOP_1, CQC_LANG, TARSKI,
      NEWTON, XREAL_1, INT_1, FUNCT_7, NAT_1, ORDINAL1, FUNCT_4, FREEALG,
      PRE_FF, INT_2, ABSVALUE, WSIERP_1, TREES_4, NUMBERS, FUNCT_1, RFUNCT_1,
      CARD_2, CARD_1, CARD_4, WELLORD2, FINSET_1, FUNCT_5, AOFA_000, MCART_1,
      XXREAL_0, JORDAN12, POWER, POLYEQ_3, FIB_NUM2, ORDINAL3, POLYNOM1, NAT_D,
      PREPOWER, VALUED_1;
 schemes FUNCT_1, FUNCT_2, WELLORD2, XBOOLE_0, AOFA_000, TARSKI;

begin :: Preliminaries

theorem Lem3:
  for x,y,z,a,b,c being set st a <> b & b <> c & c <> a
  ex f being Function st f.a = x & f.b = y & f.c = z
  proof
    let x,y,z,a,b,c be set such that
Z1: a <> b & b <> c & c <> a;
    set fa = a.-->x;
    set fb = b.-->y;
    set fc = c.-->z;
    take f = fa+*fb+*fc;
    dom fc = {c} & dom fb = {b} & dom fa = {a} by CQC_LANG:5; then
Z2: a nin dom fc & a nin dom fb & b nin dom fc & b in dom fb & c in dom fc
    by Z1,TARSKI:def 1;
    thus f.a = (fa+*fb).a by Z2,FUNCT_4:12 .= fa.a by Z2,FUNCT_4:12
    .= x by CQC_LANG:6;
    thus f.b = (fa+*fb).b by Z2,FUNCT_4:12 .= fb.b by Z2,FUNCT_4:14
    .= y by CQC_LANG:6;
    thus f.c = fc.c by Z2,FUNCT_4:14 .= z by CQC_LANG:6;
  end;

definition
  let F be non empty functional set;
  let x be set;
  let f be set;
  func F\(x,f) -> Subset of F equals {g where g is Element of F: g.x <> f};
  coherence
  proof
    set X = {g where g is Element of F: g.x <> f};
    X c= F
    proof let a be set; assume
      a in X; then
      ex g being Element of F st g = a & g.x <> f;
      hence thesis;
    end;
    hence thesis;
  end;
end;

theorem LemTS:
  for F being non empty functional set, x,y be set, g being Element of F
  holds g in F\(x,y) iff g.x <> y
  proof
    let F be non empty functional set;
    let x,y be set;
    let g be Element of F;
    g in F\(x,y) iff ex f being Element of F st g = f & f.x <> y;
    hence thesis;
  end;

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

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

definition
  let t1,t2 be integer-yielding Function;
  func t1 div t2 -> integer-yielding Function means:
DEFdiv:
  dom it = (dom t1) /\ (dom t2) & :: \ (t2"{0}) &
  for s being set st s in dom it holds it.s = (t1.s) div (t2.s);
  correctness
  proof
    deffunc F(set) = (t1.$1) div (t2.$1);
    consider f being Function such that
A1: dom f = (dom t1) /\ (dom t2) &
    for x being set st x in (dom t1) /\ (dom t2) holds f.x = F(x)
    from FUNCT_1:sch 3;
    f is integer-yielding
    proof
      let x be set;
      assume x in dom f; then
      f.x = F(x) by A1;
      hence thesis;
    end;
    hence ex f being integer-yielding Function st dom f = (dom t1)/\(dom t2) &
    for x being set st x in dom f holds f.x = F(x) by A1;
    let f1,f2 be integer-yielding Function such that
A3: dom f1 = (dom t1) /\ dom t2 and
A4: for s being set st s in dom f1 holds f1.s = F(s) and
A5: dom f2 = (dom t1) /\ dom t2 and
A6: for s being set st s in dom f2 holds f2.s = F(s);
    now
      let s be set;
      assume
A7:   s in (dom t1) /\ dom t2;
      hence f1.s = F(s) by A3,A4 .= f2.s by A5,A6,A7;
    end;
    hence thesis by A3,A5,FUNCT_1:9;
  end;
  func t1 mod t2 -> integer-yielding Function means:
DEFmod:
  dom it = (dom t1) /\ (dom t2) & :: \ (t2"{0}) &
  for s being set st s in dom it holds it.s = (t1.s) mod (t2.s);
  correctness
  proof
    deffunc F(set) = (t1.$1) mod (t2.$1);
    consider f being Function such that
A1: dom f = (dom t1) /\ (dom t2) &
    for x being set st x in (dom t1) /\ (dom t2) holds f.x = F(x)
    from FUNCT_1:sch 3;
    f is integer-yielding
    proof
      let x be set;
      assume x in dom f; then
      f.x = F(x) by A1;
      hence thesis;
    end;
    hence ex f being integer-yielding Function st dom f = (dom t1)/\(dom t2) &
    for x being set st x in dom f holds f.x = F(x) by A1;
    let f1,f2 be integer-yielding Function such that
A3: dom f1 = (dom t1) /\ dom t2 and
A4: for s being set st s in dom f1 holds f1.s = F(s) and
A5: dom f2 = (dom t1) /\ dom t2 and
A6: for s being set st s in dom f2 holds f2.s = F(s);
    now
      let s be set;
      assume
A7:   s in (dom t1) /\ dom t2;
      hence f1.s = F(s) by A3,A4 .= f2.s by A5,A6,A7;
    end;
    hence thesis by A3,A5,FUNCT_1:9;
  end;
  func leq(t1,t2) -> integer-yielding Function means:
DEFleq:
  dom it = (dom t1) /\ (dom t2) &
  for s being set st s in dom it holds it.s = IFGT(t1.s,t2.s,0,1);
  correctness
  proof
    deffunc F(set) = IFGT(t1.$1,t2.$1,0,1);
    consider f being Function such that
A1: dom f = (dom t1) /\ (dom t2) &
    for x being set st x in (dom t1) /\ (dom t2) holds f.x = F(x)
    from FUNCT_1:sch 3;
    f is integer-yielding
    proof
      let x be set;
      assume x in dom f; then
      f.x = F(x) by A1;
      hence thesis;
    end;
    hence ex f being integer-yielding Function st dom f = (dom t1)/\(dom t2) &
    for x being set st x in dom f holds f.x = F(x) by A1;
    let f1,f2 be integer-yielding Function such that
A3: dom f1 = (dom t1) /\ dom t2 and
A4: for s being set st s in dom f1 holds f1.s = F(s) and
A5: dom f2 = (dom t1) /\ dom t2 and
A6: for s being set st s in dom f2 holds f2.s = F(s);
    now
      let s be set;
      assume
A7:   s in (dom t1) /\ dom t2;
      hence f1.s = F(s) by A3,A4 .= f2.s by A5,A6,A7;
    end;
    hence thesis by A3,A5,FUNCT_1:9;
  end;
  func gt(t1,t2) -> integer-yielding Function means:
DEFgt:
  dom it = (dom t1) /\ (dom t2) &
  for s being set st s in dom it holds it.s = IFGT(t1.s,t2.s,1,0);
  correctness
  proof
    deffunc F(set) = IFGT(t1.$1,t2.$1,1,0);
    consider f being Function such that
A1: dom f = (dom t1) /\ (dom t2) &
    for x being set st x in (dom t1) /\ (dom t2) holds f.x = F(x)
    from FUNCT_1:sch 3;
    f is integer-yielding
    proof
      let x be set;
      assume x in dom f; then
      f.x = F(x) by A1;
      hence thesis;
    end;
    hence ex f being integer-yielding Function st dom f = (dom t1)/\(dom t2) &
    for x being set st x in dom f holds f.x = F(x) by A1;
    let f1,f2 be integer-yielding Function such that
A3: dom f1 = (dom t1) /\ dom t2 and
A4: for s being set st s in dom f1 holds f1.s = F(s) and
A5: dom f2 = (dom t1) /\ dom t2 and
A6: for s being set st s in dom f2 holds f2.s = F(s);
    now
      let s be set;
      assume
A7:   s in (dom t1) /\ dom t2;
      hence f1.s = F(s) by A3,A4 .= f2.s by A5,A6,A7;
    end;
    hence thesis by A3,A5,FUNCT_1:9;
  end;
  func eq(t1,t2) -> integer-yielding Function means:
DEFeq:
  dom it = (dom t1) /\ (dom t2) &
  for s being set st s in dom it holds it.s = IFEQ(t1.s,t2.s,1,0);
  correctness
  proof
    deffunc F(set) = IFEQ(t1.$1,t2.$1,1,0);
    consider f being Function such that
A1: dom f = (dom t1) /\ (dom t2) &
    for x being set st x in (dom t1) /\ (dom t2) holds f.x = F(x)
    from FUNCT_1:sch 3;
    f is integer-yielding
    proof
      let x be set;
      assume x in dom f; then
      f.x = F(x) by A1;
      hence thesis;
    end;
    hence ex f being integer-yielding Function st dom f = (dom t1)/\(dom t2) &
    for x being set st x in dom f holds f.x = F(x) by A1;
    let f1,f2 be integer-yielding Function such that
A3: dom f1 = (dom t1) /\ dom t2 and
A4: for s being set st s in dom f1 holds f1.s = F(s) and
A5: dom f2 = (dom t1) /\ dom t2 and
A6: for s being set st s in dom f2 holds f2.s = F(s);
    now
      let s be set;
      assume
A7:   s in (dom t1) /\ dom t2;
      hence f1.s = F(s) by A3,A4 .= f2.s by A5,A6,A7;
    end;
    hence thesis by A3,A5,FUNCT_1:9;
  end;
end;

definition
  let X be non empty set;
  let f be Function of X, INT;
  let x be integer number;
  redefine
  func f+x -> Function of X, INT means:
DEFplus2:
  for s being Element of X holds it.s = f.s+x;
  compatibility
  proof
    let ti be Function of X, INT;
A1: dom (f+x) = dom f & dom f = X & dom ti = X by VALUED_1:def 2,FUNCT_2:def 1;
    hence ti = f+x implies
    for s being Element of X holds ti.s = f.s+x by VALUED_1:def 2;
    assume for s being Element of X holds ti.s = f.s+x; then
    for s being set st s in X holds ti.s = x+f.s;
    hence ti = f+x by A1,VALUED_1:def 2;
  end;
  coherence
  proof
    x+f is Function of X, INT;
    hence thesis;
  end;
  func f-x -> Function of X, INT means
  for s being Element of X holds it.s = f.s-x;
  compatibility
  proof
    let ti be Function of X, INT;
A1: dom (f-x) = dom f & dom f = X & dom ti = X by VALUED_1:3,FUNCT_2:def 1;
    hence ti = f-x implies
    for s being Element of X holds ti.s = f.s-x by VALUED_1:3;
    assume
A2: for s being Element of X holds ti.s = f.s-x;
    now let s be set; assume
A3:   s in dom ti;
      hence ti.s = f.s-x by A2 .= (f-x).s by A1,A3,VALUED_1:3;
    end;
    hence ti = f-x by A1,FUNCT_1:9;
  end;
  coherence
  proof
    thus f-x is Function of X, INT;
  end;
  func f*x -> Function of X, INT means:
DEFmult2:
  for s being Element of X holds it.s = f.s*x;
  compatibility
  proof
    let ti be Function of X, INT;
A1: dom (f*x) = dom f & dom f = X & dom ti = X by VALUED_1:def 5,FUNCT_2:def 1;
    hence ti = f*x implies
    for s being Element of X holds ti.s = f.s*x by VALUED_1:def 5;
    assume
    for s being Element of X holds ti.s = f.s*x; then
    for s being set st s in dom (f*x) holds ti.s = x*f.s by A1;
    hence ti = f*x by A1,VALUED_1:def 5;
  end;
  coherence
  proof
    x(#)f is Function of X, INT;
    hence thesis;
  end;
end;

definition
  let X be set;
  let f,g be Function of X, INT;
  redefine
  func f div g -> Function of X, INT;
  coherence
  proof
A1: rng f c= INT & rng g c= INT &
    dom (f div g) = (dom f) /\ dom g & (dom f) /\ dom f = dom f &
    dom f = X & dom g = X by DEFdiv,FUNCT_2:def 1;
    rng (f div g) c= INT
    proof
      let y be set; assume y in rng (f div g); then
      consider a being set such that
A2:   a in dom (f div g) & y = (f div g).a by FUNCT_1:def 5;
      f.a in rng f & g.a in rng g by A1,A2,FUNCT_1:12; then
      reconsider i = f.a, j = g.a as Element of INT;
      thus thesis by A2,INT_1:def 2;
    end;
    hence thesis by A1,FUNCT_2:4;
  end;
  func f mod g -> Function of X, INT;
  coherence
  proof
A1: rng f c= INT & rng g c= INT &
    dom (f mod g) = (dom f) /\ dom g & (dom f) /\ dom f = dom f &
    dom f = X & dom g = X by DEFmod,FUNCT_2:def 1;
    rng (f mod g) c= INT
    proof
      let y be set; assume y in rng (f mod g); then
      consider a being set such that
A2:   a in dom (f mod g) & y = (f mod g).a by FUNCT_1:def 5;
      f.a in rng f & g.a in rng g by A1,A2,FUNCT_1:12; then
      reconsider i = f.a, j = g.a as Element of INT;
      thus thesis by A2,INT_1:def 2;
    end;
    hence thesis by A1,FUNCT_2:4;
  end;
  func leq(f,g) -> Function of X, INT;
  coherence
  proof
A1: rng f c= INT & rng g c= INT &
    dom leq(f,g) = (dom f) /\ dom g & (dom f) /\ dom f = dom f &
    dom f = X & dom g = X by DEFleq,FUNCT_2:def 1;
    rng leq(f,g) c= INT
    proof
      let y be set; assume y in rng leq(f,g); then
      consider a being set such that
A2:   a in dom leq(f,g) & y = leq(f,g).a by FUNCT_1:def 5;
      f.a in rng f & g.a in rng g by A1,A2,FUNCT_1:12; then
      reconsider i = f.a, j = g.a as Element of INT;
      thus thesis by A2,INT_1:def 2;
    end;
    hence thesis by A1,FUNCT_2:4;
  end;
  func gt(f,g) -> Function of X, INT;
  coherence
  proof
A1: rng f c= INT & rng g c= INT &
    dom gt(f,g) = (dom f) /\ dom g & (dom f) /\ dom f = dom f &
    dom f = X & dom g = X by DEFgt,FUNCT_2:def 1;
    rng gt(f,g) c= INT
    proof
      let y be set; assume y in rng gt(f,g); then
      consider a being set such that
A2:   a in dom gt(f,g) & y = gt(f,g).a by FUNCT_1:def 5;
      f.a in rng f & g.a in rng g by A1,A2,FUNCT_1:12; then
      reconsider i = f.a, j = g.a as Element of INT;
      thus thesis by A2,INT_1:def 2;
    end;
    hence thesis by A1,FUNCT_2:4;
  end;
  func eq(f,g) -> Function of X, INT;
  coherence
  proof
A1: rng f c= INT & rng g c= INT &
    dom eq(f,g) = (dom f) /\ dom g & (dom f) /\ dom f = dom f &
    dom f = X & dom g = X by DEFeq,FUNCT_2:def 1;
    rng eq(f,g) c= INT
    proof
      let y be set; assume y in rng eq(f,g); then
      consider a being set such that
A2:   a in dom eq(f,g) & y = eq(f,g).a by FUNCT_1:def 5;
      f.a in rng f & g.a in rng g by A1,A2,FUNCT_1:12; then
      reconsider i = f.a, j = g.a as Element of INT;
      thus thesis by A2,INT_1:def 2;
    end;
    hence thesis by A1,FUNCT_2:4;
  end;
end;

definition redefine
  let X be non empty set;
  let t1,t2 be Function of X, INT;
  func t1-t2 -> Function of X, INT means:
DEFminus3:
  for s being Element of X holds it.s = (t1.s)-(t2.s);
  compatibility
  proof
    let ti be Function of X, INT;
A1: dom (t1-t2) = (dom t1)/\dom t2 & dom t1 = X & dom t2 = X & dom ti = X
    by FUNCT_2:def 1,VALUED_1:12;
    thus ti = t1-t2 implies
    for s being Element of X holds ti.s = (t1.s)-(t2.s) by VALUED_1:15;
    assume
A2: for s being Element of X holds ti.s = (t1.s)-(t2.s);
    now let s be set; assume
A3:   s in X;
      hence ti.s = (t1.s)-(t2.s) by A2 .= (t1-t2).s by A3,VALUED_1:15;
    end;
    hence ti = t1-t2 by A1,FUNCT_1:9;
  end;
  coherence
  proof
    thus t1-t2 is Function of X, INT;
  end;
  func t1+t2 -> Function of X, INT means
  for s being Element of X holds it.s = (t1.s)+(t2.s);
  compatibility
  proof
    let ti be Function of X, INT;
A1: dom (t1+t2) = (dom t1)/\dom t2 & dom t1 = X & dom t2 = X & dom ti = X
    by FUNCT_2:def 1,VALUED_1:def 1;
    hence ti = t1+t2 implies
    for s being Element of X holds ti.s = (t1.s)+(t2.s) by VALUED_1:def 1;
    assume for s being Element of X holds ti.s = (t1.s)+(t2.s); then
    for s being set st s in X holds ti.s = (t1.s)+(t2.s);
    hence ti = t1+t2 by A1,VALUED_1:def 1;
  end;
  coherence
  proof
    thus t1+t2 is Function of X, INT;
  end;
end;

registration
  let A be non empty set;
  let B be infinite set;
  cluster Funcs(A, B) -> infinite;
  coherence
  proof
    consider a being Element of A;
    {a} c= A & Card {a} = 1 by ZFMISC_1:37,CARD_1:50; then
A1: Card B <> 0 & 1 <=` Card A by CARD_1:27;
    Card A = Card Card A & Card Card B = Card B; then
    Card Funcs(A, B) = exp(Card B, Card A) by FUNCT_5:68; then
    exp(Card B, 1) <=` Card Funcs(A, B) by A1,CARD_4:71; then
    Card B <=` Card Funcs(A, B) & Card B is infinite
    by CARD_2:40,CARD_4:1; then
    Card Funcs(A, B) is infinite by FINSET_1:13;
    hence thesis by CARD_4:1;
  end;
end;

definition
  let N be set;
  let v be Function;
  let f be Function;
  func v**(f,N) -> Function means:
DSTAR:
  (ex Y being set st
   (for y being set holds
      y in Y iff ex h being Function st h in dom v & y in rng h) &
   for a being set holds a in dom it iff a in Funcs(N,Y) &
        ex g being Function st a = g & g*f in dom v) &
  for g being Function st g in dom it holds it.g = v.(g*f);
  uniqueness
  proof
    let F1,F2 be Function;
    given Y1 being set such that
Y1: for y being set holds
      y in Y1 iff ex h being Function st h in dom v & y in rng h and
A1: for a being set holds a in dom F1 iff a in Funcs(N,Y1) &
        ex g being Function st a = g & g*f in dom v;
    assume
B1: for g being Function st g in dom F1 holds F1.g = v.(g*f);
    given Y2 being set such that
Y2: for y being set holds
      y in Y2 iff ex h being Function st h in dom v & y in rng h and
A2: for a being set holds a in dom F2 iff a in Funcs(N,Y2) &
        ex g being Function st a = g & g*f in dom v;
    assume
B2: for g being Function st g in dom F2 holds F2.g = v.(g*f);
    now let a be set;
      a in Y1 iff ex h being Function st h in dom v & a in rng h by Y1;
      hence a in Y1 iff a in Y2 by Y2;
    end; then
Y3: Y1 = Y2 by TARSKI:2;
    now
      let a be set;
      a in dom F1 iff a in Funcs(N,Y1) &
      ex g being Function st a = g & g*f in dom v by A1;
      hence a in dom F1 iff a in dom F2 by A2,Y3;
    end; then
A3: dom F1 = dom F2 by TARSKI:2;
    now
      let a be set;
      assume
A4:   a in dom F1; then
      consider g being Function such that
A5:   a = g & g*f in dom v by A1;
      thus F1.a = v.(g*f) by B1,A4,A5 .= F2.a by B2,A3,A4,A5;
    end;
    hence thesis by A3,FUNCT_1:9;
  end;
  existence
  proof
    defpred P[set,set] means
    ex g being Function st $1 = g & $2 = rng g;
A0: for x,y,z being set st P[x,y] & P[x,z] holds y = z;
    consider X being set such that
A1: for x being set holds x in X iff ex y being set st y in dom v & P[y,x]
    from TARSKI:sch 1(A0);
    set Y = union X;
    defpred R[set] means ex g being Function st g = $1 & g*f in dom v;
    consider D being set such that
A2: for x being set holds x in D iff x in Funcs(N,Y) & R[x]
    from XBOOLE_0:sch 1;
    defpred F[set,set] means ex g being Function st g = $1 & $2 = v.(g*f);
B1: for x,y1,y2 being set st x in D & F[x,y1] & F[x,y2] holds y1 = y2;
B2: for x being set st x in D ex y being set st F[x,y]
    proof
      let x be set; assume x in D; then
      consider y being Function such that
B4:   y = x & y*f in dom v by A2;
      take v.(y*f);
      thus F[x,v.(y*f)] by B4;
    end;
    consider F being Function such that
A3: dom F = D & for g being set st g in D holds F[g,F.g]
    from FUNCT_1:sch 2(B1,B2);
    take F;
    hereby take Y;
      hereby let y be set;
        hereby assume y in Y; then
          consider a being set such that
C2:       y in a & a in X by TARSKI:def 4;
          consider z being set such that
C3:       z in dom v & P[z,a] by C2,A1;
          thus ex h being Function st h in dom v & y in rng h by C2,C3;
        end;
        given h being Function such that
C1:     h in dom v & y in rng h;
        rng h in X by C1,A1;
        hence y in Y by C1,TARSKI:def 4;
      end;
      let a be set;
      thus a in dom F iff a in Funcs(N,Y) &
      ex g being Function st a = g & g*f in dom v by A3,A2;
    end;
    let g be Function; assume g in dom F; then
    F[g,F.g] by A3;
    hence F.g = v.(g*f);
  end;
end;

definition
  let X,Y,Z,N be non empty set;
  let v be Element of Funcs(Funcs(X,Y), Z);
  let f be Function of X,N;
  redefine func v**(f,N) -> Element of Funcs(Funcs(N,Y),Z);
  coherence
  proof
A0: dom v = Funcs(X,Y) & rng v c= Z by FUNCT_2:def 1;
    consider Y0 being set such that
A1: for y being set holds
      y in Y0 iff ex h being Function st h in dom v & y in rng h and
A2: for a being set holds a in dom (v**(f,N)) iff a in Funcs(N,Y0) &
      ex g being Function st a = g & g*f in dom v by DSTAR;
A3: Y0 = Y
    proof
      thus Y0 c= Y
      proof let y be set; assume y in Y0; then
        consider h being Function such that
B1:     h in dom v & y in rng h by A1;
        rng h c= Y by B1,FUNCT_2:169;
        hence thesis by B1;
      end;
      let y be set; assume y in Y; then
      reconsider y as Element of Y;
      reconsider h = X-->y as Function of X,Y;
      y in {y} & rng h = {y} & h in Funcs(X,Y)
      by TARSKI:def 1,FUNCOP_1:14,FUNCT_2:11;
      hence thesis by A0,A1;
    end;
A4: dom (v**(f,N)) = Funcs(N,Y)
    proof
      thus dom (v**(f,N)) c= Funcs(N,Y)
      proof
        let a be set;
        thus thesis by A2,A3;
      end;
      let a be set; assume
B2:   a in Funcs(N,Y); then
      reconsider g = a as Function of N,Y by FUNCT_2:121;
      g*f in Funcs(X,Y) by FUNCT_2:11;
      hence thesis by A0,A2,A3,B2;
    end;
    rng (v**(f,N)) c= Z
    proof
      let a be set; assume a in rng (v**(f,N)); then
      consider g being set such that
B3:   g in dom (v**(f,N)) & a = (v**(f,N)).g by FUNCT_1:def 5;
      reconsider g as Element of Funcs(N,Y) by A4,B3;
      reconsider gf = g*f as Element of Funcs(X,Y) by FUNCT_2:11;
      a = v.gf by B3,DSTAR;
      hence thesis;
    end;
    hence thesis by A4,FUNCT_2:def 2;
  end;
end;

theorem LemR:
  for f1,f2,g being Function st rng g c= dom f2 holds (f1+*f2)*g = f2*g
  proof
    let f1,f2,g be Function; assume
Z0: rng g c= dom f2;
    dom (f1+*f2) = dom f1 \/ dom f2 by FUNCT_4:def 1; then
Z2: dom ((f1+*f2)*g) = dom g & dom (f2*g) = dom g by Z0,XBOOLE_1:10,RELAT_1:46;
    now
      let x be set; assume x in dom g; then
      ((f1+*f2)*g).x = (f1+*f2).(g.x) & (f2*g).x = f2.(g.x) & g.x in rng g
      by FUNCT_1:12,23;
      hence ((f1+*f2)*g).x = (f2*g).x by Z0,FUNCT_4:14;
    end;
    hence (f1+*f2)*g = f2*g by Z2,FUNCT_1:9;
  end;

theorem LemQ:
  for X,N,I being non empty set
  for s being Function of X,I
  for c being Function of X,N st c is one-to-one
  for n being Element of I
  holds (N-->n)+*(s*c") is Function of N,I
  proof
    let X,N,I be non empty set;
    let s be Function of X,I;
    let c be Function of X,N such that
Z0: c is one-to-one;
    let n be Element of I;
    set f = N-->n, g = s*c";
Z1: dom (f+*g) = dom f \/ dom g by FUNCT_4:def 1;
Z2: dom g c= dom (c") & rng g c= rng s by RELAT_1:44,45;
Z3: dom f = N & rng f = {n} by FUNCOP_1:14,19;
    dom (c") = rng c & rng c c= N by Z0,FUNCT_1:55; then
Z4: dom (f+*g) = N by Z1,Z2,Z3,XBOOLE_1:1,12;
    rng g c= I by Z2,XBOOLE_1:1; then
    rng (f+*g) c= rng f \/ rng g & rng f \/ rng g c= I
    by XBOOLE_1:8,FUNCT_4:18;
    hence (N-->n)+*(s*c") is Function of N,I by Z4,FUNCT_2:4,XBOOLE_1:1;
  end;

theorem ThDS1:
  for N,X,I being non empty set
  for v1,v2 being Function st dom v1 = dom v2 & dom v1 = Funcs(X,I)
  for f being Function of X, N
  st f is one-to-one & v1**(f,N) = v2**(f,N)
  holds v1 = v2
  proof
    let N,X,I be non empty set;
    let v1,v2 be Function such that
Z0: dom v1 = dom v2 & dom v1 = Funcs(X,I);
    reconsider rv1 = rng v1, rv2 = rng v2 as non empty set by Z0,RELAT_1:65;
    reconsider Z = rv1\/rv2 as non empty set;
    rng v1 c= Z & rng v2 c= Z by XBOOLE_1:7; then
    reconsider f1 = v1, f2 = v2 as Element of Funcs(Funcs(X,I),Z)
    by Z0,FUNCT_2:def 2;
    let f be Function of X, N such that
Z1: f is one-to-one & v1**(f,N) = v2**(f,N);
02: dom (f1**(f,N)) = Funcs(N,I) & dom (f2**(f,N)) = Funcs(N,I)
    by FUNCT_2:def 1;
    now
      let a be set; assume a in Funcs(X,I); then
      reconsider h = a as Element of Funcs(X,I);
      consider i being Element of I;
      set g = (N-->i)+*(h*f");
      g is Function of N,I by Z1,LemQ; then
03:   g in Funcs(N,I) by FUNCT_2:11;
01:   rng (f") = dom f & dom f = X & dom h = X
      by Z1,FUNCT_1:55,FUNCT_2:def 1; then
      dom (h*f") = dom (f") by RELAT_1:46 .= rng f by Z1,FUNCT_1:55; then
      g*f = (h*f")*f by LemR .= h*(f"*f) by RELAT_1:55
      .= h*id X by Z1,01,FUNCT_1:61 .= a by 01,RELAT_1:78; then
      (v1**(f,N)).g = v1.a & (v2**(f,N)).g = v2.a by 02,03,DSTAR;
      hence v1.a =  v2.a by Z1;
    end;
    hence v1 = v2 by Z0,FUNCT_1:9;
  end;

registration
  let X be set;
  cluster one-to-one onto Function of X, Card X;
  existence
  proof
    X, Card X are_equipotent by CARD_1:def 5; then
    consider f being Function such that
A1: f is one-to-one & dom f = X & rng f = Card X by WELLORD2:def 4;
    reconsider f as Function of X,Card X by A1,FUNCT_2:4;
    take f; thus f is one-to-one by A1;
    thus rng f = Card X by A1;
  end;
  cluster one-to-one onto Function of Card X, X;
  existence
  proof
    X, Card X are_equipotent by CARD_1:def 5; then
    consider f being Function such that
A1: f is one-to-one & dom f = Card X & rng f = X by WELLORD2:def 4;
    reconsider f as Function of Card X, X by A1,FUNCT_2:4;
    take f; thus f is one-to-one by A1;
    thus rng f = X by A1;
  end;
end;

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

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

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

theorem ThNum6:
  for X being non empty set, x,y being Element of X
  for f being Enumeration of X
  holds f+*(x,f.y)+*(y,f.x) is Enumeration of X
  proof
    let X be non empty set, x,y be Element of X;
    let f be Enumeration of X;
    set g = f+*(x,f.y)+*(y,f.x);
    set A = dom g;
A1: dom (f+*(x,f.y)) = dom f & A = dom (f+*(x,f.y)) &
    dom f = X & rng f = Card X by ThNum1,FUNCT_7:32;
A2: rng (f+*(x,f.y)+*(y,f.x)) = rng f
    proof
      f.y in rng f & f.x in rng f by A1; then
      {f.y} c= rng f & {f.x} c= rng f by ZFMISC_1:37; then
A4:   rng g c= rng (f+*(x,f.y)) \/ {f.x} & rng f \/ {f.y} = rng f &
      rng f \/ {f.x} = rng f & rng (f+*(x,f.y)) c= rng f \/ {f.y}
      by XBOOLE_1:12,POLYNOM1:6; then
      rng (f+*(x,f.y)) \/ {f.x} c= rng f by XBOOLE_1:9;
      hence rng g c= rng f by A4,XBOOLE_1:1;
      let z be set; assume z in rng f; then
      consider a being set such that
A6:   a in dom f & z = f.a by FUNCT_1:def 5;
      per cases;
      suppose a <> x & a <> y; then
        g.a = (f+*(x,f.y)).a & (f+*(x,f.y)).a = z by A6,FUNCT_7:34;
        hence z in rng g by A1,A6,FUNCT_1:def 5;
      end;
      suppose a = x; then
        g.y = z by A1,A6,FUNCT_7:33;
        hence z in rng g by A1,FUNCT_1:def 5;
      end;
      suppose a = y; then
        (x = y implies g.x = z) & (f+*(x,z)).x = z &
        (x <> y implies g.x = (f+*(x,z)).x) by A1,A6,FUNCT_7:33,34;
        hence z in rng g by A1,FUNCT_1:def 5;
      end;
    end;
    f+*(x,f.y)+*(y,f.x) is one-to-one
    proof
      let a,b being set;
A3:   (a = y implies g.a = f.x) &
      (a <> y implies g.a = (f+*(x,f.y)).a) &
      (a = x implies (f+*(x,f.y)).a = f.y) &
      (a <> x implies (f+*(x,f.y)).a = f.a) by A1,FUNCT_7:33,34;
      (b = y implies g.b = f.x) &
      (b <> y implies g.b = (f+*(x,f.y)).b) &
      (b = x implies (f+*(x,f.y)).b = f.y) &
      (b <> x implies (f+*(x,f.y)).b = f.b) by A1,FUNCT_7:33,34;
      hence thesis by A1,A3,FUNCT_1:def 8;
    end;
    hence thesis by A1,A2,ThNum1;
  end;

theorem
  for X being non empty set, x being Element of X
  ex f being Enumeration of X st f.x = 0
  proof
    let X be non empty set, x be Element of X;
    consider f being Enumeration of X;
    0 in Card X & dom f = X & rng f = Card X by ThNum1,ORDINAL3:10; then
    consider y being set such that
A1: y in X & 0 = f.y by FUNCT_1:def 5;
    reconsider y as Element of X by A1;
    reconsider g = f+*(y,f.x)+*(x,0) as Enumeration of X by A1,ThNum6;
    take g;
    dom f = X by ThNum1; then
    dom (f+*(y,f.x)) = X by FUNCT_7:32;
    hence thesis by FUNCT_7:33;
  end;

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

theorem ThNum5:
  for X being countable set, f being Enumeration of X
  holds rng f c= NAT
  proof
    let X be countable set, f be Enumeration of X;
    Card X c= NAT by CARD_4:def 1,CARD_1:83;
    hence thesis by ThNum1;
  end;

definition
  let X be set;
  let f be Enumeration of X;
  redefine func f" -> Denumeration of X;
  coherence
  proof
    dom f = X & rng f = Card X & f is one-to-one by ThNum1; then
    dom (f") = Card X & rng (f") = X & f" is one-to-one by FUNCT_1:55;
    hence thesis by ThNum2;
  end;
end;

definition
  let X be set;
  let f be Denumeration of X;
  redefine func f" -> Enumeration of X;
  coherence
  proof
    dom f = Card X & rng f = X & f is one-to-one by ThNum2; then
    dom (f") = X & rng (f") = Card X & f" is one-to-one by FUNCT_1:55;
    hence thesis by ThNum1;
  end;
end;

LemP0:
  for x being real number, n being Nat holds x to_power n = x |^ n
    by POWER:46;

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

theorem LemP2:
  for x being real number
  for n,m being Nat holds (x to_power n) to_power m = x to_power (n*m)
  proof
    let x be real number;
    let n,m be Nat;
    (x to_power n) to_power m = (x to_power n) |^ m &
    x to_power n = x |^ n & x to_power (n*m) = x |^ (n*m) by LemP0;
    hence thesis by NEWTON:14;
  end;

LemP3: for x being real number holds x to_power 2 = x*x by NEWTON:100;

begin :: If-while algebra over integers

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

reserve A for preIfWhileAlgebra;

definition
  let A;
  let I be Element of A;
  let X be non empty set;
  let T be Subset of Funcs(X, INT);
  let f be ExecutionFunction of A, Funcs(X, INT), T;
  pred I is_assignment_wrt A,X,f means:
IA:
  I in ElementaryInstructions A &
  ex v being INT-Variable of X, t being INT-Expression of X st
  for s being Element of Funcs(X, INT) holds f.(s, I) = s+*(v.s,t.s);
end;

definition
  let A;
  let X be non empty set;
  let T be Subset of Funcs(X, INT);
  let f be ExecutionFunction of A, Funcs(X, INT), T;
  let v be INT-Variable of X;
  let t be INT-Expression of X;
  pred v,t form_assignment_wrt f means:
FA:
  ex I being Element of A st I in ElementaryInstructions A &
  for s being Element of Funcs(X, INT) holds f.(s, I) = s+*(v.s,t.s);
end;

definition
  let A;
  let X be non empty set;
  let T be Subset of Funcs(X, INT);
  let f be ExecutionFunction of A, Funcs(X, INT), T such that
A: ex I being Element of A st I is_assignment_wrt A,X,f;
  mode INT-Variable of A,f -> INT-Variable of X means
  ex t being INT-Expression of X st it,t form_assignment_wrt f;
  existence
  proof
    consider I being Element of A such that
A1: I is_assignment_wrt A,X,f by A;
    consider v being (INT-Variable of X), t being INT-Expression of X
    such that
A2: for s being Element of Funcs(X, INT) holds f.(s, I) = s+*(v.s,t.s)
    by A1,IA;
    take v,t,I;
    thus thesis by A1,IA,A2;
  end;
end;

definition
  let A;
  let X be non empty set;
  let T be Subset of Funcs(X, INT);
  let f be ExecutionFunction of A, Funcs(X, INT), T such that
A: ex I being Element of A st I is_assignment_wrt A,X,f;
  mode INT-Expression of A,f -> INT-Expression of X means
  ex v being INT-Variable of X st v,it form_assignment_wrt f;
  existence
  proof
    consider I being Element of A such that
A1: I is_assignment_wrt A,X,f by A;
    consider v being (INT-Variable of X), t being INT-Expression of X
    such that
A2: for s being Element of Funcs(X, INT) holds f.(s, I) = s+*(v.s,t.s)
    by A1,IA;
    take t,v,I;
    thus thesis by A1,A2,IA;
  end;
end;

definition
  let X,Y be non empty set;
  let f be Element of Funcs(X,Y);
  let x be Element of X;
  redefine func f.x -> Element of Y;
  coherence
  proof
    f.x in rng f by FUNCT_2:6;
    hence thesis;
  end;
end;

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

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

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

theorem
  for X being non empty set
  for x being Element of X
  holds .x = .(^x)
  proof
    let X be non empty set;
    let x be Element of X;
    for s being Element of Funcs(X, INT) holds .(^x).s = s.x
    proof
      let s be Element of Funcs(X, INT);
      thus .(^x).s = s.((^x).s) by DEFvarexp .= s.x by FUNCOP_1:13;
    end;
    hence .x = .(^x) by DEFvarexp1;
  end;

definition
  let X be non empty set;
  let i be integer number;
  func .(i,X) -> INT-Expression of X equals Funcs(X, INT) --> i;
  correctness
  proof
    i in INT by INT_1:def 2;
    hence thesis by FUNCOP_1:57;
  end;
end;

theorem
  for X being non empty set, t being INT-Expression of X
  holds t+ .(0,X) = t & t(#).(1,X) = t
  proof
    let X be non empty set;
    let t be INT-Expression of X;
    now
      let s be Element of Funcs(X,INT);
A1:   .(0,X).s = 0 by FUNCOP_1:13;
      dom (t+ .(0,X)) = Funcs(X,INT) by FUNCT_2:def 1;
      hence (t+ .(0,X)).s = (t.s)+(.(0,X).s) by VALUED_1:def 1
         .= t.s by A1;
    end;
    hence t+ .(0,X) = t by FUNCT_2:113;
    now
      let s be Element of Funcs(X,INT);
      dom (t(#).(1,X)) = Funcs(X,INT) by FUNCT_2:def 1;
      hence (t(#).(1,X)).s = (t.s)*(.(1,X).s) by VALUED_1:def 4
         .= (t.s)*1 by FUNCOP_1:13 .= t.s;
    end;
    hence t(#).(1,X) = t by FUNCT_2:113;
  end;

:: The word "Euclidean" is chosen in following definition
:: to suggest that Euclid algoritm could be annotated
:: in quite natural way (all needed expressions are allowed).
definition
  let A;
  let X be non empty set;
  let T be Subset of Funcs(X, INT);
  let f be ExecutionFunction of A, Funcs(X, INT), T;
  attr f is Euclidean means:
INT'iwa:
  (for v being INT-Variable of A,f, t being INT-Expression of A,f holds
  v,t form_assignment_wrt f) &
  (for i being integer number holds .(i,X) is INT-Expression of A,f) &
  (for v being INT-Variable of A,f holds .v is INT-Expression of A,f) &
  (for x being Element of X holds ^x is INT-Variable of A,f) &
  (ex a being INT-Array of X st a|Card X is one-to-one &
  for t being INT-Expression of A,f holds a*t is INT-Variable of A,f) &
  (for t being INT-Expression of A,f holds
  -t is INT-Expression of A,f) &
  (for t1,t2 being INT-Expression of A,f holds
    t1(#)t2 is INT-Expression of A,f &
    t1+t2 is INT-Expression of A,f &
    t1 div t2 is INT-Expression of A,f &
    t1 mod t2 is INT-Expression of A,f &
    leq(t1,t2) is INT-Expression of A,f &
    gt(t1,t2) is INT-Expression of A,f);
end;
:: Remark:
:: Incorrect definition of "mod" in INT_1:  5 mod 0 = 0 i 5 div 0 = 0
:: and  5 <> 0*(5 div 0)+(5 mod 0)
:: In our case "mod" is still expressible with "basic" operations
:: but in complicated way:
:: f1 mod f2
::   = (gt(f2,(dom f2)-->0)+gt((dom f2)-->0,f2))(#)(f1-f2(#)(f1 div f2))
:: To avoid complications "mod" is mentioned in the definition above.

definition
  let A;
  attr A is Euclidean means:
INT'iwa2:
  for X being non empty countable set, T being Subset of Funcs(X, INT)
  ex f being ExecutionFunction of A, Funcs(X, INT), T
  st f is Euclidean;
end;

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

definition
  mode INT-Exec -> ExecutionFunction of
  FreeUnivAlgNSG(ECIW-signature, INT-ElemIns),
  Funcs(NAT, INT), Funcs(NAT,INT)\(0,0) means:
INTiwaEXEC:
  for s being Element of Funcs(NAT, INT)
  for v being Element of Funcs(Funcs(NAT, INT), NAT)
  for e being Element of Funcs(Funcs(NAT, INT), INT)
  holds it.(s, root-tree [v,e]) = s+*(v.s,e.s);
  existence
  proof
    set S = ECIW-signature, G = INT-ElemIns;
    set A = FreeUnivAlgNSG(S,G);
    reconsider b = 0 as Nat;
    set Q = Funcs(NAT, INT), T = Q\(0,0);
AA: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
BB: Terminals DTConUA(S,G) = G by FREEALG:3;
    defpred P[set,set] means
    ex s being (Element of Q), v being (Element of Funcs(Q, NAT)),
       e being Element of Funcs(Q, INT) st
    $1 = [s, root-tree [v,e]] & $2 = s+*(v.s,e.s);
00: for x being set st x in [:Q,ElementaryInstructions A:]
    ex y being set st y in Q & P[x,y]
    proof
      let x be set; assume x in [:Q,ElementaryInstructions A:]; then
      consider s, I being set such that
00:   s in Q & I in ElementaryInstructions A & x = [s,I] by ZFMISC_1:def 2;
      consider a being Symbol of DTConUA(S,G) such that
01:   I = root-tree a & a in Terminals DTConUA(S,G) by AA,00;
      consider v,e being set such that
02:   v in Funcs(Funcs(NAT, INT), NAT) & e in Funcs(Funcs(NAT, INT), INT) &
      a = [v,e] by BB,01,ZFMISC_1:def 2;
      reconsider s as Element of Q by 00;
      reconsider v as Element of Funcs(Q, NAT) by 02;
      reconsider e as Element of Funcs(Q, INT) by 02;
      take y = s+*(v.s,e.s);
      thus y in Q by FUNCT_2:11;
      take s,v,e;
      thus x = [s, root-tree [v,e]] & y = s+*(v.s,e.s) by 00,01,02;
    end;
    consider g being Function such that
01: dom g = [:Q,ElementaryInstructions A:] & rng g c= Q and
02: for x being set st x in [:Q,ElementaryInstructions A:] holds P[x,g.x]
    from WELLORD2:sch 1(00);
    reconsider g as Function of [:Q,ElementaryInstructions A:], Q
    by 01,FUNCT_2:4;
    reconsider i0 = 0 as Element of INT by INT_1:def 1;
    reconsider q0 = NAT-->i0 as Element of Q by FUNCT_2:11;
    consider f being ExecutionFunction of A, Q, T such that
A1: f|[:Q,ElementaryInstructions A:] = g and
    for s being Element of Q
    for C,I being Element of A st not f iteration_terminates_for I\;C, f.(s,C)
    holds f.(s, while(C,I)) = q0 by AOFA_000:91;
    take f;
    let s be Element of Funcs(NAT, INT);
    let v be Element of Funcs(Funcs(NAT, INT), NAT);
    let e be Element of Funcs(Funcs(NAT, INT), INT);
    set I = root-tree [v,e];
    [v,e] in G by ZFMISC_1:106; then
    I in ElementaryInstructions A by AA,BB; then
A2: [s,I] in [:Q,ElementaryInstructions A:] by ZFMISC_1:106; then
    consider s' being (Element of Q), v' being (Element of Funcs(Q, NAT)),
    e' being Element of Funcs(Q, INT) such that
A3: [s,I] = [s', root-tree [v',e']] & g.[s,I] = s'+*(v'.s',e'.s') by 02;
A4: s = s' & I = root-tree [v',e'] by A3,ZFMISC_1:33; then
    [v,e] = [v',e'] by TREES_4:4; then
    v = v' & e = e' by ZFMISC_1:33;
    hence f.(s, root-tree [v,e]) = s+*(v.s,e.s) by A1,A2,A3,A4,FUNCT_1:72;
  end;
end;

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

definition
  let X be non empty set;
  let x be Element of X;
  mode INT-Exec of x -> ExecutionFunction of
  FreeUnivAlgNSG(ECIW-signature, INT-ElemIns X),
  Funcs(X, INT), Funcs(X,INT)\(x,0) means
  for s being Element of Funcs(X, INT)
  for v being Element of Funcs(Funcs(X, INT), X)
  for e being Element of Funcs(Funcs(X, INT), INT)
  holds it.(s, root-tree [v,e]) = s+*(v.s,e.s);
  existence
  proof
    set S = ECIW-signature, G = INT-ElemIns X;
    set A = FreeUnivAlgNSG(S,G);
    reconsider b = 0 as Nat;
    set Q = Funcs(X, INT), T = Q\(x,0);
AA: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
BB: Terminals DTConUA(S,G) = G by FREEALG:3;
    defpred P[set,set] means
    ex s being (Element of Q), v being (Element of Funcs(Q, X)),
       e being Element of Funcs(Q, INT) st
    $1 = [s, root-tree [v,e]] & $2 = s+*(v.s,e.s);
00: for x being set st x in [:Q,ElementaryInstructions A:]
    ex y being set st y in Q & P[x,y]
    proof
      let x be set; assume x in [:Q,ElementaryInstructions A:]; then
      consider s, I being set such that
00:   s in Q & I in ElementaryInstructions A & x = [s,I] by ZFMISC_1:def 2;
      consider a being Symbol of DTConUA(S,G) such that
01:   I = root-tree a & a in Terminals DTConUA(S,G) by AA,00;
      consider v,e being set such that
02:   v in Funcs(Funcs(X, INT), X) & e in Funcs(Funcs(X, INT), INT) &
      a = [v,e] by BB,01,ZFMISC_1:def 2;
      reconsider s as Element of Q by 00;
      reconsider v as Element of Funcs(Q, X) by 02;
      reconsider e as Element of Funcs(Q, INT) by 02;
      take y = s+*(v.s,e.s);
      thus y in Q by FUNCT_2:11;
      take s,v,e;
      thus x = [s, root-tree [v,e]] & y = s+*(v.s,e.s) by 00,01,02;
    end;
    consider g being Function such that
01: dom g = [:Q,ElementaryInstructions A:] & rng g c= Q and
02: for x being set st x in [:Q,ElementaryInstructions A:] holds P[x,g.x]
    from WELLORD2:sch 1(00);
    reconsider g as Function of [:Q,ElementaryInstructions A:], Q
    by 01,FUNCT_2:4;
    reconsider i0 = 0 as Element of INT by INT_1:def 1;
    reconsider q0 = X-->i0 as Element of Q by FUNCT_2:11;
    consider f being ExecutionFunction of A, Q, T such that
A1: f|[:Q,ElementaryInstructions A:] = g and
    for s being Element of Q
    for C,I being Element of A st not f iteration_terminates_for I\;C, f.(s,C)
    holds f.(s, while(C,I)) = q0 by AOFA_000:91;
    take f;
    let s be Element of Funcs(X, INT);
    let v be Element of Funcs(Funcs(X, INT), X);
    let e be Element of Funcs(Funcs(X, INT), INT);
    set I = root-tree [v,e];
    [v,e] in G by ZFMISC_1:106; then
    I in ElementaryInstructions A by AA,BB; then
A2: [s,I] in [:Q,ElementaryInstructions A:] by ZFMISC_1:106; then
    consider s' being (Element of Q), v' being (Element of Funcs(Q, X)),
    e' being Element of Funcs(Q, INT) such that
A3: [s,I] = [s', root-tree [v',e']] & g.[s,I] = s'+*(v'.s',e'.s') by 02;
A4: s = s' & I = root-tree [v',e'] by A3,ZFMISC_1:33; then
    [v,e] = [v',e'] by TREES_4:4; then
    v = v' & e = e' by ZFMISC_1:33;
    hence f.(s, root-tree [v,e]) = s+*(v.s,e.s) by A1,A2,A3,A4,FUNCT_1:72;
  end;
end;

definition
  let X be non empty set;
  let T be Subset of Funcs(X, INT);
  let c be Enumeration of X such that
A: rng c c= NAT;
  mode INT-Exec of c,T -> ExecutionFunction of
  FreeUnivAlgNSG(ECIW-signature, INT-ElemIns), Funcs(X, INT), T means:
INTiwaEXECc:
  for s being Element of Funcs(X, INT)
  for v being Element of Funcs(Funcs(X, INT), X)
  for e being Element of Funcs(Funcs(X, INT), INT)
  holds it.(s, root-tree [(c*v)**(c,NAT),e**(c,NAT)]) = s+*(v.s,e.s);
  existence
  proof
    set S = ECIW-signature, G = INT-ElemIns;
    set A = FreeUnivAlgNSG(S,G);
    set x = c".0;
    set Q = Funcs(X, INT);
    reconsider b = 0 as Nat;
    reconsider i0 = 0 as Element of INT by INT_1:def 1;
    reconsider q0 = X-->i0 as Element of Q by FUNCT_2:11;
    dom c = X by ThNum1; then
    reconsider c' = c as Function of X, NAT by A,FUNCT_2:4;
AA: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
BB: Terminals DTConUA(S,G) = G by FREEALG:3;
    defpred P[set,set] means
    ex s being (Element of Q) st $1`1 = s &
    (($2 = s & not
    ex v being (Element of Funcs(Q, X)), e being Element of Funcs(Q, INT) st
    $1`2 = root-tree [(c*v)**(c',NAT),e**(c',NAT)]) or
    ex v being (Element of Funcs(Q, X)), e being Element of Funcs(Q, INT) st
    $1`2 = root-tree [(c*v)**(c',NAT),e**(c',NAT)] & $2 = s+*(v.s,e.s));
00: for x being set st x in [:Q,ElementaryInstructions A:]
    ex y being set st y in Q & P[x,y]
    proof
      let x be set; assume x in [:Q,ElementaryInstructions A:]; then
      consider s, I being set such that
00:   s in Q & I in ElementaryInstructions A & x = [s,I] by ZFMISC_1:def 2;
05:   x`1 = s & x`2 = I by 00,MCART_1:7;
      consider a being Symbol of DTConUA(S,G) such that
01:   I = root-tree a & a in Terminals DTConUA(S,G) by AA,00;
      reconsider s as Element of Q by 00;
      per cases;
      suppose
        ex v being (Element of Funcs(Q, X)), e being Element of Funcs(Q, INT)
        st  a = [(c*v)**(c',NAT),e**(c',NAT)]; then
        consider v being (Element of Funcs(Q, X)),
        e being Element of Funcs(Q, INT) such that
03:     a = [(c*v)**(c',NAT),e**(c',NAT)];
        take y = s+*(v.s,e.s);
        thus y in Q by FUNCT_2:11;
        thus thesis by 05,01,03;
      end;
      suppose
04:     not ex v being (Element of Funcs(Q, X)),
        e being Element of Funcs(Q, INT) st a = [(c*v)**(c',NAT),e**(c',NAT)];
        take y = s;
        thus y in Q;
        not ex v being (Element of Funcs(Q, X)),
               e being Element of Funcs(Q, INT) st
        x`2 = root-tree [(c*v)**(c',NAT),e**(c',NAT)] by 04,05,01,TREES_4:4;
        hence thesis by 05;
      end;
    end;
    consider g being Function such that
01: dom g = [:Q,ElementaryInstructions A:] & rng g c= Q and
02: for x being set st x in [:Q,ElementaryInstructions A:] holds P[x,g.x]
    from WELLORD2:sch 1(00);
    reconsider g as Function of [:Q,ElementaryInstructions A:], Q
    by 01,FUNCT_2:4;
    consider f being ExecutionFunction of A, Q, T such that
A1: f|[:Q,ElementaryInstructions A:] = g and
    for s being Element of Q
    for C,I being Element of A st not f iteration_terminates_for I\;C, f.(s,C)
    holds f.(s, while(C,I)) = q0 by AOFA_000:91;
    take f;
    let s be Element of Funcs(X, INT);
    let v be Element of Funcs(Funcs(X, INT), X);
    let e be Element of Funcs(Funcs(X, INT), INT);
    reconsider vv = v as Function of Funcs(X, INT), X;
    reconsider cv = c'*vv as Element of Funcs(Funcs(X, INT), NAT)
    by FUNCT_2:11;
    set v0 = cv**(c',NAT), e0 = e**(c',NAT);
    set I = root-tree [v0,e0];
    [v0,e0] in G by ZFMISC_1:106; then
    I in ElementaryInstructions A by AA,BB; then
A2: [s,I] in [:Q,ElementaryInstructions A:] by ZFMISC_1:106; then
A4: P[[s,I],g.[s,I]] & [s,I]`2 = I & [s,I]`1 = s by 02,MCART_1:7;
    consider v' being (Element of Funcs(Q, X)),
    e' being Element of Funcs(Q, INT) such that
A3: [s,I]`2 = root-tree [(c*v')**(c',NAT),e'**(c',NAT)] &
    g.[s,I] = s+*(v'.s,e'.s) by A4;
A6: rng v c= X & rng v' c= X & dom c' = X & dom v' = Q & dom v = Q &
    dom e = Q & dom e' = Q & dom cv = Q & dom (c'*v') = Q
    by FUNCT_2:def 1;
    [v0,e0] = [(c*v')**(c',NAT),e'**(c',NAT)] by A3,A4,TREES_4:4; then
    v0 = (c*v')**(c',NAT) & e0 = e'**(c',NAT) by ZFMISC_1:33; then
A5: cv = c*v' & e = e' by A6,ThDS1;
    v = v' by A5,A6,FUNCT_1:49;
    hence f.(s, root-tree [(c*v)**(c,NAT),e**(c,NAT)]) = s+*(v.s,e.s)
    by A1,A2,A3,A5,FUNCT_1:72;
  end;
end;

theorem II1:
  for f being INT-Exec
  for v being INT-Variable of NAT
  for t being INT-Expression of NAT holds
  v,t form_assignment_wrt f
  proof
    set X = NAT;
    set S = ECIW-signature, G = INT-ElemIns;
    set A = FreeUnivAlgNSG(S,G);
    let f be INT-Exec;
    let v be INT-Variable of NAT;
    let t be INT-Expression of NAT;
    reconsider v' = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:11;
    reconsider t' = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:11;
AA: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
BB: Terminals DTConUA(S,G) = G by FREEALG:3;
CC: [v',t'] in G by ZFMISC_1:106; then
    root-tree [v',t'] in ElementaryInstructions A by AA,BB; then
    reconsider I = root-tree [v',t'] as Element of A;
    take I; thus I in ElementaryInstructions A by AA,BB,CC;
    thus for s being Element of Funcs(X, INT) holds f.(s, I) = s+*(v.s,t.s)
    by INTiwaEXEC;
  end;

theorem II2:
  for f being INT-Exec
  for v being INT-Variable of NAT holds
  v is INT-Variable of FreeUnivAlgNSG(ECIW-signature, INT-ElemIns), f
  proof
    set X = NAT;
    set S = ECIW-signature, G = INT-ElemIns;
    set A = FreeUnivAlgNSG(S,G);
    let f be INT-Exec;
    let v be INT-Variable of NAT;
    consider t being INT-Expression of NAT;
AA: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
BB: Terminals DTConUA(S,G) = G by FREEALG:3;
    reconsider v' = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:11;
    reconsider t' = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:11;
CC: [v',t'] in G by ZFMISC_1:106; then
    root-tree [v',t'] in ElementaryInstructions A by AA,BB; then
    reconsider I = root-tree [v',t'] as Element of A;
    hereby take I;
      thus I is_assignment_wrt A,X,f
      proof thus I in ElementaryInstructions A by AA,BB,CC;
        take v,t;
        thus thesis by INTiwaEXEC;
      end;
    end;
    take t; thus v,t form_assignment_wrt f by II1;
  end;

theorem II3:
  for f being INT-Exec
  for t being INT-Expression of NAT holds
  t is INT-Expression of FreeUnivAlgNSG(ECIW-signature, INT-ElemIns), f
  proof
    set X = NAT;
    set S = ECIW-signature, G = INT-ElemIns;
    set A = FreeUnivAlgNSG(S,G);
    let f be INT-Exec;
    consider v being INT-Variable of NAT;
    let t be INT-Expression of NAT;
AA: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
BB: Terminals DTConUA(S,G) = G by FREEALG:3;
    reconsider v' = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:11;
    reconsider t' = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:11;
CC: [v',t'] in G by ZFMISC_1:106; then
    root-tree [v',t'] in ElementaryInstructions A by AA,BB; then
    reconsider I = root-tree [v',t'] as Element of A;
    hereby take I;
      thus I is_assignment_wrt A,X,f
      proof thus I in ElementaryInstructions A by AA,BB,CC;
        take v,t;
        thus thesis by INTiwaEXEC;
      end;
    end;
    take v; thus v,t form_assignment_wrt f by II1;
  end;

registration
  cluster -> Euclidean INT-Exec;
  coherence
  proof let f be INT-Exec;
    set X = NAT;
    set S = ECIW-signature, G = INT-ElemIns;
    set A = FreeUnivAlgNSG(S,G);
    set T = Funcs(X, INT)\(0,0);
    thus for v being INT-Variable of A,f, t being INT-Expression of A,f
    holds v,t form_assignment_wrt f by II1;
    thus for i being integer number holds
    .(i,X) is INT-Expression of A,f by II3;
    thus for v being INT-Variable of A,f holds
    .v is INT-Expression of A,f by II3;
    thus for x being Element of X holds ^x is INT-Variable of A,f by II2;
    set a = (INT --> 0)+*(id X);
    {0} c= X by ZFMISC_1:37; then
    dom (INT --> 0) = INT & rng (INT --> 0) = {0} &
    dom id X = X & rng id X = X &
    INT \/ X = INT & {0} \/ X = X
    by NUMBERS:17,XBOOLE_1:12,RELAT_1:71,FUNCOP_1:14,19; then
    dom a = INT & rng a c= NAT by FUNCT_4:def 1,18; then
    reconsider a as INT-Array of X by FUNCT_2:4;
    hereby take a;
      Card X = X & dom id X = X by RELAT_1:71,CARD_1:84;
      hence a|Card X is one-to-one by FUNCT_4:24;
      thus for t being INT-Expression of A,f holds
      a*t is INT-Variable of A,f by II2;
    end;
    thus thesis by II3;
  end;
end;

theorem cII1:
  for X being non empty countable set
  for T being Subset of Funcs(X, INT)
  for c being Enumeration of X
  for f being INT-Exec of c,T
  for v being INT-Variable of X
  for t being INT-Expression of X holds
  v,t form_assignment_wrt f
  proof
    let X be non empty countable set;
    let T be Subset of Funcs(X, INT);
    let c be Enumeration of X;
A0: rng c c= NAT & dom c = X by ThNum1,ThNum5; then
    reconsider c' = c as Function of X,NAT by FUNCT_2:4;
    set S = ECIW-signature, G = INT-ElemIns;
    set A = FreeUnivAlgNSG(S,G);
    let f be INT-Exec of c,T;
    let v be INT-Variable of X;
    let t be INT-Expression of X;
    reconsider v' = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:11;
    reconsider t' = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:11;
    reconsider cv = c'*v as Element of Funcs(Funcs(X,INT),NAT) by FUNCT_2:11;
    set v1 = cv**(c',NAT), t1 = t'**(c',NAT);
AA: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
BB: Terminals DTConUA(S,G) = G by FREEALG:3;
CC: [v1,t1] in G by ZFMISC_1:106; then
    root-tree [v1,t1] in ElementaryInstructions A by AA,BB; then
    reconsider I = root-tree [v1,t1] as Element of A;
    take I;
    for s being Element of Funcs(X, INT)
    holds f.(s, root-tree [(c*v')**(c,NAT),t'**(c,NAT)]) = s+*(v'.s,t'.s)
    by A0,INTiwaEXECc;
    hence thesis by AA,BB,CC;
  end;

theorem cII2:
  for X being non empty countable set
  for T being Subset of Funcs(X, INT)
  for c being Enumeration of X
  for f being INT-Exec of c,T
  for v being INT-Variable of X holds
  v is INT-Variable of FreeUnivAlgNSG(ECIW-signature, INT-ElemIns), f
  proof
    let X be non empty countable set;
    let T be Subset of Funcs(X, INT);
    let c be Enumeration of X;
A0: rng c c= NAT & dom c = X by ThNum1,ThNum5; then
    reconsider c' = c as Function of X,NAT by FUNCT_2:4;
    set S = ECIW-signature, G = INT-ElemIns;
    set A = FreeUnivAlgNSG(S,G);
    let f be INT-Exec of c,T;
    let v be INT-Variable of X;
    consider t being INT-Expression of X;
AA: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
BB: Terminals DTConUA(S,G) = G by FREEALG:3;
    reconsider v' = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:11;
    reconsider t' = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:11;
    reconsider cv = c'*v as Element of Funcs(Funcs(X,INT),NAT) by FUNCT_2:11;
    set v1 = cv**(c',NAT), t1 = t'**(c',NAT);
CC: [v1,t1] in G by ZFMISC_1:106; then
    root-tree [v1,t1] in ElementaryInstructions A by AA,BB; then
    reconsider I = root-tree [v1,t1] as Element of A;
    hereby take I;
      thus I is_assignment_wrt A,X,f
      proof thus I in ElementaryInstructions A by AA,BB,CC;
        take v,t;
        for s being Element of Funcs(X, INT)
        holds f.(s, root-tree [(c*v')**(c,NAT),t'**(c,NAT)]) = s+*(v'.s,t'.s)
        by A0,INTiwaEXECc;
        hence thesis;
      end;
    end;
    take t; thus v,t form_assignment_wrt f by cII1;
  end;

theorem cII3:
  for X being non empty countable set
  for T being Subset of Funcs(X, INT)
  for c being Enumeration of X
  for f being INT-Exec of c,T
  for t being INT-Expression of X holds
  t is INT-Expression of FreeUnivAlgNSG(ECIW-signature, INT-ElemIns), f
  proof
    let X be non empty countable set;
    let T be Subset of Funcs(X, INT);
    let c be Enumeration of X;
A0: rng c c= NAT & dom c = X by ThNum1,ThNum5; then
    reconsider c' = c as Function of X,NAT by FUNCT_2:4;
    set S = ECIW-signature, G = INT-ElemIns;
    set A = FreeUnivAlgNSG(S,G);
    let f be INT-Exec of c,T;
    consider v being INT-Variable of X;
    let t be INT-Expression of X;
AA: ElementaryInstructions A = FreeGenSetNSG(S,G) by AOFA_000:70;
BB: Terminals DTConUA(S,G) = G by FREEALG:3;
    reconsider v' = v as Element of Funcs(Funcs(X,INT),X) by FUNCT_2:11;
    reconsider t' = t as Element of Funcs(Funcs(X,INT),INT) by FUNCT_2:11;
    reconsider cv = c'*v as Element of Funcs(Funcs(X,INT),NAT) by FUNCT_2:11;
    set v1 = cv**(c',NAT), t1 = t'**(c',NAT);
CC: [v1,t1] in G by ZFMISC_1:106; then
    root-tree [v1,t1] in ElementaryInstructions A by AA,BB; then
    reconsider I = root-tree [v1,t1] as Element of A;
    hereby take I;
      thus I is_assignment_wrt A,X,f
      proof thus I in ElementaryInstructions A by AA,BB,CC;
        take v,t;
        for s being Element of Funcs(X, INT)
        holds f.(s, root-tree [(c*v')**(c,NAT),t'**(c,NAT)]) = s+*(v'.s,t'.s)
        by A0,INTiwaEXECc;
        hence thesis;
      end;
    end;
    take v; thus v,t form_assignment_wrt f by cII1;
  end;

registration
  let X be countable non empty set;
  let T be Subset of Funcs(X, INT);
  let c be Enumeration of X;
  cluster -> Euclidean INT-Exec of c,T;
  coherence
  proof let f be INT-Exec of c,T;
    set S = ECIW-signature, G = INT-ElemIns;
    set A = FreeUnivAlgNSG(S,G);
    set x = c".0;
    thus for v being INT-Variable of A,f, t being INT-Expression of A,f
    holds v,t form_assignment_wrt f by cII1;
    thus for i being integer number holds
    .(i,X) is INT-Expression of A,f by cII3;
    thus for v being INT-Variable of A,f holds
    .v is INT-Expression of A,f by cII3;
    thus for x being Element of X holds ^x is INT-Variable of A,f by cII2;
    set a = (INT --> x)+*(c");
    x in X & Card X = rng c & rng c c= NAT by ThNum1,ThNum4,ThNum5; then
    {x} c= X & Card X c= INT by XBOOLE_1:1,ZFMISC_1:37,NUMBERS:17; then
    dom (INT --> x) = INT & rng (INT --> x) = {x} &
    dom (c") = Card X & rng (c") = X & {x} \/ X = X & INT \/ Card X = INT
    by ThNum2,XBOOLE_1:12,FUNCOP_1:14,19; then
    dom a = INT & rng a c= X by FUNCT_4:def 1,18; then
    reconsider a as INT-Array of X by FUNCT_2:4;
    hereby take a;
      dom (c") = Card X by ThNum2;
      hence a|Card X is one-to-one by FUNCT_4:24;
      thus for t being INT-Expression of A,f holds
      a*t is INT-Variable of A,f by cII2;
    end;
    thus thesis by cII3;
  end;
end;

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

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

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

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

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

definition redefine
  let A,X,T,f;
  let t be INT-Expression of A,f;
  let i be integer number;
  func t+i -> INT-Expression of A,f;
  coherence
  proof
    .(i,X) is INT-Expression of A,f by INT'iwa; then
A1: t+.(i,X) is INT-Expression of A,f by INT'iwa;
A2: dom (t+.(i,X)) = Funcs(X,INT) & dom t = Funcs(X,INT) by FUNCT_2:def 1;
    now
      let a be set;
      assume a in Funcs(X,INT); then
      reconsider s = a as Element of Funcs(X,INT);
      thus (t+.(i,X)).a = (t.s)+(.(i,X).s) by A2,VALUED_1:def 1
        .= i+(t.a) by FUNCOP_1:13;
    end;
    hence thesis by A1,A2,VALUED_1:def 2;
  end;
  func t-i -> INT-Expression of A,f;
  coherence
  proof
    .(i,X) is INT-Expression of A,f by INT'iwa; then
    -.(i,X) is INT-Expression of A,f by INT'iwa; then
A1: t+-.(i,X) is INT-Expression of A,f by INT'iwa;
A2: dom (t+-.(i,X)) = Funcs(X,INT) & dom t = Funcs(X,INT) &
    dom (t-i) = dom t & dom (-.(i,X)) = Funcs(X,INT)
    by FUNCT_2:def 1,VALUED_1:3;
    now
      let a be set;
      assume a in Funcs(X,INT); then
      reconsider s = a as Element of Funcs(X,INT);
      thus (t+-.(i,X)).a = (t.s)+(-.(i,X)).s by A2,VALUED_1:def 1
        .= (t.s)+-(.(i,X).s) by VALUED_1:8
        .= (t.s)-i by FUNCOP_1:13
        .= (t-i).a by A2,VALUED_1:3;
    end;
    hence thesis by A1,A2,FUNCT_1:9;
  end;
  func t*i -> INT-Expression of A,f;
  coherence
  proof
    .(i,X) is INT-Expression of A,f by INT'iwa; then
A1: t(#).(i,X) is INT-Expression of A,f by INT'iwa;
A2: dom (t(#).(i,X)) = Funcs(X,INT) & dom t = Funcs(X,INT) by FUNCT_2:def 1;
    now
      let a be set;
      assume a in Funcs(X,INT); then
      reconsider s = a as Element of Funcs(X,INT);
      thus (t(#).(i,X)).a = (t.s)*(.(i,X).s) by A2,VALUED_1:def 4
        .= i*(t.a) by FUNCOP_1:13;
    end;
    hence thesis by A1,A2,VALUED_1:def 5;
  end;
end;

definition redefine
  let A,X,T,f;
  let t1,t2 be INT-Expression of A,f;
  func t1-t2 -> INT-Expression of A,f;
  coherence
  proof
    -t2 is INT-Expression of A,f &
    t1-t2 = t1+-t2 by RFUNCT_1:40;
    hence thesis by INT'iwa;
  end;
  func t1+t2 -> INT-Expression of A,f;
  coherence by INT'iwa;
  func t1(#)t2 -> INT-Expression of A,f;
  coherence by INT'iwa;
end;

definition redefine
  let A,X,T,f;
  let t1,t2 be INT-Expression of A,f;
  func t1 div t2 -> INT-Expression of A,f means:
DEFdiv2:
  for s being Element of Funcs(X, INT) holds it.s = t1.s div t2.s;
  coherence by INT'iwa;
  compatibility
  proof
    let ti be INT-Expression of A,f;
A1: dom (t1 div t2) = (dom t1)/\dom t2 & dom t1 = Funcs(X, INT) &
    dom t2 = Funcs(X, INT) & dom ti = Funcs(X, INT) by DEFdiv,FUNCT_2:def 1;
    hence ti = t1 div t2 implies
    for s being Element of Funcs(X, INT) holds ti.s = t1.s div t2.s by DEFdiv;
    assume
    for s being Element of Funcs(X, INT) holds ti.s = t1.s div t2.s; then
    for s being set st s in Funcs(X, INT) holds ti.s = t1.s div t2.s;
    hence ti = t1 div t2 by A1,DEFdiv;
  end;
  func t1 mod t2 -> INT-Expression of A,f means:
DEFmod2:
  for s being Element of Funcs(X, INT) holds it.s = t1.s mod t2.s;
  coherence by INT'iwa;
  compatibility
  proof
    let ti be INT-Expression of A,f;
A1: dom (t1 mod t2) = (dom t1)/\dom t2 & dom t1 = Funcs(X, INT) &
    dom t2 = Funcs(X, INT) & dom ti = Funcs(X, INT) by DEFmod,FUNCT_2:def 1;
    hence ti = t1 mod t2 implies
    for s being Element of Funcs(X, INT) holds ti.s = t1.s mod t2.s by DEFmod;
    assume
    for s being Element of Funcs(X, INT) holds ti.s = t1.s mod t2.s; then
    for s being set st s in Funcs(X, INT) holds ti.s = t1.s mod t2.s;
    hence ti = t1 mod t2 by A1,DEFmod;
  end;
  func leq(t1,t2) -> INT-Expression of A,f means:
DEFleq2:
  for s being Element of Funcs(X, INT) holds it.s = IFGT(t1.s,t2.s,0,1);
  compatibility
  proof
    let ti be INT-Expression of A,f;
A1: dom leq(t1,t2) = (dom t1)/\dom t2 & dom t1 = Funcs(X, INT) &
    dom t2 = Funcs(X, INT) & dom ti = Funcs(X, INT) by DEFleq,FUNCT_2:def 1;
    hence ti = leq(t1,t2) implies
    for s being Element of Funcs(X, INT) holds ti.s = IFGT(t1.s,t2.s,0,1)
    by DEFleq;
    assume
    for s being Element of Funcs(X, INT) holds ti.s = IFGT(t1.s,t2.s,0,1); then
    for s being set st s in Funcs(X, INT) holds ti.s = IFGT(t1.s,t2.s,0,1);
    hence ti = leq(t1,t2) by A1,DEFleq;
  end;
  coherence by INT'iwa;
  func gt(t1,t2) -> INT-Expression of A,f means:
DEFgt2:
  for s being Element of Funcs(X, INT) holds it.s = IFGT(t1.s,t2.s,1,0);
  coherence by INT'iwa;
  compatibility
  proof
    let ti be INT-Expression of A,f;
A1: dom gt(t1,t2) = (dom t1)/\dom t2 & dom t1 = Funcs(X, INT) &
    dom t2 = Funcs(X, INT) & dom ti = Funcs(X, INT) by DEFgt,FUNCT_2:def 1;
    hence ti = gt(t1,t2) implies
    for s being Element of Funcs(X, INT) holds ti.s = IFGT(t1.s,t2.s,1,0)
    by DEFgt;
    assume
    for s being Element of Funcs(X, INT) holds ti.s = IFGT(t1.s,t2.s,1,0); then
    for s being set st s in Funcs(X, INT) holds ti.s = IFGT(t1.s,t2.s,1,0);
    hence ti = gt(t1,t2) by A1,DEFgt;
  end;
end;

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

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


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

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

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

theorem ThE1:
  for x being Variable of f
  for s being Element of Funcs(X, INT) holds (.x).s = s.x
  proof
    let x be Variable of f;
    let s be Element of Funcs(X, INT);
    thus (.x).s = s.((x^(A,f)).s) by DEFvarexp .= s.x by FUNCOP_1:13;
  end;

definition
  let A,X,T,f;
  let i be integer number;
  func .(i,A,f) -> INT-Expression of A,f equals .(i,X);
  coherence by INT'iwa;
end;

definition  :: "choose" function may cause some problems in further development.
  let A,X,T,f;
  let v be INT-Variable of A,f;
  let t be INT-Expression of A,f;
  func v:=t -> Element of A equals choose {I where I is Element of A:
  I in ElementaryInstructions A &
  for s being Element of Funcs(X, INT) holds f.(s,I) = s+*(v.s,t.s)};
  coherence
  proof set Y = {I where I is Element of A:
    I in ElementaryInstructions A &
    for s being Element of Funcs(X, INT) holds f.(s,I) = s+*(v.s,t.s)};
    v,t form_assignment_wrt f by INT'iwa; then
    consider I0 being Element of A such that
A0: I0 in ElementaryInstructions A and
A1: for s being Element of Funcs(X, INT) holds f.(s,I0) = s+*(v.s,t.s) by FA;
A2: Y c= the carrier of A
    proof let i be set;
      assume i in Y; then
      ex I being Element of A st i = I & I in ElementaryInstructions A &
      for s being Element of Funcs(X, INT) holds f.(s,I) = s+*(v.s,t.s);
      hence thesis;
    end;
    I0 in Y by A0,A1; then
    choose Y in Y;
    hence thesis by A2;
  end;
end;

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

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

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

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

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

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

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

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

definition
  let A,X,T,f;
  let v1,v2 be INT-Variable of A,f;
  let x be Variable of f;
  func swap(v1,x,v2) -> absolutely-terminating Element of A
  equals x:=v1\;v1:=v2\;v2:=.x;
  coherence;
end;

definition
  let A,X,T,f;
  let x be Variable of f;
  let t be INT-Expression of A,f;
  func x+=t -> absolutely-terminating Element of A equals x:=(.x+t);
  correctness;
  func x*=t -> absolutely-terminating Element of A equals x:=(.x(#)t);
  correctness;
  func x%=t -> absolutely-terminating Element of A equals x:=(.x mod t);
  correctness;
  func x/=t -> absolutely-terminating Element of A equals x:=(.x div t);
  correctness;
end;

definition
  let A,X,T,f;
  let x be Variable of f;
  let i be integer number;
  func x+=i -> absolutely-terminating Element of A equals x:=(.x+i);
  correctness;
  func x*=i -> absolutely-terminating Element of A equals x:=(.x*i);
  correctness;
  func x%=i -> absolutely-terminating Element of A equals x:=(.x mod .(i,A,f));
  correctness;
  func x/=i -> absolutely-terminating Element of A equals x:=(.x div .(i,A,f));
  correctness;
  func x div i -> INT-Expression of A,f equals .x div .(i,A,f);
  correctness;
end;

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

definition
  let A,X,T,f;
  let v be INT-Variable of A,f;
  let i be integer number;
  func v+=i -> absolutely-terminating Element of A equals v:=(.v+i);
  correctness;
  func v*=i -> absolutely-terminating Element of A equals v:=(.v*i);
  correctness;
end;

definition
  let A,X;
  let b be Element of X;
  let g be Euclidean ExecutionFunction of A, Funcs(X,INT), Funcs(X, INT)\(b,0);
  let t1 be INT-Expression of A,g;
  func t1 is_odd -> absolutely-terminating Element of A
  equals b:=(t1 mod .(2,A,g));
  coherence;
  func t1 is_even -> absolutely-terminating Element of A
  equals b:=((t1+1) mod .(2,A,g));
  coherence;
  let t2 be INT-Expression of A,g;
  func t1 leq t2 -> absolutely-terminating Element of A equals b:=leq(t1,t2);
  coherence;
  func t1 gt t2 -> absolutely-terminating Element of A equals b:=gt(t1,t2);
  coherence;
  func t1 eq t2 -> absolutely-terminating Element of A equals b:=eq(t1,t2);
  coherence;
end;

notation
  let A,X;
  let b be Element of X;
  let g be Euclidean ExecutionFunction of A, Funcs(X,INT), Funcs(X, INT)\(b,0);
  let t1,t2 be INT-Expression of A,g;
  synonym t2 geq t1 for t1 leq t2;
  synonym t2 lt t1 for t1 gt t2;
end;

definition
  let A,X;
  let b be Element of X;
  let g be Euclidean ExecutionFunction of A, Funcs(X,INT), Funcs(X, INT)\(b,0);
  let v1,v2 be INT-Variable of A,g;
  func v1 leq v2 -> absolutely-terminating Element of A equals .v1 leq .v2;
  coherence;
  func v1 gt v2 -> absolutely-terminating Element of A equals .v1 gt .v2;
  coherence;
end;

notation
  let A,X;
  let b be Element of X;
  let g be Euclidean ExecutionFunction of A, Funcs(X,INT), Funcs(X, INT)\(b,0);
  let v1,v2 be INT-Variable of A,g;
  synonym v2 geq v1 for v1 leq v2;
  synonym v2 lt v1 for v1 gt v2;
end;

definition
  let A,X;
  let b be Element of X;
  let g be Euclidean ExecutionFunction of A, Funcs(X,INT), Funcs(X, INT)\(b,0);
  let x1 be Variable of g;
  func x1 is_odd -> absolutely-terminating Element of A equals .x1 is_odd;
  coherence;
  func x1 is_even -> absolutely-terminating Element of A equals .x1 is_even;
  coherence;
  let x2 be Variable of g;
  func x1 leq x2 -> absolutely-terminating Element of A equals .x1 leq .x2;
  coherence;
  func x1 gt x2 -> absolutely-terminating Element of A equals .x1 gt .x2;
  coherence;
end;

notation
  let A,X;
  let b be Element of X;
  let g be Euclidean ExecutionFunction of A, Funcs(X,INT), Funcs(X, INT)\(b,0);
  let x1,x2 be Variable of g;
  synonym x2 geq x1 for x1 leq x2;
  synonym x2 lt x1 for x1 gt x2;
end;

definition
  let A,X;
  let b be Element of X;
  let g be Euclidean ExecutionFunction of A, Funcs(X,INT), Funcs(X, INT)\(b,0);
  let x be Variable of g;
  let i be integer number;
  func x leq i -> absolutely-terminating Element of A equals .x leq .(i,A,g);
  coherence;
  func x geq i -> absolutely-terminating Element of A equals .x geq .(i,A,g);
  coherence;
  func x gt i -> absolutely-terminating Element of A equals .x gt .(i,A,g);
  coherence;
  func x lt i -> absolutely-terminating Element of A equals .x lt .(i,A,g);
  coherence;
  func x / i -> INT-Expression of A,g equals (.x) div .(i,A,g);
  coherence;
end;

definition
  let A,X,T,f;
  let x1,x2 be Variable of f;
  func x1+=x2 -> absolutely-terminating Element of A equals x1+=.x2;
  coherence;
  func x1*=x2 -> absolutely-terminating Element of A equals x1*=.x2;
  coherence;
  func x1%=x2 -> absolutely-terminating Element of A equals x1:=(.x1 mod .x2);
  coherence;
  func x1/=x2 -> absolutely-terminating Element of A equals x1:=(.x1 div .x2);
  coherence;
  func x1+x2 -> INT-Expression of A,f equals (.x1)+(.x2); coherence;
  func x1*x2 -> INT-Expression of A,f equals (.x1)(#)(.x2); coherence;
  func x1 mod x2 -> INT-Expression of A,f equals (.x1)mod(.x2); coherence;
  func x1 div x2 -> INT-Expression of A,f equals (.x1)div(.x2); coherence;
end;

reserve
  A for Euclidean preIfWhileAlgebra,
  X for non empty countable set, x,y,z for (Element of X),
  s,s' for (Element of Funcs(X, INT)),
  T for Subset of Funcs(X, INT),
  f for Euclidean ExecutionFunction of A, Funcs(X, INT), T,
  v for INT-Variable of A,f,
  t for INT-Expression of A,f;
reserve i,j,k for integer number;

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

theorem Th011:
  for x being Variable of f
  for i being integer number holds
  f.(s, x:=i).x = i &
  for z st z <> x holds f.(s, x:=i).z = s.z
  proof
    let x be Variable of f;
    let i be integer number;
    x:=i = ^x:=.(i,A,f) & (^x).s = x & .(i,A,f).s = i by FUNCOP_1:13;
    hence thesis by Th100;
  end;

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

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

theorem Th012:
  for x being Variable of f holds f.(s, x+=i).x = s.x+i &
  for z st z <> x holds f.(s, x+=i).z = s.z
  proof
    let x be Variable of f;
    x+=i = x:=(.x+i) & x:=(.x+i) = ^x:=(.x+i) & .x = .(^x) &
    (^x).s = x & (.x+i).s = ((.x).s+i) &
    .(^(x qua Element of X)).s = s.((^(x qua Element of X)).s)
    by DEFvarexp,DEFplus2,FUNCOP_1:13;
    hence thesis by Th100;
  end;

theorem Th112:
  for x being Variable of f
  for t being INT-Expression of A,f holds
  f.(s, x+=t).x = s.x+t.s &
  for z st z <> x holds f.(s, x+=t).z = s.z
  proof
    let x be Variable of f;
    let t be INT-Expression of A,f;
00: dom (.x+t) = Funcs(X, INT) by FUNCT_2:def 1;
    x+=t = x:=(.x+t)  & (^x).s = x & (.x+t).s = (.x).s+t.s & (.x).s = s.x
    by 00,ThE1,FUNCOP_1:13,VALUED_1:def 1;
    hence thesis by Th100;
  end;

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

theorem Th013:
  for x being Variable of f holds f.(s, x*=i).x = s.x*i &
  for z st z <> x holds f.(s, x*=i).z = s.z
  proof
    let x be Variable of f;
    x*=i = x:=(.x*i) & x:=(.x*i) = ^x:=(.x*i) & .x = .(^x) &
    (^x).s = x & (.x*i).s = ((.x).s*i) &
    .(^(x qua Element of X)).s = s.((^(x qua Element of X)).s)
    by DEFvarexp,DEFmult2,FUNCOP_1:13;
    hence thesis by Th100;
  end;

theorem Th113:
  for x being Variable of f
  for t being INT-Expression of A,f holds
  f.(s, x*=t).x = s.x*t.s &
  for z st z <> x holds f.(s, x*=t).z = s.z
  proof
    let x be Variable of f;
    let t be INT-Expression of A,f;
00: dom (.x(#)t) = Funcs(X, INT) by FUNCT_2:def 1;
    x*=t = x:=(.x(#)t)  & (^x).s = x & (.x(#)t).s = (.x).s*t.s & (.x).s = s.x
    by 00,ThE1,FUNCOP_1:13,VALUED_1:def 4;
    hence thesis by Th100;
  end;

theorem Th213:
  for x,y being Variable of f holds f.(s, x*=y).x = s.x*s.y &
  for z st z <> x holds f.(s, x*=y).z = s.z
  proof
    let x,y be Variable of f;
01: dom (.x(#).y) = Funcs(X, INT) by FUNCT_2:def 1;
    (^x).s = x by FUNCOP_1:13;
    hence f.(s, x*=y).x = (.x(#).y).s by Th100
    .= ((.x).s)*(.y.s) by 01,VALUED_1:def 4 .= (s.x)*(.y.s) by ThE1
    .= (s.x)*(s.y) by ThE1;
    thus thesis by Th111;
  end;

theorem Th014:
  for b being Element of X
  for g being Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0)
  for x being Variable of g holds
  for i being integer number holds
  (s.x <= i implies g.(s, x leq i).b = 1) &
  (s.x > i implies g.(s, x leq i).b = 0) &
  (s.x >= i implies g.(s, x geq i).b = 1) &
  (s.x < i implies g.(s, x geq i).b = 0) &
  for z st z <> b holds g.(s, x leq i).z = s.z & g.(s, x geq i).z = s.z
  proof
    let b be Element of X;
    let f be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
    let x be Variable of f;
    let i be integer number;
    reconsider b' = b as Variable of f by ELEM;
    reconsider x' = x as Element of X;
    set v = ^b';
    set t = leq(.x,.(i,A,f));
04: (.(i,A,f)).s = i by FUNCOP_1:13;
    (.x).s = s.((^x).s) & ^x = Funcs(X,INT) --> x by DEFvarexp; then
01: s.x = (.x).s & v.s = b by FUNCOP_1:13;
02: (.x).s <= i implies IFGT((.x).s,i,0,1) = 1 by XXREAL_0:def 10;
03: (.x).s > i implies IFGT((.x).s,i,0,1) = 0 by XXREAL_0:def 10;
05: (.x).s >= i implies IFGT(i,(.x).s,0,1) = 1 by XXREAL_0:def 10;
06: (.x).s < i implies IFGT(i,(.x).s,0,1) = 0 by XXREAL_0:def 10;
    .x leq .(i,A,f) = v:=leq(.x,.(i,A,f)) &
    leq(.x,.(i,A,f)).s = IFGT((.x).s,.(i,A,f).s,0,1) &
    .x geq .(i,A,f) = v:=leq(.(i,A,f),.x) &
    leq(.(i,A,f),.x).s = IFGT(.(i,A,f).s,(.x).s,0,1)
    by DEFleq2;
    hence thesis by 01,02,03,04,05,06,Th100;
  end;

theorem Th114:
  for b being Element of X
  for g being Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0)
  for x,y being Variable of g holds
  (s.x <= s.y implies g.(s, x leq y).b = 1) &
  (s.x > s.y implies g.(s, x leq y).b = 0) &
  for z st z <> b holds g.(s, x leq y).z = s.z
  proof
    let b be Element of X;
    let f be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
    let x,y be Variable of f;
    reconsider b' = b as Variable of f by ELEM;
    reconsider x' = x, y' = y as Element of X;
    set v = ^b';
    set t = leq(.x,.y);
    (.x).s = s.((^x).s) & ^x = Funcs(X,INT) --> x &
    (.y).s = s.((^y).s) & ^y = Funcs(X,INT) --> y by DEFvarexp; then
01: s.x = (.x).s & s.y = (.y).s & v.s = b by FUNCOP_1:13;
02: (.x).s <= .y.s implies IFGT((.x).s,(.y).s,0,1) = 1 by XXREAL_0:def 10;
03: (.x).s > .y.s implies IFGT((.x).s,(.y).s,0,1) = 0 by XXREAL_0:def 10;
    .x leq .y = v:=leq(.x,.y) & leq(.x,.y).s = IFGT((.x).s,(.y).s,0,1)
    by DEFleq2;
    hence thesis by 01,02,03,Th100;
  end;

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

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

theorem Th015:
  for b being Element of X
  for g being Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0)
  for x being Variable of g
  for i being integer number holds
  (s.x > i implies g.(s, x gt i).b = 1) &
  (s.x <= i implies g.(s, x gt i).b = 0) &
  (s.x < i implies g.(s, x lt i).b = 1) &
  (s.x >= i implies g.(s, x lt i).b = 0) &
  for z st z <> b holds g.(s, x gt i).z = s.z & g.(s, x lt i).z = s.z
  proof
    let b be Element of X;
    let f be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
    let x be Variable of f;
    let i be integer number;
    reconsider b' = b as Variable of f by ELEM;
    reconsider x' = x as Element of X;
    set v = ^b';
    set t = gt(.x,.(i,A,f));
04: (.x).s = s.((^x).s) & ^x = Funcs(X,INT) --> x &
    (.(i,A,f)).s = i by DEFvarexp,FUNCOP_1:13; then
01: s.x = (.x).s & v.s = b by FUNCOP_1:13;
02: (.x).s > i implies IFGT((.x).s,i,1,0) = 1 by XXREAL_0:def 10;
03: (.x).s <= i implies IFGT((.x).s,i,1,0) = 0 by XXREAL_0:def 10;
05: (.x).s < i implies IFGT(i,(.x).s,1,0) = 1 by XXREAL_0:def 10;
06: (.x).s >= i implies IFGT(i,(.x).s,1,0) = 0 by XXREAL_0:def 10;
    .x gt .(i,A,f) = v:=gt(.x,.(i,A,f)) &
    gt(.x,.(i,A,f)).s = IFGT((.x).s,(.(i,A,f)).s,1,0) &
    .x lt .(i,A,f) = v:=gt(.(i,A,f),.x) &
    gt(.(i,A,f),.x).s = IFGT((.(i,A,f)).s,(.x).s,1,0) by DEFgt2;
    hence thesis by 01,02,03,04,05,06,Th100;
  end;

theorem Th115:
  for b being Element of X
  for g being Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0)
  for x,y being Variable of g holds
  (s.x > s.y implies g.(s, x gt y).b = 1) &
  (s.x <= s.y implies g.(s, x gt y).b = 0) &
  (s.x < s.y implies g.(s, x lt y).b = 1) &
  (s.x >= s.y implies g.(s, x lt y).b = 0) &
  for z st z <> b holds g.(s, x gt y).z = s.z & g.(s, x lt y).z = s.z
  proof
    let b be Element of X;
    let f be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
    let x,y be Variable of f;
    reconsider b' = b as Variable of f by ELEM;
    reconsider x' = x, y' = y as Element of X;
    set v = ^b';
    set t = gt(.x,.y);
    (.x).s = s.((^x).s) & ^x = Funcs(X,INT) --> x &
    (.y).s = s.((^y).s) & ^y = Funcs(X,INT) --> y by DEFvarexp; then
01: s.x = (.x).s & s.y = (.y).s & v.s = b by FUNCOP_1:13;
02: (.x).s > .y.s implies IFGT((.x).s,(.y).s,1,0) = 1 by XXREAL_0:def 10;
03: (.x).s <= .y.s implies IFGT((.x).s,(.y).s,1,0) = 0 by XXREAL_0:def 10;
04: (.x).s < .y.s implies IFGT((.y).s,(.x).s,1,0) = 1 by XXREAL_0:def 10;
05: (.x).s >= .y.s implies IFGT((.y).s,(.x).s,1,0) = 0 by XXREAL_0:def 10;
    .x gt .y = v:=gt(.x,.y) & gt(.x,.y).s = IFGT((.x).s,(.y).s,1,0) &
    .x lt .y = v:=gt(.y,.x) & gt(.y,.x).s = IFGT((.y).s,(.x).s,1,0)
    by DEFgt2;
    hence thesis by 01,02,03,04,05,Th100;
  end;

theorem Th015':
  for b being Element of X
  for g being Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0)
  for x being Variable of g
  for i being integer number holds
  (s.x > i iff g.(s, x gt i) in Funcs(X,INT)\(b,0)) &
  (s.x < i iff g.(s, x lt i) in Funcs(X,INT)\(b,0))
  proof
    let b be Element of X;
    let g be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
    let x be Variable of g;
    let i be integer number;
    g.(s, x gt i) in Funcs(X,INT)\(b,0) iff g.(s, x gt i).b <> 0 by LemTS;
    hence (s.x > i iff g.(s, x gt i) in Funcs(X,INT)\(b,0)) by Th015;
    g.(s, x lt i) in Funcs(X,INT)\(b,0) iff g.(s, x lt i).b <> 0 by LemTS;
    hence thesis by Th015;
  end;

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

theorem
  for x being Variable of f holds f.(s, x%=i).x = s.x mod i &
  for z st z <> x holds f.(s, x%=i).z = s.z
  proof
    let x be Variable of f;
    x%=i = ^x:=(.x mod .(i,A,f)) & .(i,A,f).s = i & .x = .(^x) &
    (^x).s = x & (.x mod .(i,A,f)).s = (.x).s mod (.(i,A,f).s) &
    .(^(x qua Element of X)).s = s.((^(x qua Element of X)).s)
    by DEFvarexp,DEFmod2,FUNCOP_1:13;
    hence thesis by Th100;
  end;

theorem Th116:
  for x being Variable of f
  for t being INT-Expression of A,f holds
  f.(s, x%=t).x = s.x mod t.s &
  for z st z <> x holds f.(s, x%=t).z = s.z
  proof
    let x be Variable of f;
    let t be INT-Expression of A,f;
    x%=t = x:=(.x mod t)  & (^x).s = x & (.x mod t).s = (.x).s mod t.s &
    (.x).s = s.x by ThE1,DEFmod2,FUNCOP_1:13;
    hence thesis by Th100;
  end;

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

theorem Th017:
  for x being Variable of f holds f.(s, x/=i).x = s.x div i &
  for z st z <> x holds f.(s, x/=i).z = s.z
  proof
    let x be Variable of f;

    x/=i = ^x:=(.x div .(i,A,f)) & .(i,A,f).s = i & .x = .(^x) &
    (^x).s = x & (.x div .(i,A,f)).s = (.x).s div (.(i,A,f).s) &
    .(^(x qua Element of X)).s = s.((^(x qua Element of X)).s)
    by DEFvarexp,DEFdiv2,FUNCOP_1:13;
    hence thesis by Th100;
  end;

theorem Th117:
  for x being Variable of f
  for t being INT-Expression of A,f holds
  f.(s, x/=t).x = s.x div t.s &
  for z st z <> x holds f.(s, x/=t).z = s.z
  proof
    let x be Variable of f;
    let t be INT-Expression of A,f;
    x/=t = x:=(.x div t)  & (^x).s = x & (.x div t).s = (.x).s div t.s &
    (.x).s = s.x by ThE1,DEFdiv2,FUNCOP_1:13;
    hence thesis by Th100;
  end;

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

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

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

LemMod:
for i,j being integer number holds
(i is even iff j is even) iff i+j is even
proof
  let i,j be integer number;
  i is even or i is odd; then
  consider i0 being even Integer, i1 being odd Integer such that
A: i = i0 or i = i1;
  j is even or j is odd; then
  consider j0 being even Integer, j1 being odd Integer such that
B: j = j0 or j = j1;
   i0+j0 is even & i0+j1 is odd & i1+j0 is odd & i1+j1 is even;
   hence thesis by A,B;
end;

theorem Th318:
  for b being Element of X
  for g being Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0)
  for t being INT-Expression of A,g holds
  (t.s is odd iff g.(s, t is_odd) in Funcs(X,INT)\(b,0)) &
  (t.s is even iff g.(s, t is_even) in Funcs(X,INT)\(b,0))
  proof
    let b be Element of X;
    let f be Euclidean ExecutionFunction of A,Funcs(X,INT), Funcs(X,INT)\(b,0);
    let t be INT-Expression of A,f;
01: f.(s, t is_odd).b = (t.s) mod 2 & f.(s, t is_even).b = (t.s+1) mod 2
    by Th118;
02: (t.s) mod 2 = 0 or (t.s) mod 2 = 1 by PRE_FF:6;
03: t.s = ((t.s) div 2)*2 + ((t.s) mod 2) by INT_1:86;
04: ((t.s) div 2)*2 is even & ((t.s) div 2)*2 + 1 is odd;
    thus (t.s is odd iff f.(s, t is_odd) in Funcs(X,INT)\(b,0))
    by      01,    02,     03,     04, LemTS;
02: (t.s+1) mod 2 = 0 or (t.s+1) mod 2 = 1 by PRE_FF:6;
03: t.s+1 = ((t.s+1) div 2)*2 + ((t.s+1) mod 2) by INT_1:86;
    thus thesis by    01,   02,  03,  JORDAN12:3,  LemMod, LemTS;
  end;

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


scheme ForToIteration
  {A() -> Euclidean preIfWhileAlgebra,
   X() -> countable non empty set,
   b() -> (Element of X()),
   I,F() -> (Element of A()),
   g() -> Euclidean ExecutionFunction of A(),
          Funcs(X(),INT), Funcs(X(),INT)\(b(),0),
   i,n() -> (Variable of g()),
   s() -> (Element of Funcs(X(),INT)),
   a() -> INT-Expression of A(),g(),
   P[set]
  }:
  P[g().(s(),F())] &
  (a().s() <= s().n() implies g().(s(),F()).i() = s().n()+1) &
  (a().s() > s().n() implies g().(s(),F()).i() = a().s()) &
  g().(s(),F()).n() = s().n()
provided
F: F() = for-do(i():=a(), i() leq n(), i()+=1, I()) and
A: P[g().(s(),i():=a())] and
B: for s being Element of Funcs(X(),INT) st P[s]
   holds P[g().(s,I()\;i()+=1)] & P[g().(s, i() leq n())] and
C: for s being Element of Funcs(X(),INT) st P[s]
   holds g().(s,I()).i() = s.i() & g().(s,I()).n() = s.n() and
D: n() <> i() & n() <> b() & i() <> b()
  proof
    set S = Funcs(X(),INT);
    set T = S\(b(),0);
    set C = i() leq n();
    set II = I()\;i()+=1;
Z0: g() is complying_with_catenation & g() complies_with_while_wrt T
    by AOFA_000:def 32;
    reconsider s1 = g().(s(),i():=a()) as Element of S;
    reconsider s2 = g().(s1,C) as Element of S;
S1: s1.i() = a().s() & s1.n() = s().n() by D,Th111; then
S2: s2.i() = a().s() & s2.n() = s().n() by D,Th114;
Sn: g().(s(),F()) = g().(s1,while(C, II)) by F,AOFA_000:def 29;
    defpred R[Element of S] means $1.i() <= $1.n();
    defpred Q[Element of S] means P[$1] &
    (a().s() <= s().n() implies $1.i()-1 <= s().n()) &
    $1.n() = s().n();
    a().s()-1 < a().s() by XREAL_1:46; then
A1: Q[s1] by A,S1,XXREAL_0:2;
A2: P[s2] by B,A;
    per cases;
    suppose
C1:   a().s() <= s().n(); then
B':   s2.b() = 1 by S1,Th114;
      defpred PR[Element of S] means P[$1] & R[$1];
BB:   g().(s1,C) in T iff PR[g().(s1,C) qua Element of S] by A,B,C1,S2,B';
      deffunc F(Element of S) = In($1.n()+1-$1.i(),NAT);
Ct:   for s being Element of S st PR[s]
      holds (PR[g().(s,II\;C) qua Element of S] iff g().(s,II\;C) in T) &
      F(g().(s,II\;C) qua Element of S) < F(s)
      proof
        let s be Element of S; assume
00:     PR[s];
        reconsider s' = g().(s,I()) as Element of S;
        reconsider s'' = g().(s',i()+=1) as Element of S;
        reconsider s''' = g().(s'',C) as Element of S;
01:     g().(s,II\;C) = g().(g().(s,II),C) & s'' = g().(s,II)
        by AOFA_000:def 29;
02:     s'''.i() = s''.i() & s'''.n() = s''.n() &
        (s''.i() > s''.n() implies s'''.b() = 0) &
        (s''.i() <= s''.n() implies s'''.b() = 1) by D,Th114;
03:     s'.i() = s.i() & s'.n() = s.n() by C,00;
04:     s''.i() = s'.i()+1 & s''.n() = s'.n() & P[s''] by 00,01,B,D,Th012;
        hence (PR[g().(s,II\;C) qua Element of S] iff g().(s,II\;C) in T)
        by 01,02,B,LemTS;
        reconsider j = s.n()-s.i() as Element of NAT by 00,INT_1:18;
        F(s''') = j by 02,03,04,FUNCT_7:def 1; then
        F(s''')+1 = F(s) by FUNCT_7:def 1;
        hence F(g().(s,II\;C) qua Element of S) < F(s) by 01,NAT_1:13;
      end;
C':   g() iteration_terminates_for II\;C, g().(s1,C)
      from AOFA_000:sch 3(BB,Ct);
D':   for s being Element of S st Q[s] & s in T & R[s]
      holds Q[g().(s,II) qua Element of S]
      proof
        let s be Element of S; assume
01:     Q[s] & s in T & R[s];
        thus P[g().(s,II)] by B,01;
        reconsider s' = g().(s,I()) as Element of S;
        reconsider s'' = g().(s',i()+=1) as Element of S;
03:     s'.i() = s.i() & s'.n() = s.n() &
        s''.i() = s'.i()+1 & s''.n() = s'.n() by 01,C,D,Th012;
        s'' = g().(s,II) by AOFA_000:def 29;
        hence thesis by 01,03;
      end;
E':   for s being Element of S st Q[s] holds Q[g().(s,C) qua Element of S] &
      (g().(s,C) in T iff R[g().(s,C) qua Element of S])
      proof
        let s be Element of S; assume
01:     Q[s];
        hence P[g().(s,C)] by B;
        g().(s,C).i() = s.i() & g().(s,C).n() = s.n() &
        (s.i() > s.n() implies g().(s,C).b() = 0) &
        (s.i() <= s.n() implies g().(s,C).b() = 1) by D,Th114;
        hence thesis by 01,LemTS;
      end;
F':   Q[g().(s1,while(C,II)) qua Element of S] &
      not R[g().(s1,while(C,II)) qua Element of S]
      from AOFA_000:sch 5(A1,C',D',E'); then
      (g().(s(),F()) qua Element of S).i() >= s().n()+1 by Sn,INT_1:20; then
      (g().(s(),F()) qua Element of S).i()-1 >= s().n()+1-1 by XREAL_1:15; then
      (g().(s(),F()) qua Element of S).i()-1 = s().n() by C1,Sn,F',XXREAL_0:1;
      hence thesis by C1,F,F',AOFA_000:def 29;
    end;
    suppose
C2:   a().s() > s().n(); then
      s2.b() = 0 by S1,Th114; then
      s2 nin T by LemTS;
      hence thesis by A2,C2,S2,Sn,Z0,AOFA_000:def 31;
    end;
  end;

scheme ForDowntoIteration
  {A() -> Euclidean preIfWhileAlgebra,
   X() -> countable non empty set,
   b() -> (Element of X()),
   I,F() -> (Element of A()),
   f() -> Euclidean ExecutionFunction of A(),
          Funcs(X(),INT), Funcs(X(),INT)\(b(),0),
   i,n() -> (Variable of f()),
   s() -> (Element of Funcs(X(),INT)),
   a() -> INT-Expression of A(),f(),
   P[set]
  }:
  P[f().(s(),F())] &
  (a().s() >= s().n() implies f().(s(),F()).i() = s().n()-1) &
  (a().s() < s().n() implies f().(s(),F()).i() = a().s()) &
  f().(s(),F()).n() = s().n()
provided
F: F() = for-do(i():=a(),.n() leq .i(),i()+=-1,I()) and
A: P[f().(s(),i():=a())] and
B: for s being Element of Funcs(X(),INT) st P[s]
   holds P[f().(s,I()\;i()+=-1)] & P[f().(s, n() leq i())] and
C: for s being Element of Funcs(X(),INT) st P[s]
   holds f().(s,I()).i() = s.i() & f().(s,I()).n() = s.n() and
D: n() <> i() & n() <> b() & i() <> b()
  proof
    set S = Funcs(X(),INT);
    set T = S\(b(),0);
    set C = n() leq i();
    set II = I()\;i()+=-1;
Z0: f() is complying_with_catenation & f() complies_with_while_wrt T
    by AOFA_000:def 32;
    reconsider s1 = f().(s(),i():=a()) as Element of S;
    reconsider s2 = f().(s1,C) as Element of S;
S1: s1.i() = a().s() & s1.n() = s().n() by D,Th111; then
S2: s2.i() = a().s() & s2.n() = s().n() by D,Th114;
Sn: f().(s(),F()) = f().(s1,while(C, II)) by F,AOFA_000:def 29;
    defpred R[Element of S] means $1.i() >= $1.n();
    defpred Q[Element of S] means P[$1] &
    (a().s() >= s().n() implies $1.i()+1 >= s().n()) &
    $1.n() = s().n();
A1: Q[s1] by A,S1,XREAL_1:41;
A2: P[s2] by B,A;
    per cases;
    suppose
C1:   a().s() >= s().n(); then
B':      s2.b() = 1 by S1,Th114;
      defpred PR[Element of S] means P[$1] & R[$1];
BB:   f().(s1,C) in T iff PR[f().(s1,C) qua Element of S] by B',A,B,C1,S2;
      deffunc F(Element of S) = In($1.i()+1-$1.n(),NAT);
Ct:   for s being Element of S st PR[s]
      holds (PR[f().(s,II\;C) qua Element of S] iff f().(s,II\;C) in T) &
      F(f().(s,II\;C) qua Element of S) < F(s)
      proof
        let s be Element of S; assume
00:     PR[s];
        reconsider s' = f().(s,I()) as Element of S;
        reconsider s'' = f().(s',i()+=-1) as Element of S;
        reconsider s''' = f().(s'',C) as Element of S;
01:     f().(s,II\;C) = f().(f().(s,II),C) & s'' = f().(s,II)
        by AOFA_000:def 29;
02:     s'''.i() = s''.i() & s'''.n() = s''.n() &
        (s''.i() < s''.n() implies s'''.b() = 0) &
        (s''.i() >= s''.n() implies s'''.b() = 1) by D,Th114;
03:     s'.i() = s.i() & s'.n() = s.n() by C,00;
04:     s''.i() = s'.i()-1 & s''.n() = s'.n() & P[s''] by 00,01,B,D,Th012;
        hence (PR[f().(s,II\;C) qua Element of S] iff f().(s,II\;C) in T)
        by 01,02,B,LemTS;
        reconsider j = s.i()-s.n() as Element of NAT by 00,INT_1:18;
        F(s''') = j by 02,03,04,FUNCT_7:def 1; then
        F(s''')+1 = F(s) by FUNCT_7:def 1;
        hence F(f().(s,II\;C) qua Element of S) < F(s) by 01,NAT_1:13;
      end;
C':   f() iteration_terminates_for II\;C, f().(s1,C)
      from AOFA_000:sch 3(BB,Ct);
D':   for s being Element of S st Q[s] & s in T & R[s]
      holds Q[f().(s,II) qua Element of S]
      proof
        let s be Element of S; assume
01:     Q[s] & s in T & R[s];
        thus P[f().(s,II)] by 01,B;
        reconsider s'' = f().(s,I()) as Element of S;
        reconsider s''' = f().(s'',i()+=-1) as Element of S;
03:     s''.i() = s.i() & s''.n() = s.n() &
        s'''.i() = s''.i()-1 & s'''.n() = s''.n() by 01,C,D,Th012;
        s''' = f().(s,II) by AOFA_000:def 29;
        hence thesis by 01,03;
      end;
E':   for s being Element of S st Q[s] holds Q[f().(s,C) qua Element of S] &
      (f().(s,C) in T iff R[f().(s,C) qua Element of S])
      proof
        let s be Element of S; assume
01:     Q[s];
        hence P[f().(s,C)] by B;
        f().(s,C).i() = s.i() & f().(s,C).n() = s.n() &
        (s.i() < s.n() implies f().(s,C).b() = 0) &
        (s.i() >= s.n() implies f().(s,C).b() = 1) by D,Th114;
        hence thesis by 01,LemTS;
      end;
F':   Q[f().(s1,while(C,II)) qua Element of S] &
      not R[f().(s1,while(C,II)) qua Element of S]
      from AOFA_000:sch 5(A1,C',D',E'); then
      (f().(s(),F())qua Element of S).i()+1 <= s().n()+1-1 by Sn,INT_1:20; then
      (f().(s(),F()) qua Element of S).i()+1 = s().n() by C1,Sn,F',XXREAL_0:1;
      hence thesis by C1,F',F,AOFA_000:def 29;
    end;
    suppose
C2:   a().s() < s().n(); then
      s2.b() = 0 by S1,Th114; then
      s2 nin T by LemTS;
      hence thesis by A2,C2,S2,Sn,Z0,AOFA_000:def 31;
    end;
  end;

begin :: Termination in if-while algebras over integers

reserve
  b for (Element of X),
  g for Euclidean ExecutionFunction of A, Funcs(X, INT), Funcs(X, INT)\(b,0);


theorem ThT1:
  for I being Element of A
  for i,n being Variable of g
  st (ex d being Function st d.b = 0 & d.n = 1 & d.i = 2) &
     for s holds g.(s,I).n = s.n & g.(s,I).i = s.i
  holds
  g iteration_terminates_for I\; i+=1\; i leq n, g.(s, i leq n)
  proof let I be Element of A;
    let i,n be Variable of g;
    given d being Function such that
A0: d.b = 0 & d.n = 1 & d.i = 2;
D1: b <> i & b <> n & i <> n by A0;
    assume
00: for s holds g.(s,I).n = s.n & g.(s,I).i = s.i;
    set h = g;
    set S = Funcs(X, INT);
    set T = S\(b,0);
    set C = i leq n;
    set J = i+=1;
    reconsider s1 = h.(s, C) as Element of S;
    defpred R[Element of S] means $1.i <= $1.n;
    deffunc F(Element of S) = In($1.n+1-$1.i, NAT);
    (s.i > s.n implies s1.b = 0) & (s.i > s.n or s.i <= s.n) & s1.i = s.i &
    s1.n = s.n & (s.i <= s.n implies s1.b = 1) by A0,Th114; then
AB: s1 in T iff R[s1] by LemTS;
C:  for s being Element of S st R[s]
    holds (R[h.(s,I\;J\;C) qua Element of S] iff h.(s,I\;J\;C) in T) &
    F(h.(s,I\;J\;C) qua Element of S) < F(s)
    proof
      let s be Element of S; assume
      R[s]; then
      reconsider ni = s.n-s.i as Element of NAT by INT_1:16,XREAL_1:50;
      set s1 = h.(s, I);
      set q = h.(s, I\;J);
      set q1 = h.(q, C);
01:   (q.i > q.n implies q1.b = 0) & (q.i > q.n or q.i <= q.n) & q1.i = q.i &
      q1.n = q.n & (q.i <= q.n implies q1.b = 1) by A0,Th114;
02:   q = h.(s1, J) & q1 = h.(s, I\;J\;C) by AOFA_000:def 29;
      hence R[h.(s,I\;J\;C) qua Element of S] iff h.(s,I\;J\;C) in T
      by 01,LemTS;
      s1.i = s.i & s1.n = s.n by 00; then
      q.i = s.i+1 & q.n = s.n by 02,D1,Th012; then
      q1.i = s.i+1 & q1.n = s.n by A0,Th114; then
      F(q1 qua Element of S) = ni & F(s) = ni+1 by FUNCT_7:def 1;
      hence F(h.(s,I\;J\;C) qua Element of S) < F(s) by 02,NAT_1:13;
    end;
    h iteration_terminates_for I\;J\;C, s1 from AOFA_000:sch 3(AB,C);
    hence thesis;
  end;

theorem ThT12:
  for P being set
  for I being Element of A
  for i,n being Variable of g
  st (ex d being Function st d.b = 0 & d.n = 1 & d.i = 2) &
     for s st s in P holds g.(s,I).n = s.n & g.(s,I).i = s.i & g.(s, I) in P &
     g.(s, i leq n) in P & g.(s, i+=1) in P
  holds s in P implies
  g iteration_terminates_for I\; i+=1\; i leq n, g.(s, i leq n)
  proof let P be set;
    let I be Element of A;
    let i,n be Variable of g;
    given d being Function such that
D0: d.b = 0 & d.n = 1 & d.i = 2;
D1: b <> i & b <> n & i <> n by D0;
    assume that
00: for s st s in P holds g.(s,I).n = s.n & g.(s,I).i = s.i & g.(s, I) in P &
    g.(s, i leq n) in P & g.(s, i+=1) in P and
A0: s in P;
    set h = g;
    set S = Funcs(X, INT);
    set T = S\(b,0);
    set C = i leq n;
    set J = i+=1;
    reconsider s1 = h.(s, C) as Element of S;
    defpred P[Element of S] means $1 in P;
    defpred R[Element of S] means $1.i <= $1.n;
    deffunc F(Element of S) = In($1.n+1-$1.i, NAT);
AA: P[s1] by A0,00;
    (s.i > s.n implies s1.b = 0) & (s.i > s.n or s.i <= s.n) & s1.i = s.i &
    s1.n = s.n & (s.i <= s.n implies s1.b = 1) by D0,Th114; then
AB: s1 in T iff R[s1] by LemTS;
C:  for s being Element of S st P[s] & s in T & R[s]
    holds P[h.(s,I\;J\;C) qua Element of S] &
    (R[h.(s,I\;J\;C) qua Element of S] iff h.(s,I\;J\;C) in T) &
    F(h.(s,I\;J\;C) qua Element of S) < F(s)
    proof
      let s be Element of S; assume
01:   P[s] & s in T & R[s]; then
      reconsider ni = s.n-s.i as Element of NAT by INT_1:16,XREAL_1:50;
      set s1 = h.(s, I);
      set q = h.(s, I\;J);
      set q1 = h.(q, C);
03:   (q.i > q.n implies q1.b = 0) & (q.i > q.n or q.i <= q.n) & q1.i = q.i &
      q1.n = q.n & (q.i <= q.n implies q1.b = 1) by D0,Th114;
02:   q = h.(s1, J) & q1 = h.(s, I\;J\;C) by AOFA_000:def 29;
      P[s1 qua Element of S]  by 01,00; then
      P[q qua Element of S] by 00,02;
      hence P[h.(s,I\;J\;C) qua Element of S] by 00,02;
      thus R[h.(s,I\;J\;C) qua Element of S] iff h.(s,I\;J\;C) in T
      by 02,03,LemTS;
      s1.i = s.i & s1.n = s.n by 01,00; then
      q.i = s.i+1 & q.n = s.n by 02,D1,Th012; then
      q1.i = s.i+1 & q1.n = s.n by D0,Th114; then
      F(q1 qua Element of S) = ni & F(s) = ni+1 by FUNCT_7:def 1;
      hence F(h.(s,I\;J\;C) qua Element of S) < F(s) by 02,NAT_1:13;
    end;
    h iteration_terminates_for I\;J\;C, s1 from AOFA_000:sch 4(AA,AB,C);
    hence thesis;
  end;

theorem ThT4:
  for I being Element of A st I is_terminating_wrt g
  for i,n being Variable of g
  st (ex d being Function st d.b = 0 & d.n = 1 & d.i = 2) &
     for s holds g.(s,I).n = s.n & g.(s,I).i = s.i
  holds for-do(i:=t, i leq n, i+=1, I) is_terminating_wrt g
  proof
    set S = Funcs(X, INT);
    set T = Funcs(X, INT)\(b,0);
    let I be Element of A such that
A0: I is_terminating_wrt g;
    let i,n be Variable of g;
    given d being Function such that
00: d.b = 0 & d.n = 1 & d.i = 2;
    assume
01: for s holds g.(s,I).n = s.n & g.(s,I).i = s.i;
    let s;
    set P = for-do(i:=t, i leq n, i+=1, I);
02: g iteration_terminates_for I\; i+=1\; i leq n, g.(g.(s, i:=t), i leq n)
    by 00,01,ThT1;
    set Q = while(i leq n, I\; i+=1);
04: i+=1 is_terminating_wrt g & i leq n is_terminating_wrt g
    by AOFA_000:104; then
    I\; i+=1 is_terminating_wrt g by A0,AOFA_000:110; then
03: [g.(s, i:=t), Q] in TerminatingPrograms(A,S,T,g) by 02,04,AOFA_000:114;
    P = i:=t\; Q & [s, i:=t] in TerminatingPrograms(A,S,T,g)
    by AOFA_000:def 36;
    hence [s, P] in TerminatingPrograms(A,S,T,g) by 03,AOFA_000:def 35;
  end;

theorem
  for P being set
  for I being Element of A st I is_terminating_wrt g, P
  for i,n being Variable of g
  st (ex d being Function st d.b = 0 & d.n = 1 & d.i = 2) &
     (for s st s in P holds g.(s,I).n = s.n & g.(s,I).i = s.i) &
     P is_invariant_wrt i:=t, g & P is_invariant_wrt I, g &
     P is_invariant_wrt i leq n, g & P is_invariant_wrt i+=1, g
  holds for-do(i:=t, i leq n, i+=1, I) is_terminating_wrt g, P
  proof
    set Z = Funcs(X, INT);
    set T = Funcs(X, INT)\(b,0);
    let S be set;
    let I be Element of A; assume
00: I is_terminating_wrt g, S;
    let i,n be Variable of g;
    given d being Function such that
01: d.b = 0 & d.n = 1 & d.i = 2;
    assume that
02: for s st s in S holds g.(s,I).n = s.n & g.(s,I).i = s.i and
04: S is_invariant_wrt i:=t, g & S is_invariant_wrt I, g &
    S is_invariant_wrt i leq n, g & S is_invariant_wrt i+=1, g;
    let s; assume
    s in S; then
03: g.(s, i:=t) in S by 04,AOFA_000:def 39;
    set P = for-do(i:=t, i leq n, i+=1, I);
    set C = i leq n, J = I\; i+=1;
    set Q = while(C, J);
    for s being Element of Z st s in S holds
    g.(s,I).n = s.n & g.(s,I).i = s.i & g.(s, I) in S &
     g.(s, i leq n) in S & g.(s, i+=1) in S by 02,04,AOFA_000:def 39; then
06: g iteration_terminates_for J\; C, g.(g.(s, i:=t), C) by 01,03,ThT12;
07: i+=1 is_terminating_wrt g, S & C is_terminating_wrt g
    by AOFA_000:104,107; then
09: S is_invariant_wrt J, g & J is_terminating_wrt g, S
    by 00,04,AOFA_000:109,111; then
    for s st s in S & g.(g.(s, J), C) in T holds g.(s,J) in S
    by AOFA_000:def 39; then
08: [g.(s, i:=t), Q] in TerminatingPrograms(A,Z,T,g)
    by 03,04,06,07,09,AOFA_000:116;
    P = i:=t\; Q & [s, i:=t] in TerminatingPrograms(A,Z,T,g)
    by AOFA_000:def 36;
    hence [s, P] in TerminatingPrograms(A,Z,T,g) by 08,AOFA_000:def 35;
  end;

begin :: Examples

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

theorem
  for n,s,i being Variable of g
  st ex d being Function st d.n = 1 & d.s = 2 & d.i = 3 & d.b = 4
  holds s:=1\;for-do(i:=2, i leq n, i+=1, s*=i) is_terminating_wrt g
  proof
    set S = Funcs(X, INT);
    set T = S\(b,0);
    let n,s,i be Variable of g;
    given d being Function such that
00: d.n = 1 & d.s = 2 & d.i = 3 & d.b = 4;
D1: s <> i & s <> n & i <> n & b <> i & n <> b by 00;
    set t = .(2,A,g);
    let q be Element of S;
01: s*=i is_terminating_wrt g by AOFA_000:104;
02: [q,s:=1] in TerminatingPrograms(A,S,T,g) by AOFA_000:def 36;
03: for q be Element of S holds g.(q,s*=i).n = q.n & g.(q,s*=i).i = q.i
    by D1,Th213;
    ex d' being Function st d'.b = 0 & d'.n = 1 & d'.i = 2 by D1,Lem3; then
    for-do(i:=t, i leq n, i+=1, s*=i) is_terminating_wrt g by 01,03,ThT4; then
    [g.(q, s:=1) qua Element of S, for-do(i:=t, i leq n, i+=1, s*=i)]
    in TerminatingPrograms(A,S,T,g) by AOFA_000:def 37;
    hence thesis by 02,AOFA_000:def 35;
  end;

theorem
  for n,s,i being Variable of g
  st ex d being Function st d.n = 1 & d.s = 2 & d.i = 3 & d.b = 4
  for q being Element of Funcs(X, INT)
  for N being natural number st N = q.n
  holds g.(q, s:=1\;for-do(i:=2, i leq n, i+=1, s*=i)).s = N!
  proof set f = g;
    let n,s,i be Variable of f;
    given d being Function such that
A0: d.n = 1 & d.s = 2 & d.i = 3 & d.b = 4;
    let q be Element of Funcs(X, INT);
    let N be natural number;
    assume
A1: N = q.n;
    set S = Funcs(X,INT);
    set T = S\(b,0);
    reconsider q1 = f.(q, s:=1) as Element of S;
    reconsider q2 = f.(q1, i:=2) as Element of S;
    set I = s*=i;
    reconsider a = .(2,A,f) as INT-Expression of A,g;
    reconsider F = for-do(i:=a, i leq n, i+=1, I) as Element of A;
    defpred P[Element of S] means
    ex K being natural number st K = $1.i-1  & $1.s = K!;
F:  F = for-do(i:=a, i leq n, i+=1, I);
A2: s <> n & s <> i & s <> b by A0;
D:  n <> i & n <> b & i <> b by A0;
Q1: q1.n = q.n & q1.s = 1 & q.n+1-1 = q.n by A2,Th011;
Q2: q2.n = q1.n & q2.s = q1.s & q2.i = 2 & 2-1 = 1 by A2,D,Th011;
A:  P[f.(q1,i:=a)] by Q1,Q2,NEWTON:19;
C:  for q being Element of Funcs(X,INT) st P[q]
    holds f.(q,I).i = q.i & f.(q,I).n = q.n by A2,Th113;
B:  for q being Element of Funcs(X,INT) st P[q]
    holds P[f.(q,I\;i+=1)] & P[f.(q, i leq n)]
    proof
      let q be Element of Funcs(X,INT);
      given Ki being natural number such that
A3:   Ki = q.i-1 & q.s = Ki!;
      reconsider q3 = f.(q,I) as Element of S;
      reconsider q4 = f.(q3,i+=1) as Element of S;
      reconsider q' = f.(q, i leq n) as Element of S;
A4:   q4 = f.(q,I\;i+=1) by AOFA_000:def 29;
      q3.i = q.i & q3.s = q.s*q.i & q4.s = q3.s & q.i+1-1 = q.i &
      q.i-1+1 = q.i & q4.i = q3.i+1
      by A2,Th012,Th213; then
      Ki+1 = q4.i-1 & q4.s = (Ki+1)! by A3,NEWTON:21;
      hence P[f.(q,I\;i+=1) qua Element of S] by A4;
      q'.s = q.s & q'.i = q.i by A2,D,Th114;
      hence P[f.(q, i leq n) qua Element of S] by A3;
    end;
E:  P[f.(q1,F)] & (a.q1 <= q1.n implies f.(q1,F).i = q1.n+1) &
    (a.q1 > q1.n implies f.(q1,F).i = a.q1) & f.(q1,F).n = q1.n
    from ForToIteration(F,A,B,C,D);
M:  a.q1 = 2 by FUNCOP_1:13;
    thus f.(q, s:=1\;for-do(i:=2, i leq n, i+=1, s*=i)).s
    = f.(q1, F).s by AOFA_000:def 29
    .= N! by M,A1,Q1,E,NAT_1:27,NEWTON:18,19;
  end;

theorem
  for x,n,s,i being Variable of g
  st ex d being Function st d.x = 0 & d.n = 1 & d.s = 2 & d.i = 3 & d.b = 4
  holds s:=1\;for-do(i:=1, i leq n, i+=1, s*=x) is_terminating_wrt g
  proof
    set S = Funcs(X, INT);
    set T = S\(b,0);
    let x,n,s,i be Variable of g;
    given d being Function such that
00: d.x = 0 & d.n = 1 & d.s = 2 & d.i = 3 & d.b = 4;
D1: s <> i & s <> n & i <> n & b <> i & n <> b by 00;
    set t = .(1,A,g);
    let q be Element of S;
01: s*=x is_terminating_wrt g by AOFA_000:104;
02: [q,s:=1] in TerminatingPrograms(A,S,T,g) by AOFA_000:def 36;
03: for q be Element of S holds g.(q,s*=x).n = q.n & g.(q,s*=x).i = q.i
    by D1,Th213;
    ex d' being Function st d'.b = 0 & d'.n = 1 & d'.i = 2 by D1,Lem3; then
    for-do(i:=t, i leq n, i+=1, s*=x) is_terminating_wrt g by 01,03,ThT4; then
    [g.(q, s:=1) qua Element of S, for-do(i:=t, i leq n, i+=1, s*=x)]
    in TerminatingPrograms(A,S,T,g) by AOFA_000:def 37;
    hence thesis by 02,AOFA_000:def 35;
  end;

theorem
  for x,n,s,i being Variable of g
  st ex d being Function st d.x = 0 & d.n = 1 & d.s = 2 & d.i = 3 & d.b = 4
  for q being Element of Funcs(X, INT)
  for N being natural number st N = q.n
  holds g.(q, s:=1\;for-do(i:=1, i leq n, i+=1, s*=x)).s = (q.x)|^N
  proof set f = g;
    let x,n,s,i be Variable of f;
    given d being Function such that
A0: d.x = 0 & d.n = 1 & d.s = 2 & d.i = 3 & d.b = 4;
    let q be Element of Funcs(X, INT);
    let N be natural number;
    assume
A1: N = q.n;
    set S = Funcs(X,INT);
    set T = S\(b,0);
    set q0 = q;
    reconsider q1 = f.(q, s:=1) as Element of S;
    reconsider q2 = f.(q1, i:=1) as Element of S;
    set I = s*=x;
    reconsider a = .(1,A,f) as INT-Expression of A,g;
    reconsider F = for-do(i:=a, i leq n, i+=1, I) as Element of A;
    defpred P[Element of S] means
    ex K being natural number st K = $1.i-1  & $1.s = (q.x)|^K & $1.x = q.x;
F:  F = for-do(i:=a, i leq n, i+=1, I);
A2: i <> x & b <> x & s <> x & s <> n & s <> i & s <> b by A0;
D:  n <> i & n <> b & i <> b by A0;
Q1: q1.n = q.n & q1.s = 1 & q.n+1-1 = q.n & q1.x = q.x by A2,Th011;
Q2: q2.n = q1.n & q2.s = q1.s & q2.i = 1 & q2.x = q1. x & 1-1 = 0
    by A2,D,Th011;
    (q.x)|^0 = 1 by NEWTON:9; then
A:  P[f.(q1,i:=a)] by Q1,Q2;
C:  for q being Element of Funcs(X,INT) st P[q]
    holds f.(q,I).i = q.i & f.(q,I).n = q.n by A2,Th113;
B:  for q being Element of Funcs(X,INT) st P[q]
    holds P[f.(q,I\;i+=1)] & P[f.(q, i leq n)]
    proof
      let q be Element of Funcs(X,INT);
      given Ki being natural number such that
A3:   Ki = q.i-1 & q.s = (q0.x)|^Ki & q.x = q0.x;
      reconsider q3 = f.(q,I) as Element of S;
      reconsider q4 = f.(q3,i+=1) as Element of S;
      reconsider q' = f.(q, i leq n) as Element of S;
A4:   q4 = f.(q,I\;i+=1) by AOFA_000:def 29;
A5:   q3.i = q.i & q3.s = q.s*q.x & q4.s = q3.s & q.i+1-1 = q.i &
      q3.x = q.x & q4.x = q3.x & q.i-1+1 = q.i & q4.i = q3.i+1
      by A2,Th012,Th213; then
      Ki+1 = q4.i-1 & q4.s = (q0.x)|^(Ki+1) by A3,NEWTON:11;
      hence P[f.(q,I\;i+=1) qua Element of S] by A3,A4,A5;
      q'.s = q.s & q'.i = q.i & q'.x = q.x by A2,D,Th114;
      hence P[f.(q, i leq n) qua Element of S] by A3;
    end;
E:  P[f.(q1,F)] & (a.q1 <= q1.n implies f.(q1,F).i = q1.n+1) &
    (a.q1 > q1.n implies f.(q1,F).i = a.q1) & f.(q1,F).n = q1.n
    from ForToIteration(F,A,B,C,D);
N:  N = 0 or N >= 1 by NAT_1:26;
    thus f.(q, s:=1\;for-do(i:=1, i leq n, i+=1, s*=x)).s
    = f.(q1, F).s by AOFA_000:def 29
    .= (q.x)|^N by A1,Q1,E,N,FUNCOP_1:13;
  end;

theorem
  for n,x,y,z,i being Variable of g
  st ex d being Function st
    d.b = 0 & d.n = 1 & d.x = 2 & d.y = 3 & d.z = 4 & d.i = 5
  holds x:=0\;y:=1\;for-do(i:=1, i leq n, i+=1, z:=x\;x:=y\;y+=z)
  is_terminating_wrt g
  proof
    set S = Funcs(X, INT);
    set T = S\(b,0);
    let n,x,y,z,i be Variable of g;
    given d being Function such that
00: d.b = 0 & d.n = 1 & d.x = 2 & d.y = 3 & d.z = 4 & d.i = 5;
D1: i <> n & b <> i & n <> b by 00;
D2: i <> x & i <> y & i <> z & n <> x & n <> y & n <> z by 00;
    let s;
    set s2 = g.(s, x:=0\;y:=1);
    set I1 = z:=x, I2 = x:=y, I3 = y+=z;
    set I = z:=x\;x:=y\;y+=z;
01: I is_terminating_wrt g by AOFA_000:104;
02: [s, x:=0\;y:=1] in TerminatingPrograms(A,S,T,g) by AOFA_000:def 36;
03: for q be Element of S holds g.(q,I).n = q.n & g.(q,I).i = q.i
    proof
      let q be Element of S;
      thus g.(q,I).n
         = g.(g.(q,I1\;I2),I3).n by AOFA_000:def 29
        .= g.(q,I1\;I2).n by D2,Th212
        .= g.(g.(q,I1),I2).n by AOFA_000:def 29
        .= g.(q,I1).n by D2,Th211
        .= q.n by D2,Th211;
      thus g.(q,I).i
         = g.(g.(q,I1\;I2),I3).i by AOFA_000:def 29
        .= g.(q,I1\;I2).i by D2,Th212
        .= g.(g.(q,I1),I2).i by AOFA_000:def 29
        .= g.(q,I1).i by D2,Th211
        .= q.i by D2,Th211;
    end;
    ex d' being Function st d'.b = 0 & d'.n = 1 & d'.i = 2 by D1,Lem3; then
    for-do(i:=1, i leq n, i+=1, z:=x\;x:=y\;y+=z) is_terminating_wrt g
    by 01,03,ThT4; then
    [s2, for-do(i:=1, i leq n, i+=1, z:=x\;x:=y\;y+=z)] in
    TerminatingPrograms(A,S,T,g) by AOFA_000:def 37;
    hence [s,x:=0\;y:=1\;for-do(i:=1, i leq n, i+=1, z:=x\;x:=y\;y+=z)]
    in TerminatingPrograms(A,S,T,g) by 02,AOFA_000:def 35;
  end;

theorem
  for n,x,y,z,i being Variable of g
  st ex d being Function st
  d.b = 0 & d.n = 1 & d.x = 2 & d.y = 3 & d.z = 4 & d.i = 5
  for s being Element of Funcs(X, INT)
  for N being Element of NAT st N = s.n holds
  g.(s, x:=0\;y:=1\;for-do(i:=1, i leq n, i+=1, z:=x\;x:=y\;y+=z)).x = Fib N
  proof
    set S = Funcs(X, INT);
    set T = S\(b,0);
    let n,x,y,z,i be Variable of g;
    given d being Function such that
A0: d.b = 0 & d.n = 1 & d.x = 2 & d.y = 3 & d.z = 4 & d.i = 5;
    let s be Element of Funcs(X, INT);
    let N be Element of NAT;
    assume
A1: N = s.n;
    reconsider s1 = g.(s, x:=0) as Element of S;
    reconsider s2 = g.(s1, y:=1) as Element of S;
    reconsider s3 = g.(s2, for-do(i:=1, i leq n, i+=1, z:=x\;x:=y\;y+=z))
    as Element of S;
    reconsider s4 = g.(s2, i:=1) as Element of S;
    set I = z:=x\;x:=y\;y+=z;
    reconsider a = .(1,A,g) as INT-Expression of A,g;
    reconsider F = for-do(i:=a, i leq n, i+=1, I) as Element of A;
    g.(s, x:=0\;y:=1) = s2 by AOFA_000:def 29; then
S0: g.(s, x:=0\;y:=1\;F) = s3 by AOFA_000:def 29;
D0: n <> x & i <> x & n <> y & i <> y & x <> y & i <> n & n <> z & i <> z &
    x <> z & y <> z by A0; then
S1: s1.n = s.n & s1.x = 0 by Th011;
S2: s2.n = s1.n & s2.y = 1 & s2.x = s1.x by D0,Th011;
S3: s4.n = s2.n & s4.y = s2.y & s4.x = s2.x & s4.i = 1 by D0,Th011;
    defpred P[Element of S] means
    ex N being Element of NAT st N = $1.i-1 & $1.x = Fib N & $1.y = Fib(N+1);
F:  F = for-do(i:=a,i leq n,i+=1,I);
    1-1 = 0 & (0 qua Element of NAT)+1 = 1; then
A:  P[g.(s2,i:=a)] by S1,S2,S3,PRE_FF:1;
Si: now let s be Element of S;
      reconsider s1 = g.(s,z:=x) as Element of S;
      reconsider s2 = g.(s1,x:=y) as Element of S;
      reconsider s3 = g.(s2,y+=z) as Element of S;
R1:   s1.n = s.n & s1.x = s.x & s1.y = s.y & s1.z = s.x & s1.i = s.i
      by D0,Th211;
R2:   s2.n = s1.n & s2.x = s1.y & s2.y = s1.y & s2.z = s1.z & s2.i = s1.i
      by D0,Th211;
R4:   g.(s,I) = g.(g.(s, z:=x\;x:=y), y+=z) by AOFA_000:def 29
      .= s3 by AOFA_000:def 29;
      thus g.(s,I).i = s.i & g.(s,I).n = s.n & g.(s,I).x = s.y &
      g.(s,I).y = s.x+s.y by R1,R2,D0,R4,Th212;
    end;
B:  for s being Element of Funcs(X,INT) st P[s]
    holds P[g.(s,I\;i+=1)] & P[g.(s, i leq n)]
    proof
      let s be Element of Funcs(X,INT);
      given N being Element of NAT such that
Q0:   N = s.i-1 & s.x = Fib N & s.y = Fib(N+1);
      reconsider s1 = g.(s,I) as Element of S;
      reconsider s2 = g.(s1,i+=1) as Element of S;
Q1:   s1.x = s.y & s1.y = s.x+s.y & s1.i = s.i by Si;
Q2:   s2.x = s1.x & s2.y = s1.y & s2.i = s1.i+1 by D0,Th012;
      thus P[g.(s,I\;i+=1) qua Element of S]
      proof take N1 = N+1;
        g.(s,I\;i+=1) = s2 & N1-1 = N by AOFA_000:def 29;
        hence thesis by Q0,Q1,Q2,PRE_FF:1;
      end;
      take N;
      thus thesis by Q0,A0,Th114;
    end;
C:  for s being Element of Funcs(X,INT) st P[s]
    holds g.(s,I).i = s.i & g.(s,I).n = s.n by Si;
D:  n <> i & n <> b & i <> b by A0;
E:  P[g.(s2,F)] & (a.s2 <= s2.n implies g.(s2,F).i = s2.n+1) &
    (a.s2 > s2.n implies g.(s2,F).i = a.s2) & g.(s2,F).n = s2.n
    from ForToIteration(F,A,B,C,D);
E2: 0 <= N & N <= 0 or N >= (0 qua Element of NAT)+1 by NAT_1:13;
    a.s2 = 1 by FUNCOP_1:13;
    hence thesis by A1,S0,D0,Th011,S2,E,E2,XXREAL_0:1;
  end;

LemEAterm:
  for x,y,z being Variable of g
  st ex d being Function st d.b = 0 & d.x = 1 & d.y = 2 & d.z = 3
  for s being Element of Funcs(X, INT) holds
    g.(s, z:=x\;z%=y\;x:=y\;y:=z).x = s.y &
    g.(s, z:=x\;z%=y\;x:=y\;y:=z).y = s.x mod s.y &
  for n,m being Element of NAT st n = s.x & m = s.y & n > m &
     (s in Funcs(X, INT)\(b,0) iff m > 0)
  holds
  g iteration_terminates_for z:=x\;z%=y\;x:=y\;y:=z\;y gt 0, s
  proof set h = g;
    set S = Funcs(X, INT);
    set T = S\(b,0);
    let x,y,z be Variable of h;
    given d being Function such that
A0: d.b = 0 & d.x = 1 & d.y = 2 & d.z = 3;
D1: x <> y & y <> z & z <> x by A0;
    set I = z:=x\;z%=y\;x:=y\;y:=z;
    set C = y gt 0;
IT: now let s be Element of S;
      reconsider s1 = h.(s, z:=x) as Element of S;
      reconsider s2 = h.(s1, z%=y) as Element of S;
      reconsider s3 = h.(s2, x:=y) as Element of S;
      reconsider s4 = h.(s3, y:=z) as Element of S;
00:   h.(s, I) = h.(h.(s, z:=x\;z%=y\;x:=y), y:=z) by AOFA_000:def 29
      .= h.(h.(h.(s, z:=x\;z%=y), x:=y), y:=z) by AOFA_000:def 29
      .= s4 by AOFA_000:def 29;
01:   s1.x = s.x & s1.y = s.y & s1.z = s.x by D1,Th211;
02:   s2.x = s1.x & s2.y = s1.y & s2.z = s1.z mod s1.y by D1,Th216;
03:   s3.x = s2.y & s3.y = s2.y & s3.z = s2.z by D1,Th211;
      thus h.(s, I).x = s.y & h.(s, I).y = s.x mod s.y by 00,01,02,03,D1,Th211;
    end;
    let s be Element of Funcs(X, INT);
    thus g.(s, I).x = s.y & h.(s, I).y = s.x mod s.y by IT;
    let n,m be Element of NAT; assume
A1: n = s.x & m = s.y & n > m;
    reconsider s1 = h.(s, C) as Element of S;
    reconsider fin = h.(s, while(C,I)) as Element of S;
    defpred R[Element of S] means $1.y > 0;
    deffunc F(Element of S) = In($1.y, NAT);
    defpred P[Element of S] means
    n hcf m divides $1.x & n hcf m divides $1.y & $1.x > $1.y & $1.y >= 0;
    defpred Q[Element of S] means
    fin.x divides $1.x & fin.x divides $1.y;
    assume s in T iff m > 0; then
AB: s in T iff R[s] by A1;
C:  for s being Element of S st R[s]
    holds (R[h.(s,I\;C) qua Element of S] iff h.(s,I\;C) in T) &
    F(h.(s,I\;C) qua Element of S) < F(s)
    proof
      let s be Element of S; assume
00:   s.y > 0;
      reconsider s' = h.(s, I) as Element of S;
      reconsider s'' = h.(s', C) as Element of S;
01:   h.(s,I\;C) = s'' by AOFA_000:def 29;
02:   s''.x = s'.x & s''.y = s'.y & (s'.y > 0 implies s''.b = 1) &
      (s'.y <= 0 implies s''.b = 0) by A0,Th015;
      hence (R[h.(s,I\;C) qua Element of S] iff h.(s,I\;C) in T) by 01,LemTS;
      s'.y = s.x mod s.y by IT; then
03:   0 <= s'.y & s'.y < s.y by 00,NEWTON:78,79; then
      F(s'') = s'.y & F(s) = s.y by 02,FUNCT_7:def 1,INT_1:16;
      hence F(h.(s,I\;C) qua Element of S) < F(s) by 03,AOFA_000:def 29;
    end;
    h iteration_terminates_for I\;C, s from AOFA_000:sch 3(AB,C);
    hence h iteration_terminates_for I\;C, s;
  end;

theorem :: Termination of Euclid algorithm
  for x,y,z being Variable of g
  st ex d being Function st d.b = 0 & d.x = 1 & d.y = 2 & d.z = 3
  holds while(y gt 0, z:=x\;z%=y\;x:=y\;y:=z) is_terminating_wrt g,
  {s: s.x > s.y & s.y >= 0}
  proof
    set S = Funcs(X, INT);
    set T = S\(b,0);
    let x,y,z be Variable of g;
    set P = {s: s.x > s.y & s.y >= 0};
    given d being Function such that
00: d.b = 0 & d.x = 1 & d.y = 2 & d.z = 3;
    set C = y gt 0, I = z:=x\;z%=y\;x:=y\;y:=z;
01: P is_invariant_wrt C,g
    proof
      let s; assume s in P; then
A0:   ex s' st s' = s & s'.x > s'.y & s'.y >= 0;
      set s1 = g.(s,C);
      s1.x = s.x & s1.y = s.y by 00,Th015;
      hence thesis by A0;
    end;
02: C is_terminating_wrt g & I is_terminating_wrt g,P by AOFA_000:104,107;
03: now
      let s; assume s in P; then
      ex s' st s' = s & s'.x > s'.y & s'.y >= 0; then
      reconsider n = s.x, m = s.y as Element of NAT by INT_1:16;
      assume g.(g.(s,I),C) in T; then
A2:   g.(g.(s,I),C).b <> 0 & g.(s,I).y = s.x mod s.y & g.(s,I).x = s.y
      by 00,LemTS,LemEAterm; then
A1:   g.(s,I).y > 0 by Th015; then
      m <> 0 by A2,INT_1:def 8; then
      m > 0; then
      g.(s,I).x > g.(s,I).y by A2,NEWTON:79;
      hence g.(s,I) in P by A1;
    end;
    now let s; set s1 = g.(s,C);
      assume g.(s,C) in P; then
A0:   ex s' st s' = g.(s,C) & s'.x > s'.y & s'.y >= 0; then
      reconsider n = s1.x, m = s1.y as Element of NAT by INT_1:16;
      s1.x = s.x & s1.y = s.y & (s.y > 0 implies s1.b = 1) &
      (s.y <= 0 implies s1.b = 0) by 00,Th015; then
      n > m & (s1 in T iff m > 0) by A0,LemTS;
      hence g iteration_terminates_for I\;C, g.(s,C) by 00,LemEAterm;
    end;
    hence while(y gt 0, z:=x\;z%=y\;x:=y\;y:=z) is_terminating_wrt g, P
    by 01,02,03,AOFA_000:118;
  end;

theorem :: Correctness of Euclid algorithm
  for x,y,z being Variable of g
  st ex d being Function st d.b = 0 & d.x = 1 & d.y = 2 & d.z = 3
  for s being Element of Funcs(X, INT)
  for n,m being Element of NAT st n = s.x & m = s.y & n > m holds
  g.(s, while(y gt 0, z:=x\;z%=y\;x:=y\;y:=z)).x = n hcf m
  proof set h = g;
    set S = Funcs(X, INT);
    set T = S\(b,0);
    let x,y,z be Variable of h;
    given d being Function such that
A0: d.b = 0 & d.x = 1 & d.y = 2 & d.z = 3;
    let s be Element of Funcs(X, INT);
    let n,m be Element of NAT; assume
A1: n = s.x & m = s.y & n > m;
    set I = z:=x\;z%=y\;x:=y\;y:=z;
    set C = y gt 0;
    reconsider s1 = h.(s, C) as Element of S;
    reconsider fin = h.(s, while(C,I)) as Element of S;
S1: s1.x = s.x & s1.y = s.y & (s.y > 0 implies s1.b = 1) &
    (s.y <= 0 implies s1.b = 0) by A0,Th015;
    defpred R[Element of S] means $1.y > 0;
    deffunc F(Element of S) = In($1.y, NAT);
    defpred P[Element of S] means
    n hcf m divides $1.x & n hcf m divides $1.y & $1.x > $1.y & $1.y >= 0;
    defpred Q[Element of S] means
    fin.x divides $1.x & fin.x divides $1.y;
AB: s1 in T iff m > 0 by A1,S1,LemTS;
    s1.x = s.x & s1.y = s.y by A0,Th015; then
II: h iteration_terminates_for I\;C, h.(s,C) by AB,A0,A1,LemEAterm;
IA: P[s] by A1,NAT_D:def 5;
ID: for s being Element of S st P[s] & s in T & R[s]
    holds P[h.(s,I)]
    proof
      let s be Element of S; assume
00:   P[s];
      reconsider n' = s.x, m' = s.y as Element of NAT by 00,INT_1:16;
      assume
01:   s in T & R[s];
      reconsider s'' = h.(s, I) as Element of S;
04:   s''.x = s.y & s''.y = s.x mod s.y by A0,LemEAterm;
      n hcf m divides n' mod m' & s.x mod s.y = n' mod m'
      by 00,NAT_D:11;
      hence P[h.(s,I)] by 01,00,04,NEWTON:79;
    end;
IE: for s being Element of S st P[s] holds P[h.(s,C) qua Element of S] &
    (h.(s,C) in T iff R[h.(s,C) qua Element of S])
    proof
      let s be Element of S; assume
01:   P[s];
      reconsider s' = h.(s,C) as Element of S;
02:   s'.x = s.x & s'.y = s.y & (s.y > 0 implies s'.b = 1) &
      (s.y <= 0 implies s'.b = 0) by A0,Th015;
      hence P[h.(s,C) qua Element of S] by 01;
      thus thesis by 02,LemTS;
    end;
08: P[h.(s,while(C,I)) qua Element of S] &
    not R[h.(s,while(C,I)) qua Element of S]
    from AOFA_000:sch 5(IA,II,ID,IE); then
    n hcf m divides fin.x & fin.x > fin.y & fin.y = 0; then
cA: Q[h.(s,while(C,I)) qua Element of S] by INT_2:16;
cD: for s being Element of S st Q[h.(h.(s,C),I) qua Element of S] &
    h.(s,C) in T holds Q[h.(s,C) qua Element of S]
    proof
      let s be Element of S; assume
00:   Q[h.(h.(s,C),I) qua Element of S];
      assume
01:   h.(s,C) in T;
      reconsider s1 = h.(s,C) as Element of S;
      reconsider s2 = h.(s1,I) as Element of S;
02:   s1.x = s.x & s1.y = s.y & (s.y > 0 implies s1.b = 1) &
      (s.y <= 0 implies s1.b = 0) by A0,Th015;
03:   s2.x = s1.y & s2.y = s1.x mod s1.y by A0,LemEAterm;
      s.x = (s.x div s.y)*(s2.x)+s2.y*1 by 01,02,03,LemTS,NEWTON:80;
      hence Q[h.(s,C) qua Element of S] by 00,02,A0,LemEAterm,WSIERP_1:10;
    end;
cE: for s being Element of S st Q[h.(s,C) qua Element of S] holds Q[s]
    by A0,Th015;
    Q[s] from AOFA_000:sch 6(cA,II,cD,cE); then
    fin.x divides n hcf m by A1,INT_2:33; then
    fin.x = n hcf m or fin.x = -(n hcf m) by 08,INT_2:15;
    hence h.(s, while(y gt 0, z:=x\;z%=y\;x:=y\;y:=z)).x = n hcf m by 08;
  end;

LemEA2term:
  for x,y,z being Variable of g
  st ex d being Function st d.b = 0 & d.x = 1 & d.y = 2 & d.z = 3
  for s being Element of Funcs(X, INT) holds
    g.(s, z:=(.x-.y)\; if-then(z lt 0, z*=-1)\; x:=y\; y:=z).x = s.y &
    g.(s, z:=(.x-.y)\; if-then(z lt 0, z*=-1)\; x:=y\; y:=z).y = abs(s.x-s.y) &
  for n,m being Element of NAT st n = s.x & m = s.y &
     (s in Funcs(X, INT)\(b,0) iff m > 0)
  holds g iteration_terminates_for z:=(.x-.y)\;
  if-then(z lt 0, z*=-1)\; x:=y\; y:=z\; y gt 0, s
  proof
    set S = Funcs(X, INT);
    set T = S\(b,0);
    let x,y,z be Variable of g;
    given d being Function such that
A0: d.b = 0 & d.x = 1 & d.y = 2 & d.z = 3;
D1: x <> y & y <> z & z <> x by A0;
Z0: g complies_with_if_wrt T & g complies_with_while_wrt T by AOFA_000:def 32;
    set J = if-then(z lt 0, z*=-1);
    set I = z:=(.x-.y)\; J\; x:=y\; y:=z;
    set C = y gt 0;
IT: now let s be Element of S;
      set s1 = g.(s, z:=(.x-.y));
      set s2 = g.(s1, z lt 0);
      set q = g.(s1, J);
      set qz = g.(s2, z*=-1);
      (s2.b = 0 implies s2 nin T) & (s2.b = 1 implies s2 in T) by LemTS; then
Q5:   (s2.b = 0 implies q = s2) & (s2.b = 1 implies q = qz)
      by Z0,AOFA_000:def 30,80;
02:   s2.x = s1.x & s2.y = s1.y & s2.z = s1.z by A0,Th015;
04:   (s1.z < 0 implies s2.b = 1) & (s1.z >= 0 implies s2.b = 0)
      by Th015;
05:   qz.x = s2.x & qz.y = s2.y & qz.z = (s2.z)*(-1) & (s2.z)*(-1) = -(s2.z)
      by D1,Th013;
      set s3 = g.(q, x:=y);
      set s4 = g.(s3, y:=z);
00:   g.(s, I) = g.(g.(s, z:=(.x-.y)\; J\; x:=y), y:=z) by AOFA_000:def 29
      .= g.(g.(g.(s, z:=(.x-.y)\; J), x:=y), y:=z) by AOFA_000:def 29
      .= s4 by AOFA_000:def 29;
      (.x-.y).s = ((.x).s)-((.y).s) & (.x).s = s.x & (.y).s = s.y
      by ThE1,DEFminus3; then
01:   s1.x = s.x & s1.y = s.y & s1.z = (s.x)-(s.y) by D1,Th111;
03:   s3.x = q.y & s3.y = q.y & s3.z = q.z by D1,Th211;
      s4.x = s3.x & s4.y = s3.z by D1,Th211;
      hence g.(s, I).x = s.y & g.(s, I).y = abs(s.x-s.y)
      by 00,01,02,03,04,05,Q5,ABSVALUE:def 1;
    end;
    let s be Element of Funcs(X, INT);
    thus g.(s, I).x = s.y & g.(s, I).y = abs(s.x-s.y) by IT;
    let n,m be Element of NAT; assume
A1: n = s.x & m = s.y;
    reconsider s1 = g.(s, C) as Element of S;
    reconsider fin = g.(s, while(C,I)) as Element of S;
    defpred R[Element of S] means $1.x >= 0 & $1.y > 0;
    deffunc F(Element of S) =
       IFEQ($1.y,0,0,
       IFEQ($1.x,0,2,
       IFEQ($1.x,$1.y,1,
       In(max(2*$1.x,2*$1.y+1), NAT))));
    defpred P[Element of S] means
    n hcf m divides $1.x & n hcf m divides $1.y & $1.x > 0 & $1.y >= 0 &
    for c being Nat st c divides $1.x & c divides $1.y holds c divides n hcf m;
    assume s in T iff m > 0; then
AB: s in T iff R[s] by A1;
C:  for s being Element of S st R[s]
    holds (R[g.(s,I\;C) qua Element of S] iff g.(s,I\;C) in T) &
    F(g.(s,I\;C) qua Element of S) < F(s)
    proof
      let s be Element of S; assume
00:   s.x >= 0 & s.y > 0;
      reconsider s' = g.(s, I) as Element of S;
      reconsider s'' = g.(s', C) as Element of S;
01:   g.(s,I\;C) = s'' by AOFA_000:def 29;
02:   s''.x = s'.x & s''.y = s'.y & (s'.y > 0 implies s''.b = 1) &
      (s'.y <= 0 implies s''.b = 0) by A0,Th015;
04:   s'.y = abs(s.x-s.y) & s'.x = s.y by IT;
      thus R[g.(s,I\;C) qua Element of S] iff g.(s,I\;C) in T
      by 00,01,02,LemTS,IT;
      reconsider nx = s.x, ny = s.y, nn = s''.y as Element of NAT
      by 00,04,A0,Th015,INT_1:16;
      (max(2*ny,2*nn+1) = 2*ny or max(2*ny,2*nn+1) = 2*nn+1)
      by XXREAL_0:16; then
03:   F(s'') = IFEQ(nn,0,0, IFEQ(ny,0,2, IFEQ(ny,nn,1,max(2*ny,2*nn+1))))
      by 02,04,FUNCT_7:def 1;
      (max(2*nx,2*ny+1) = 2*nx or max(2*nx,2*ny+1) = 2*ny+1)
      by XXREAL_0:16; then
03':  F(s) = IFEQ(ny,0,0, IFEQ(nx,0,2, IFEQ(nx,ny,1,max(2*nx,2*ny+1))))
      by FUNCT_7:def 1
      .= IFEQ(nx,0,2, IFEQ(nx,ny,1,max(2*nx,2*ny+1))) by 00,FUNCOP_1:def 8;
      2*ny+1 > 2*ny by NAT_1:13; then
05:   max(2*nx,2*ny+1) > 2*ny by XXREAL_0:30;
      per cases by XXREAL_0:1;
      suppose
07:     nx = ny; then
06:     nx-ny = 0 & F(s) = IFEQ(nx,ny,1,max(2*nx,2*ny+1)) &
        IFEQ(nx,ny,1,max(2*nx,2*ny+1)) = 1
        by 00,03',FUNCOP_1:def 8;
        nn = 0 by 02,04,07,ABSVALUE:7;
        hence F(g.(s,I\;C) qua Element of S) < F(s) by 01,06,FUNCOP_1:def 8;
      end;
      suppose nx > ny; then
06:     nx-ny > 0 & nx > 0 & IFEQ(nx,ny,1,max(2*nx,2*ny+1)) = max(2*nx,2*ny+1)
        by XREAL_1:52,FUNCOP_1:def 8; then
07:     nn = nx-ny & F(s) = max(2*nx,2*ny+1)
        by 03',FUNCOP_1:def 8; then
        F(s'') = IFEQ(ny,0,2, IFEQ(ny,nn,1,max(2*ny,2*nn+1)))
        by 03,06,FUNCOP_1:def 8
        .= IFEQ(ny,nn,1,max(2*ny,2*nn+1)) by 00,FUNCOP_1:def 8; then
08:     (ny = nn implies F(s'') = 1) &
        (ny <> nn implies F(s'') = max(2*ny,2*nn+1)) by FUNCOP_1:def 8;
        nn < nx by 00,07,XREAL_1:46; then
        nn+1 <= nx by NAT_1:13; then
        2*(nn+1) <= 2*nx & 2*(nn+1) = 2*nn+2*1 & 2*nn+2 = 2*nn+1+1
        by XREAL_1:66; then
        2*nn+1 < 2*nx by NAT_1:13; then
        1 <= 2*nn+1 & 2*nn+1 < F(s) by 07,XXREAL_0:30,NAT_1:11;
        hence F(g.(s,I\;C) qua Element of S) < F(s)
        by 01,08,05,07,XXREAL_0:29,2;
      end;
      suppose
0A:     nx < ny & nx > 0; then
        nx-ny < 0 by XREAL_1:51; then
        nn = -(nx-ny) & -(nx-ny) = ny-nx
        by 04,02,ABSVALUE:def 1; then
0D:     nn < ny & nn > 0 by 0A,XREAL_1:46,52; then
        2*nn < 2*ny by XREAL_1:70; then
        2*nn+1 < 2*ny+1 by XREAL_1:8; then
0B:     2*nn+1 < max(2*nx,2*ny+1) by XXREAL_0:30;
0C:     F(s) = IFEQ(nx,ny,1,max(2*nx,2*ny+1)) by 03',0A,FUNCOP_1:def 8
        .= max(2*nx,2*ny+1) by 0A,FUNCOP_1:def 8;
        F(s'') = IFEQ(ny,0,2, IFEQ(ny,nn,1,max(2*ny,2*nn+1)))
        by 03,0D,FUNCOP_1:def 8
        .= IFEQ(ny,nn,1,max(2*ny,2*nn+1)) by 00,FUNCOP_1:def 8
        .= max(2*ny,2*nn+1) by 0D,FUNCOP_1:def 8;
        hence F(g.(s,I\;C) qua Element of S) < F(s) by 01,05,0B,0C,XXREAL_0:29;
      end;
      suppose
09:     nx = 0; then
0A:     F(s) = 2 by 03',FUNCOP_1:def 8;
        nx-ny < 0 by 00,09,XREAL_1:51; then
0B:     nn = -(nx-ny) by 04,02,ABSVALUE:def 1 .= ny by 09; then
        F(s'') = IFEQ(ny,0,2, IFEQ(ny,nn,1,max(2*ny,2*nn+1)))
        by 00,03,FUNCOP_1:def 8
        .= IFEQ(ny,nn,1,max(2*ny,2*nn+1)) by 00,FUNCOP_1:def 8
        .= 1 by 0B,FUNCOP_1:def 8;
        hence F(g.(s,I\;C) qua Element of S) < F(s) by 01,0A;
      end;
    end;
    g iteration_terminates_for I\;C, s from AOFA_000:sch 3(AB,C);
    hence g iteration_terminates_for I\;C, s;
  end;

theorem :: Termination of Euclid algorithm 2
  for x,y,z being Variable of g
  st ex d being Function st d.b = 0 & d.x = 1 & d.y = 2 & d.z = 3
  holds while(y gt 0, z:=(.x-.y)\; if-then(z lt 0, z*=-1)\; x:=y\; y:=z)
   is_terminating_wrt g, {s: s.x >= 0 & s.y >= 0}
  proof
    set S = Funcs(X, INT);
    set T = S\(b,0);
    let x,y,z be Variable of g;
    set P = {s: s.x >= 0 & s.y >= 0};
    given d being Function such that
00: d.b = 0 & d.x = 1 & d.y = 2 & d.z = 3;
    set C = y gt 0, I = z:=(.x-.y)\; if-then(z lt 0, z*=-1)\; x:=y\; y:=z;
01: P is_invariant_wrt C,g
    proof
      let s; assume s in P; then
A0:   ex s' st s' = s & s'.x >= 0 & s'.y >= 0;
      set s1 = g.(s,C);
      s1.x = s.x & s1.y = s.y by 00,Th015;
      hence thesis by A0;
    end;
02: C is_terminating_wrt g & I is_terminating_wrt g,P by AOFA_000:104,107;
03: now
      let s; assume s in P; then
      ex s' st s' = s & s'.x >= 0 & s'.y >= 0; then
      reconsider n = s.x, m = s.y as Element of NAT by INT_1:16;
      assume g.(g.(s,I),C) in T; then
      g.(g.(s,I),C).b <> 0 & g.(s,I).y = abs(s.x-s.y) & g.(s,I).x = m
      by 00,LemTS,LemEA2term;
      hence g.(s,I) in P;
    end;
    now let s; set s1 = g.(s,C);
      assume g.(s,C) in P; then
      ex s' st s' = g.(s,C) & s'.x >= 0 & s'.y >= 0; then
      reconsider n = s1.x, m = s1.y as Element of NAT by INT_1:16;
      s1.x = s.x & s1.y = s.y & (s.y > 0 implies s1.b = 1) &
      (s.y <= 0 implies s1.b = 0) by 00,Th015; then
      (s1 in T iff m > 0) & n = n by LemTS;
      hence g iteration_terminates_for I\;C, g.(s,C) by 00,LemEA2term;
    end;
    hence while(y gt 0, z:=(.x-.y)\; if-then(z lt 0, z*=-1)\; x:=y\; y:=z)
    is_terminating_wrt g, P by 01,02,03,AOFA_000:118;
  end;

theorem :: Euclid algorithm 2
  for x,y,z being Variable of g
  st ex d being Function st d.b = 0 & d.x = 1 & d.y = 2 & d.z = 3
  for s being Element of Funcs(X, INT)
  for n,m being Element of NAT st n = s.x & m = s.y & n > 0 holds
  g.(s, while(y gt 0,
          z:=(.x-.y)\; if-then(z lt 0, z*=-1)\; x:=y\; y:=z
        )
     ).x = n hcf m
  proof set h = g;
    set S = Funcs(X, INT);
    set T = S\(b,0);
Z0: h complies_with_if_wrt T & h complies_with_while_wrt T by AOFA_000:def 32;
    let x,y,z be Variable of h;
    given d being Function such that
A0: d.b = 0 & d.x = 1 & d.y = 2 & d.z = 3;
    let s be Element of Funcs(X, INT);
    let n,m be Element of NAT; assume
A1: n = s.x & m = s.y & n > 0;
    set J = if-then(z lt 0, z*=-1);
    set I = z:=(.x-.y)\; J\; x:=y\; y:=z;
    set C = y gt 0;
    reconsider s1 = h.(s, C) as Element of S;
    reconsider fin = h.(s, while(C,I)) as Element of S;
D1: x <> y & y <> z & z <> x by A0;
S1: s1.x = s.x & s1.y = s.y & (s.y > 0 implies s1.b = 1) &
    (s.y <= 0 implies s1.b = 0) by A0,Th015;
    defpred R[Element of S] means $1.x > 0 & $1.y > 0;
    deffunc F(Element of S) = In(max(2*$1.x,2*$1.y+1), NAT);
    defpred P[Element of S] means
    n hcf m divides $1.x & n hcf m divides $1.y & $1.x > 0 & $1.y >= 0 &
    for c being Nat st c divides $1.x & c divides $1.y holds c divides n hcf m;
AB: s1 in T iff R[s1] by A1,S1,LemTS;
IT: now let s be Element of S;
      set s1 = h.(s, z:=(.x-.y));
      set s2 = h.(s1, z lt 0);
      set q = h.(s1, J);
      set qz = h.(s2, z*=-1);
      (s2.b = 0 implies s2 nin T) & (s2.b = 1 implies s2 in T) by LemTS; then
Q5:   (s2.b = 0 implies q = s2) & (s2.b = 1 implies q = qz)
      by Z0,AOFA_000:def 30,80;
02:   s2.x = s1.x & s2.y = s1.y & s2.z = s1.z by A0,Th015;
04:   (s1.z < 0 implies s2.b = 1) & (s1.z >= 0 implies s2.b = 0)
      by Th015;
05:   qz.x = s2.x & qz.y = s2.y & qz.z = (s2.z)*(-1) & (s2.z)*(-1) = -(s2.z)
      by D1,Th013;
      set s3 = h.(q, x:=y);
      set s4 = h.(s3, y:=z);
00:   h.(s, I) = h.(h.(s, z:=(.x-.y)\; J\; x:=y), y:=z) by AOFA_000:def 29
      .= h.(h.(h.(s, z:=(.x-.y)\; J), x:=y), y:=z) by AOFA_000:def 29
      .= s4 by AOFA_000:def 29;
      (.x-.y).s = ((.x).s)-((.y).s) & (.x).s = s.x & (.y).s = s.y
      by ThE1,DEFminus3; then
01:   s1.x = s.x & s1.y = s.y & s1.z = (s.x)-(s.y) by D1,Th111;
03:   s3.x = q.y & s3.y = q.y & s3.z = q.z by D1,Th211;
      s4.x = s3.x & s4.y = s3.z by D1,Th211;
      hence h.(s, I).x = s.y & h.(s, I).y = abs(s.x-s.y)
      by 00,01,02,03,04,05,Q5,ABSVALUE:def 1;
    end;
II: h iteration_terminates_for I\;C, h.(s,C) by AB,A0,A1,S1,LemEA2term;
IA: P[s] by A1,NAT_D:def 5;
ID: for s being Element of S st P[s] & s in T & R[s]
    holds P[h.(s,I)]
    proof
      let s be Element of S; assume
00:   P[s];
      reconsider n' = s.x, m' = s.y as Element of NAT by 00,INT_1:16;
      assume
01:   s in T & R[s];
      reconsider s'' = h.(s, I) as Element of S;
04:   s''.x = s.y & s''.y = abs(s.x-s.y) by IT;
      n hcf m divides n'-m' & abs(n hcf m) = n hcf m
      by 00,PREPOWER:108,ABSVALUE:def 1;
      hence n hcf m divides h.(s,I).x & n hcf m divides h.(s,I).y &
      h.(s,I).x > 0 & h.(s,I).y >= 0 by 01,00,04,INT_2:21;
      let c be Nat; reconsider c' = c as Element of NAT by ORDINAL1:def 13;
      assume
05:   c divides h.(s,I).x & c divides h.(s,I).y;
      c' divides m' & c' divides abs(n'-m') & abs c = c
      by 05,IT,ABSVALUE:def 1; then
      c qua Integer divides m' & c divides n'-m' by INT_2:21; then
      c divides (n'-m')+m' & (n'-m')+m' = n' by WSIERP_1:9;
      hence c divides n hcf m by 00,04,05;
    end;
IE: for s being Element of S st P[s] holds P[h.(s,C) qua Element of S] &
    (h.(s,C) in T iff R[h.(s,C) qua Element of S])
    proof
      let s be Element of S; assume
01:   P[s];
      reconsider s' = h.(s,C) as Element of S;
02:   s'.x = s.x & s'.y = s.y & (s.y > 0 implies s'.b = 1) &
      (s.y <= 0 implies s'.b = 0) by A0,Th015;
      hence P[h.(s,C) qua Element of S] by 01;
      thus thesis by 01,02,LemTS;
    end;
K:  P[h.(s,while(C,I)) qua Element of S] &
    not R[h.(s,while(C,I)) qua Element of S]
    from AOFA_000:sch 5(IA,II,ID,IE); then
    reconsider fn = fin.x as Element of NAT by INT_1:16;
    now
      thus n hcf m divides fn by K;
      fn divides 0 & fin.y = 0 by K,NAT_D:6;
      hence fn divides n hcf m by K;
    end;
    hence h.(s, while(y gt 0, I)).x = n hcf m by NAT_D:5;
  end;

theorem
  for x,y,m being Variable of g
  st ex d being Function st d.b = 0 & d.x = 1 & d.y = 2 & d.m = 3
  holds
    y:=1\;
    while(m gt 0,
      if-then(m is_odd, y*=x)\; m/=2\; x*=x
    )
    is_terminating_wrt g, {s: s.m >= 0}
  proof set S = Funcs(X, INT); set T = S\(b,0);
    let x,y,m be Variable of g;
    set P = {s: s.m >= 0};
    given d being Function such that
A0: d.b = 0 & d.x = 1 & d.y = 2 & d.m = 3;
D0: m <> x & m <> y & x <> y & b <> x & b <> y & b <> m by A0;
A1: y:=1 is_terminating_wrt g, P by AOFA_000:107;
A2: P is_invariant_wrt y:=1, g
    proof let s;
      assume s in P; then
B1:   ex s' st s = s' & s'.m >= 0;
      g.(s, y:=1).m = s.m by D0,Th011;
      hence g.(s, y:=1) in P by B1;
    end;
    set C = m gt 0;
    set I = if-then(m is_odd, y*=x);
    set J = I\; m/=2\; x*=x;
A3: C is_terminating_wrt g by AOFA_000:104;
A4: J is_terminating_wrt g,P by AOFA_000:107;
A5: P is_invariant_wrt C,g
    proof let s;
      assume s in P; then
B1:   ex s' st s = s' & s'.m >= 0;
      g.(s, C).m = s.m by A0,Th015;
      hence g.(s, C) in P by B1;
    end;
A6: for s st s in P & g.(g.(s,J),C) in T holds g.(s,J) in P
    proof let s such that s in P;
      assume g.(g.(s,J),C) in T; then
      g.(s,J).m > 0 by Th015';
      hence g.(s,J) in P;
    end;
    defpred R[Element of S] means $1.m > 0;
    deffunc F(Element of S) = In($1.m, NAT);
Z0: g complies_with_while_wrt T & g complies_with_if_wrt T by AOFA_000:def 32;
    for s st g.(s,C) in P holds g iteration_terminates_for J\;C, g.(s,C)
    proof let s0 be Element of S such that g.(s0,C) in P;
      set s1 = g.(s0,C);
A4:   s1.x = s0.x & s1.m = s0.m & s1.y = s0.y &
      (s0.m > 0 implies s1.b = 1) & (s0.m <= 0 implies s1.b = 0) by A0,Th015;
B0:   g.(s0,C) in T iff R[g.(s0,C)] by A4,LemTS;
B1:   for s being Element of S st R[s]
      holds (R[g.(s,J\;C)] iff g.(s,J\;C) in T) & F(g.(s,J\;C)) < F(s)
      proof
        let s be Element of S such that
00:     s.m > 0;
        set sJ = g.(s,J);
        set sC = g.(sJ,C);
01:     (sJ.m > 0 implies sC.b = 1) & (sJ.m <= 0 implies sC.b = 0) &
        sC.m = sJ.m & g.(s,J\;C) = sC by A0,Th015,AOFA_000:def 29;
        hence R[g.(s,J\;C)] iff g.(s,J\;C) in T by LemTS;
        set q0 = g.(s, m is_odd);
        set q1 = g.(s,I);
        set q2 = g.(q1,m/=2);
        set q3 = g.(q2,x*=x);
        q0 in T or q0 nin T; then
03:     q1 = g.(q0, y*=x) or q1 = g.(q0, EmptyIns A) by Z0,AOFA_000:def 30;
        q2 = g.(s,I\;m/=2) by AOFA_000:def 29; then
        q3 = g.(s,J) by AOFA_000:def 29; then
02:     sJ.m = q2.m by D0,Th213 .= (q1.m) div 2 by Th017
        .= (q0.m) div 2 by D0,03,Th213,AOFA_000:def 28
        .= (s.m) div 2 by A0,Th218; then
        sC.m in NAT & s.m in NAT by 00,01,INT_1:16,88; then
        F(s) = s.m & F(sC) = sC.m by FUNCT_7:def 1;
        hence F(g.(s,J\;C)) < F(s) by 00,01,02,INT_1:83;
      end;
      thus g iteration_terminates_for J\;C, g.(s0,C)
      from AOFA_000:sch 3(B0,B1);
    end; then
    while(m gt 0,
      if-then(m is_odd, y*=x)\; m/=2\; x*=x
    ) is_terminating_wrt g, P by A3,A4,A5,A6,AOFA_000:118;
    hence y:=1\;
      while(m gt 0,
        if-then(m is_odd, y*=x)\; m/=2\; x*=x
      ) is_terminating_wrt g, {s: s.m >= 0} by A1,A2,AOFA_000:111;
  end;

theorem
  for x,y,m being Variable of g
  st ex d being Function st d.b = 0 & d.x = 1 & d.y = 2 & d.m = 3
  for s being Element of Funcs(X, INT)
  for n being Nat st n = s.m holds
  g.(s,  y:=1\;
         while(m gt 0,
           if-then(m is_odd, y*=x)\; m/=2\; x*=x
         )
     ).y = (s.x)|^n
  proof set S = Funcs(X, INT);
    set T = S\(b,0);
Z0: g complies_with_while_wrt T & g complies_with_if_wrt T by AOFA_000:def 32;
    let x,y,m be Variable of g;
    given d being Function such that
A0: d.b = 0 & d.x = 1 & d.y = 2 & d.m = 3;
D0: m <> x & m <> y & x <> y & b <> x & b <> y & b <> m by A0;
    let s be Element of Funcs(X, INT);
    set q = s;
    let n be Nat;
    assume
A1: n = s.m;
    set C = m gt 0;
    set I = if-then(m is_odd, y*=x);
    set J = I\; m/=2\; x*=x;
    set s0 = g.(s, y:=1);
    set s1 = g.(s0,C);
    set fs = g.(s0, while(C,J));
A3: s0.x = s.x & s0.m = s.m & s0.y = 1 by D0,Th011;
A4: s1.x = s0.x & s1.m = s0.m & s1.y = s0.y &
    (s0.m > 0 implies s1.b = 1) & (s0.m <= 0 implies s1.b = 0) by A0,Th015;
    defpred P[Element of S] means
    (s.x)|^n = ($1.y)*(($1.x)to_power($1.m)) & $1.m >= 0;
    defpred R[Element of S] means $1.m > 0;
    reconsider n' = n as Element of NAT by ORDINAL1:def 13;
    (n = 0 or n > 0) & (n > 0 implies 0 to_power n = 0) & 0 to_power 0 = 1 &
    (s.x = 0 or s.x <> 0) by POWER:def 2,29; then
A:  P[s0] by A1,A3,POLYEQ_3:50,NEWTON:9,POWER:46;
    deffunc F(Element of S) = In($1.m, NAT);
B0: g.(s0,C) in T iff R[g.(s0,C)] by A4,LemTS;
B1: for s being Element of S st R[s]
    holds (R[g.(s,J\;C)] iff g.(s,J\;C) in T) & F(g.(s,J\;C)) < F(s)
    proof
      let s be Element of S such that
00:   s.m > 0;
      set sJ = g.(s,J);
      set sC = g.(sJ,C);
01:   (sJ.m > 0 implies sC.b = 1) & (sJ.m <= 0 implies sC.b = 0) &
      sC.m = sJ.m & g.(s,J\;C) = sC by A0,Th015,AOFA_000:def 29;
      hence R[g.(s,J\;C)] iff g.(s,J\;C) in T by LemTS;
      set q0 = g.(s, m is_odd);
      set q1 = g.(s,I);
      set q2 = g.(q1,m/=2);
      set q3 = g.(q2,x*=x);
      q0 in T or q0 nin T; then
03:   q1 = g.(q0, y*=x) or q1 = g.(q0, EmptyIns A) by Z0,AOFA_000:def 30;
      q2 = g.(s,I\;m/=2) by AOFA_000:def 29; then
      q3 = g.(s,J) by AOFA_000:def 29; then
02:   sJ.m = q2.m by D0,Th213 .= (q1.m) div 2 by Th017
      .= (q0.m) div 2 by D0,03,Th213,AOFA_000:def 28
      .= (s.m) div 2 by A0,Th218; then
      sC.m in NAT & s.m in NAT by 00,01,INT_1:16,88; then
      F(s) = s.m & F(sC) = sC.m by FUNCT_7:def 1;
      hence F(g.(s,J\;C)) < F(s) by 00,01,02,INT_1:83;
    end;
B:  g iteration_terminates_for J\;C, g.(s0,C) from AOFA_000:sch 3(B0,B1);
C:  for s being Element of S st P[s] & s in T & R[s]
    holds P[g.(s,J)]
    proof
      let s be Element of S such that
00:   P[s] & s in T & R[s];
      reconsider sm = s.m as Element of NAT by 00,INT_1:16;
      set sJ = g.(s,J);
      set q0 = g.(s, m is_odd);
      set q1 = g.(s,I);
      set q2 = g.(q1,m/=2);
      set q3 = g.(q2,x*=x);
      q0 in T or q0 nin T; then
03:   q1 = g.(q0, y*=x) or q1 = g.(q0, EmptyIns A) by Z0,AOFA_000:def 30;
      q2 = g.(s,I\;m/=2) by AOFA_000:def 29; then
07:   q3 = g.(s,J) by AOFA_000:def 29; then
02:   sJ.m = q2.m by D0,Th213 .= (q1.m) div 2 by Th017
      .= (q0.m) div 2 by D0,03,Th213,AOFA_000:def 28
      .= (s.m) div 2 by A0,Th218;
      q2.x = q1.x by D0,Th017 .= q0.x by D0,03,Th213,AOFA_000:def 28; then
06:   sJ.x = (q0.x)*(q0.x) & q0.x = s.x by A0,Th218,07,Th213;
08:   sJ.y = q2.y & q2.y = q1.y & q0.y = s.y by 07,D0,Th213,Th017,Th218;
04:   sm div 2 = s.m div 2 & sm mod 2 = s.m mod 2;
09:   now
I1:     q0.b = (s.m) mod 2 by Th218;
        per cases by 04,I1,NAT_D:12;
        suppose
I2:       q0.b = 0; then
          q0 nin T by LemTS; then
          q1 = g.(q0, EmptyIns A) by Z0,AOFA_000:def 30; then
          q1.y = q0.y & (s.x)to_power 0 = 1 & (s.y)*1 = s.y
          by AOFA_000:def 28,POWER:29;
          hence (s.y)*((s.x)to_power(sm mod 2)) = sJ.y by I2,08,Th218;
        end;
        suppose
I3:       q0.b = 1; then
          q0 in T; then
          q1 = g.(q0, y*=x) by Z0,AOFA_000:def 30; then
          q1.y = (q0.y)*(q0.x) & (s.x)to_power 1 = s.x
          by Th213,POWER:30;
          hence (s.y)*((s.x)to_power(sm mod 2)) = sJ.y by I3,08,06,Th218;
        end;
      end;
05:   s.x = 0 or s.x is non empty;
      s.m = ((s.m) div 2)*2+((s.m) mod 2) by NEWTON:80; then
      (q.x)|^n
      = (s.y)*(((s.x)to_power((sm div 2)*2))*((s.x)to_power(sm mod 2)))
      by 00,05,LemP1,FIB_NUM2:7
      .= (s.y)*((s.x)to_power(sm mod 2))*((s.x)to_power((sm div 2)*2))
      .= (s.y)*((s.x)to_power(sm mod 2))*
         (((s.x)to_power 2) to_power (sm div 2)) by LemP2
      .= (s.y)*((s.x)to_power(sm mod 2))*
         (((s.x)*(s.x)) to_power (sm div 2)) by LemP3;
      hence P[g.(s,J)] by 02,06,09;
    end;
D:  for s being Element of S st P[s] holds
    P[g.(s,C)] & (g.(s,C) in T iff R[g.(s,C)])
    proof
      let s be Element of S such that
00:   P[s];
      set s1 = g.(s, C);
      s1.m = s.m & s1.x = s.x & s1.y = s.y by A0,Th015;
      hence P[g.(s,C)] by 00;
      (s.m > 0 implies s1.b = 1) & (s.m > 0 or s.m <= 0) &
      (s.m <= 0 implies s1.b = 0) by Th015;
      hence thesis by Th015,LemTS;
    end;
E:  P[g.(s0,while(C,J))] & not R[g.(s0,while(C,J))]
    from AOFA_000:sch 5(A,B,C,D); then
    fs.m = 0 & (fs.x) to_power 0 = 1 by POWER:29;
    hence g.(s, y:=1\; while(m gt 0, J)).y = (s.x)|^n by E,AOFA_000:def 29;
  end;