:: 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, ABSVALUE, FUNCT_1, AMI_3, AMI_1, CAT_1,
      FUNCT_4, RELAT_1, BOOLE, AMI_2, INT_2, PARTFUN1, FUNCOP_1, AMI_4, ARYTM;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, RELAT_1, FUNCT_1,
      INT_1, NAT_1, NAT_D, FUNCOP_1, INT_2, STRUCT_0, PARTFUN1, AMI_1, SCMNORM,
      AMI_3, XXREAL_0;
 constructors ENUMSET1, XXREAL_0, NAT_1, NAT_D, AMI_3;
 registrations SETFAM_1, ORDINAL1, RELSET_1, FRAENKEL, NUMBERS, XXREAL_0,
      XREAL_0, NAT_1, INT_1, CARD_3, STRUCT_0, AMI_3, AMI_1, XBOOLE_0,
      FINSEQ_1, FINSET_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions FUNCOP_1, AMI_1, TARSKI, AMI_3;
 theorems AMI_1, INT_1, ABSVALUE, INT_2, TARSKI, ENUMSET1, NAT_1, FUNCOP_1,
      PARTFUN1, FUNCT_4, FUNCT_1, GRFUNC_1, ZFMISC_1, AMI_3, RELAT_1, RELSET_1,
      XBOOLE_0, XBOOLE_1, NEWTON, XXREAL_0, ORDINAL1, NAT_D, CARD_1, AMI_2,
      CARD_3;
 schemes NAT_1, NAT_D, FUNCT_1, RELSET_1, NEWTON;

begin :: Preliminaries

reserve i,j,k for Element of NAT;

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

Lm1: a <> b & b <> c & c <> a by AMI_3:52;

begin :: Euclide algorithm

definition let i be Nat, I be Instruction of SCM;
 redefine func i .--> I -> programmed FinPartState of SCM;
 correctness
  proof i in NAT by ORDINAL1:def 13;
   then reconsider i as Instruction-Location of SCM by AMI_1:def 4;
    i .--> I is programmed FinPartState of SCM;
   hence thesis;
  end;
end;

definition
  func Euclide-Algorithm -> programmed FinPartState of SCM equals
  (0 .--> (dl.2 := dl.1)) +* ((1 .--> Divide(dl.0,dl.1)) +*
  ((2 .--> (dl.0 := dl.2)) +* ((3 .--> (dl.1 >0_goto il.0)) +*
  (4 .--> halt SCM))));
  coherence;
end;

defpred P[State of SCM] means $1.0 = c := b & $1.1 = Divide(a,b) &
$1.2 = a := c & $1.3 = b >0_goto il.0 & $1 halts_at 4;
set IN0 = 0 .--> (dl.2 := b);
set IN1 = 1 .--> Divide(a,b);
set IN2 = 2 .--> (a := dl.2);
set IN3 = 3 .--> (b >0_goto il.0);
set IN4 = 4 .--> halt SCM;
set EA3 = IN3 +* IN4;
set EA2 = IN2 +* EA3;
set EA1 = IN1 +* EA2;
set EA0 = IN0 +* EA1;

canceled 3;

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

Lm2: for s being State of SCM st Euclide-Algorithm c= s holds P[s]
proof
  let s be State of SCM;
A1: dom IN1 = { 1 } by FUNCOP_1:19;
A2: dom IN2 = { 2 } by FUNCOP_1:19;
A3: dom IN3 = { 3 } by FUNCOP_1:19;
A4: dom IN4 = { 4 } by FUNCOP_1:19;
  then
A5: dom EA3 = { 3 } \/ { 4 } by A3,FUNCT_4:def 1
    .= { 3,4 } by ENUMSET1:41;
  then
A6: dom EA2 = { 2 } \/ { 3,4 } by A2,FUNCT_4:def 1
    .= { 2,3,4 } by ENUMSET1:42;
  then
A7: dom EA1 = { 1 } \/ { 2,3,4 } by A1,FUNCT_4:def 1
    .= { 1,2,3,4 } by ENUMSET1:44;
  assume
A8: Euclide-Algorithm c= s;
A9: not 0 in dom EA1 by A7;
  0 in dom EA0 by Th4,ENUMSET1:def 3,CARD_1:91;
  hence s.0 = EA0.0 by A8,GRFUNC_1:8
    .= IN0.0 by A9,FUNCT_4:12
    .= c := b by FUNCOP_1:87;
  EA1 c= EA0 by FUNCT_4:26;
  then
A10: EA1 c= s by A8,XBOOLE_1:1;
A11: not 1 in dom EA2 by A6,ENUMSET1:def 1;
  1 in dom EA1 by A7,ENUMSET1:def 2;
  hence s.1 = EA1.1 by A10,GRFUNC_1:8
    .= IN1.1 by A11,FUNCT_4:12
    .= Divide(a,b) by FUNCOP_1:87;
  EA2 c= EA1 by FUNCT_4:26;
  then
A12: EA2 c= s by A10,XBOOLE_1:1;
A13: not 2 in dom EA3 by A5,TARSKI:def 2;
  2 in dom EA2 by A6,ENUMSET1:def 1;
  hence s.2 = EA2.2 by A12,GRFUNC_1:8
    .= IN2.2 by A13,FUNCT_4:12
    .= a := c by FUNCOP_1:87;
  EA3 c= EA2 by FUNCT_4:26;
  then
A14: EA3 c= s by A12,XBOOLE_1:1;
A15: not 3 in dom IN4 by A4,TARSKI:def 1;
  3 in dom EA3 by A5,TARSKI:def 2;
  hence s.3 = EA3.3 by A14,GRFUNC_1:8
    .= IN3.3 by A15,FUNCT_4:12
    .= b >0_goto il.0 by FUNCOP_1:87;
A16: 4 in dom EA3 by A5,TARSKI:def 2;
A17: 4 in dom IN4 by A4,TARSKI:def 1;
  thus s.4 = EA3.4 by A14,A16,GRFUNC_1:8
    .= IN4.4 by A17,FUNCT_4:14
    .= halt SCM by FUNCOP_1:87;
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) = 0 holds IC  Computation(s,k+1) = 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) = 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,Lm2;
  hence IC  Computation(s,k+1) = Next IC  Computation(s,k) by AMI_3:8
    .= (0+1) by A2
    .= 1;
  thus  Computation(s,k+1).a =  Computation(s,k).a &
   Computation(s,k+1).b =  Computation(s,k).b by A3,AMI_3:52,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) = 1 holds IC  Computation(s,k+1) = 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) = 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,Lm2;
  hence IC  Computation(s,k+1) = Next IC  Computation(s,k) by AMI_3:12
    .= 1+1 by A2
    .= 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,Lm1,AMI_3:12;
end;

theorem Th7:
  for s being State of SCM st Euclide-Algorithm c= s
  for k st IC  Computation(s,k) = 2 holds IC  Computation(s,k+1) = 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) = 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,Lm2;
  hence IC  Computation(s,k+1) = Next IC  Computation(s,k) by AMI_3:8
    .= (2+1) by A2
    .= 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:52,AMI_3:8;
end;

theorem Th8:
  for s being State of SCM st Euclide-Algorithm c= s
  for k st IC  Computation(s,k) = 3 holds
  ( Computation(s,k).dl.1 > 0 implies IC  Computation(s,k+1) = 0) &
  ( Computation(s,k).dl.1 <= 0 implies IC  Computation(s,k+1) = 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) = 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,Lm2;
  hence  Computation(s,k).b > 0 implies IC  Computation(s,k+1) = 0
  by AMI_3:15;
  thus  Computation(s,k).b <= 0 implies IC  Computation(s,k+1) = 4
  proof
    assume  Computation(s,k).b <= 0;
    hence IC  Computation(s,k+1) = Next IC  Computation(s,k) by A3,AMI_3:15
      .= (3+1) by A2
      .= 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) = 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;
  assume IC  Computation(s,k) = 4;
  then s halts_at IC  Computation(s,k) by A1,Lm2;
  hence  Computation(s,k+i) =  Computation(s,k) by AMI_1:89,NAT_1:11;
end;

Lm3: for s being State of SCM st s starts_at 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) = 0 or
 Computation(s,4*k).b = 0 & IC  Computation(s,4*k) = 4)
proof
  let s be State of SCM such that
A1: IC s = 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) = 0 or
   Computation(s,4*$1).b = 0 & IC  Computation(s,4*$1) = 4);
A4: P[0] by A1,A3,AMI_1:13;
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 = 0 or c4.b = 0 & IC c4 = 4;
    now per cases by A10;
      case
A11:    c4.b > 0;
        then
A12:    IC c5 = 1 & c5.a = c4.a & c5.b = c4.b & c5.c = c4.b by A2,A10,Th5;
        then
A13:    IC c6 = 2 & c6.b = c5.a mod c5.b & c6.c = c5.c by A2,A6,Th6;
        then
A14:    IC c7 = 3 & c7.a = c6.c & c7.b = c6.b & c7.c = c6.c by A2,A7,Th7;
        then (c7.b > 0 implies IC c8 = 0) &
        (c7.b <= 0 implies IC c8 = 4) & c8.a = c7.a &
        c8.b = c7.b by A2,A8,Th8;
        hence c8.a > 0 & (c8.b > 0 & IC c8 = 0 or c8.b = 0 & IC c8 = 4)
        by A11,A12,A13,A14,NEWTON:78;
      end;
      case c4.b = 0;
        hence c8.a > 0 & c8.b = 0 & IC c8 = 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;

Lm4: for s being State of SCM st s starts_at 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 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 = 0 or c4.b = 0 & IC c4 = 4 by A1,A2,A3,Lm3;
  then
A8: IC c5 = 1 & c5.a = c4.a & c5.b = c4.b & c5.c = c4.b by A2,A4,Th5;
  then
A9: IC c6 = 2 & c6.b = c5.a mod c5.b & c6.c = c5.c by A2,A5,Th6;
  then
A10: IC c7 = 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;

Lm5: for s being State of SCM st s starts_at 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 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;
  reconsider x' = x, y' = y as Element of NAT by A4,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:13
    .= x' by ABSVALUE:def 1;
A8: G(0) = abs(y) by A3,AMI_1:13
    .= 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,Lm3;
    assume
A11: G(k) > 0;
    hence F(k+1) = G(k) by A1,A2,A3,A4,A10,Lm4,ABSVALUE:7;
A12:  Computation(s,4*(k+1)).b >= 0 by A1,A2,A3,A4,Lm3;
A13:  Computation(s,4*k).a >= 0 by A1,A2,A3,A4,Lm3;
    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,Lm4,ABSVALUE:7
      .= F(k) mod G(k) by A10,A13,INT_2:49;
  end;
  consider k such that
A14: F(k) = x' hcf y' and
A15: G(k) = 0 from NEWTON:sch 1(A5,A6,A7,A8,A9);
A16: ( Computation(s,4*k)).a > 0 by A1,A2,A3,A4,Lm3;
   Computation(s,4*k).b = 0 by A15,ABSVALUE:7;
  then
A17: IC  Computation(s,4*k) = 4 by A1,A2,A3,A4,Lm3;
A18: s halts_at 4 by A2,Lm2;
  hence (Result s).a = ( Computation(s,4*k)).a by A17,AMI_1:87
    .= x gcd y by A14,A16,ABSVALUE:def 1;
  thus thesis by A17,A18;
end;

theorem Th10:
  for s being State of SCM st s starts_at 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 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;
A7: abs y = y by A6,ABSVALUE:def 1;
  now per cases by XXREAL_0:1;
    case x > y;
      hence (Result s).a = x gcd y by A1,A2,A3,A4,A6,Lm5;
    end;
    case
A8:   x = y;
      take s' =  Computation(s,4);
      reconsider x' = x, y' = y as Element of NAT by A5,A6,INT_1:16;
A9:   x mod y = x' mod y'
        .= 0 by A8,NAT_D:25;
A10:  s =  Computation(s,4*0) & s' =  Computation(s,4*(0+1)) by AMI_1:13;
      then s'.b = 0 by A1,A2,A3,A4,A5,A6,A9,Lm4;
      then IC s' = 4 by A1,A2,A3,A4,A5,A6,A10,Lm3;
      then s halts_at IC s' by A2,Lm2;
      hence (Result s).a = s'.a by AMI_1:87
        .= y by A1,A2,A3,A4,A5,A6,A10,Lm4
        .= x gcd y by A7,A8,NAT_D:32;
    end;
    case
A11:  y > x;
      take s' =  Computation(s,4);
      reconsider x' = x, y' = y as Element of NAT by A5,A6,INT_1:16;
A12:  x mod y = x' mod y'
        .= x' by A11,NAT_D:24;
A13:  s =  Computation(s,4*0) & s' =  Computation(s,4*(0+1)) by
      AMI_1:13;
      then
A14:  s'.a = y & s'.b = x by A1,A2,A3,A4,A5,A6,A12,Lm4;
      then IC s' = 0 by A1,A2,A3,A4,A5,A6,A13,Lm3;
      then
A15:  s' starts_at 0 by AMI_1:def 41;
A16:  Euclide-Algorithm c= s' by A2,AMI_1:86;
      then consider k0 being Element of NAT such that
A17:  s' halts_at IC  Computation(s',k0) by A5,A11,A14,A15,Lm5;
       Computation(s,k0+4) =  Computation(s',k0) by AMI_1:51;
      then
A18:  s halts_at IC  Computation(s,k0+4) by A17,AMI_1:91;
      (Result s').a = x gcd y by A5,A11,A14,A15,A16,Lm5;
      hence (Result s).a = x gcd y by A18,AMI_1:90;
    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 AMI_3:52,FUNCT_4:66
        .= x2 by A2,A3,AMI_3:52,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;
    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;
    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];
A11: for p,q being Element of FinPartSt SCM holds [p,q] in IT1 iff P[p,q]
    proof
      let p,q being Element of FinPartSt SCM;
      thus [p,q] in IT1 implies P[p,q]
      proof
        assume
A12:    [p,q] in IT1;
        reconsider p,q as FinPartState of SCM by AMI_1:125;
        P[p,q] by A9,A12;
        hence thesis;
      end;
      thus thesis by A9;
    end;
A13: for p,q being Element of FinPartSt SCM holds [p,q] in IT2 iff P[p,q]
    proof
      let p,q being Element of FinPartSt SCM;
      thus [p,q] in IT2 implies P[p,q]
      proof
        assume
A14:    [p,q] in IT2;
        reconsider p,q as FinPartState of SCM by AMI_1:125;
        P[p,q] by A10,A14;
        hence thesis;
      end;
      thus thesis by A10;
    end;
    thus IT1 = IT2 from RELSET_1:sch 4(A11,A13);
  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_1:125;
    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 } \/ 5 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 5 by A5,A7,XBOOLE_0:def 2;
    then
A8: x = IC SCM or x = 0 or x = 1 or x = 2 or x = 3 or x = 4
    by ENUMSET1:def 3,TARSKI:def 1,CARD_1:91;
    x = a or x = b by A3,A7,TARSKI:def 2;
    hence contradiction by A8,AMI_3:56,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 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 <> 0 & IC SCM <> 1 & IC SCM <> 2 &
    IC SCM <> 3 & IC SCM <> 4 by AMI_3:57;
    then
A15: not IC SCM in dom q by Th4,ENUMSET1:def 3,CARD_1:91;
    thus IC(p +* s) = (p +* s).IC SCM by A12,A13,AMI_1:def 43
      .= p.IC SCM by A14,FUNCT_4:12
      .= (Start-At il.0).IC SCM by A15,FUNCT_4:12
      .= 0 by FUNCOP_1:87;
  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,AMI_3:52,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 0 by A11,A20,AMI_1:92;
A23: Euclide-Algorithm c= s1 by A10,A20,XBOOLE_1:1;
A24: s2 starts_at 0 by A11,A21,AMI_1:92;
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 = 5;
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;
A28: Euclide-Algorithm c=  Computation(s2,k) by A25,AMI_1:86;
    Euclide-Algorithm c=  Computation(s1,k) by A23,AMI_1:86;
    then
A29: ( Computation(s1,k))|C = Euclide-Algorithm by Th4,GRFUNC_1:64
      .= ( Computation(s2,k))|C by A28,Th4,GRFUNC_1:64;
A30: dom( Computation(s1,k)) = the carrier of SCM by AMI_1:79
      .= dom( Computation(s2,k)) by AMI_1:79;
    defpred P[Element of NAT] means
     Computation(s1,$1).IC SCM =  Computation(s2,$1).IC SCM &
      Computation(s1,$1).a =  Computation(s2,$1).a &
      Computation(s1,$1).b =  Computation(s2,$1).b;
A31: P[0]
    proof
A32:   Computation(s1,0) = s1 &  Computation(s2,0) = s2 by AMI_1:13;
      thus ( Computation(s1,0)).IC SCM = IC s1 by AMI_1:13
        .= 0 by A22,AMI_1:def 41
        .= IC s2 by A24,AMI_1:def 41
        .= ( Computation(s2,0)).IC SCM by AMI_1:13;
      thus ( Computation(s1,0)).a = ( Computation(s2,0)).a &
       ( Computation(s1,0)).b = ( Computation(s2,0)).b by A16,A20,A26,A32;
    end;
A33: for i,j being Nat st P[4*i] & j<>0 & j<=4 holds P[4*i+j]
    proof
      let i,j be Nat;
      assume that
A34:   Computation(s1,4*i).IC SCM =  Computation(s2,4*i).IC SCM and
A35:   Computation(s1,4*i).a =  Computation(s2,4*i).a and
A36:   Computation(s1,4*i).b =  Computation(s2,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;
A38:  i in NAT & j in NAT by ORDINAL1:def 13;
      per cases by A1,A24,A25,A26,A38,Lm3;
      suppose
A39:    IC  Computation(s2,4*i) = 0;
A40:    4*i + 1 + 1 = 4*i + (1 + 1);
A41:    (4*i+2)+1 = 4*i+(2+1);
A42:    4*i + 3 + 1 = 4*i + (3 + 1);
A43:   IC Computation(s1,4*i) = 0 by A34,A39;
        then
A44:    IC  Computation(s1,4*i+1) = 1 &
   IC  Computation(s2,4*i+1) = 1 by A23,A25, A39,Th5;
A45:    ( Computation(s1,4*i+1)).a =  Computation(s1,4*i).a by A23,A43,Th5
          .= ( Computation(s2,4*i+1)).a by A25,A35,A39,Th5;
A46:    ( Computation(s1,4*i+1)).b =  Computation(s1,4*i).b by A23,A43,Th5
          .= ( Computation(s2,4*i+1)).b by A25,A36,A39,Th5;
A47:    ( Computation(s1,4*i+1)).dl.2 =  Computation(s1,4*i).b by A23,A43,Th5
          .= ( Computation(s2,4*i+1)).dl.2 by A25,A36,A39,Th5;
A48:    IC  Computation(s1,4*i+2) = 2 &
IC  Computation(s2,4*i+2) = 2 by A23,A25,A40,A44,Th6;
A49:    ( Computation(s1,4*i+2)).a
           = ( Computation(s1,4*i+1)).a div ( Computation(s1,4*i+1)).b
            by A23,A40,A44,Th6
          .= ( Computation(s2,4*i+2)).a by A25,A40,A44,A45,A46,Th6;
A50:    ( Computation(s1,4*i+2)).b
= ( Computation(s1,4*i+1)).a mod ( Computation(s1,4*i+1)).b
 by A23,A40,A44,Th6
          .= ( Computation(s2,4*i+2)).b by A25,A40,A44,A45,A46,Th6;
A51:    ( Computation(s1,4*i+2)).dl.2 = ( Computation(s1,4*i+1)).dl.2
 by A23,A40,A44,Th6
          .= ( Computation(s2,4*i+2)).dl.2 by A25,A40,A44,A47,Th6;
A52:    IC  Computation(s1,4*i+3) = 3 &
IC  Computation(s2,4*i+3) = 3 by A23,A25,A41,A48,Th7;
A53:    ( Computation(s1,4*i+3)).a = ( Computation(s1,4*i+2)).dl.2
 by A23,A41,A48,Th7
          .= ( Computation(s2,4*i+3)).a by A25,A41,A48,A51,Th7;
A54:    ( Computation(s1,4*i+3)).b = ( Computation(s1,4*i+2)).b
 by A23,A41,A48,Th7
          .= ( Computation(s2,4*i+3)).b by A25,A41,A48,A50,Th7;
        ( Computation(s1,4*i+3)).b <= 0 or ( Computation(s1,4*i+3)).b > 0;
        then
A55:    IC  Computation(s1,4*i+4) = 4 & IC  Computation(s2,4*i+4) = 4 or
    IC  Computation(s1,4*i+4) = 0 & IC  Computation(s2,4*i+4) = 0
 by A23,A25,A42,A52,A54,Th8;
A56:    ( Computation(s1,4*i+4)).a = ( Computation(s1,4*i+3)).a
 by A23,A42,A52,Th8
          .= ( Computation(s2,4*i+4)).a by A25,A42,A52,A53,Th8;
A57:    ( Computation(s1,4*i+4)).b = ( Computation(s1,4*i+3)).b
 by A23,A42,A52,Th8
          .= ( Computation(s2,4*i+4)).b by A25,A42,A52,A54,Th8;
        thus  Computation(s1,4*i+j).IC SCM
        =  Computation(s2,4*i+j).IC SCM by A37,A44,A48,A52,A55;
        thus  Computation(s1,4*i+j).a
        =  Computation(s2,4*i+j).a by A37,A45,A49,A53,A56;
        thus  Computation(s1,4*i+j).b
        =  Computation(s2,4*i+j).b by A37,A46,A50,A54,A57;
      end;
      suppose IC  Computation(s2,4*i) = 4;
        then
X:         s1 halts_at  IC Computation(s1,4*i) &
         s2 halts_at IC  Computation(s2,4*i)
         by A23,A25,A34, Lm2;
        4*i <= 4*i+j by NAT_1:11;
        then  Computation(s1,4*i+j) =  Computation(s1,4*i) &
         Computation(s2,4*i+j) =  Computation(s2,4*i)
         by AMI_1:89,X;
        hence  Computation(s1,4*i+j).IC SCM =  Computation(s2,4*i+j).IC SCM &
         Computation(s1,4*i+j).a =  Computation(s2,4*i+j).a &
         Computation(s1,4*i+j).b =  Computation(s2,4*i+j).b by A34,A35,A36;
      end;
    end;
A58: 4 > 0;
    P[k] from NAT_D:sch 2(A31,A58,A33);
    then ( Computation(s1,k))|A = ( Computation(s2,k))|A by A30,GRFUNC_1:92;
    hence  Computation(s1,k)|dom(p +* s) =  Computation(s2,k)|dom(p +* s)
    by A27,A29,RELAT_1:185;
  end;
A59: p +* s is halting
  proof
    let t be State of SCM;
    assume
A60: p +* s c= t;
    then
A61: q c= t by A10,XBOOLE_1:1;
A62: t starts_at 0 by A11,A60,AMI_1:92;
A63: t.a = i1 & t.b = i2 by A16,A60;
    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,A61,A62,A63,Lm5;
      hence thesis by AMI_1:83;
    end;
    suppose
A64:  i1 = i2;
A65:  i1 mod i2 = i1' mod i2'
        .= 0 by A64,NAT_D:25;
A66:  t =  Computation(t,4*0) & t' =  Computation(t,4*(0+1)) by
      AMI_1:13;
      then t'.a = t.b & t'.b = t.a mod t.b by A1,A61,A62,A63,Lm4;
      then IC t' = 4 by A1,A61,A62,A63,A65,A66,Lm3;
      then t halts_at IC t' by A61,Lm2;
      hence thesis by AMI_1:83;
    end;
    suppose
A67:  i1 < i2;
A68:  i1 mod i2 = i1' mod i2'
        .= i1' by A67,NAT_D:24;
A69:  t =  Computation(t,4*0) & t' =  Computation(t,4*(0+1)) by
      AMI_1:13;
      then
A70:  t'.a = i2 & t'.b = i1 by A1,A61,A62,A63,A68,Lm4;
      then IC t' = 0 by A1,A61,A62,A63,A69,Lm3;
      then
A71:  t' starts_at 0 by AMI_1:def 41;
      Euclide-Algorithm c= t' by A61,AMI_1:86;
      then consider k0 being Element of NAT such that
A72:  t' halts_at IC  Computation(t',k0) by A1,A67,A70,A71,Lm5;
       Computation(t,k0+4) =  Computation(t',k0) by AMI_1:51;
      then t halts_at IC  Computation(t,k0+4) by A72,AMI_1:91;
      hence thesis by AMI_1:83;
    end;
  end;
  hence p +* s is pre-program of SCM by A19;
A73: Euclide-Function.s = a .--> (i1 gcd i2) by A1,A2,Th12;
  consider t being State of SCM such that
A74: p +* s c= t by CARD_3:97;
A75: dom s = { a, b } by A2,FUNCT_4:65;
  then
A76: a in dom s & b in dom s by TARSKI:def 2;
A77: s c= p +* s by FUNCT_4:26;
  then
A78: s c= t by A74,XBOOLE_1:1;
  q c= p by FUNCT_4:26;
  then
A79: q c= p +* s by A9,XBOOLE_1:1;
A80: t starts_at 0 by A11,A74,AMI_1:92;
  a in the carrier of SCM;
  then
A81: a in dom Result t by AMI_1:79;
  s.a = i1 & s.b = i2 by A2,AMI_3:52,FUNCT_4:66;
  then t.a = i1 & t.b = i2 by A76,A78,GRFUNC_1:8;
  then
A82: (Result t).a = i1 gcd i2 by A1,A74,A79,A80,Th10,XBOOLE_1:1;
A83: dom s c= dom(p +* s) by A77,RELAT_1:25;
  dom(a .--> (i1 gcd i2)) = { a } by FUNCOP_1:19;
  then dom(a .--> (i1 gcd i2)) c= dom s by A75,ZFMISC_1:12;
  then
A84: dom(a .--> (i1 gcd i2)) c= dom(p +* s) by A83,XBOOLE_1:1;
  Result(p +* s) = (Result t)|dom(p +* s) by A19,A59,A74,AMI_1:def 28;
  hence Euclide-Function.s c= Result(p +* s) by A73,A81,A82,A84,FUNCT_4:90,
  RELAT_1:186;
end;