:: Euclide Algorithm
::  by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received October 8, 1993
:: Copyright (c) 1993 Association of Mizar Users

environ

 vocabularies INT_1, NAT_1, ARYTM_3, ARYTM_1, ABSVALUE, FUNCT_1, CQC_LANG,
      AMI_3, AMI_1, CAT_1, FUNCT_4, RELAT_1, BOOLE, AMI_2, INT_2, PARTFUN1,
      FUNCOP_1, AMI_4;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, XCMPLX_0, RELAT_1,
      FUNCT_1, FUNCT_2, INT_1, NAT_1, NAT_D, CQC_LANG, INT_2, STRUCT_0,
      PARTFUN1, AMI_1, AMI_3, XXREAL_0;
 constructors ENUMSET1, FRAENKEL, XXREAL_0, REAL_1, NAT_1, INT_2, FUNCOP_1,
      AMI_3, NAT_D;
 registrations AMI_1, AMI_3, RELSET_1, XREAL_0, INT_1, FRAENKEL, NUMBERS,
      ORDINAL1, SETFAM_1, STRUCT_0, XXREAL_0, CARD_3;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions CQC_LANG, AMI_1, TARSKI, AMI_3;
 theorems AMI_1, INT_1, ABSVALUE, INT_2, TARSKI, ENUMSET1, NAT_1, CQC_LANG,
      REAL_2, PARTFUN1, FUNCT_4, FUNCT_1, GRFUNC_1, ZFMISC_1, AMI_3, RELAT_1,
      RELSET_1, XBOOLE_0, XBOOLE_1, NEWTON, XREAL_1, XXREAL_0, ORDINAL1,
      FUNCOP_1, NAT_D;
 schemes NAT_1, NAT_D, RECDEF_1, FUNCT_1, AMI_3;

begin :: Preliminaries

theorem Th1:
 for i,j being Integer st i >= 0 & j >= 0
  holds i div j >= 0
  proof let i,j be Integer such that
A1:   i >= 0 & j >= 0;
A2:  i div j = [\ i / j /] by INT_1:def 7;
A3:  i / j - 1 < [\ i / j /] by INT_1:def 4;
       i / j >= 0 & 0 - 1 = - 1 by A1,REAL_2:125;
    then i / j - 1 >= -1 by XREAL_1:11;
    then - 1 < [\ i / j /] by A3,XXREAL_0:2;
   hence i div j >= 0 by A2,INT_1:21;
  end;

theorem Th2:
 for i,j being Integer st i >= 0 & j >= 0
  holds abs(i) mod abs(j) = i mod j
      & abs(i) div abs(j) = i div j
proof let i,j be Integer;
assume that A1: i >= 0 and A2: j >= 0;
per cases by A2;
suppose A3:j > 0;
then A4: i = abs(i) & j = abs(j) by A1,ABSVALUE:def 1;
     i mod j >= 0 & i div j >= 0 by A1,A3,Th1,NEWTON:78;
  then reconsider n = i mod j, m = i div j as Element of NAT by INT_1:16;
A5: n < j by A3,NEWTON:79;
     n = i - m * j by A3,INT_1:def 8;
  then i = j * m + n;
 hence thesis by A4,A5,NAT_D:def 1,NAT_D:def 2;
 end;
 suppose
 A6:j = 0;
  abs(0) = 0 by ABSVALUE:def 1;
 then abs(i) mod abs(0) = 0 & abs(i) div abs(0) = 0
  by NAT_D:def 1,NAT_D:def 2;
 hence thesis by A6,INT_1:75,def 8;
 end;
end;

reserve i,j,k for Element of NAT;

scheme Euklides' { F(Element of NAT)->Element of NAT,G(Element of NAT)->
Element of NAT,a()->Element of NAT,b()->Element of NAT } :
  ex k st F(k) = a() hcf b() & G(k) = 0
   provided
A1: 0 < b() and
A2: b() < a() and
A3: F(0) = a() and
A4: G(0) = b() and
A5: for k st G(k) > 0 holds F(k+1) = G(k) & G(k+1) = F(k) mod G(k)
proof

A6: 0 < b() & b() < a() by A1,A2;
   deffunc F(Element of NAT,set) = IFEQ($2,0,0,G($1));
   consider q being Function of NAT,NAT such that
A7: q.0 = a() and
A8: for i holds q.(i+1) = F(i,q.i) from RECDEF_1:sch 4;
   deffunc Q(Element of NAT) = q.$1;
      q.(0+1) = IFEQ(q.0,0,0,G(0)) by A8
     .= G(0) by A2,A7,CQC_LANG:def 1;
then A9: Q(0) = a() & Q(1) = b() by A4,A7;
A10: for k st q.k qua Element of NAT > 0 holds q.k = F(k)
    proof let k such that
A11:    q.k qua Element of NAT > 0;
        now per cases;
      case k = 0;
       hence q.k = F(k) by A3,A7;
      end;
      case k <> 0;
       then consider i being Nat such that
A12:       k = i+1 by NAT_1:6;
           reconsider i as Element of NAT by ORDINAL1:def 13;
A13:      now assume
A14:        q.i qua Element of NAT = 0;
             q.k = IFEQ(q.i,0,0,G(i)) by A8,A12
             .= 0 by A14,CQC_LANG:def 1;
         hence contradiction by A11;
        end;
           q.k = IFEQ(q.i,0,0,G(i)) by A8,A12
          .= G(i) by A13,CQC_LANG:def 1;
      hence q.k = F(k) by A5,A11,A12;
     end;
     end;
     hence q.k = F(k);
    end;
A15: for k holds Q(k+2) = Q(k) mod Q(k+1)
    proof let k;
         now per cases;
       case
A16:      q.(k+1) <> 0;
            now assume
A17:        G(k) = 0;
A18:        q.k = 0 or q.k <> 0;

              q.(k+1) = IFEQ(q.k,0,0,G(k)) by A8
            .= 0 by A17,A18,CQC_LANG:def 1;
          hence contradiction by A16;
         end;
         then A19:       G(k) > 0;
A20:       q.(k+(1+1)) = q.((k+1)+1)
           .= IFEQ(q.(k+1),0,0,G(k+1)) by A8
           .= G(k+1) by A16,CQC_LANG:def 1
           .= F(k) mod G(k) by A5,A19;
A21:       now assume
A22:         q.k = 0;
              q.(k+1) = IFEQ(q.k,0,0,G(k)) by A8
            .= 0 by A22,CQC_LANG:def 1;
          hence contradiction by A16;
         end;
then A23:       q.k qua Element of NAT > 0;
            q.(k+1) = IFEQ(q.k,0,0,G(k)) by A8
            .= G(k) by A21,CQC_LANG:def 1;
        hence q.(k+2) = q.(k) mod q.(k+1) by A10,A20,A23;
       end;
       case
A24:       q.(k+1) = 0;
        thus q.(k+2) = q.((k+1)+1)
           .= IFEQ(q.(k+1),0,0,G(k+1)) by A8
           .= 0 by A24,CQC_LANG:def 1
           .= q.(k) mod q.(k+1) by A24,NAT_D:def 2;
      end;
      end;
     hence q.(k+2) = q.(k) mod q.(k+1);
    end;
   consider k such that
A25:  Q(k) = a() hcf b() & Q(k + 1) = 0 from NAT_D:sch 1(A6,A9,A15);
  take k;
A26: a() hcf b() > 0 by A1,NEWTON:71;
  hence F(k) = a() hcf b() by A10,A25;
  thus G(k) = IFEQ(q.k,0,0,G(k)) by A25,A26,CQC_LANG:def 1
     .= 0 by A8,A25;
 end;

set a = dl.0, b = dl.1, c = dl.2;

begin :: Euclide algorithm

definition
 func Euclide-Algorithm -> programmed FinPartState of SCM equals

 (il.0 .--> (dl.2 := dl.1)) +*
  ((il.1 .--> Divide(dl.0,dl.1)) +*
   ((il.2 .--> (dl.0 := dl.2)) +*
    ((il.3 .--> (dl.1 >0_goto il.0)) +*
     (il.4 .--> halt SCM))));
 coherence
  proof
    set EA3 = (il.3 .--> (b >0_goto il.0)) +* (il.4 .--> halt SCM);
    set EA2 = (il.2 .--> (a := dl.2)) +* EA3;
       EA3 is programmed by AMI_3:35;
    then EA2 is programmed by AMI_3:35;
    then (il.1 .--> Divide(a,b)) +* EA2 is programmed by AMI_3:35;
    hence thesis by AMI_3:35;
  end;
 correctness;
end;

defpred P[State of SCM] means
 $1.il.0 = c := b &
 $1.il.1 = Divide(a,b) &
 $1.il.2 = a := c &
 $1.il.3 = b >0_goto il.0 &
 $1 halts_at il.4;

 set IN0 = il.0 .--> (dl.2 := b);
 set IN1 = il.1 .--> Divide(a,b);
 set IN2 = il.2 .--> (a := dl.2);
 set IN3 = il.3 .--> (b >0_goto il.0);
 set IN4 = il.4 .--> halt SCM;
 set EA3 = IN3 +* IN4;
 set EA2 = IN2 +* EA3;
 set EA1 = IN1 +* EA2;
 set EA0 = IN0 +* EA1;

canceled;

theorem Th4:
 dom (Euclide-Algorithm qua Function) = { il.0,il.1,il.2,il.3,il.4 }
 proof
A1: dom IN0 = { il.0 } by CQC_LANG:5;
A2: dom IN1 = { il.1 } by CQC_LANG:5;
A3: dom IN2 = { il.2 } by CQC_LANG:5;
A4: dom IN3 = { il.3 } by CQC_LANG:5;
    dom IN4 = { il.4 } by CQC_LANG:5;
then dom EA3 = { il.3 } \/ { il.4 } by A4,FUNCT_4:def 1
          .= { il.3,il.4 } by ENUMSET1:41;
then dom EA2 = { il.2 } \/ { il.3,il.4 } by A3,FUNCT_4:def 1
          .= { il.2,il.3,il.4 } by ENUMSET1:42;
then dom EA1 = { il.1 } \/ { il.2,il.3,il.4 } by A2,FUNCT_4:def 1
          .= { il.1,il.2,il.3,il.4 } by ENUMSET1:44;
   then dom EA0 = { il.0 } \/ { il.1,il.2,il.3,il.4 } by A1,FUNCT_4:def 1
          .= { il.0,il.1,il.2,il.3,il.4 } by ENUMSET1:47;
  hence thesis;
 end;

Lm1:
 for s being State of SCM st Euclide-Algorithm c= s holds P[s]
 proof let s be State of SCM;
A1: dom IN1 = { il.1 } by CQC_LANG:5;
A2: dom IN2 = { il.2 } by CQC_LANG:5;
A3: dom IN3 = { il.3 } by CQC_LANG:5;
A4: dom IN4 = { il.4 } by CQC_LANG:5;
then A5: dom EA3 = { il.3 } \/ { il.4 } by A3,FUNCT_4:def 1
          .= { il.3,il.4 } by ENUMSET1:41;
then A6: dom EA2 = { il.2 } \/ { il.3,il.4 } by A2,FUNCT_4:def 1
          .= { il.2,il.3,il.4 } by ENUMSET1:42;
then A7: dom EA1 = { il.1 } \/ { il.2,il.3,il.4 } by A1,FUNCT_4:def 1
          .= { il.1,il.2,il.3,il.4 } by ENUMSET1:44;
  assume A8: Euclide-Algorithm c= s;
    A9: not il.0 in dom EA1 by A7,ENUMSET1:def 2;
    il.0 in dom EA0 by Th4,ENUMSET1:def 3;
  hence s.il.0 = EA0.il.0 by A8,GRFUNC_1:8
      .= IN0.il.0 by A9,FUNCT_4:12
      .= c := b by CQC_LANG:6;
      EA1 c= EA0 by FUNCT_4:26;
then A10: EA1 c= s by A8,XBOOLE_1:1;
A11: not il.1 in dom EA2 by A6,ENUMSET1:def 1;
    il.1 in dom EA1 by A7,ENUMSET1:def 2;
  hence s.il.1 = EA1.il.1 by A10,GRFUNC_1:8
      .= IN1.il.1 by A11,FUNCT_4:12
      .= Divide(a,b) by CQC_LANG:6;
      EA2 c= EA1 by FUNCT_4:26;
then A12: EA2 c= s by A10,XBOOLE_1:1;
A13: not il.2 in dom EA3 by A5,TARSKI:def 2;
    il.2 in dom EA2 by A6,ENUMSET1:def 1;
  hence s.il.2 = EA2.il.2 by A12,GRFUNC_1:8
      .= IN2.il.2 by A13,FUNCT_4:12
      .= a := c by CQC_LANG:6;
      EA3 c= EA2 by FUNCT_4:26;
then A14: EA3 c= s by A12,XBOOLE_1:1;
A15: not il.3 in dom IN4 by A4,TARSKI:def 1;
    il.3 in dom EA3 by A5,TARSKI:def 2;
  hence s.il.3 = EA3.il.3 by A14,GRFUNC_1:8
      .= IN3.il.3 by A15,FUNCT_4:12
      .= b >0_goto il.0 by CQC_LANG:6;
A16: il.4 in dom EA3 by A5,TARSKI:def 2;
A17: il.4 in dom IN4 by A4,TARSKI:def 1;
  thus s.il.4 = EA3.il.4 by A14,A16,GRFUNC_1:8
      .= IN4.il.4 by A17,FUNCT_4:14
      .= halt SCM by CQC_LANG:6;
 end;

begin :: Natural semantics of the program

theorem Th5:
  for s being State of SCM st Euclide-Algorithm c= s
  for k st IC (Computation s).k = il.0
  holds IC (Computation s).(k+1) = il.1 &
   (Computation s).(k+1).dl.0 = (Computation s).k.dl.0 &
   (Computation s).(k+1).dl.1 = (Computation s).k.dl.1 &
   (Computation s).(k+1).dl.2 = (Computation s).k.dl.1
 proof let s be State of SCM such that
A1: Euclide-Algorithm c= s;
  let k;
  assume A2: IC (Computation s).k = il.0;
A3: (Computation s).(k+1)
     = Exec(s.(IC (Computation s).k),(Computation s).k) by AMI_1:55
    .= Exec(c := b,(Computation s).k) by A1,A2,Lm1;
  thus IC (Computation s).(k+1) = Next IC (Computation s).k by A3,AMI_3:8
     .= il.(0+1) by A2,AMI_3:54
     .= il.1;
  thus (Computation s).(k+1).a = (Computation s).k.a &
       (Computation s).(k+1).b = (Computation s).k.b by A3,AMI_3:8;
  thus (Computation s).(k+1).c = (Computation s).k.b by A3,AMI_3:8;
 end;

theorem Th6:
  for s being State of SCM st Euclide-Algorithm c= s
  for k st IC (Computation s).k = il.1
  holds IC (Computation s).(k+1) = il.2 &
   (Computation s).(k+1).dl.0 =
    (Computation s).k.dl.0 div (Computation s).k.dl.1 &
   (Computation s).(k+1).dl.1 =
    (Computation s).k.dl.0 mod (Computation s).k.dl.1 &
   (Computation s).(k+1).dl.2 = (Computation s).k.dl.2
 proof let s be State of SCM such that
A1: Euclide-Algorithm c= s;
   let k such that
A2: IC (Computation s).k = il.1;
A3: (Computation s).(k+1)
     = Exec(s.(IC (Computation s).k),(Computation s).k) by AMI_1:55
    .= Exec(Divide(a,b),(Computation s).k) by A1,A2,Lm1;
  thus IC (Computation s).(k+1)
      = Next IC (Computation s).k by A3,AMI_3:12
     .= il.(1+1) by A2,AMI_3:54
     .= il.2;
   thus
       (Computation s).(k+1).a = (Computation s).k.a div (Computation s).k.b &
    (Computation s).(k+1).b = (Computation s).k.a mod (Computation s).k.b &
    (Computation s).(k+1).c = (Computation s).k.c by A3,AMI_3:12;
 end;

theorem Th7:
  for s being State of SCM st Euclide-Algorithm c= s
  for k st IC (Computation s).k = il.2
  holds IC (Computation s).(k+1) = il.3 &
   (Computation s).(k+1).dl.0 = (Computation s).k.dl.2 &
   (Computation s).(k+1).dl.1 = (Computation s).k.dl.1 &
   (Computation s).(k+1).dl.2 = (Computation s).k.dl.2
 proof let s be State of SCM such that
A1: Euclide-Algorithm c= s;
  let k;
  assume A2: IC (Computation s).k = il.2;
A3: (Computation s).(k+1)
     = Exec(s.(IC (Computation s).k),(Computation s).k) by AMI_1:55
    .= Exec(a := c,(Computation s).k) by A1,A2,Lm1;
  thus IC (Computation s).(k+1)
      = Next IC (Computation s).k by A3,AMI_3:8
     .= il.(2+1) by A2,AMI_3:54
     .= il.3;
  thus (Computation s).(k+1).a = (Computation s).k.c by A3,AMI_3:8;
  thus (Computation s).(k+1).b = (Computation s).k.b
     & (Computation s).(k+1).c = (Computation s).k.c by A3,AMI_3:8;
 end;

theorem Th8:
  for s being State of SCM st Euclide-Algorithm c= s
  for k st IC (Computation s).k = il.3
  holds
   ((Computation s).k.dl.1 > 0 implies IC (Computation s).(k+1) = il.0) &
   ((Computation s).k.dl.1 <= 0 implies IC (Computation s).(k+1) = il.4) &
   (Computation s).(k+1).dl.0 = (Computation s).k.dl.0 &
   (Computation s).(k+1).dl.1 = (Computation s).k.dl.1
 proof let s be State of SCM such that
A1: Euclide-Algorithm c= s;
  let k; assume
A2: IC (Computation s).k = il.3;
A3: (Computation s).(k+1)
     = Exec(s.(IC (Computation s).k),(Computation s).k) by AMI_1:55
    .= Exec(b >0_goto il.0,(Computation s).k) by A1,A2,Lm1;
  thus (Computation s).k.b > 0 implies IC (Computation s).(k+1) = il.0
    by A3,AMI_3:15;
  thus (Computation s).k.b <= 0 implies IC (Computation s).(k+1) = il.4
   proof assume
A4:  (Computation s).k.b <= 0;
    thus IC (Computation s).(k+1)
        = Next IC (Computation s).k by A3,A4,AMI_3:15
       .= il.(3+1) by A2,AMI_3:54
       .= il.4;
   end;
  thus (Computation s).(k+1).a = (Computation s).k.a
     & (Computation s).(k+1).b = (Computation s).k.b by A3,AMI_3:15;
 end;

theorem Th9:
  for s being State of SCM st Euclide-Algorithm c= s
  for k,i st IC (Computation s).k = il.4
  holds (Computation s).(k+i) = (Computation s).k
 proof let s be State of SCM such that
A1: Euclide-Algorithm c= s;
   let k,i;
A2: k <= k + i by NAT_1:11;
   assume IC (Computation s).k = il.4;
    then s halts_at IC (Computation s).k by A1,Lm1;
   hence (Computation s).(k+i) = (Computation s).k by A2,AMI_3:46;
 end;

Lm2:
  for s being State of SCM st s starts_at il.0 & Euclide-Algorithm c= s
    & s.a > 0 & s.b > 0
  holds
   (Computation s).(4*k).a > 0 &
   ((Computation s).(4*k).b > 0 & IC (Computation s).(4*k) = il.0 or
   (Computation s).(4*k).b = 0 & IC (Computation s).(4*k) = il.4)
 proof let s be State of SCM such that
A1: IC s = il.0 and
A2:  Euclide-Algorithm c= s and
A3:  s.a > 0 & s.b > 0;
    defpred P[Element of NAT] means
(Computation s).(4*$1).a > 0 &
   ((Computation s).(4*$1).b > 0 & IC (Computation s).(4*$1) = il.0 or
   (Computation s).(4*$1).b = 0 & IC (Computation s).(4*$1) = il.4);
A4: P[0]  by A1,A3,AMI_1:def 19;
A5: for k st P[k] holds P[k+1] proof let k;
    set c4 = (Computation s).(4*k), c5 = (Computation s).(4*k+1),
        c6 = (Computation s).(4*k+2), c7 = (Computation s).(4*k+3),
        c8 = (Computation s).(4*k+4);
A6: c6 = (Computation s).((4*k+1)+1);
A7: c7 = (Computation s).((4*k+2)+1);
A8: c8 = (Computation s).((4*k+3)+1);
    assume
A9: c4.a > 0;
    assume
A10:   c4.b > 0 & IC c4 = il.0 or c4.b = 0 & IC c4 = il.4;
        now per cases by A10;
      case
A11:     c4.b > 0;
       then A12:    IC c5 = il.1 &
        c5.a = c4.a &
        c5.b = c4.b &
        c5.c = c4.b by A2,A10,Th5;
then A13:    IC c6 = il.2 &
        c6.b = c5.a mod c5.b &
        c6.c = c5.c by A2,A6,Th6;
    then A14: IC c7 = il.3 &
        c7.a = c6.c &
        c7.b = c6.b &
        c7.c = c6.c by A2,A7,Th7;
then (c7.b > 0 implies IC c8 = il.0) &
        (c7.b <= 0 implies IC c8 = il.4) &
        c8.a = c7.a &
        c8.b = c7.b by A2,A8,Th8;
      hence c8.a > 0 & (c8.b > 0 & IC c8 = il.0 or c8.b = 0 & IC c8 = il.4)
       by A11,A12,A13,A14,NEWTON:78;
      end;
      case c4.b = 0;
       hence c8.a > 0 & c8.b = 0 & IC c8 = il.4 by A2,A9,A10,Th9;
     end;
     end;
    hence P[k+1];
   end;
      for k holds P[k] from NAT_1:sch 1(A4,A5);
  hence thesis;
 end;

Lm3:
  for s being State of SCM st s starts_at il.0 & Euclide-Algorithm c= s
    & s.a > 0 & s.b > 0
  holds (Computation s).(4*k).b > 0 implies
   (Computation s).(4*(k+1)).a = (Computation s).(4*k).b &
   (Computation s).(4*(k+1)).b
     = (Computation s).(4*k).a mod (Computation s).(4*k).b
proof let s be State of SCM such that
A1: s starts_at il.0 and
A2: Euclide-Algorithm c= s and
A3: s.a > 0 & s.b > 0 and
A4: (Computation s).(4*k).b > 0;
  set c4 = (Computation s).(4*k), c5 = (Computation s).(4*k+1),
      c6 = (Computation s).(4*k+2), c7 = (Computation s).(4*k+3);
A5: c6 = (Computation s).((4*k+1)+1);
A6: c7 = (Computation s).((4*k+2)+1);
A7: (Computation s).(4*k+4) = (Computation s).((4*k+3)+1);
      c4.b > 0 & IC c4 = il.0 or c4.b = 0 & IC c4 = il.4 by A1,A2,A3,Lm2;
   then A8:    IC c5 = il.1 &
        c5.a = c4.a &
        c5.b = c4.b &
        c5.c = c4.b by A2,A4,Th5;
then A9:    IC c6 = il.2 &
        c6.b = c5.a mod c5.b &
        c6.c = c5.c by A2,A5,Th6;
then A10:    IC c7 = il.3 &
        c7.a = c6.c &
        c7.b = c6.b &
        c7.c = c6.c by A2,A6,Th7;
 hence (Computation s).(4*(k+1)).a = (Computation s).(4*k).b by A2,A7,A8,A9,Th8
;
 thus (Computation s).(4*(k+1)).b =
(Computation s).(4*k).a mod (Computation s).(4*k).b by A2,A7,A8,A9,A10,Th8;
end;

Lm4:
  for s being State of SCM st s starts_at il.0 & Euclide-Algorithm c= s
  for x, y being Integer st s.a = x & s.b = y & x > y & y > 0
  holds (Result s).a = x gcd y
   & ex k st s halts_at IC (Computation s).k
 proof
  let s be State of SCM such that
A1: s starts_at il.0 and
A2: Euclide-Algorithm c= s;
  let x, y be Integer such that
A3: s.a = x & s.b = y and
A4: x > y & y > 0;
    x >= 0 & y >= 0 by A4;
   then reconsider x' = x, y' = y as Element of NAT by INT_1:16;
A5: 0 < y' by A4;
A6: y' < x' by A4;
   deffunc F(Element of NAT) = abs((Computation s).(4*$1).a);
   deffunc G(Element of NAT) = abs((Computation s).(4*$1).b);
A7: F(0) = abs(x) by A3,AMI_1:def 19
      .= x' by ABSVALUE:def 1;
A8: G(0) = abs(y) by A3,AMI_1:def 19
      .= y' by ABSVALUE:def 1;
A9:
  now let k;
A10: (Computation s).(4*k).b > 0 or (Computation s).(4*k).b = 0
      by A1,A2,A3,A4,Lm2;
   assume A11: G(k) > 0;
   hence F(k+1) = G(k) by A1,A2,A3,A4,A10,Lm3,ABSVALUE:7;
A12: (Computation s).(4*(k+1)).b >= 0 by A1,A2,A3,A4,Lm2;
    A13: (Computation s).(4*k).a >= 0 by A1,A2,A3,A4,Lm2;
   thus G(k+1) = (Computation s).(4*(k+1)).b by A12,ABSVALUE:def 1
        .= (Computation s).(4*k).a mod (Computation s).(4*k).b
              by A1,A2,A3,A4,A10,A11,Lm3,ABSVALUE:7
        .= F(k) mod G(k) by A10,A13,Th2;
  end;
  consider k such that
A14: F(k) = x' hcf y' and
A15: G(k) = 0 from Euklides'(A5,A6,A7,A8,A9);
A16: abs(x) = x' & abs(y) = y' by ABSVALUE:def 1;
A17: ((Computation s).(4*k)).a > 0 by A1,A2,A3,A4,Lm2;
      (Computation s).(4*k).b = 0 by A15,ABSVALUE:7;
   then A18: IC (Computation s).(4*k) = il.4 by A1,A2,A3,A4,Lm2;
A19: s halts_at il.4 by A2,Lm1;
  hence (Result s).a = ((Computation s).(4*k)).a by A18,AMI_3:44
   .= x' hcf y' by A14,A17,ABSVALUE:def 1
   .= x gcd y by A16,INT_2:def 3;
  thus thesis by A18,A19;
 end;

theorem Th10:
  for s being State of SCM st s starts_at il.0 & Euclide-Algorithm c= s
  for x, y being Integer st s.dl.0 = x & s.dl.1 = y & x > 0 & y > 0
  holds (Result s).dl.0 = x gcd y
proof let s be State of SCM such that
A1: s starts_at il.0 and
A2: Euclide-Algorithm c= s;
  let x, y be Integer such that
A3: s.a = x and
A4: s.b = y and
A5: x > 0 and
A6: y > 0;
     now per cases by XXREAL_0:1;
   case x > y;
    hence (Result s).a = x gcd y by A1,A2,A3,A4,A6,Lm4;
   end;
   case
A7:  x = y;
     take s' = (Computation s).4;
     reconsider x' = x, y' = y as Element of NAT by A5,A6,INT_1:16;
       abs(x) = x' & abs(y) = y' by ABSVALUE:def 1;
    then A8:  x mod y = x' mod y' by Th2
           .= 0 by A7,NAT_D:25;

A9:  s = (Computation s).(4*0) & s' = (Computation s).(4*(0+1)) by AMI_1:def 19
;
     then s'.b = 0 by A1,A2,A3,A4,A5,A6,A8,Lm3;
     then IC s' = il.4 by A1,A2,A3,A4,A5,A6,A9,Lm2;
     then s halts_at IC s' by A2,Lm1;
    hence (Result s).a = s'.a by AMI_3:44 .= y by A1,A2,A3,A4,A5,A6,A9,Lm3
       .= abs(x) hcf abs(y) by A6,A7,ABSVALUE:def 1
       .= x gcd y by INT_2:def 3;
   end;
   case
A10:  y > x;
     take s' = (Computation s).4;
     reconsider x' = x, y' = y as Element of NAT by A5,A6,INT_1:16;
       abs(x) = x' & abs(y) = y' by ABSVALUE:def 1;
    then A11:  x mod y = x' mod y' by Th2
           .= x' by A10,NAT_D:24;

A12:  s = (Computation s).(4*0) & s' = (Computation s).(4*(0+1)) by
AMI_1:def 19;
then A13:  s'.a = y & s'.b = x by A1,A2,A3,A4,A5,A6,A11,Lm3;
     then IC s' = il.0 by A1,A2,A3,A4,A5,A6,A12,Lm2;
then A14: s' starts_at il.0 by AMI_3:def 14;
A15: Euclide-Algorithm c= s' by A2,AMI_3:43;
     then consider k0 being Element of NAT such that
A16:   s' halts_at IC (Computation s').k0 by A5,A10,A13,A14,Lm4;
        (Computation s).(k0+4) = (Computation s').k0 by AMI_1:51;
then A17:  s halts_at IC (Computation s).(k0+4) by A16,AMI_3:48;
        (Result s').a = x gcd y by A5,A10,A13,A14,A15,Lm4;
    hence (Result s).a = x gcd y by A17,AMI_3:47;
  end;
  end;
 hence (Result s).a = x gcd y;
end;

definition
 func Euclide-Function -> PartFunc of FinPartSt SCM, FinPartSt SCM means
:Def2:  for p,q being FinPartState of SCM holds [p,q] in it
   iff ex x,y being Integer st x > 0 & y > 0 &
    p = (dl.0,dl.1) --> (x,y) & q = dl.0 .--> (x gcd y);
 existence
  proof
    defpred P[set,set] means ex x,y being Integer st x > 0 & y > 0 &
       $1 = (a,b) --> (x,y) & $2 = a .--> (x gcd y);
A1: for p,q1,q2 being set st P[p,q1] & P[p,q2] holds q1=q2
    proof let p,q1,q2 be set;
     given x1,y1 being Integer such that
A2:    x1 > 0 & y1 > 0 &  p = (a,b) --> (x1,y1) & q1 = a .--> (x1 gcd y1);
     given x2,y2 being Integer such that
A3:    x2 > 0 & y2 > 0 &  p = (a,b) --> (x2,y2) & q2 = a .--> (x2 gcd y2);
A4:    x1 = ((a,b) --> (x1,y1)).a by FUNCT_4:66
        .= x2 by A2,A3,FUNCT_4:66;
       y1 = ((a,b) --> (x1,y1)).b by FUNCT_4:66 .= y2 by A2,A3,FUNCT_4:66
;
     hence q1 = q2 by A2,A3,A4;
    end;
    consider f being Function such that
A5:   for p,q being set holds [p,q] in f iff p in FinPartSt SCM & P[p,q]
    from FUNCT_1:sch 1(A1);
A6:  dom f c= FinPartSt SCM
     proof let e be set;
      assume e in dom f;
       then [e,f.e] in f by FUNCT_1:8;
      hence e in FinPartSt SCM by A5;
     end;
       rng f c= FinPartSt SCM
     proof let q be set;
      assume q in rng f;
       then consider p being set such that
A7:     [p,q] in f by RELAT_1:def 5;
          ex x,y being Integer st
        x > 0 & y > 0 &p = (a,b) --> (x,y) & q = a .--> (x gcd y) by A5,A7;
      hence q in FinPartSt SCM by AMI_3:31;
     end;
    then reconsider f as PartFunc of FinPartSt SCM, FinPartSt SCM
      by A6,RELSET_1:11;
   take f;
   let p,q be FinPartState of SCM;
   thus [p,q] in f
   implies ex x,y being Integer st x > 0 & y > 0 &
    p = (a,b) --> (x,y) & q = a .--> (x gcd y) by A5;
   given x,y being Integer such that
A8:   x > 0 & y > 0 &
     p = (a,b) --> (x,y) & q = a .--> (x gcd y);
       p in FinPartSt SCM by AMI_3:31;
   hence [p,q] in f by A5,A8;
  end;
 uniqueness
  proof
   defpred P[set,set] means ex x,y being Integer st x > 0 & y > 0 &
     $1 = (a,b) --> (x,y) & $2 = a .--> (x gcd y);
   let IT1,IT2 be PartFunc of FinPartSt SCM, FinPartSt SCM such that
A9: for p,q being FinPartState of SCM holds [p,q] in IT1 iff P[p,q] and
A10: for p,q being FinPartState of SCM holds [p,q] in IT2 iff P[p,q];
   thus IT1 = IT2 from AMI_3:sch 2(A9,A10);
  end;
end;

theorem Th11:
 for p being set holds p in dom Euclide-Function iff
   ex x,y being Integer st x > 0 & y > 0 & p = (dl.0,dl.1) --> (x,y)
 proof let p be set;
A1:  p in dom Euclide-Function iff [p,Euclide-Function.p] in Euclide-Function
   by FUNCT_1:8;
A2: dom Euclide-Function c= FinPartSt SCM by RELSET_1:12;
  hereby assume
A3:  p in dom Euclide-Function;
   then p in FinPartSt SCM & Euclide-Function.p in FinPartSt SCM
      by A2,PARTFUN1:27;
   then p is FinPartState of SCM & Euclide-Function.p is FinPartState of SCM
    by AMI_3:32;
   then ex x,y being Integer st x > 0 & y > 0 &
    p = (a,b) --> (x,y) & Euclide-Function.p = a .--> (x gcd y)
     by A1,A3,Def2;
   hence ex x,y being Integer st x > 0 & y > 0 & p = (a,b) --> (x,y);
  end;
  given x,y being Integer such that
A4:  x > 0 & y > 0 & p = (a,b) --> (x,y);
       [p,a .--> (x gcd y)] in Euclide-Function by A4,Def2;
  hence thesis by FUNCT_1:8;
 end;

theorem Th12:
 for i,j being Integer st i > 0 & j > 0 holds
  Euclide-Function.((dl.0,dl.1) --> (i,j)) = dl.0 .--> (i gcd j)
 proof let i,j be Integer;
  assume i > 0 & j > 0;
   then [((a,b) --> (i,j)),a .--> (i gcd j)] in Euclide-Function by Def2;
  hence Euclide-Function.((a,b) --> (i,j)) = a .--> (i gcd j)
   by FUNCT_1:8;
 end;

theorem
    (Start-At il.0) +* Euclide-Algorithm computes Euclide-Function
 proof let x be set;
  assume x in dom Euclide-Function;
   then consider i1,i2 being Integer such that
A1: i1 > 0 & i2 > 0 and
A2:  x = (a,b) --> (i1,i2) by Th11;
   reconsider s = x as FinPartState of SCM by A2;
   set p = (Start-At il.0) +* Euclide-Algorithm;
   set q = Euclide-Algorithm;
A3: dom s = { a, b } by A2,FUNCT_4:65;
then A4: a in dom s & b in dom s by TARSKI:def 2;
   dom(Start-At il.0) = { IC SCM } by FUNCOP_1:19;
    then A5:  dom p = { IC SCM } \/ { il.0,il.1,il.2,il.3,il.4 }
      by Th4,FUNCT_4:def 1;
A6: now assume
       dom p meets dom s;
      then consider x being set such that
A7:    x in dom p & x in dom s by XBOOLE_0:3;
         x in { IC SCM } or x in { il.0,il.1,il.2,il.3,il.4 }
        by A5,A7,XBOOLE_0:def 2;
then A8:     x = IC SCM or x = il.0 or x = il.1 or x = il.2 or x = il.3 or x =
il.4
       by ENUMSET1:def 3,TARSKI:def 1;
         x = a or x = b by A3,A7,TARSKI:def 2;
     hence contradiction by A8,AMI_3:57;
    end;
    then A9:  p c= p +* s by FUNCT_4:33;
        q c= p by FUNCT_4:26;
then A10: q c= p +* s by A9,XBOOLE_1:1;
A11: p +* s starts_at il.0
     proof
A12:   dom p c= dom(p +* s) by A9,RELAT_1:25;
          IC SCM in { IC SCM } by TARSKI:def 1;
       then A13:     IC SCM in dom p by A5,XBOOLE_0:def 2;
          dom p /\ dom s = {} by A6,XBOOLE_0:def 7;
then A14:     not IC SCM in dom s by A13,XBOOLE_0:def 3;
      thus
      IC SCM in dom(p +* s) by A12,A13;
          IC SCM <> il.0 & IC SCM <> il.1 & IC SCM <> il.2 &
        IC SCM <> il.3 & IC SCM <> il.4 by AMI_3:57;
then A15:    not IC SCM in dom q by Th4,ENUMSET1:def 3;
      thus IC(p +* s) = (p +* s).IC SCM by A12,A13,AMI_3:def 16
        .= p.IC SCM by A14,FUNCT_4:12
        .= (Start-At il.0).IC SCM by A15,FUNCT_4:12
        .= il.0 by CQC_LANG:6;
     end;
  take s;
  thus x = s;
A16: for t being State of SCM st p +* s c= t holds t.a = i1 & t.b = i2
   proof let t be State of SCM such that
A17: p +* s c= t;
       s c= p +* s by FUNCT_4:26;
then A18: s c= t by A17,XBOOLE_1:1;
    hence t.a = s.a by A4,GRFUNC_1:8
      .= i1 by A2,FUNCT_4:66;
    thus t.b = s.b by A4,A18,GRFUNC_1:8
      .= i2 by A2,FUNCT_4:66;
   end;
A19:  p +* s is autonomic
   proof let s1,s2 be State of SCM such that
A20:  p +* s c= s1 and
A21:  p +* s c= s2;
A22: s1 starts_at il.0 by A11,A20,AMI_3:49;
A23: Euclide-Algorithm c= s1 by A10,A20,XBOOLE_1:1;
A24: s2 starts_at il.0 by A11,A21,AMI_3:49;
A25: Euclide-Algorithm c= s2 by A10,A21,XBOOLE_1:1;
A26: s2.a = i1 & s2.b = i2 by A16,A21;
 set A = { IC SCM, a,b },
     C = { il.0,il.1,il.2,il.3,il.4};
A27: dom(p +* s) = { IC SCM } \/ C \/ { a, b } by A3,A5,FUNCT_4:def 1
      .= { IC SCM } \/ { a, b } \/ C by XBOOLE_1:4
      .= A \/ C by ENUMSET1:42;
    let k;
    set Cs = Computation s1, Cs2 = Computation s2;
A28:  Euclide-Algorithm c= Cs2.k by A25,AMI_3:43;
       Euclide-Algorithm c= Cs.k by A23,AMI_3:43;
    then A29:   (Cs.k)|C = Euclide-Algorithm by Th4,GRFUNC_1:64
      .= (Cs2.k)|C by A28,Th4,GRFUNC_1:64;
A30: dom(Cs.k) = the carrier of SCM by AMI_3:36
     .= dom(Cs2.k) by AMI_3:36;
    defpred P[Element of NAT] means  (Cs.$1).IC SCM = (Cs2.$1).IC SCM &
    (Cs.$1).a = (Cs2.$1).a & (Cs.$1).b = (Cs2.$1).b;
A31: P[0] proof
A32:   Cs.0 = s1 & Cs2.0 = s2 by AMI_1:def 19;
     hence (Cs.0).IC SCM = IC s1
      .= il.0 by A22,AMI_3:def 14
      .= IC s2 by A24,AMI_3:def 14
      .= (Cs2.0).IC SCM by A32;
     thus (Cs.0).a = (Cs2.0).a &
          (Cs.0).b = (Cs2.0).b by A16,A20,A26,A32;
    end;
A33: for i,j st P[4*i] & j<>0 & j<=4 holds P[4*i+j] proof let i,j;
     assume that
A34:   (Cs.(4*i)).IC SCM = (Cs2.(4*i)).IC SCM and
A35:   (Cs.(4*i)).a = (Cs2.(4*i)).a and
A36:   (Cs.(4*i)).b = (Cs2.(4*i)).b;
     assume j <> 0 & j <= 4;
then A37:   j = 1 or j = 2 or j = 3 or j = 4 by NAT_1:29;
     per cases by A1,A24,A25,A26,Lm2;
     suppose
A38:   IC Cs2.(4*i) = il.0;
A39:   4*i + 1 + 1 = 4*i + (1 + 1);
A40:   (4*i+2)+1 = 4*i+(2+1);
A41:   4*i + 3 + 1 = 4*i + (3 + 1);
A42:   IC Cs.(4*i) = il.0 by A34,A38;
      then A43: IC Cs.(4*i+1) = il.1 & IC Cs2.(4*i+1) = il.1 by A23,A25,A38,Th5
;
A44:  (Cs.(4*i+1)).a = (Cs.(4*i)).a by A23,A42,Th5
           .= (Cs2.(4*i+1)).a by A25,A35,A38,Th5;
A45:  (Cs.(4*i+1)).b = (Cs.(4*i)).b by A23,A42,Th5
           .= (Cs2.(4*i+1)).b by A25,A36,A38,Th5;
A46:  (Cs.(4*i+1)).dl.2 = (Cs.(4*i)).b by A23,A42,Th5
           .= (Cs2.(4*i+1)).dl.2 by A25,A36,A38,Th5;

A47: IC Cs.(4*i+2) = il.2 & IC Cs2.(4*i+2) = il.2 by A23,A25,A39,A43,Th6;
A48:  (Cs.(4*i+2)).a = (Cs.(4*i+1)).a div (Cs.(4*i+1)).b
                             by A23,A39,A43,Th6
             .= (Cs2.(4*i+2)).a by A25,A39,A43,A44,A45,Th6;
A49:  (Cs.(4*i+2)).b = (Cs.(4*i+1)).a mod (Cs.(4*i+1)).b
                             by A23,A39,A43,Th6
             .= (Cs2.(4*i+2)).b by A25,A39,A43,A44,A45,Th6;
A50:  (Cs.(4*i+2)).dl.2 = (Cs.(4*i+1)).dl.2 by A23,A39,A43,Th6
           .= (Cs2.(4*i+2)).dl.2 by A25,A39,A43,A46,Th6;

A51: IC Cs.(4*i+3) = il.3 & IC Cs2.(4*i+3) = il.3 by A23,A25,A40,A47,Th7;
A52:  (Cs.(4*i+3)).a = (Cs.(4*i+2)).dl.2 by A23,A40,A47,Th7
           .= (Cs2.(4*i+3)).a by A25,A40,A47,A50,Th7;
A53:  (Cs.(4*i+3)).b = (Cs.(4*i+2)).b by A23,A40,A47,Th7
           .= (Cs2.(4*i+3)).b by A25,A40,A47,A49,Th7;
        (Cs.(4*i+3)).b <= 0 or (Cs.(4*i+3)).b > 0;
    then A54: IC Cs.(4*i+4) = il.4 & IC Cs2.(4*i+4) = il.4 or
    IC Cs.(4*i+4) = il.0 & IC Cs2.(4*i+4) = il.0 by A23,A25,A41,A51,A53,Th8;
A55:  (Cs.(4*i+4)).a = (Cs.(4*i+3)).a by A23,A41,A51,Th8
             .= (Cs2.(4*i+4)).a by A25,A41,A51,A52,Th8;
A56:  (Cs.(4*i+4)).b = (Cs.(4*i+3)).b by A23,A41,A51,Th8
             .= (Cs2.(4*i+4)).b by A25,A41,A51,A53,Th8;
     thus (Cs.(4*i+j)).IC SCM = (Cs2.(4*i+j)).IC SCM by A37,A43,A47,A51,A54;
     thus (Cs.(4*i+j)).a = (Cs2.(4*i+j)).a
       by A37,A44,A48,A52,A55;
     thus (Cs.(4*i+j)).b = (Cs2.(4*i+j)).b
       by A37,A45,A49,A53,A56;
     end;
     suppose
A57:    IC Cs2.(4*i) = il.4;
A58:    4*i + j >= 4*i by NAT_1:11;
         IC Cs.(4*i) = il.4 by A34,A57;
      then s1 halts_at IC Cs.(4*i) & s2 halts_at IC Cs2.(4*i) by A23,A25,A57,
Lm1;
      then Cs.(4*i+j) = Cs.(4*i) & Cs2.(4*i+j) = Cs2.(4*i) by A58,AMI_3:46;
     hence (Cs.(4*i+j)).IC SCM = (Cs2.(4*i+j)).IC SCM &
          (Cs.(4*i+j)).a = (Cs2.(4*i+j)).a &
          (Cs.(4*i+j)).b = (Cs2.(4*i+j)).b by A34,A35,A36;
    end;
    end;
A59: 4 > 0;
      P[k] from AMI_3:sch 1(A31,A59,A33);
   then (Cs.k)|A = (Cs2.k)|A by A30,AMI_3:26;
    hence (Computation s1).k|dom(p +* s) = (Computation s2).k|dom(p +* s)
     by A27,A29,RELAT_1:185;
   end;
   A60: p +* s is halting
    proof let t be State of SCM;
     assume
A61:    p +* s c= t;
then A62:   q c= t by A10,XBOOLE_1:1;
A63:   t starts_at il.0 by A11,A61,AMI_3:49;
A64:   t.a = i1 & t.b = i2 by A16,A61;
     reconsider i1' = i1, i2' = i2 as Element of NAT by A1,INT_1:16;
     set t' = (Computation t).4;
  per cases by XXREAL_0:1;
   suppose i1 > i2;
      then ex k st t halts_at IC (Computation t).k by A1,A62,A63,A64,Lm4;
     hence thesis by AMI_3:40;
   end;
   suppose
A65:   i1 = i2;
       abs(i1) = i1' & abs(i2) = i2' by ABSVALUE:def 1;
    then A66:  i1 mod i2 = i1' mod i2' by Th2
           .= 0 by A65,NAT_D:25;

A67:  t = (Computation t).(4*0) & t' = (Computation t).(4*(0+1)) by
AMI_1:def 19;
    then t'.a = t.b & t'.b = t.a mod t.b by A1,A62,A63,A64,Lm3;
     then IC t' = il.4 by A1,A62,A63,A64,A66,A67,Lm2;
     then t halts_at IC t' by A62,Lm1;
     hence thesis by AMI_3:40;
   end;
   suppose
A68:  i1 < i2;
       abs(i1) = i1' & abs(i2) = i2' by ABSVALUE:def 1;
    then A69:  i1 mod i2 = i1' mod i2' by Th2
           .= i1' by A68,NAT_D:24;

A70:  t = (Computation t).(4*0) & t' = (Computation t).(4*(0+1)) by
AMI_1:def 19;
    then A71:  t'.a = i2 & t'.b = i1 by A1,A62,A63,A64,A69,Lm3;
     then IC t' = il.0 by A1,A62,A63,A64,A70,Lm2;
then A72: t' starts_at il.0 by AMI_3:def 14;
        Euclide-Algorithm c= t' by A62,AMI_3:43;
     then consider k0 being Element of NAT

      such that
A73:   t' halts_at IC (Computation t').k0 by A1,A68,A71,A72,Lm4;
        (Computation t).(k0+4) = (Computation t').k0 by AMI_1:51;
     then t halts_at IC (Computation t).(k0+4) by A73,AMI_3:48;
     hence thesis by AMI_3:40;
    end;
    end;
  hence
   p +* s is pre-program of SCM by A19;
A74: Euclide-Function.s = a .--> (i1 gcd i2) by A1,A2,Th12;
   consider t being State of SCM such that
A75:  p +* s c= t by AMI_3:39;
A76: dom s = { a, b } by A2,FUNCT_4:65;
then A77: a in dom s & b in dom s by TARSKI:def 2;
A78: s c= p +* s by FUNCT_4:26;
then A79: s c= t by A75,XBOOLE_1:1;
       q c= p by FUNCT_4:26;
    then q c= p +* s by A9,XBOOLE_1:1;
then A80: q c= t by A75,XBOOLE_1:1;
A81: t starts_at il.0 by A11,A75,AMI_3:49;
       a in the carrier of SCM;
then A82: a in dom Result t by AMI_3:36;
   s.a = i1 & s.b = i2 by A2,FUNCT_4:66;
   then t.a = i1 & t.b = i2 by A77,A79,GRFUNC_1:8;
   then (Result t).a = i1 gcd i2 by A1,A80,A81,Th10;
then A83: Euclide-Function.s c= Result t by A74,A82,AMI_3:27;
A84: dom s c= dom(p +* s) by A78,RELAT_1:25;
       dom(a .--> (i1 gcd i2)) = { a } by CQC_LANG:5;
    then dom(a .--> (i1 gcd i2)) c= dom s by A76,ZFMISC_1:12;
then A85: dom(a .--> (i1 gcd i2)) c= dom(p +* s) by A84,XBOOLE_1:1;
      Result(p +* s) = (Result t)|dom(p +* s) by A19,A60,A75,AMI_1:def 28;
  hence Euclide-Function.s c= Result(p +* s) by A74,A83,A85,RELAT_1:186;
 end;