The Mizar article:

Justifying the Correctness of the Fibonacci Sequence and the Euclide Algorithm by Loop-Invariant

by
Jing-Chao Chen

Received June 14, 2000

Copyright (c) 2000 Association of Mizar Users

MML identifier: SCPINVAR
[ MML identifier index ]


environ

 vocabulary AMI_3, AMI_1, SCMPDS_2, SCMPDS_4, ARYTM_3, ARYTM_1, NAT_1, INT_1,
      ABSVALUE, INT_2, SCMFSA6A, FUNCT_1, SCMPDS_3, SCMFSA_7, RELAT_1, CARD_1,
      CARD_3, SQUARE_1, AMI_2, SCMPDS_5, SCMPDS_8, SCMFSA6B, SCMFSA_9,
      UNIALG_2, SCMFSA7B, SCMP_GCD, SEMI_AF1, FINSEQ_1, SCPISORT, RLVECT_1,
      SFMASTR2, PRE_FF, FUNCT_4, RELOC, FUNCT_7, SCM_1, BOOLE, AMI_5, SCMFSA8B,
      SCPINVAR;
 notation XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, GROUP_1, RELAT_1,
      FUNCT_1, FUNCT_4, INT_1, INT_2, NAT_1, STRUCT_0, AMI_1, AMI_2, AMI_3,
      FUNCT_7, SCMPDS_2, SCMPDS_3, CARD_1, SCMPDS_4, SCM_1, SCMPDS_6, SCMP_GCD,
      SCMPDS_5, SCMPDS_8, SQUARE_1, FUNCT_2, AMI_5, CARD_3, DOMAIN_1, FINSEQ_1,
      TREES_4, WSIERP_1, PRE_FF, SCPISORT;
 constructors REAL_1, DOMAIN_1, AMI_5, RECDEF_1, SCMPDS_4, SCM_1, SCMPDS_6,
      SCMP_GCD, SCMPDS_8, SCMPDS_5, SQUARE_1, PRE_FF, SCPISORT, INT_2, NAT_1,
      WSIERP_1, MEMBERED, RAT_1;
 clusters AMI_1, INT_1, FUNCT_1, SCMPDS_2, SCMFSA_4, SCMPDS_4, SCMPDS_6,
      SCMPDS_8, SCMPDS_5, RELSET_1, WSIERP_1, FRAENKEL, MEMBERED, NUMBERS,
      ORDINAL2;
 requirements NUMERALS, REAL, SUBSET, ARITHM;
 theorems AMI_1, AMI_3, NAT_1, REAL_1, TARSKI, FUNCT_4, INT_1, AMI_5, SCMPDS_2,
      SCMPDS_3, ABSVALUE, GRFUNC_1, AXIOMS, SCMPDS_4, SCMPDS_5, REAL_2,
      SCMPDS_6, ENUMSET1, INT_2, SCMPDS_8, RELAT_1, SCMP_GCD, SCMPDS_7,
      FUNCT_1, SCMFSA6B, SCM_1, SQUARE_1, FINSEQ_1, RVSUM_1, FINSEQ_2, PRE_FF,
      SCPISORT, XBOOLE_1, XCMPLX_0, XCMPLX_1;
 schemes NAT_1, SCMPDS_8, FUNCT_2;

begin :: Preliminaries

reserve m,n for Nat,
        i,j for Instruction of SCMPDS,
        I for Program-block,
        a for Int_position;

theorem Th1:
 for n,m,l be Nat st n divides m & n divides l holds n divides m-l
proof let n,m,l be Nat;
    assume A1: n divides m & n divides l;
then A2:  m = n * (m div n) by NAT_1:49;
A3:  -l =-n*(l div n) by A1,NAT_1:49
     .=n*(-(l div n)) by XCMPLX_1:175;
       m - l = m+ -l by XCMPLX_0:def 8
     .=n * ((m div n) + -(l div n)) by A2,A3,XCMPLX_1:8;
    hence n divides m - l by INT_1:def 9;
end;

theorem Th2:
   m divides n iff m divides (n qua Integer)
proof
   reconsider nn=n as Integer;
   thus m divides n implies m divides (n qua Integer)
   proof
       assume m divides n;
     then consider t be Nat such that
A1:   n = m * t by NAT_1:def 3;
      thus m divides (n qua Integer) by A1,INT_1:def 9;
   end;
   hereby
       assume A2: m divides (n qua Integer);
       per cases;
       suppose n=0;
       hence m divides n by NAT_1:53;
       suppose n<>0;
then A3:    n > 0 by NAT_1:19;
     consider t be Integer such that
A4:   nn = m * t by A2,INT_1:def 9;
    0 < m & 0 < t or m < 0 & t < 0 by A3,A4,SQUARE_1:26;
      then reconsider k=t as Nat by INT_1:16,NAT_1:18;
        n = m * k by A4;
     hence m divides n by NAT_1:def 3;
    end;
end;

theorem Th3:
  m hcf n= m hcf abs(n-m)
proof
   set x=m hcf n,
       y=m hcf abs( n - m );
A1:  x divides m & x divides n by NAT_1:def 5;
A2:  y divides m by NAT_1:def 5;
    per cases;
    suppose A3: n-m >= 0;
      then reconsider nm=n-m as Nat by INT_1:16;
A4:   abs( n - m )=nm by A3,ABSVALUE:def 1;
        x divides n-m by A1,Th1;
then x divides abs( nm ) by A4,Th2;
then A5:   x divides y by A1,NAT_1:def 5;
        y divides nm by A4,NAT_1:def 5;
then A6:   y divides nm+m by A2,NAT_1:55;
        nm+m=n+-m+m by XCMPLX_0:def 8
      .=n by XCMPLX_1:139;
      then y divides x by A2,A6,NAT_1:def 5;
     hence x=y by A5,NAT_1:52;

    suppose n-m < 0;
then A7:   abs( n - m )=-(n-m) by ABSVALUE:def 1
      .=m-n by XCMPLX_1:143;
      then reconsider mn=m-n as Nat;
        x divides m-n by A1,Th1;
then x divides abs( n-m ) by A7,Th2;
then A8:   x divides y by A1,NAT_1:def 5;
        y divides mn by A7,NAT_1:def 5;
then A9:   y divides mn-m by A2,Th1;
    reconsider nn=n as Integer;
        mn-m=-n+m-m by XCMPLX_0:def 8
      .=-n by XCMPLX_1:26;
      then y divides nn by A9,INT_2:14;
      then y divides n by Th2;
      then y divides x by A2,NAT_1:def 5;
     hence x=y by A8,NAT_1:52;
end;

theorem Th4:
  for a,b be Integer st a>=0 & b>=0 holds a gcd b = a gcd (b-a)
proof
   let a,b be Integer;
   assume A1: a>=0 & b>=0;
  thus
    a gcd b=abs(a) hcf abs(b) by INT_2:def 3
  .=abs(a) hcf abs(abs(b)-abs(a)) by Th3
  .=abs(a) hcf abs(b-abs(a)) by A1,ABSVALUE:def 1
  .=abs(a) hcf abs(b-a) by A1,ABSVALUE:def 1
  .=a gcd (b-a) by INT_2:def 3;
end;

theorem Th5:
   (i ';' j ';' I).inspos 0=i & (i ';' j ';' I).inspos 1=j
proof
      set jI=j ';' I;
A1:  i ';' j ';' I =i ';' jI by SCMPDS_4:52
     .=Load i ';' jI by SCMPDS_4:def 4;
   inspos 0 in dom Load i by SCMPDS_5:2;
     hence (i ';' j ';' I).inspos 0
         =(Load i).inspos 0 by A1,SCMPDS_4:37
         .=i by SCMPDS_5:4;
A2:  card Load i=1 by SCMPDS_5:6;
       card jI=card I+1 by SCMPDS_6:15;
      then 0 <> card jI by NAT_1:21;
      then 0 < card jI by NAT_1:19;
then A3:  inspos 0 in dom jI by SCMPDS_4:1;
A4:  inspos 0 in dom Load j by SCMPDS_5:2;
     thus (i ';' j ';' I).inspos 1
         =(Load i ';' jI).inspos (0+1) by A1
         .=(Load i ';' jI).(inspos 0+1) by SCMPDS_3:def 3
         .=jI.inspos 0 by A2,A3,SCMPDS_4:38
         .=(Load j ';' I).inspos 0 by SCMPDS_4:def 4
         .=(Load j).inspos 0 by A4,SCMPDS_4:37
         .=j by SCMPDS_5:4;
end;

theorem Th6:
 for a,b be Int_position holds
 (ex f be Function of product the Object-Kind of SCMPDS,NAT st
     for s being State of SCMPDS holds
 (s.a = s.b implies f.s =0) & (s.a <> s.b implies f.s=max(abs(s.a),abs(s.b))))
proof let a,b be Int_position;
    defpred P[set,set] means ex t be State of SCMPDS st
    t=$1 & (t.a = t.b implies $2 =0) &
    (t.a <> t.b implies $2=max(abs(t.a),abs(t.b)));
A1: now let s be State of SCMPDS;
       per cases;
       suppose A2:s.a = s.b;
        reconsider y=0 as Element of NAT;
        take y;
        thus P[s,y] by A2;
       suppose A3: s.a <> s.b;
        set mm=max(abs(s.a),abs(s.b));
        reconsider y=mm as Element of NAT by SQUARE_1:49;
        take y;
        thus P[s,y] by A3;
   end;
  ex f be Function of product the Object-Kind of SCMPDS,NAT st
     for s being State of SCMPDS holds P[s,f.s] from FuncExD(A1);
   then consider f be Function of product the Object-Kind of SCMPDS,NAT
   such that
A4: for s be State of SCMPDS holds P[s,f.s];
    take f;
    hereby
       let s be State of SCMPDS;
         P[s,f.s] by A4;
       hence (s.a = s.b implies f.s =0) &
        (s.a <> s.b implies f.s=max(abs(s.a),abs(s.b)));
    end;
end;

theorem Th7:
 ex f be Function of product the Object-Kind of SCMPDS,NAT st
     for s being State of SCMPDS holds
 (s.a >= 0 implies f.s =0) & (s.a < 0 implies f.s=-s.a)
proof
    defpred P[set,set] means ex t be State of SCMPDS st
    t=$1 & (t.a >= 0 implies $2 =0) & (t.a < 0 implies $2=-t.a);
A1: now let s be State of SCMPDS;
       per cases;
       suppose A2:s.a >= 0;
        reconsider y=0 as Element of NAT;
        take y;
        thus P[s,y] by A2;
       suppose A3: s.a < 0;
          then -s.a > 0 by REAL_1:66;
        then reconsider y=-s.a as Element of NAT by INT_1:16;
        take y;
        thus P[s,y] by A3;
   end;
  ex f be Function of product the Object-Kind of SCMPDS,NAT st
     for s be State of SCMPDS holds P[s,f.s] from FuncExD(A1);
   then consider f be Function of product the Object-Kind of SCMPDS,NAT
   such that
A4: for s be State of SCMPDS holds P[s,f.s];
    take f;
    hereby
       let s be State of SCMPDS;
         P[s,f.s] by A4;
       hence (s.a >= 0 implies f.s =0) & (s.a < 0 implies f.s=-s.a);
    end;
end;

set A = the Instruction-Locations of SCMPDS,
    D = SCM-Data-Loc;

begin :: Computing directly the result of "while<0" program by loop-invariant

scheme WhileLEnd { F(State of SCMPDS)-> Nat,
 s() -> State of SCMPDS,I() -> No-StopCode shiftable Program-block,
 a() -> Int_position,i() -> Integer,P[set]}:
   F(Dstate IExec(while<0(a(),i(),I()),s()))=0 &
   P[Dstate IExec(while<0(a(),i(),I()),s())]
provided
A1: card I() > 0 and
A2: for t be State of SCMPDS st P[Dstate t] holds
    F(Dstate(t))=0 iff t.DataLoc(s().a(),i()) >= 0 and
A3: P[Dstate s()] and
A4: for t be State of SCMPDS st
       P[Dstate t] & t.a()=s().a() & t.DataLoc(s().a(),i()) < 0
    holds IExec(I(),t).a()=t.a() & I() is_closed_on t &
        I() is_halting_on t & F(Dstate IExec(I(),t)) < F(Dstate t) &
        P[Dstate(IExec(I(),t))]
proof
   set b=DataLoc(s().a(),i()),
       WHL=while<0(a(),i(),I());

    defpred Q[Nat] means
       for t be State of SCMPDS st F(Dstate t) <= $1 &
        t.a()=s().a() & P[Dstate t]
      holds F(Dstate IExec(WHL,t))=0 & P[Dstate IExec(WHL,t)];
A5: Q[0]
    proof
       let t be State of SCMPDS;
       assume A6: F(Dstate t) <= 0 & t.a()=s().a() & P[Dstate t];
       F(Dstate t) >= 0 by NAT_1:18;
then A7:  F(Dstate t)=0 by A6,AXIOMS:21;
     then t.DataLoc(s().a(),i()) >= 0 by A2,A6;
     then for b be Int_position holds IExec(WHL,t).b = t.b by A6,SCMPDS_8:12;
     hence F(Dstate IExec(WHL,t))=0 & P[Dstate IExec(WHL,t)]
      by A6,A7,SCPISORT:5;
   end;
A8: now
       let k be Nat;
       assume A9:Q[k];
         now
         let u be State of SCMPDS;
         assume A10: F(Dstate u) <= k+1 & u.a()=s().a() & P[Dstate u];
         per cases;
         suppose F(Dstate u)=0;
         hence F(Dstate IExec(WHL,u))=0 & P[Dstate IExec(WHL,u)] by A5,A10;

         suppose A11: F(Dstate u) <> 0;
            then A12: u.b < 0 by A2,A10;
        A13: u.DataLoc(u.a(),i()) < 0 by A2,A10,A11;
        defpred X[set] means P[$1];
        deffunc U(State of SCMPDS) = F($1);
        A14: for t be State of SCMPDS st X[Dstate t] & U(Dstate(t))=0 holds
            t.DataLoc(u.a(),i()) >= 0 by A2,A10;
        A15: X[Dstate u] by A10;
        A16: for t being State of SCMPDS st
          X[Dstate t] & t.a()=u.a() & t.DataLoc(u.a(),i()) < 0 holds
            IExec(I(),t).a()=t.a() & I() is_closed_on t &
            I() is_halting_on t & U(Dstate IExec(I(),t)) < U(Dstate t) &
            X[Dstate(IExec(I(),t))] by A4,A10;
           set Iu=IExec(I(),u);
       A17:  (U(u)=U(u) or X[u]) &
            IExec(WHL,u) = IExec(WHL,Iu) from WhileLExec(A1,A13,A14,A15,A16);
              F(Dstate Iu) < F(Dstate u) by A4,A10,A12;
            then F(Dstate Iu)+1 <= F(Dstate u) by INT_1:20;
            then F(Dstate Iu)+1 <= k+1 by A10,AXIOMS:22;
       then A18:  F(Dstate Iu) <= k by REAL_1:53;
       A19:  Iu.a()=s().a() by A4,A10,A12;
              P[Dstate Iu] by A4,A10,A12;
         hence F(Dstate IExec(WHL,u))=0 & P[Dstate IExec(WHL,u)] by A9,A17,A18,
A19;
      end;
      hence Q[k+1];
   end;
A20:  for k being Nat holds Q[k] from Ind(A5,A8);
       Q[F(Dstate s())] by A20;
     hence thesis by A3;
end;

  set a1=intpos 1,
      a2=intpos 2,
      a3=intpos 3;

begin :: An Example : Summing directly n integers by loop-invariant

:: sum=Sum=x1+x2+...+xn

definition
 let n, p0 be Nat;
 func sum(n,p0) -> Program-block equals
:Def1:
  (GBP:=0) ';' (intpos 1:=0) ';'
  (intpos 2:=-n) ';' (intpos 3:=(p0+1)) ';'
  while<0(GBP,2,AddTo(GBP,1,intpos 3,0) ';'
      AddTo(GBP,2,1) ';' AddTo(GBP,3,1));
 coherence;
end;

theorem Th8:        :: SCMPDS_7:73
  for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
  a,b,c being Int_position,n,i,p0 be Nat,f be FinSequence of INT
  st card I >0 & f is_FinSequence_on s,p0 & len f=n & s.b=0 & s.a=0 &
  s.intpos i=-n & s.c = p0+1 &
  (for t be State of SCMPDS st
       (ex g be FinSequence of INT st g is_FinSequence_on s,p0 &
       len g=t.intpos i+n & t.b=Sum g & t.c = p0+1+len g) & t.a=0 &
       t.intpos i < 0 & for i be Nat st i > p0 holds t.intpos i=s.intpos i
    holds IExec(I,t).a=0 & I is_closed_on t & I is_halting_on t &
       IExec(I,t).intpos i=t.intpos i+1 &
       (ex g be FinSequence of INT st g is_FinSequence_on s,p0 &
       len g=t.intpos i+n+1 & IExec(I,t).c = p0+1+len g &
       IExec(I,t).b=Sum g) &
       for i be Nat st i > p0 holds IExec(I,t).intpos i=s.intpos i)
holds IExec(while<0(a,i,I),s).b=Sum f & while<0(a,i,I) is_closed_on s &
      while<0(a,i,I) is_halting_on s
proof
     let s be State of SCMPDS,I be No-StopCode shiftable Program-block,
     a,b,c be Int_position,n,i,p0 be Nat,f be FinSequence of INT;
     assume A1: card I > 0;
     assume A2: f is_FinSequence_on s,p0 & len f=n & s.b=0 &
          s.a=0 & s.intpos i=-n & s.c = p0+1;
     assume A3: for t be State of SCMPDS st
       (ex g be FinSequence of INT st g is_FinSequence_on s,p0 &
       len g=t.intpos i+n & t.b=Sum g & t.c = p0+1+len g) & t.a=0 &
       t.intpos i < 0 & for i be Nat st i > p0 holds t.intpos i=s.intpos i
     holds IExec(I,t).a=0 & I is_closed_on t & I is_halting_on t &
       IExec(I,t).intpos i=t.intpos i+1 &
       (ex g be FinSequence of INT st g is_FinSequence_on s,p0 &
       len g=t.intpos i+n+1 & IExec(I,t).c = p0+1+len g &
       IExec(I,t).b=Sum g) &
       for i be Nat st i > p0 holds IExec(I,t).intpos i=s.intpos i;
     defpred P[State of SCMPDS] means
      (for i be Nat st i > p0 holds $1.intpos i=s.intpos i) &
     (ex g be FinSequence of INT st g is_FinSequence_on s,p0 &
   len g=$1.intpos i+n & $1.b=Sum g & $1.intpos i <= 0 & $1.c = p0+1+len g);

    set da=DataLoc(s.a,i);
    consider ff be Function of product the Object-Kind of SCMPDS,NAT such that
A4: for t be State of SCMPDS holds (t.da >= 0 implies ff.t =0) &
    (t.da < 0 implies ff.t=-t.da) by Th7;
    deffunc F(State of SCMPDS) = ff.$1;
A5: now
        let t be State of SCMPDS;
        set dt=Dstate t;
        assume P[dt];
        hereby
            assume A6: F(dt)=0;
            assume t.da < 0;
          then A7: dt.da < 0 by SCMPDS_8:4;
              then F(dt)=-dt.da by A4;
            hence contradiction by A6,A7,REAL_1:66;
        end;
        assume t.da >= 0;
       then dt.da >= 0 by SCMPDS_8:4;
        hence F(dt)=0 by A4;
    end;
A8: P[Dstate s]
    proof
        set Ds=Dstate s;
      thus for i be Nat st i > p0 holds Ds.intpos i=s.intpos i by SCMPDS_8:4;
         consider h be FinSequence of INT such that
     A9: len h=0 & h is_FinSequence_on s,p0 by SCPISORT:3;
         take h;
        thus h is_FinSequence_on s,p0 by A9;
        thus len h=s.intpos i+n by A2,A9,XCMPLX_0:def 6
             .=Ds.intpos i+n by SCMPDS_8:4;
       h=<*> REAL by A9,FINSEQ_1:32;
         hence Ds.b=Sum h by A2,RVSUM_1:102,SCMPDS_8:4;
               n>=0 by NAT_1:18;
             then -n <= -0 by REAL_1:50;
           hence Ds.intpos i <= 0 by A2,SCMPDS_8:4;
           thus Ds.c = p0+1+len h by A2,A9,SCMPDS_8:4;
    end;
A10: now
      let t be State of SCMPDS;
      set Dt=Dstate t;
      assume A11: P[Dstate t] & t.a=s.a & t.DataLoc(s.a,i) < 0;
    A12: now
          let i be Nat;
          assume A13: i > p0;
          thus t.intpos i=Dt.intpos i by SCMPDS_8:4
          .=s.intpos i by A11,A13;
        end;
       consider h be FinSequence of INT such that
    A14: h is_FinSequence_on s,p0 & len h=Dt.intpos i+n & Dt.b=Sum h &
        Dt.c = p0+1+len h by A11;
A15: len h=t.intpos i+n & t.b=Sum h & t.c = p0+1+len h by A14,SCMPDS_8:4;
    A16: intpos (0+i)=da by A2,SCMP_GCD:5;
      hence IExec(I,t).a=t.a by A2,A3,A11,A12,A14,A15;
      thus I is_closed_on t & I is_halting_on t by A2,A3,A11,A12,A14,A15,A16;
        set It=IExec(I,t);
   A17:  It.intpos i=t.intpos i+1 by A2,A3,A11,A12,A14,A15,A16;
        set Dit=Dstate It;
        hereby
           per cases;
           suppose It.intpos i >= 0;
              then Dit.da >= 0 by A16,SCMPDS_8:4;
          then A18: F(Dit)=0 by A4;
                F(Dt) <> 0 by A5,A11;
            hence F(Dit) < F(Dt) by A18,NAT_1:19;
           suppose It.intpos i < 0;
              then Dit.da < 0 by A16,SCMPDS_8:4;
          then A19: F(Dit)=-Dit.da by A4
               .=-(t.intpos i+1) by A16,A17,SCMPDS_8:4
               .=-t.intpos i-1 by XCMPLX_1:161;
                Dt.da < 0 by A11,SCMPDS_8:4;
              then F(Dt)=-Dt.da by A4
               .=-t.intpos i by A16,SCMPDS_8:4;
            hence F(Dit) < F(Dt) by A19,INT_1:26;
        end;
        consider g be FinSequence of INT such that
  A20:   g is_FinSequence_on s,p0 & len g=t.intpos i+n+1 &
        IExec(I,t).c = p0+1+len g & IExec(I,t).b=Sum
g by A2,A3,A11,A12,A14,A15,A16;
      thus P[Dstate IExec(I,t)]
       proof
        hereby let i be Nat;
          assume A21: i > p0;
          thus Dit.intpos i=It.intpos i by SCMPDS_8:4
          .=s.intpos i by A2,A3,A11,A12,A14,A15,A16,A21;
        end;
        take g;
        thus g is_FinSequence_on s,p0 by A20;
        thus len g=IExec(I,t).intpos i+n by A17,A20,XCMPLX_1:1
          .=Dit.intpos i+n by SCMPDS_8:4;
        thus Dit.b=Sum g by A20,SCMPDS_8:4;
            Dit.intpos i=t.intpos i+1 by A17,SCMPDS_8:4;
        hence Dit.intpos i <= 0 by A11,A16,INT_1:20;
        thus Dit.c = p0+1+len g by A20,SCMPDS_8:4;
      end;
   end;
    set Iw=IExec(while<0(a,i,I),s),
        Dw=Dstate Iw;
A22:  F(Dw)=0 & P[Dw]
     from WhileLEnd(A1,A5,A8,A10);
     then consider g be FinSequence of INT such that
A23:  g is_FinSequence_on s,p0 & len g=Dw.intpos i+n & Dw.b=Sum g &
     Dw.intpos i <= 0;
       Dw.intpos i=Iw.intpos(0+i) by SCMPDS_8:4
      .=Iw.da by A2,SCMP_GCD:5;
     then Dw.intpos i >= 0 by A5,A22;
     then A24: Dw.intpos i=0 by A23,AXIOMS:21;
       now let i be Nat;
          assume i in Seg n;
   then A25:    1 <= i & i <= n by FINSEQ_1:3;
          hence f.i = s.intpos(p0+i) by A2,SCPISORT:def 1
               .=g.i by A23,A24,A25,SCPISORT:def 1;
     end;
then f = g by A2,A23,A24,FINSEQ_2:10;
   hence Iw.b=Sum f by A23,SCMPDS_8:4;
A26:  for t be State of SCMPDS st P[Dstate t] & F(Dstate(t))=0 holds
     t.da >= 0 by A5;
       (F(s)=F(s) or P[s]) & while<0(a,i,I) is_closed_on s &
     while<0(a,i,I) is_halting_on s from WhileLHalt(A1,A26,A8,A10);
     hence thesis;
end;

 set
     j1= AddTo(GBP,1,a3,0),
     j2= AddTo(GBP,2,1),
     j3= AddTo(GBP,3,1),
     WB= j1 ';' j2 ';' j3,
     WH= while<0(GBP,2,WB);
Lm1:
  for s being State of SCMPDS,m be Nat st s.GBP=0 & s.a3=m holds
   IExec(WB,s).GBP=0 & IExec(WB,s).a1=s.a1+s.intpos m &
   IExec(WB,s).a2=s.a2+1 & IExec(WB,s).a3=m+1 &
   for i be Nat st i >3 holds IExec(WB,s).intpos i=s.intpos i
proof
     let s be State of SCMPDS,m be Nat;
     set a=GBP;
     assume A1: s.a=0 & s.a3=m;
   set t0=Initialized s,
       t1=IExec(WB,s),
       t2=IExec(j1 ';' j2,s),
       t3=Exec(j1, t0);
A2: t0.a=0 by A1,SCMPDS_5:40;
A3: t0.a1=s.a1 by SCMPDS_5:40;
A4: t0.a3=m by A1,SCMPDS_5:40;

A5:  DataLoc(t0.a,1)=intpos (0+1) by A2,SCMP_GCD:5;
     then a <> DataLoc(t0.a,1) by SCMP_GCD:4,def 2;
then A6: t3.a=0 by A2,SCMPDS_2:61;
A7: t3.a1=t0.a1+t0.DataLoc(t0.a3,0) by A5,SCMPDS_2:61
     .=t0.a1+t0.intpos(m+0) by A4,SCMP_GCD:5
     .=s.a1+s.intpos m by A3,SCMPDS_5:40;
       a2 <> DataLoc(t0.a,1) by A5,SCMP_GCD:4;
then A8: t3.a2=t0.a2 by SCMPDS_2:61
     .=s.a2 by SCMPDS_5:40;
       a3 <> DataLoc(t0.a,1) by A5,SCMP_GCD:4;
then A9: t3.a3=m by A4,SCMPDS_2:61;

A10:  DataLoc(t3.a,2)=intpos (0+2) by A6,SCMP_GCD:5;
then A11:  a<>DataLoc(t3.a,2) by SCMP_GCD:4,def 2;
A12: t2.a=Exec(j2,t3).a by SCMPDS_5:47
     .=0 by A6,A11,SCMPDS_2:60;
A13:  a1<>DataLoc(t3.a,2) by A10,SCMP_GCD:4;
A14: t2.a1=Exec(j2,t3).a1 by SCMPDS_5:47
     .=s.a1+s.intpos m by A7,A13,SCMPDS_2:60;
A15: t2.a2=Exec(j2,t3).a2 by SCMPDS_5:47
     .=s.a2+1 by A8,A10,SCMPDS_2:60;
A16:  a3<>DataLoc(t3.a,2) by A10,SCMP_GCD:4;
A17: t2.a3=Exec(j2,t3).a3 by SCMPDS_5:47
     .=m by A9,A16,SCMPDS_2:60;

A18:  DataLoc(t2.a,3)=intpos (0+3) by A12,SCMP_GCD:5;
then A19:  a<>DataLoc(t2.a,3) by SCMP_GCD:4,def 2;
   thus t1.a=Exec(j3,t2).a by SCMPDS_5:46
       .=0 by A12,A19,SCMPDS_2:60;
A20:  a1<>DataLoc(t2.a,3) by A18,SCMP_GCD:4;
   thus t1.a1=Exec(j3,t2).a1 by SCMPDS_5:46
     .=s.a1+s.intpos m by A14,A20,SCMPDS_2:60;
A21:  a2<>DataLoc(t2.a,3) by A18,SCMP_GCD:4;
  thus t1.a2=Exec(j3,t2).a2 by SCMPDS_5:46
     .=s.a2+1 by A15,A21,SCMPDS_2:60;
  thus t1.a3=Exec(j3,t2).a3 by SCMPDS_5:46
     .=m+1 by A17,A18,SCMPDS_2:60;
   hereby let i be Nat;
     assume A22: i >3;
      then A23: intpos i <> DataLoc(t2.a,3) by A18,SCMP_GCD:4;
             i > 2 by A22,AXIOMS:22;
      then A24: intpos i <> DataLoc(t3.a,2) by A10,SCMP_GCD:4;
             i > 1 by A22,AXIOMS:22;
      then A25: intpos i <> DataLoc(t0.a,1) by A5,SCMP_GCD:4;
      thus t1.intpos i=Exec(j3,t2).intpos i by SCMPDS_5:46
       .=t2.intpos i by A23,SCMPDS_2:60
       .=Exec(j2,t3).intpos i by SCMPDS_5:47
       .=t3.intpos i by A24,SCMPDS_2:60
       .=t0.intpos i by A25,SCMPDS_2:61
       .=s.intpos i by SCMPDS_5:40;
   end;
end;

Lm2:
   card WB=3
proof
   thus card WB=card (j1 ';' j2) +1 by SCMP_GCD:8
     .=2+1 by SCMP_GCD:9
     .=3;
end;

Lm3:
  for s being State of SCMPDS,n,p0 be Nat,f be FinSequence of INT
  st p0 >= 3 & f is_FinSequence_on s,p0 &
  len f=n & s.a1=0 & s.GBP=0 & s.a2=-n & s.a3=p0+1
holds IExec(WH,s).a1=Sum f & WH is_closed_on s & WH is_halting_on s
proof
   set a=GBP;
   let s be State of SCMPDS,n,p0 be Nat,f be FinSequence of INT;
   assume A1: p0 >= 3 & f is_FinSequence_on s,p0 &
    len f=n & s.a1=0 & s.a=0 & s.a2=-n & s.a3=p0+1;
      now
       let t be State of SCMPDS;
       given g be FinSequence of INT such that
    A2:  g is_FinSequence_on s,p0 & len g=t.a2+n &
         t.a1=Sum g & t.a3 = p0+1+len g;
       assume A3: t.a=0 & t.a2 < 0;
       assume A4: for i be Nat st i > p0 holds t.intpos i=s.intpos i;
      thus IExec(WB,t).a=0 by A2,A3,Lm1;
      thus WB is_closed_on t & WB is_halting_on t by SCMPDS_6:34,35;
      thus IExec(WB,t).a2=t.a2+1 by A2,A3,Lm1;
      thus ex g be FinSequence of INT st g is_FinSequence_on s,p0 &
       len g=t.a2+n+1 & IExec(WB,t).a3 = p0+1+len g & IExec(WB,t).a1=Sum g
      proof
          consider h be FinSequence of INT such that
        A5: len h=len g+1 & h is_FinSequence_on s,p0 by SCPISORT:3;
           take h;
           thus h is_FinSequence_on s,p0 by A5;
           thus len h=t.a2+n+1 by A2,A5;
           thus IExec(WB,t).a3 =p0+1+len g+1 by A2,A3,Lm1
               .=p0+1+len h by A5,XCMPLX_1:1;
           set m=len h;
           reconsider q = h.m as Element of INT by INT_1:def 2;
       A6: now let i be Nat;
             assume A7: 1 <= i & i <= len h;
            per cases;
                suppose i=len h;
                 hence h.i=(g^<*q*>).i by A5,FINSEQ_1:59;
                suppose i<>len h;
                   then i < len h by A7,REAL_1:def 5;
              then A8:  i <= len g by A5,INT_1:20;
                   then i in Seg (len g) by A7,FINSEQ_1:3;
              then A9:  i in dom g by FINSEQ_1:def 3;
               thus h.i = s.intpos(p0+i) by A5,A7,SCPISORT:def 1
                      .= g.i by A2,A7,A8,SCPISORT:def 1
                      .= (g^<*q*>).i by A9,FINSEQ_1:def 7;
            end;
              len (g^<*q*>)=len h by A5,FINSEQ_2:19;
        then A10: g^<*q*>=h by A6,FINSEQ_1:18;
        A11: m >= 1 by A5,NAT_1:29;
        then A12: p0+m >= p0+1 by AXIOMS:24;
              p0+1 > p0 by REAL_1:69;
        then A13: p0+m > p0 by A12,AXIOMS:22;
          h.m=s.intpos(p0+m) by A5,A11,SCPISORT:def 1
            .=t.intpos(p0+m) by A4,A13
            .=t.intpos(p0+1+len g) by A5,XCMPLX_1:1;
         hence IExec(WB,t).a1=t.a1+h.m by A2,A3,Lm1
               .=Sum h by A2,A10,RVSUM_1:104;
      end;
      hereby
         let i be Nat;
         assume A14: i > p0;
            then i > 3 by A1,AXIOMS:22;
            hence IExec(WB,t).intpos i=t.intpos i by A2,A3,Lm1
            .=s.intpos i by A4,A14;
      end;
   end;
  hence thesis by A1,Lm2,Th8;
end;

Lm4:
  for s being State of SCMPDS,n,p0 be Nat,f be FinSequence of INT
  st p0 >= 3 & f is_FinSequence_on s,p0 & len f=n
  holds IExec(sum(n,p0),s).a1=Sum f & sum(n,p0) is_halting_on s
proof
    let s be State of SCMPDS,n,p0 be Nat,f be FinSequence of INT;
    assume A1: p0 >= 3 & f is_FinSequence_on s,p0 & len f=n;
 set a=GBP,
       i1=a:=0,
       i2=a1:=0,
       i3=a2:=-n,
       i4=a3:=(p0+1),
       t0=Initialized s,
       I4=i1 ';' i2 ';' i3 ';' i4,
       t1=IExec(I4,s),
       t2=IExec(i1 ';' i2 ';' i3,s),
       t3=IExec(i1 ';' i2,s),
       t4=Exec(i1, t0);
A2: t4.a=0 by SCMPDS_2:57;
A3:  a <> a1 by SCMP_GCD:4,def 2;
A4: t3.a=Exec(i2, t4).a by SCMPDS_5:47
      .=0 by A2,A3,SCMPDS_2:57;
A5: t3.a1=Exec(i2, t4).a1 by SCMPDS_5:47
     .=0 by SCMPDS_2:57;
A6:  a <> a2 by SCMP_GCD:4,def 2;
A7: t2.a=Exec(i3, t3).a by SCMPDS_5:46
      .=0 by A4,A6,SCMPDS_2:57;
A8:  a1 <> a2 by SCMP_GCD:4;
A9: t2.a1=Exec(i3, t3).a1 by SCMPDS_5:46
      .=0 by A5,A8,SCMPDS_2:57;
A10:  t2.a2=Exec(i3, t3).a2 by SCMPDS_5:46
     .=-n by SCMPDS_2:57;
A11:  a <> a3 by SCMP_GCD:4,def 2;
A12: t1.a=Exec(i4, t2).a by SCMPDS_5:46
      .=0 by A7,A11,SCMPDS_2:57;
A13:  a1 <> a3 by SCMP_GCD:4;
A14: t1.a1=Exec(i4, t2).a1 by SCMPDS_5:46
      .=0 by A9,A13,SCMPDS_2:57;
A15:  a2 <> a3 by SCMP_GCD:4;
A16: t1.a2=Exec(i4, t2).a2 by SCMPDS_5:46
     .=-n by A10,A15,SCMPDS_2:57;
A17: t1.a3=Exec(i4, t2).a3 by SCMPDS_5:46
     .=p0+1 by SCMPDS_2:57;
       now
        let i be Nat;
        assume A18: 1 <= i & i <= len f;
       A19: p0+1 >= 3+1 by A1,AXIOMS:24;
             p0+i >= p0+ 1 by A18,AXIOMS:24;
       then A20: p0+i >= 4 by A19,AXIOMS:22;
           then p0+i > 3 by AXIOMS:22;
       then A21: intpos (p0+i) <> a3 by SCMP_GCD:4;
             p0+i > 2 by A20,AXIOMS:22;
       then A22: intpos (p0+i) <> a2 by SCMP_GCD:4;
             p0+i > 1 by A20,AXIOMS:22;
       then A23: intpos (p0+i) <> a1 by SCMP_GCD:4;
             p0+i > 0 by A20,AXIOMS:22;
       then A24: intpos (p0+i) <> a by SCMP_GCD:4,def 2;
       thus t1.intpos (p0+i)=Exec(i4, t2).intpos (p0+i) by SCMPDS_5:46
           .=t2.intpos (p0+i) by A21,SCMPDS_2:57
           .=Exec(i3, t3).intpos (p0+i) by SCMPDS_5:46
           .=t3.intpos (p0+i) by A22,SCMPDS_2:57
           .=Exec(i2, t4).intpos (p0+i) by SCMPDS_5:47
           .=t4.intpos (p0+i) by A23,SCMPDS_2:57
           .=t0.intpos (p0+i) by A24,SCMPDS_2:57
           .=s.intpos (p0+i) by SCMPDS_5:40
           .=f.i by A1,A18,SCPISORT:def 1;
      end;
      then f is_FinSequence_on t1,p0 by SCPISORT:def 1;
then A25:  IExec(WH,t1).a1=Sum f & WH is_closed_on t1 & WH is_halting_on t1
        by A1,A12,A14,A16,A17,Lm3;
A26:  sum(n,p0)=I4 ';' WH by Def1;
     hence IExec(sum(n,p0),s).a1=Sum f by A25,SCPISORT:8;
      thus thesis by A25,A26,SCPISORT:10;
end;

theorem
    for s being State of SCMPDS,n,p0 be Nat,f be FinSequence of INT
  st p0 >= 3 & f is_FinSequence_on s,p0 & len f=n
  holds IExec(sum(n,p0),s).intpos 1=Sum f & sum(n,p0) is parahalting
proof
    let s be State of SCMPDS,n,p0 be Nat,f be FinSequence of INT;
    assume A1: p0 >= 3 & f is_FinSequence_on s,p0 & len f=n;
    hence IExec(sum(n,p0),s).a1=Sum f by Lm4;
      now
       let t be State of SCMPDS;
       consider g be FinSequence of INT such that
   A2: len g=n & g is_FinSequence_on t,p0 by SCPISORT:3;
       thus sum(n,p0) is_halting_on t by A1,A2,Lm4;
    end;
    hence thesis by SCMPDS_6:35;
end;

begin :: Computing directly the result of "while>0" program by loop-invariant

scheme WhileGEnd { F(State of SCMPDS)-> Nat,
 s() -> State of SCMPDS,I() -> No-StopCode shiftable Program-block,
 a() -> Int_position,i() -> Integer,P[set]}:
   F(Dstate IExec(while>0(a(),i(),I()),s()))=0 &
   P[Dstate IExec(while>0(a(),i(),I()),s())]
provided
A1: card I() > 0 and
A2: for t be State of SCMPDS st P[Dstate t] holds
    F(Dstate(t))=0 iff t.DataLoc(s().a(),i()) <= 0 and
A3: P[Dstate s()] and
A4: for t be State of SCMPDS st
       P[Dstate t] & t.a()=s().a() & t.DataLoc(s().a(),i()) > 0
    holds IExec(I(),t).a()=t.a() & I() is_closed_on t &
        I() is_halting_on t & F(Dstate IExec(I(),t)) < F(Dstate t) &
        P[Dstate(IExec(I(),t))]
proof
   set b=DataLoc(s().a(),i()),
       WHL=while>0(a(),i(),I());
    defpred Q[Nat] means
       for t be State of SCMPDS st F(Dstate t) <= $1 &
        t.a()=s().a() & P[Dstate t]
      holds F(Dstate IExec(WHL,t))=0 & P[Dstate IExec(WHL,t)];
A5: Q[0]
    proof
       let t be State of SCMPDS;
       assume A6: F(Dstate t) <= 0 & t.a()=s().a() & P[Dstate t];
       F(Dstate t) >= 0 by NAT_1:18;
then A7:  F(Dstate t)=0 by A6,AXIOMS:21;
     then t.DataLoc(s().a(),i()) <= 0 by A2,A6;
     then for b be Int_position holds IExec(WHL,t).b = t.b by A6,SCMPDS_8:23;
     hence F(Dstate IExec(WHL,t))=0 & P[Dstate IExec(WHL,t)] by A6,A7,SCPISORT:
5;
   end;
A8: now
       let k be Nat;
       assume A9:Q[k];
         now
         let u be State of SCMPDS;
         assume A10: F(Dstate u) <= k+1 & u.a()=s().a() & P[Dstate u];
         per cases;
         suppose F(Dstate u)=0;
         hence F(Dstate IExec(WHL,u))=0 & P[Dstate IExec(WHL,u)] by A5,A10;

         suppose A11: F(Dstate u) <> 0;
            then A12: u.b > 0 by A2,A10;
        A13: u.DataLoc(u.a(),i()) > 0 by A2,A10,A11;
        defpred X[set] means P[$1];
        deffunc U(State of SCMPDS) = F($1);
        A14: for t be State of SCMPDS st X[Dstate t] & U(Dstate(t))=0 holds
            t.DataLoc(u.a(),i()) <= 0 by A2,A10;
        A15: X[Dstate u] by A10;
        A16: for t being State of SCMPDS st
            X[Dstate t] & t.a()=u.a() & t.DataLoc(u.a(),i()) > 0 holds
            IExec(I(),t).a()=t.a() & I() is_closed_on t &
            I() is_halting_on t & U(Dstate IExec(I(),t)) < U(Dstate t) &
            X[Dstate(IExec(I(),t))] by A4,A10;
           set Iu=IExec(I(),u);
       A17:  (U(u)=U(u) or X[u]) &
            IExec(WHL,u) = IExec(WHL,Iu) from WhileGExec(A1,A13,A14,A15,A16);
              F(Dstate Iu) < F(Dstate u) by A4,A10,A12;
            then F(Dstate Iu)+1 <= F(Dstate u) by INT_1:20;
            then F(Dstate Iu)+1 <= k+1 by A10,AXIOMS:22;
       then A18:  F(Dstate Iu) <= k by REAL_1:53;
       A19:  Iu.a()=s().a() by A4,A10,A12;
              P[Dstate Iu] by A4,A10,A12;
         hence F(Dstate IExec(WHL,u))=0 & P[Dstate IExec(WHL,u)] by A9,A17,A18,
A19;
      end;
      hence Q[k+1];
   end;
A20:  for k being Nat holds Q[k] from Ind(A5,A8);
       Q[F(Dstate s())] by A20;
     hence thesis by A3;
end;

begin :: An Example : Computing directly Fibonacci sequence by loop-invariant

definition
 let n be Nat;
 func Fib-macro(n) -> Program-block equals
:Def2:
  (GBP:=0) ';' (intpos 1:=0) ';'
  (intpos 2:=1) ';' (intpos 3:=n) ';'
  while>0(GBP,3,((GBP,4):=(GBP,2)) ';' AddTo(GBP,2,GBP,1) ';'
      ((GBP,1):=(GBP,4)) ';' AddTo(GBP,3,-1));
 coherence;
end;

theorem Th10:
  for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
  a,f0,f1 being Int_position,n,i be Nat
  st card I >0 & s.a=0 & s.f0=0 & s.f1=1 & s.intpos i=n &
  (for t be State of SCMPDS,k be Nat st
     n=t.intpos i+k & t.f0=Fib k & t.f1 = Fib (k+1) & t.a=0 & t.intpos i > 0
    holds IExec(I,t).a=0 & I is_closed_on t & I is_halting_on t &
     IExec(I,t).intpos i=t.intpos i-1 &
     IExec(I,t).f0=Fib (k+1) & IExec(I,t).f1 = Fib (k+1+1))
  holds
    IExec(while>0(a,i,I),s).f0=Fib n & IExec(while>0(a,i,I),s).f1=Fib (n+1) &
    while>0(a,i,I) is_closed_on s & while>0(a,i,I) is_halting_on s
proof
     let s be State of SCMPDS,I be No-StopCode shiftable Program-block,
     a,f0,f1 be Int_position,n,i be Nat;
     assume A1: card I > 0;
     assume A2: s.a=0 & s.f0=0 & s.f1=1 & s.intpos i=n;
     assume A3: for t be State of SCMPDS,k be Nat st
       n=t.intpos i+k & t.f0=Fib k & t.f1 = Fib (k+1) & t.a=0 &
       t.intpos i > 0
    holds IExec(I,t).a=0 & I is_closed_on t & I is_halting_on t &
       IExec(I,t).intpos i=t.intpos i-1 &
       IExec(I,t).f0=Fib (k+1) & IExec(I,t).f1 = Fib (k+1+1);

     defpred P[State of SCMPDS] means
      $1.intpos i >= 0 &
     ex k be Nat st n=$1.intpos i+k & $1.f0=Fib k & $1.f1=Fib (k+1);

    set da=DataLoc(s.a,i);
    consider ff be Function of product the Object-Kind of SCMPDS,NAT such that
A4: for t be State of SCMPDS holds (t.da <= 0 implies ff.t =0) &
    (t.da > 0 implies ff.t=t.da) by SCMPDS_8:5;
    deffunc F(State of SCMPDS) = ff.$1;
A5: now
        let t be State of SCMPDS;
        set dt=Dstate t;
        assume P[dt];
        hereby
            assume A6: F(dt)=0;
            assume t.da > 0;
          then dt.da > 0 by SCMPDS_8:4;
            hence contradiction by A4,A6;
        end;
        assume t.da <= 0;
       then dt.da <= 0 by SCMPDS_8:4;
        hence F(dt)=0 by A4;
    end;
A7: P[Dstate s]
    proof
        set Ds=Dstate s;
          Ds.intpos i =n by A2,SCMPDS_8:4;
     hence Ds.intpos i >= 0 by NAT_1:18;
        take k=0;
     thus n=Ds.intpos i+k by A2,SCMPDS_8:4;
     thus Ds.f0=Fib k by A2,PRE_FF:1,SCMPDS_8:4;
     thus Ds.f1=Fib (k+1) by A2,PRE_FF:1,SCMPDS_8:4;
    end;
A8: now
      let t be State of SCMPDS;
      set Dt=Dstate t;
      assume A9: P[Dstate t] & t.a=s.a & t.DataLoc(s.a,i) > 0;
       then consider k be Nat such that
   A10: n=Dt.intpos i+k & Dt.f0=Fib k & Dt.f1=Fib (k+1);
   A11: n=t.intpos i+k & t.f0=Fib k & t.f1=Fib (k+1) by A10,SCMPDS_8:4;
   A12: intpos (0+i)=da by A2,SCMP_GCD:5;
      hence IExec(I,t).a=t.a by A2,A3,A9,A11;
      thus I is_closed_on t & I is_halting_on t by A2,A3,A9,A11,A12;
        set It=IExec(I,t);
   A13:  It.intpos i=t.intpos i-1 by A2,A3,A9,A11,A12;
        set Dit=Dstate It;
        hereby
           per cases;
           suppose It.intpos i <= 0;
              then Dit.da <= 0 by A12,SCMPDS_8:4;
          then A14: F(Dit)=0 by A4;
                F(Dt) <> 0 by A5,A9;
            hence F(Dit) < F(Dt) by A14,NAT_1:19;
           suppose It.intpos i > 0;
              then Dit.da > 0 by A12,SCMPDS_8:4;
          then A15: F(Dit)=Dit.da by A4
               .=t.intpos i-1 by A12,A13,SCMPDS_8:4;
                Dt.da > 0 by A9,SCMPDS_8:4;
              then F(Dt)=Dt.da by A4
               .=t.intpos i by A12,SCMPDS_8:4;
            hence F(Dit) < F(Dt) by A15,INT_1:26;
        end;
      thus P[Dit]
      proof
           t.intpos i >= 1+0 by A9,A12,INT_1:20;
         then t.intpos i-1 >= 0 by SQUARE_1:12;
         hence Dit.intpos i >= 0 by A13,SCMPDS_8:4;
           take m=k+1;
         thus n=t.intpos i+-1+1+k by A11,XCMPLX_1:139
              .=t.intpos i-1+1+k by XCMPLX_0:def 8
              .=Dit.intpos i+1+k by A13,SCMPDS_8:4
              .=Dit.intpos i+m by XCMPLX_1:1;
           It.f0=Fib m & It.f1=Fib (k+1+1) by A2,A3,A9,A11,A12;
        hence Dit.f0=Fib m & Dit.f1=Fib (m+1) by SCMPDS_8:4;
      end;
   end;
    set Iw=IExec(while>0(a,i,I),s),
        Dw=Dstate Iw;
A16: F(Dw)=0 & P[Dw]
     from WhileGEnd(A1,A5,A7,A8);
       Dw.intpos i=Iw.intpos(0+i) by SCMPDS_8:4
      .=Iw.da by A2,SCMP_GCD:5;
     then Dw.intpos i <= 0 by A5,A16;
then A17:  Dw.intpos i=0 by A16,AXIOMS:21;
     consider k be Nat such that
A18:  n=Dw.intpos i+k & Dw.f0=Fib k & Dw.f1=Fib (k+1) by A16;
     thus Iw.f0=Fib n & Iw.f1=Fib (n+1) by A17,A18,SCMPDS_8:4;
A19:  for t be State of SCMPDS st P[Dstate t] & F(Dstate(t))=0 holds
     t.da <= 0 by A5;
       (F(s)=F(s) or P[s]) & while>0(a,i,I) is_closed_on s &
     while>0(a,i,I) is_halting_on s from WhileGHalt(A1,A19,A7,A8);
     hence thesis;
end;

 set
     j1= (GBP,4):=(GBP,2),
     j2= AddTo(GBP,2,GBP,1),
     j3= (GBP,1):=(GBP,4),
     j4= AddTo(GBP,3,-1),
     WB= j1 ';' j2 ';' j3 ';' j4,
     WH= while>0(GBP,3,WB);

Lm5:
  for s being State of SCMPDS st s.GBP=0 holds
    IExec(WB,s).GBP=0 & IExec(WB,s).a1=s.a2 &
    IExec(WB,s).a2=s.a1+s.a2 & IExec(WB,s).a3=s.a3-1
proof
     let s be State of SCMPDS;
     set a=GBP;
     assume A1: s.a=0;
   set t0=Initialized s,
       t1=IExec(WB,s),
       t2=IExec(j1 ';' j2 ';' j3,s),
       t3=IExec(j1 ';' j2,s),
       t4=Exec(j1, t0),
       a4=intpos 4;
A2: t0.a=0 by A1,SCMPDS_5:40;

then A3:  DataLoc(t0.a,4)=intpos (0+4) by SCMP_GCD:5;
     then a <> DataLoc(t0.a,4) by SCMP_GCD:4,def 2;
then A4: t4.a=0 by A2,SCMPDS_2:59;
       a1 <> DataLoc(t0.a,4) by A3,SCMP_GCD:4;
then A5: t4.a1=t0.a1 by SCMPDS_2:59
     .=s.a1 by SCMPDS_5:40;
       a2 <> DataLoc(t0.a,4) by A3,SCMP_GCD:4;
then A6: t4.a2=t0.a2 by SCMPDS_2:59
     .=s.a2 by SCMPDS_5:40;
       a3 <> DataLoc(t0.a,4) by A3,SCMP_GCD:4;
then A7: t4.a3=t0.a3 by SCMPDS_2:59
     .=s.a3 by SCMPDS_5:40;
A8: t4.a4=t0.DataLoc(t0.a,2) by A3,SCMPDS_2:59
     .=t0.intpos(0+2) by A2,SCMP_GCD:5
     .=s.a2 by SCMPDS_5:40;

A9:  DataLoc(t4.a,2)=intpos (0+2) by A4,SCMP_GCD:5;
then A10:  a<>DataLoc(t4.a,2) by SCMP_GCD:4,def 2;
A11: t3.a=Exec(j2,t4).a by SCMPDS_5:47
     .=0 by A4,A10,SCMPDS_2:61;
A12: t3.a2=Exec(j2,t4).a2 by SCMPDS_5:47
     .=t4.a2+t4.DataLoc(t4.a,1) by A9,SCMPDS_2:61
     .=t4.a2+t4.intpos(0+1) by A4,SCMP_GCD:5
     .=s.a2+s.a1 by A5,A6;
A13:  a3<>DataLoc(t4.a,2) by A9,SCMP_GCD:4;
A14: t3.a3=Exec(j2,t4).a3 by SCMPDS_5:47
     .=s.a3 by A7,A13,SCMPDS_2:61;
A15:  a4<>DataLoc(t4.a,2) by A9,SCMP_GCD:4;
A16: t3.a4=Exec(j2,t4).a4 by SCMPDS_5:47
     .=s.a2 by A8,A15,SCMPDS_2:61;

A17:  DataLoc(t3.a,1)=intpos (0+1) by A11,SCMP_GCD:5;
then A18:  a<>DataLoc(t3.a,1) by SCMP_GCD:4,def 2;
A19: t2.a=Exec(j3,t3).a by SCMPDS_5:46
       .=0 by A11,A18,SCMPDS_2:59;
A20: t2.a1=Exec(j3,t3).a1 by SCMPDS_5:46
     .=t3.DataLoc(t3.a,4) by A17,SCMPDS_2:59
     .=t3.intpos(0+4) by A11,SCMP_GCD:5
     .=s.a2 by A16;
A21:  a2<>DataLoc(t3.a,1) by A17,SCMP_GCD:4;
A22: t2.a2=Exec(j3,t3).a2 by SCMPDS_5:46
       .=s.a2+s.a1 by A12,A21,SCMPDS_2:59;
A23:  a3<>DataLoc(t3.a,1) by A17,SCMP_GCD:4;
A24: t2.a3=Exec(j3,t3).a3 by SCMPDS_5:46
       .=s.a3 by A14,A23,SCMPDS_2:59;

A25:  DataLoc(t2.a,3)=intpos (0+3) by A19,SCMP_GCD:5;
then A26:  a<>DataLoc(t2.a,3) by SCMP_GCD:4,def 2;
    thus t1.a=Exec(j4,t2).a by SCMPDS_5:46
       .=0 by A19,A26,SCMPDS_2:60;
A27:  a1<>DataLoc(t2.a,3) by A25,SCMP_GCD:4;
    thus t1.a1=Exec(j4,t2).a1 by SCMPDS_5:46
       .=s.a2 by A20,A27,SCMPDS_2:60;
A28:  a2<>DataLoc(t2.a,3) by A25,SCMP_GCD:4;
    thus t1.a2=Exec(j4,t2).a2 by SCMPDS_5:46
       .=s.a1+s.a2 by A22,A28,SCMPDS_2:60;
    thus t1.a3=Exec(j4,t2).a3 by SCMPDS_5:46
       .=t2.a3+-1 by A25,SCMPDS_2:60
       .=s.a3-1 by A24,XCMPLX_0:def 8;
end;

Lm6:
   card WB=4
proof
   thus card WB=card (j1 ';' j2 ';' j3) +1 by SCMP_GCD:8
     .=card (j1 ';' j2)+1+1 by SCMP_GCD:8
     .=2+1+1 by SCMP_GCD:9
     .=4;
end;

Lm7:
  for s being State of SCMPDS,n be Nat st
   s.GBP=0 & s.a1=0 & s.a2=1 & s.a3=n
holds IExec(WH,s).a1=Fib n & IExec(WH,s).a2=Fib (n+1) &
      WH is_closed_on s & WH is_halting_on s
proof
   set a=GBP;
   let s be State of SCMPDS,n be Nat;
   assume A1: s.GBP=0 & s.a1=0 & s.a2=1 & s.a3=n;
      now
       let t be State of SCMPDS,k be Nat;
       assume A2: n=t.a3+k & t.a1=Fib k & t.a2 = Fib (k+1) & t.a=0 &
        t.a3 > 0;
    hence IExec(WB,t).a=0 by Lm5;
    thus WB is_closed_on t & WB is_halting_on t by SCMPDS_6:34,35;

    thus IExec(WB,t).a3=t.a3-1 by A2,Lm5;
    thus IExec(WB,t).a1=Fib (k+1) by A2,Lm5;
    thus IExec(WB,t).a2 =t.a1+t.a2 by A2,Lm5
         .=Fib (k+1+1) by A2,PRE_FF:1;
   end;
   hence thesis by A1,Lm6,Th10;
end;

Lm8:
  for s being State of SCMPDS,n be Nat holds
   IExec(Fib-macro(n),s).a1=Fib n & IExec(Fib-macro(n),s).a2=Fib (n+1) &
   Fib-macro(n) is_halting_on s
proof
    let s be State of SCMPDS,n be Nat;
 set a=GBP,
     i1=a:=0,
     i2=a1:=0,
     i3=a2:=1,
     i4=a3:=n,
     I4=i1 ';' i2 ';' i3 ';' i4,
     t1=IExec(I4,s),
     t2=IExec(i1 ';' i2 ';' i3,s),
     t3=IExec(i1 ';' i2,s),
     t4=Exec(i1, Initialized s);
A1: t4.a=0 by SCMPDS_2:57;
A2:  a <> a1 by SCMP_GCD:4,def 2;
A3: t3.a=Exec(i2, t4).a by SCMPDS_5:47
      .=0 by A1,A2,SCMPDS_2:57;
A4: t3.a1=Exec(i2, t4).a1 by SCMPDS_5:47
     .=0 by SCMPDS_2:57;
A5:  a <> a2 by SCMP_GCD:4,def 2;
A6: t2.a=Exec(i3, t3).a by SCMPDS_5:46
      .=0 by A3,A5,SCMPDS_2:57;
A7:  a1 <> a2 by SCMP_GCD:4;
A8: t2.a1=Exec(i3, t3).a1 by SCMPDS_5:46
      .=0 by A4,A7,SCMPDS_2:57;
A9:  t2.a2=Exec(i3, t3).a2 by SCMPDS_5:46
     .=1 by SCMPDS_2:57;
A10:  a <> a3 by SCMP_GCD:4,def 2;
A11: t1.a=Exec(i4, t2).a by SCMPDS_5:46
      .=0 by A6,A10,SCMPDS_2:57;
A12:  a1 <> a3 by SCMP_GCD:4;
A13: t1.a1=Exec(i4, t2).a1 by SCMPDS_5:46
      .=0 by A8,A12,SCMPDS_2:57;
A14:  a2 <> a3 by SCMP_GCD:4;
A15: t1.a2=Exec(i4, t2).a2 by SCMPDS_5:46
     .=1 by A9,A14,SCMPDS_2:57;
  t1.a3=Exec(i4, t2).a3 by SCMPDS_5:46
     .=n by SCMPDS_2:57;
then A16:  IExec(WH,t1).a1=Fib n & IExec(WH,t1).a2=Fib (n+1) &
     WH is_closed_on t1 & WH is_halting_on t1 by A11,A13,A15,Lm7;
A17:  Fib-macro(n)=I4 ';' WH by Def2;
     hence IExec(Fib-macro(n),s).a1=Fib n by A16,SCPISORT:8;
     thus IExec(Fib-macro(n),s).a2=Fib (n+1) by A16,A17,SCPISORT:8;
      thus thesis by A16,A17,SCPISORT:10;
end;

theorem
    for s being State of SCMPDS,n be Nat
  holds IExec(Fib-macro(n),s).intpos 1=Fib n &
  IExec(Fib-macro(n),s).intpos 2=Fib (n+1) & Fib-macro(n) is parahalting
proof
    let s be State of SCMPDS,n be Nat;
    thus IExec(Fib-macro(n),s).a1=Fib n &
         IExec(Fib-macro(n),s).a2=Fib (n+1) by Lm8;
      for t be State of SCMPDS holds
       Fib-macro(n) is_halting_on t by Lm8;
    hence thesis by SCMPDS_6:35;
end;

begin :: The construction of while<>0 loop program
:: while (a,i)<>0 do I
definition
 let a be Int_position, i be Integer;
 let I be Program-block;
 func while<>0(a,i,I) -> Program-block equals
:Def3:
   (a,i)<>0_goto 2 ';' goto (card I+2) ';' I ';' goto -(card I+2);
 coherence;
end;

begin :: The basic property of "while<>0" program

theorem Th12:
 for a be Int_position,i be Integer,I be Program-block holds
  card while<>0(a,i,I)= card I +3
proof
  let a be Int_position,i be Integer, I be Program-block;
  set i1=(a,i)<>0_goto 2,
      i2=goto (card I+2),
      i3=goto -(card I+2);
  set I4=i1 ';' i2 ';' I;
    thus card while<>0(a,i,I)=card (I4 ';' i3) by Def3
    .=card I4+1 by SCMP_GCD:8
    .=card (i1 ';' i2)+ card I+1 by SCMPDS_4:45
    .=2+card I +1 by SCMP_GCD:9
    .=card I+ (2+1) by XCMPLX_1:1
    .=card I + 3;
end;

Lm9:
 for a be Int_position,i be Integer,I be Program-block holds
  card stop while<>0(a,i,I)= card I+4
proof
   let a be Int_position,i be Integer,I be Program-block;
   thus card stop while<>0(a,i,I)= card while<>0(a,i,I) +1 by SCMPDS_5:7
   .= card I +3+1 by Th12
   .= card I +(3+1) by XCMPLX_1:1
   .= card I + 4;
end;

theorem Th13:
 for a be Int_position,i be Integer,m be Nat,I be Program-block holds
   m < card I+3 iff inspos m in dom while<>0(a,i,I)
proof
   let a be Int_position,i be Integer,m be Nat,I be Program-block;
     card while<>0(a,i,I)=card I + 3 by Th12;
   hence thesis by SCMPDS_4:1;
end;

theorem Th14:
  for a be Int_position,i be Integer,I be Program-block holds
     inspos 0 in dom while<>0(a,i,I) & inspos 1 in dom while<>0(a,i,I)
proof
   let a be Int_position,i be Integer,I be Program-block;
A1:  3 <= card I+3 by NAT_1:29;
then A2:  0 < card I+3 by AXIOMS:22;
       1 < card I+3 by A1,AXIOMS:22;
     hence thesis by A2,Th13;
end;

theorem Th15:
 for a be Int_position,i be Integer,I be Program-block holds
    while<>0(a,i,I).inspos 0=(a,i)<>0_goto 2 &
    while<>0(a,i,I).inspos 1= goto (card I +2) &
    while<>0(a,i,I).inspos (card I+2)=goto -(card I+2)
proof
    let a be Int_position,i be Integer,I be Program-block;
    set i1=(a,i)<>0_goto 2,
        i2=goto (card I+2),
        i3=goto -(card I+2);
    set I4=i1 ';' i2 ';' I;
A1: card I4=card (i1 ';' i2)+ card I by SCMPDS_4:45
    .=card I +2 by SCMP_GCD:9;
    set WHL=while<>0(a,i,I);
A2: WHL=I4 ';' i3 by Def3;
then A3: WHL=i1 ';' i2 ';' (I ';' i3) by SCMPDS_4:47;
   hence WHL.inspos 0=i1 by Th5;
   thus WHL.inspos 1=i2 by A3,Th5;
   thus WHL.inspos(card I+2)=i3 by A1,A2,SCMP_GCD:10;
end;

Lm10:
 for a be Int_position,i be Integer,I be Program-block holds
   while<>0(a,i,I)= ((a,i)<>0_goto 2) ';' (goto (card I+2) ';' I ';'
   goto -(card I+2))
proof
   let a be Int_position,i be Integer,I be Program-block;
  set i1=(a,i)<>0_goto 2,
      i2=goto (card I+2),
      i3=goto -(card I+2);

   thus while<>0(a,i,I) = i1 ';' i2 ';' I ';' i3 by Def3
       .= i1 ';' (i2 ';' I) ';' i3 by SCMPDS_4:52
       .= i1 ';' (i2 ';' I ';' i3) by SCMPDS_4:51;
end;

theorem Th16:
 for s being State of SCMPDS,I being Program-block,a being Int_position,
 i being Integer st s.DataLoc(s.a,i) = 0 holds
 while<>0(a,i,I) is_closed_on s & while<>0(a,i,I) is_halting_on s
proof
  let s be State of SCMPDS,I be Program-block,a be Int_position,
  i be Integer;
  set b=DataLoc(s.a,i);
  assume A1: s.b = 0;
  set WHL=while<>0(a,i,I),
       pWH=stop WHL,
       iWH=Initialized pWH,
       s3 = s +* iWH,
       C3 = Computation s3,
       s4 = C3.1,
       s5 = C3.2;
  set i1=(a,i)<>0_goto 2,
      i2=goto (card I+2),
      i3=goto -(card I+2);

A2: IC s3 =inspos 0 by SCMPDS_6:21;
      WHL = i1 ';' (i2 ';' I ';' i3 ) by Lm10;
then A3: CurInstr s3 = i1 by SCMPDS_6:22;
A4: (Computation s3).(0 + 1) = Following (Computation s3).0 by AMI_1:def 19
     .= Following s3 by AMI_1:def 19
     .= Exec(i1,s3) by A3,AMI_1:def 18;
A5:  not b in dom iWH & b in dom s by SCMPDS_2:49,SCMPDS_4:31;
       not a in dom iWH & a in dom s by SCMPDS_2:49,SCMPDS_4:31;
then A6: s3.DataLoc(s3.a,i)=s3.b by FUNCT_4:12
     .= 0 by A1,A5,FUNCT_4:12;
       iWH c= s3 by FUNCT_4:26;
then A7:  pWH c= s3 by SCMPDS_4:57;
then A8:  pWH c= s4 by AMI_3:38;
A9:  inspos 1 in dom WHL by Th14;
then A10:  inspos 1 in dom pWH by SCMPDS_6:18;
A11:  IC s4 = s4.IC SCMPDS by AMI_1:def 15
     .= Next IC s3 by A4,A6,SCMPDS_2:67
     .= inspos(0+1) by A2,SCMPDS_4:70;
       s4.inspos 1 = pWH.inspos 1 by A8,A10,GRFUNC_1:8
     .=WHL.inspos 1 by A9,SCMPDS_6:19
     .=i2 by Th15;
then A12:  CurInstr s4 = i2 by A11,AMI_1:def 17;
A13:  (Computation s3).(1 + 1) = Following s4 by AMI_1:def 19
     .= Exec(i2,s4) by A12,AMI_1:def 18;
A14:  pWH c= s5 by A7,AMI_3:38;
A15:  card WHL=card I+3 by Th12;
then A16:  inspos(card I+3) in dom pWH by SCMPDS_6:25;
A17:  IC s5 = s5.IC SCMPDS by AMI_1:def 15
     .= ICplusConst(s4,card I+2) by A13,SCMPDS_2:66
     .= inspos(card I+2+1) by A11,SCMPDS_6:23
     .= inspos(card I+(2+1)) by XCMPLX_1:1;
       s5.inspos(card I+3) = pWH.inspos(card I+3) by A14,A16,GRFUNC_1:8
     .=halt SCMPDS by A15,SCMPDS_6:25;
then A18:  CurInstr s5 = halt SCMPDS by A17,AMI_1:def 17;
       now
       let k be Nat;
          k = 0 or 0 < k by NAT_1:19;
        then A19: k = 0 or 0 + 1 <= k by INT_1:20;
       per cases by A19,REAL_1:def 5;
      suppose k = 0;
          then C3.k = s3 by AMI_1:def 19;
         hence IC C3.k in dom pWH by A2,SCMPDS_4:75;
      suppose k = 1;
         hence IC C3.k in dom pWH by A9,A11,SCMPDS_6:18;
       suppose 1 < k;
         then 1+1 <= k by INT_1:20;
         hence IC C3.k in dom pWH by A16,A17,A18,AMI_1:52;
     end;
     hence WHL is_closed_on s by SCMPDS_6:def 2;
       s3 is halting by A18,AMI_1:def 20;
     hence WHL is_halting_on s by SCMPDS_6:def 3;
end;

theorem Th17:
 for s being State of SCMPDS,I being Program-block,a,c being Int_position,
 i being Integer st s.DataLoc(s.a,i) = 0 holds
 IExec(while<>0(a,i,I),s) = s +* Start-At inspos (card I + 3)
proof
   let s be State of SCMPDS,I be Program-block, a,c be Int_position,
   i be Integer;
   set b=DataLoc(s.a,i);
   assume A1: s.b = 0;
   set WHL=while<>0(a,i,I),
       pWH=stop WHL,
       iWH=Initialized pWH,
       s3 = s +* iWH,
       C3 = Computation s3,
       s4 = C3.1,
       s5 = C3.2;
  set i1=(a,i)<>0_goto 2,
      i2=goto (card I+2),
      i3=goto -(card I+2);
   set SAl=Start-At inspos (card I + 3);

A2: IC s3 =inspos 0 by SCMPDS_6:21;
      WHL = i1 ';' (i2 ';' I ';' i3 ) by Lm10;
then A3: CurInstr s3 = i1 by SCMPDS_6:22;
A4: (Computation s3).(0 + 1) = Following (Computation s3).0 by AMI_1:def 19
     .= Following s3 by AMI_1:def 19
     .= Exec(i1,s3) by A3,AMI_1:def 18;
A5: not b in dom iWH & b in dom s by SCMPDS_2:49,SCMPDS_4:31;
      not a in dom iWH & a in dom s by SCMPDS_2:49,SCMPDS_4:31;
then A6: s3.DataLoc(s3.a,i)=s3.b by FUNCT_4:12
     .= 0 by A1,A5,FUNCT_4:12;
       iWH c= s3 by FUNCT_4:26;
then A7:  pWH c= s3 by SCMPDS_4:57;
then A8:  pWH c= s4 by AMI_3:38;
A9:  inspos 1 in dom WHL by Th14;
then A10:  inspos 1 in dom pWH by SCMPDS_6:18;
A11:  IC s4 = s4.IC SCMPDS by AMI_1:def 15
     .= Next IC s3 by A4,A6,SCMPDS_2:67
     .= inspos(0+1) by A2,SCMPDS_4:70;
       s4.inspos 1 = pWH.inspos 1 by A8,A10,GRFUNC_1:8
     .=WHL.inspos 1 by A9,SCMPDS_6:19
     .=i2 by Th15;
then A12:  CurInstr s4 = i2 by A11,AMI_1:def 17;
A13:  (Computation s3).(1 + 1) = Following s4 by AMI_1:def 19
     .= Exec(i2,s4) by A12,AMI_1:def 18;
A14:  pWH c= s5 by A7,AMI_3:38;
A15:  card WHL=card I+3 by Th12;
then A16:  inspos(card I+3) in dom pWH by SCMPDS_6:25;
A17:  IC s5 = s5.IC SCMPDS by AMI_1:def 15
     .= ICplusConst(s4,card I+2) by A13,SCMPDS_2:66
     .= inspos(card I+2+1) by A11,SCMPDS_6:23
     .= inspos(card I+(2+1)) by XCMPLX_1:1;
       s5.inspos(card I+3) = pWH.inspos(card I+3) by A14,A16,GRFUNC_1:8
     .=halt SCMPDS by A15,SCMPDS_6:25;
then A18:  CurInstr s5 = halt SCMPDS by A17,AMI_1:def 17;
then s3 is halting by AMI_1:def 20;
then A19:  s5 = Result s3 by A18,AMI_1:def 22;
A20:  IExec(WHL,s) = Result s3 +* s | A by SCMPDS_4:def 8;
A21:  dom (s | A) = A by SCMPDS_6:1;
A22:  now let x be set;
        assume
  A23:    x in dom IExec(WHL,s);
  A24:    dom SAl = {IC SCMPDS} by AMI_3:34;
       per cases by A23,SCMPDS_4:20;
       suppose A25: x is Int_position;
         then x <> IC SCMPDS by SCMPDS_2:52;
  then A26:    not x in dom SAl by A24,TARSKI:def 1;
       not x in dom (s | A) by A21,A25,SCMPDS_2:53;
      hence IExec(WHL,s).x = s5.x by A19,A20,FUNCT_4:12
        .= s4.x by A13,A25,SCMPDS_2:66
        .= s3.x by A4,A25,SCMPDS_2:67
        .= s.x by A25,SCMPDS_5:19
        .= (s +* SAl).x by A26,FUNCT_4:12;
      suppose A27: x = IC SCMPDS;
        then x in dom Result s3 & not x in dom (s | A) by A21,AMI_1:48,AMI_5:25
;
      hence IExec(WHL,s).x = s5.x by A19,A20,FUNCT_4:12
        .= inspos(card I + 3) by A17,A27,AMI_1:def 15
        .= (s +* SAl).x by A27,SCMPDS_7:12;
      suppose x is Instruction-Location of SCMPDS;
        hence IExec(WHL,s).x = (s +* SAl).x by SCMPDS_6:27;
    end;
      dom IExec(WHL,s) = the carrier of SCMPDS by AMI_3:36
      .= dom (s +* SAl) by AMI_3:36;
    hence IExec(WHL,s) = s +* SAl by A22,FUNCT_1:9;
end;

theorem
   for s being State of SCMPDS,I being Program-block,a being Int_position,
 i being Integer st s.DataLoc(s.a,i) = 0
 holds IC IExec(while<>0(a,i,I),s) = inspos (card I + 3)
proof
  let s be State of SCMPDS,I be Program-block,a be Int_position,
  i be Integer;
  assume s.DataLoc(s.a,i) = 0;
      then IExec(while<>0(a,i,I),s) =s +* Start-At inspos (card I+ 3) by Th17;
      hence thesis by AMI_5:79;
end;

theorem Th19:
 for s being State of SCMPDS,I being Program-block,a,b being Int_position,
 i being Integer st s.DataLoc(s.a,i) = 0
 holds IExec(while<>0(a,i,I),s).b = s.b
proof
   let s be State of SCMPDS,I be Program-block,a,b be Int_position,
   i be Integer;
    assume s.DataLoc(s.a,i) = 0;
then A1: IExec(while<>0(a,i,I),s) = s +* Start-At inspos (card I + 3) by Th17;
      not b in dom Start-At inspos (card I + 3) by SCMPDS_4:59;
    hence IExec(while<>0(a,i,I),s).b = s.b by A1,FUNCT_4:12;
end;

Lm11:
 for I being Program-block,a being Int_position,i being Integer
 holds Shift(I,2) c= while<>0(a,i,I)
proof
  let I be Program-block,a be Int_position,i be Integer;
   set i1=(a,i)<>0_goto 2,
       i2=goto (card I+2),
       i3=goto -(card I+2);
A1: card (i1 ';' i2)=2 by SCMP_GCD:9;
      while<>0(a,i,I) = i1 ';' i2 ';' I ';' i3 by Def3
     .= i1 ';' i2 ';' I ';' Load i3 by SCMPDS_4:def 5;
    hence thesis by A1,SCMPDS_7:16;
end;

definition
   let I be shiftable Program-block,
   a be Int_position,i be Integer;
   cluster while<>0(a,i,I) -> shiftable;
   correctness
   proof
    set WHL=while<>0(a,i,I),
        i1=(a,i)<>0_goto 2,
        i2=goto (card I+2),
        i3=goto -(card I+2),
        PF= i1 ';' i2 ';' I;
     A1: PF=Load i1 ';' Load i2 ';' I by SCMPDS_4:def 6;
      card PF=card (i1 ';' i2)+ card I by SCMPDS_4:45
    .=2+card I by SCMP_GCD:9;
then A2:  card PF+ -(card I+2) =0 by XCMPLX_0:def 6;
       WHL= PF ';' i3 by Def3;
     hence WHL is shiftable by A1,A2,SCMPDS_4:78;
  end;
end;

definition
   let I be No-StopCode Program-block,
   a be Int_position,i be Integer;
   cluster while<>0(a,i,I) -> No-StopCode;
   correctness
   proof
       card I+2 >= 2 by NAT_1:29;
then A1:  card I +2 >0 by AXIOMS:22;
     then -(card I+2) <> 0 by XCMPLX_1:135;
     then reconsider i3=goto -(card I+2) as No-StopCode Instruction of SCMPDS
       by SCMPDS_5:25;
     reconsider i2=goto (card I+2) as No-StopCode Instruction of SCMPDS
       by A1,SCMPDS_5:25;
       while<>0(a,i,I) =(a,i)<>0_goto 2 ';' i2 ';' I ';' i3 by Def3;
     hence thesis;
   end;
end;

begin :: Computing directly the result of "while<>0" program by loop-invariant

scheme WhileNHalt { F(State of SCMPDS)-> Nat,
 s() -> State of SCMPDS,I() -> No-StopCode shiftable Program-block,
 a() -> Int_position,i() -> Integer,P[set]}:
   while<>0(a(),i(),I()) is_closed_on s() &
   while<>0(a(),i(),I()) is_halting_on s()
provided
A1: card I() > 0 and
A2: (for t be State of SCMPDS st P[Dstate t] & F(Dstate(t))=0 holds
    t.DataLoc(s().a(),i()) = 0) and
A3: P[Dstate s()] and
A4: for t be State of SCMPDS st
       P[Dstate t] & t.a()=s().a() & t.DataLoc(s().a(),i()) <> 0
    holds IExec(I(),t).a()=t.a() & I() is_closed_on t &
        I() is_halting_on t & F(Dstate IExec(I(),t)) < F(Dstate t) &
        P[Dstate(IExec(I(),t))]
proof
   set b=DataLoc(s().a(),i());
   set WHL=while<>0(a(),i(),I()),
       pWH=stop WHL,
       iWH=Initialized pWH,
       pI=stop I(),
       IsI= Initialized pI;
   set i1=(a(),i())<>0_goto 2,
       i2=goto (card I()+2),
       i3=goto -(card I()+2);
    defpred Q[Nat] means
       for t be State of SCMPDS st F(Dstate(t)) <= $1 & P[Dstate t] &
       t.a()=s().a()
       holds WHL is_closed_on t & WHL is_halting_on t;
A5:  Q[0]
      proof
        let t be State of SCMPDS;
        assume A6: F(Dstate t) <= 0 & P[Dstate t] & t.a()=s().a();
          F(Dstate t) >= 0 by NAT_1:18;
        then F(Dstate t)=0 by A6,AXIOMS:21;
        then t.b = 0 by A2,A6;
        hence WHL is_closed_on t & WHL is_halting_on t by A6,Th16;
      end;
A7:  for k be Nat st Q[k] holds Q[k + 1]
     proof
     let k be Nat;
     assume A8: Q[k];
        now
        let t be State of SCMPDS;
        assume A9: F(Dstate t) <= k+1;
        assume A10: P[Dstate t];
        assume A11: t.a()=s().a();
        per cases;
        suppose t.b = 0;
          hence WHL is_closed_on t & WHL is_halting_on t by A11,Th16;
        suppose A12: t.b <> 0;
        set t2 = t +* IsI,
            t3 = t +* iWH,
            C3 = Computation t3,
            t4 = C3.1;
A13:     IExec(I(),t).a()=t.a() & I() is_closed_on t & I() is_halting_on t &
        F(Dstate IExec(I(),t)) < F(Dstate t) &
        P[Dstate(IExec(I(),t))] by A4,A10,A11,A12;
A14:     IsI c= t2 by FUNCT_4:26;
A15:     t2 is halting by A13,SCMPDS_6:def 3;
        then t2 +* IsI is halting by A14,AMI_5:10;
then A16:     I() is_halting_on t2 by SCMPDS_6:def 3;
A17:     I() is_closed_on t2 by A13,SCMPDS_6:38;
A18:     inspos 0 in dom pWH by SCMPDS_4:75;
A19:     IC t3 =inspos 0 by SCMPDS_6:21;
          WHL = i1 ';' (i2 ';' I() ';' i3) by Lm10;
then A20:     CurInstr t3 = i1 by SCMPDS_6:22;
A21:     (Computation t3).(0 + 1) = Following (Computation t3).0 by AMI_1:def
19
        .= Following t3 by AMI_1:def 19
        .= Exec(i1,t3) by A20,AMI_1:def 18;
A22:     not a() in dom iWH & a() in dom t by SCMPDS_2:49,SCMPDS_4:31;
A23:     not b in dom iWH & b in dom t by SCMPDS_2:49,SCMPDS_4:31;
        A24: t3.DataLoc(t3.a(),i())= t3.b by A11,A22,FUNCT_4:12
        .= t.b by A23,FUNCT_4:12;
A25:     IC t4 = t4.IC SCMPDS by AMI_1:def 15
        .= ICplusConst(t3,2) by A12,A21,A24,SCMPDS_2:67
        .= inspos(0+2) by A19,SCMPDS_6:23;
          t2,t3 equal_outside A by SCMPDS_4:36;
then A26:     t2 | D = t3 | D by SCMPDS_4:24;
          now let a;
          thus t2.a = t3.a by A26,SCMPDS_4:23
          .= t4.a by A21,SCMPDS_2:67;
        end;
then A27:    t2 | D = t4 | D by SCMPDS_4:23;

        set m2=LifeSpan t2,
            t5=(Computation t4).m2,
            l2=inspos (card I() + 2);

A28:     IExec(I(),t) = Result t2 +* t | A by SCMPDS_4:def 8;
      dom (t | A) = A by SCMPDS_6:1;
then A29:     not a() in dom (t | A) by SCMPDS_2:53;
          card I() + 2 < card I() + 3 by REAL_1:53;
then A30:     l2 in dom WHL by Th13;
A31:     WHL c= iWH by SCMPDS_6:17;
          iWH c= t3 by FUNCT_4:26;
then A32:     WHL c= t3 by A31,XBOOLE_1:1;
          Shift(I(),2) c= WHL by Lm11;
        then Shift(I(),2) c= t3 by A32,XBOOLE_1:1;
then A33:     Shift(I(),2) c= t4 by AMI_3:38;
then A34:     (Computation t2).m2 | D = t5 | D by A1,A14,A16,A17,A25,A27,
SCMPDS_7:36;
then A35:     t5.a()=(Computation t2).m2.a() by SCMPDS_4:23
        .=(Result t2).a() by A15,SCMFSA6B:16
        .=s().a() by A11,A13,A28,A29,FUNCT_4:12;
        A36: dom (t | A) = A by SCMPDS_6:1;
A37:     t5|D =(Result t2)|D by A15,A34,SCMFSA6B:16
        .= (Result t2 +* t | A)|D by A36,AMI_5:7,SCMPDS_2:10
        .=IExec(I(),t)|D by SCMPDS_4:def 8;

        set m3=m2 +1;
        set t6=(Computation t3).m3;
A38:     IC t5=l2 by A1,A14,A16,A17,A25,A27,A33,SCMPDS_7:36;
A39:     t6=t5 by AMI_1:51;
then A40:     CurInstr t6=t5.l2 by A38,AMI_1:def 17
        .=t4.l2 by AMI_1:54
        .=t3.l2 by AMI_1:54
        .=WHL.l2 by A30,A32,GRFUNC_1:8
        .=i3 by Th15;
        set t7=(Computation t3).(m3+ 1);
A41:     t7 = Following t6 by AMI_1:def 19
        .= Exec(i3,t6) by A40,AMI_1:def 18;
A42:    IC t7=t7.IC SCMPDS by AMI_1:def 15
       .=ICplusConst(t6,-(card I()+2)) by A41,SCMPDS_2:66
       .=ICplusConst(t6,0-(card I()+2)) by XCMPLX_1:150
       .=inspos 0 by A38,A39,SCMPDS_7:1;
A43:    t7.a()=t6.a() by A41,SCMPDS_2:66
       .=s().a() by A35,AMI_1:51;

         InsCode i3=0 by SCMPDS_2:21;
       then InsCode i3 in {0,4,5,6} by ENUMSET1:19;
then A44:    Dstate(t7)=Dstate(t6) by A41,SCMPDS_8:3
       .=Dstate(IExec(I(),t)) by A37,A39,SCMPDS_8:2;
        now
         assume A45:F(Dstate(t7)) > k;
           F(Dstate(IExec(I(),t))) < F(Dstate(t)) by A4,A10,A11,A12;
    then F(Dstate(t7)) < k+1 by A9,A44,AXIOMS:22;
         hence contradiction by A45,INT_1:20;
       end;
then A46:    WHL is_closed_on t7 & WHL is_halting_on t7 by A8,A13,A43,A44;
A47:    t7 +* iWH=t7 by A42,SCMPDS_7:37;
         now
          let k be Nat;
          per cases;
          suppose k < m3+1;
           then A48: k <= m3 by INT_1:20;
           hereby
              per cases by A48,NAT_1:26;
              suppose A49:k <= m2;
               hereby
               per cases;
                 suppose k=0;
                 hence IC (Computation t3).k in dom pWH by A18,A19,AMI_1:def 19
;
                 suppose k<>0;
                  then consider kn be Nat such that
              A50: k=kn+1 by NAT_1:22;
                    kn < k by A50,REAL_1:69;
                  then kn < m2 by A49,AXIOMS:22;
              then A51: IC (Computation t2).kn + 2 = IC (Computation t4).kn
                  by A1,A14,A16,A17,A25,A27,A33,SCMPDS_7:34;
              A52: IC (Computation t2).kn in dom pI by A13,SCMPDS_6:def 2;
                  consider lm be Nat such that
              A53: IC (Computation t2).kn=inspos lm by SCMPDS_3:32;
                    lm < card pI by A52,A53,SCMPDS_4:1;
                  then lm < card I()+1 by SCMPDS_5:7;
                  then lm+2 < card I() +1+2 by REAL_1:53;
              then A54: lm+2 < card I() +(1+2) by XCMPLX_1:1;
                    card I() + 3 < card I() + 4 by REAL_1:53;
                  then lm+2 < card I() +4 by A54,AXIOMS:22;
                  then A55: lm+2 < card pWH by Lm9;
                    IC (Computation t3).k=inspos lm +2 by A50,A51,A53,AMI_1:51
                  .=inspos (lm+2) by SCMPDS_3:def 3;
                  hence IC (Computation t3).k in dom pWH by A55,SCMPDS_4:1;
               end;
              suppose A56:k=m3;
                 l2 in dom pWH by A30,SCMPDS_6:18;
               hence IC (Computation t3).k in dom pWH by A1,A14,A16,A17,A25,A27
,A33,A39,A56,SCMPDS_7:36;
            end;
          suppose k >= m3+1;
          then consider nn be Nat such that
         A57: k=m3+1+nn by NAT_1:28;
               C3.k=(Computation (t7 +* iWH)).nn by A47,A57,AMI_1:51;
           hence IC (Computation t3).k in dom pWH by A46,SCMPDS_6:def 2;
       end;
       hence WHL is_closed_on t by SCMPDS_6:def 2;
         t7 is halting by A46,A47,SCMPDS_6:def 3;
       then t3 is halting by SCM_1:27;
       hence WHL is_halting_on t by SCMPDS_6:def 3;
     end;
     hence Q[k+1];
     end;
A58:  for k being Nat holds Q[k] from Ind(A5,A7);
     set n=F(Dstate s());
     A59: Q[n] by A58;
     thus WHL is_closed_on s() & WHL is_halting_on s() by A3,A59;
end;

scheme WhileNExec { F(State of SCMPDS)-> Nat,
 s() -> State of SCMPDS,I() -> No-StopCode shiftable Program-block,
 a() -> Int_position,i() -> Integer,P[set]}:
   IExec(while<>0(a(),i(),I()),s()) =
   IExec(while<>0(a(),i(),I()),IExec(I(),s()))
provided
A1: card I() > 0 and
A2: s().DataLoc(s().a(),i()) <> 0 and
A3: (for t be State of SCMPDS st P[Dstate t] & F(Dstate(t))=0 holds
    t.DataLoc(s().a(),i()) = 0) and
A4: P[Dstate s()] and
A5: for t be State of SCMPDS st
       P[Dstate t] & t.a()=s().a() & t.DataLoc(s().a(),i()) <> 0
    holds IExec(I(),t).a()=t.a() & I() is_closed_on t &
        I() is_halting_on t & F(Dstate IExec(I(),t)) < F(Dstate t) &
        P[Dstate(IExec(I(),t))]
proof
   set b=DataLoc(s().a(),i());
   set WHL=while<>0(a(),i(),I()),
       iWH=Initialized stop WHL,
       iI= Initialized stop I(),
       s1= s() +* iWH,
       C1=Computation s1,
       ps= s() | A;
   set i1=(a(),i())<>0_goto 2,
       i2=goto (card I()+2),
       i3=goto -(card I()+2);

        defpred X[set] means P[$1];
        deffunc U(State of SCMPDS) = F($1);
A6: (for t be State of SCMPDS st X[Dstate t] & U(Dstate(t))=0 holds
    t.DataLoc(s().a(),i()) = 0) by A3;
A7: X[Dstate s()] by A4;
A8: for t be State of SCMPDS st
       X[Dstate t] & t.a()=s().a() & t.DataLoc(s().a(),i()) <> 0
    holds IExec(I(),t).a()=t.a() & I() is_closed_on t &
        I() is_halting_on t & U(Dstate IExec(I(),t)) < U(Dstate t) &
        X[Dstate(IExec(I(),t))] by A5;
      WHL is_closed_on s() &
    WHL is_halting_on s() from WhileNHalt(A1,A6,A7,A8);
then A9: s1 is halting by SCMPDS_6:def 3;
    set sI= s() +* iI,
       m1=LifeSpan sI+2,
       s2=IExec(I(),s()) +* iWH,
       C2=Computation s2,
       m2=LifeSpan s2;
       set Es=IExec(I(),s()),
           bj=DataLoc(Es.a(),i());
A10: I() is_closed_on s() & I() is_halting_on s() by A2,A7,A8;
        defpred X[set] means P[$1];
        deffunc U(State of SCMPDS) = F($1);
A11: IExec(I(), s()).a()=s().a() by A2,A7,A8;
then A12: for t be State of SCMPDS st X[Dstate t] & U(Dstate(t))=0
    holds t.bj = 0 by A6;
A13: X[Dstate Es] by A2,A7,A8;
A14: for t being State of SCMPDS st
      X[Dstate t] & t.a()=Es.a() & t.bj <> 0 holds
      IExec(I(),t).a()=t.a() & I() is_closed_on t &
      I() is_halting_on t & U(Dstate IExec(I(),t)) < U(Dstate t)
        & X[Dstate(IExec(I(),t))] by A8,A11;
A15:  WHL is_closed_on Es &
     WHL is_halting_on Es from WhileNHalt(A1,A12,A13,A14);
   set s4 = C1.1;
A16:   sI is halting by A10,SCMPDS_6:def 3;
A17:   iI c= sI by FUNCT_4:26;
      then sI +* iI is halting by A16,AMI_5:10;
then A18:   I() is_halting_on sI by SCMPDS_6:def 3;
A19:   I() is_closed_on sI by A10,SCMPDS_6:38;
A20:   WHL = i1 ';' (i2 ';' I() ';' i3) by Lm10;
then A21:  CurInstr s1 = i1 by SCMPDS_6:22;
A22:  IC s1 =inspos 0 by SCMPDS_6:21;
A23:  (Computation s1).(0 + 1) = Following (Computation s1).0 by AMI_1:def 19
     .= Following s1 by AMI_1:def 19
     .= Exec(i1,s1) by A21,AMI_1:def 18;
     A24: s1.DataLoc(s1.a(),i())=s1.b by SCMPDS_5:19
     .= s().b by SCMPDS_5:19;
A25:  IC s4 = s4.IC SCMPDS by AMI_1:def 15
     .= ICplusConst(s1,2) by A2,A23,A24,SCMPDS_2:67
     .= inspos(0+2) by A22,SCMPDS_6:23;
       sI,s1 equal_outside A by SCMPDS_4:36;
then A26:  sI | D = s1 | D by SCMPDS_4:24;
       now let a;
         thus sI.a = s1.a by A26,SCMPDS_4:23
          .= s4.a by A23,SCMPDS_2:67;
     end;
then A27:  sI | D = s4 | D by SCMPDS_4:23;

     set mI=LifeSpan sI,
         s5=(Computation s4).mI,
         l2=inspos (card I() + 2);

A28:    IExec(I(),s()) = Result sI +* s() | A by SCMPDS_4:def 8;
A29:    dom (s() | A) = A by SCMPDS_6:1;
         card I() + 2 < card I() + 3 by REAL_1:53;
then A30:    l2 in dom WHL by Th13;
A31:    WHL c= iWH by SCMPDS_6:17;
         iWH c= s1 by FUNCT_4:26;
then A32:    WHL c= s1 by A31,XBOOLE_1:1;
         Shift(I(),2) c= WHL by Lm11;
       then Shift(I(),2) c= s1 by A32,XBOOLE_1:1;
then A33:    Shift(I(),2) c= s4 by AMI_3:38;
then A34:    (Computation sI).mI | D = s5 | D
       by A1,A17,A18,A19,A25,A27,SCMPDS_7:36;

        set m3=mI +1;
        set s6=(Computation s1).m3;
A35:     IC s5=l2 by A1,A17,A18,A19,A25,A27,A33,SCMPDS_7:36;
A36:     s6=s5 by AMI_1:51;
then A37:     CurInstr s6=s5.l2 by A35,AMI_1:def 17
        .=s4.l2 by AMI_1:54
        .=s1.l2 by AMI_1:54
        .=WHL.l2 by A30,A32,GRFUNC_1:8
        .=i3 by Th15;
        set s7=(Computation s1).(m3+ 1);
A38:     s7 = Following s6 by AMI_1:def 19
        .= Exec(i3,s6) by A37,AMI_1:def 18;
A39:    IC s7=s7.IC SCMPDS by AMI_1:def 15
       .=ICplusConst(s6,-(card I()+2)) by A38,SCMPDS_2:66
       .=ICplusConst(s6,0-(card I()+2)) by XCMPLX_1:150
       .=inspos 0 by A35,A36,SCMPDS_7:1;
       A40: m3+1=mI+(1+1) by XCMPLX_1:1
       .=mI+2;
         now
          let x be Int_position;
  A41:     not x in dom iWH & x in dom IExec(I(),s())
          by SCMPDS_2:49,SCMPDS_4:31;
  A42:     not x in dom (s() | A) by A29,SCMPDS_2:53;
        s5.x=(Computation sI).mI.x by A34,SCMPDS_4:23
         .=(Result sI).x by A16,SCMFSA6B:16
         .=IExec(I(),s()).x by A28,A42,FUNCT_4:12;
       hence s7.x=IExec(I(),s()).x by A36,A38,SCMPDS_2:66
         .=s2.x by A41,FUNCT_4:12;
     end;
     then A43: s7 | D = s2 | D by SCMPDS_4:23;
A44:  IC s2 =IC C1.m1 by A39,A40,SCMPDS_6:21;
A45: s2 is halting by A15,SCMPDS_6:def 3;
A46: dom ps = dom s() /\ A by RELAT_1:90
    .= ({IC SCMPDS} \/ D \/ A) /\ A by SCMPDS_4:19
    .= A by XBOOLE_1:21;
      s2 | A= (Result sI +* ps +* iWH) | A by SCMPDS_4:def 8
    .=(Result sI +* ps)|A +* iWH | A by AMI_5:6
    .= ps +* iWH | A by A46,FUNCT_4:24
    .= s1 | A by AMI_5:6
    .= C1.m1 | A by SCMPDS_7:6;
then A47: C1.m1=s2 by A40,A43,A44,SCMPDS_7:7;
    then CurInstr C1.m1=i1 by A20,SCMPDS_6:22;
then A48: CurInstr C1.m1 <> halt SCMPDS by SCMPDS_6:29;
    set m0=LifeSpan s1;
      m0 > m1 by A9,A48,SCMPDS_6:2;
    then consider nn be Nat such that
A49: m0=m1+nn by NAT_1:28;
A50: C1.m0 = C2.nn by A47,A49,AMI_1:51;
    then CurInstr C2.nn =halt SCMPDS by A9,SCM_1:def 2;
then A51: nn >= m2 by A45,SCM_1:def 2;
      C1.(m1 + m2) = C2.m2 by A47,AMI_1:51;
    then CurInstr C1.(m1 + m2) = halt SCMPDS by A45,SCM_1:def 2;
    then m1 + m2 >= m0 by A9,SCM_1:def 2;
    then m2 >= nn by A49,REAL_1:53;
then nn=m2 by A51,AXIOMS:21;
then A52: Result s1 = C2.m2 by A9,A50,SCMFSA6B:16;
A53: IExec(I(),s()) | A= (Result sI +* ps) | A by SCMPDS_4:def 8
    .= ps by A46,FUNCT_4:24;
    thus IExec(WHL,s())
     = C2.m2 +* ps by A52,SCMPDS_4:def 8
    .= Result s2 +* IExec(I(),s()) | A by A45,A53,SCMFSA6B:16
    .= IExec(WHL,IExec(I(),s())) by SCMPDS_4:def 8;
end;

scheme WhileNEnd { F(State of SCMPDS)-> Nat,
 s() -> State of SCMPDS,I() -> No-StopCode shiftable Program-block,
 a() -> Int_position,i() -> Integer,P[set]}:
   F(Dstate IExec(while<>0(a(),i(),I()),s()))=0 &
   P[Dstate IExec(while<>0(a(),i(),I()),s())]
provided
A1: card I() > 0 and
A2: for t be State of SCMPDS st P[Dstate t] holds
    F(Dstate(t))=0 iff t.DataLoc(s().a(),i()) = 0 and
A3: P[Dstate s()] and
A4: for t be State of SCMPDS st
       P[Dstate t] & t.a()=s().a() & t.DataLoc(s().a(),i()) <> 0
    holds IExec(I(),t).a()=t.a() & I() is_closed_on t &
        I() is_halting_on t & F(Dstate IExec(I(),t)) < F(Dstate t) &
        P[Dstate(IExec(I(),t))]
proof
   set b=DataLoc(s().a(),i()),
       WHL=while<>0(a(),i(),I());

    defpred Q[Nat] means
       for t be State of SCMPDS st F(Dstate t) <= $1 &
        t.a()=s().a() & P[Dstate t]
      holds F(Dstate IExec(WHL,t))=0 & P[Dstate IExec(WHL,t)];
A5: Q[0]
    proof
       let t be State of SCMPDS;
       assume A6: F(Dstate t) <= 0 & t.a()=s().a() & P[Dstate t];
       F(Dstate t) >= 0 by NAT_1:18;
then A7:  F(Dstate t)=0 by A6,AXIOMS:21;
then t.DataLoc(t.a(),i()) = 0 by A2,A6;
     then for b be Int_position holds IExec(WHL,t).b = t.b by Th19;
     hence F(Dstate IExec(WHL,t))=0 & P[Dstate IExec(WHL,t)] by A6,A7,SCPISORT:
5;
   end;
A8: now
       let k be Nat;
       assume A9:Q[k];
         now
         let u be State of SCMPDS;
         assume A10: F(Dstate u) <= k+1 & u.a()=s().a() & P[Dstate u];
         per cases;
         suppose F(Dstate u)=0;
         hence F(Dstate IExec(WHL,u))=0 & P[Dstate IExec(WHL,u)] by A5,A10;

         suppose A11: F(Dstate u) <> 0;
            then A12: u.b <> 0 by A2,A10;
        A13: u.DataLoc(u.a(),i()) <> 0 by A2,A10,A11;
           set Iu=IExec(I(),u);
        deffunc U(State of SCMPDS) = F($1);
        defpred X[set] means P[$1];
        A14: for t be State of SCMPDS st X[Dstate t] & U(Dstate t)=0
            holds t.DataLoc(u.a(),i()) = 0 by A2,A10;
        A15: X[Dstate u] by A10;
        A16: for t being State of SCMPDS st
            X[Dstate t] & t.a()=u.a() & t.DataLoc(u.a(),i()) <> 0 holds
            IExec(I(),t).a()=t.a() & I() is_closed_on t &
            I() is_halting_on t & U(Dstate IExec(I(),t)) < U(Dstate t) &
            X[Dstate(IExec(I(),t))] by A4,A10;

       A17: IExec(WHL,u) = IExec(WHL,Iu) from WhileNExec(A1,A13,A14,A15,A16);
              F(Dstate Iu) < F(Dstate u) by A4,A10,A12;
            then F(Dstate Iu)+1 <= F(Dstate u) by INT_1:20;
            then F(Dstate Iu)+1 <= k+1 by A10,AXIOMS:22;
       then A18:  F(Dstate Iu) <= k by REAL_1:53;
       A19:  Iu.a()=s().a() by A4,A10,A12;
              P[Dstate Iu] by A4,A10,A12;
         hence F(Dstate IExec(WHL,u))=0 & P[Dstate IExec(WHL,u)] by A9,A17,A18,
A19;
      end;
      hence Q[k+1];
   end;
   for k being Nat holds Q[k] from Ind(A5,A8);
     then Q[F(Dstate s())];
    hence thesis by A3;
end;

theorem Th20:
 for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a,b,c be Int_position,i,d be Integer st
 card I > 0 & s.a=d & s.b > 0 & s.c > 0 & s.DataLoc(d,i)=s.b-s.c &
   (for t be State of SCMPDS st
    t.b > 0 & t.c > 0 & t.a=d & t.DataLoc(d,i)=t.b-t.c & t.b<>t.c
  holds IExec(I,t).a=d & I is_closed_on t & I is_halting_on t &
   (t.b > t.c implies IExec(I,t).b=t.b-t.c & IExec(I,t).c = t.c) &
   (t.b <= t.c implies IExec(I,t).c = t.c-t.b & IExec(I,t).b=t.b) &
   IExec(I,t).DataLoc(d,i)=IExec(I,t).b-IExec(I,t).c)
 holds
    while<>0(a,i,I) is_closed_on s & while<>0(a,i,I) is_halting_on s &
    (s.DataLoc(s.a,i) <> 0 implies
    IExec(while<>0(a,i,I),s) =IExec(while<>0(a,i,I),IExec(I,s)))
proof
   let s be State of SCMPDS,I be No-StopCode shiftable Program-block,
  a,b,c be Int_position, i,d be Integer;
   set ci=DataLoc(s.a,i);

   assume A1: card I > 0;
   assume A2: s.a=d & s.b > 0 & s.c > 0 & s.DataLoc(d,i)=s.b-s.c;
   assume A3: for t be State of SCMPDS st
      t.b > 0 & t.c > 0 & t.a=d & t.DataLoc(d,i)=t.b-t.c & t.b<>t.c
  holds IExec(I,t).a=d & I is_closed_on t & I is_halting_on t &
     (t.b > t.c implies IExec(I,t).b=t.b-t.c & IExec(I,t).c = t.c) &
     (t.b <= t.c implies IExec(I,t).c = t.c-t.b & IExec(I,t).b=t.b) &
     IExec(I,t).DataLoc(d,i)=IExec(I,t).b-IExec(I,t).c;

     defpred P[set] means ex t be State of SCMPDS st
     t=$1 & t.b > 0 & t.c > 0 & t.DataLoc(d,i)=t.b-t.c;

    consider f be Function of product the Object-Kind of SCMPDS,NAT such that
A4: for s be State of SCMPDS holds (s.b = s.c implies f.s =0) &
    (s.b <> s.c implies f.s=max(abs(s.b),abs(s.c))) by Th6;
     deffunc F(State of SCMPDS) = f.$1;
A5:  for t be State of SCMPDS st P[Dstate t] & F(Dstate t)=0 holds t.ci = 0
     proof
       let t be State of SCMPDS;
       assume A6: P[Dstate t] & F(Dstate t)=0;
         then consider v be State of SCMPDS such that
     A7: v=Dstate t & v.b > 0 & v.c > 0 & v.DataLoc(d,i)=v.b-v.c;
       A8: now
          assume t.b <> t.c;
          then (Dstate t).b <> t.c by SCMPDS_8:4;
          then (Dstate t).b <> (Dstate t).c by SCMPDS_8:4;
          then A9: F(Dstate t)=max(abs((Dstate t).b),abs((Dstate t).c)) by A4
          .=max(abs(t.b),abs((Dstate t).c)) by SCMPDS_8:4
          .=max(abs(t.b),abs(t.c)) by SCMPDS_8:4;
            t.b > 0 by A7,SCMPDS_8:4;
          then abs(t.b) > 0 by ABSVALUE:6;
          hence contradiction by A6,A9,SQUARE_1:46;
       end;
      thus t.ci=v.b-v.c by A2,A7,SCMPDS_8:4
         .=t.b-v.c by A7,SCMPDS_8:4
         .=t.b-t.c by A7,SCMPDS_8:4
         .=0 by A8,XCMPLX_1:14;
     end;
A10: P[Dstate s]
    proof
       take t=Dstate s;
       thus t=Dstate s;
       thus t.b > 0 by A2,SCMPDS_8:4;
       thus t.c > 0 by A2,SCMPDS_8:4;
       thus t.DataLoc(d,i)=s.b-s.c by A2,SCMPDS_8:4
            .=t.b-s.c by SCMPDS_8:4
            .=t.b-t.c by SCMPDS_8:4;
    end;
A11:  now
         let t be State of SCMPDS;
         assume A12:P[Dstate t] & t.a=s.a & t.ci <> 0;
         then consider v be State of SCMPDS such that
     A13: v=Dstate t & v.b > 0 & v.c > 0 & v.DataLoc(d,i)=v.b-v.c;
     A14: t.b > 0 & t.c > 0 by A13,SCMPDS_8:4;
     A15: t.DataLoc(d,i)=v.b-v.c by A13,SCMPDS_8:4
         .=t.b-v.c by A13,SCMPDS_8:4
         .=t.b-t.c by A13,SCMPDS_8:4;
     then A16: t.b<>t.c by A2,A12,XCMPLX_1:14;
      hence IExec(I,t).a=t.a by A2,A3,A12,A14,A15;
      thus I is_closed_on t & I is_halting_on t by A2,A3,A12,A14,A15,A16;

   A17: (t.b > t.c implies IExec(I,t).b=t.b-t.c & IExec(I,t).c = t.c) &
       (t.b <= t.c implies IExec(I,t).c =t.c-t.b & IExec(I,t).b=t.b) &
       IExec(I,t).DataLoc(d,i)=IExec(I,t).b-IExec(I,t).c by A2,A3,A12,A14,A15,
A16;
       set x=IExec(I,t).b,
       y=IExec(I,t).c;
   A18: now
         per cases;
          suppose A19: t.b > t.c;
        then A20: t.b-t.c > 0 by SQUARE_1:11;
        A21: x=t.b-t.c by A2,A3,A12,A14,A15,A19;
           thus x > 0 by A2,A3,A12,A14,A15,A19,A20;
          thus y > 0 by A2,A3,A12,A14,A15,A19;
          hereby
    A22:      max(t.b,t.c)=t.b by A19,SQUARE_1:def 2;
             per cases by SQUARE_1:49;
             suppose max(x,y) = x;
               hence max(x,y) < max(t.b,t.c) by A14,A21,A22,SQUARE_1:29;
            suppose max(x,y) = y;
               hence max(x,y) < max(t.b,t.c) by A2,A3,A12,A14,A15,A19,A22;
          end;
          suppose A23: t.b <= t.c;
         then t.b < t.c by A16,REAL_1:def 5;
         then A24: t.c-t.b > 0 by SQUARE_1:11;
         A25: x=t.b by A2,A3,A12,A14,A15,A16,A23;
          thus x > 0 by A2,A3,A12,A14,A15,A16,A23;
         A26: y=t.c-t.b by A2,A3,A12,A14,A15,A16,A23;
          thus y > 0 by A2,A3,A12,A14,A15,A16,A23,A24;
          hereby
    A27:      max(t.b,t.c)=t.c by A23,SQUARE_1:def 2;
             per cases by SQUARE_1:49;
             suppose max(x,y) = y;
               hence max(x,y) < max(t.b,t.c) by A14,A26,A27,SQUARE_1:29;
            suppose max(x,y) = x;
               hence max(x,y) < max(t.b,t.c) by A16,A23,A25,A27,REAL_1:def 5;
          end;
       end;
        set It=IExec(I,t),
            t2=Dstate It,
            t1=Dstate t;

        thus F(t2) < F(t1)
        proof
            t1.b <> t.c by A16,SCMPDS_8:4;
          then t1.b <> t1.c by SCMPDS_8:4;
     then A28:  F(t1)=max(abs(t1.b),abs(t1.c)) by A4
          .=max(abs(t.b),abs(t1.c)) by SCMPDS_8:4
          .=max(abs(t.b),abs(t.c)) by SCMPDS_8:4
          .=max( t.b,abs(t.c)) by A14,ABSVALUE:def 1
          .=max(t.b,t.c) by A14,ABSVALUE:def 1;
          then F(t1) >= t.b by SQUARE_1:46;
      then A29: F(t1) > 0 by A14,AXIOMS:22;
          per cases;
          suppose t2.b=t2.c;
            hence thesis by A4,A29;
          suppose t2.b<>t2.c;
           then F(t2)=max(abs(t2.b),abs(t2.c)) by A4
          .=max(abs(x),abs(t2.c)) by SCMPDS_8:4
          .=max(abs(x),abs(y)) by SCMPDS_8:4
          .=max( x,abs(y)) by A18,ABSVALUE:def 1
          .=max(x,y) by A18,ABSVALUE:def 1;
          hence thesis by A18,A28;
       end;
       thus P[Dstate It]
       proof
            take v=Dstate It;
            thus v=Dstate It;
       thus v.b > 0 & v.c > 0 by A18,SCMPDS_8:4;
       thus v.DataLoc(d,i)=x-y by A17,SCMPDS_8:4
            .=v.b-y by SCMPDS_8:4
            .=v.b-v.c by SCMPDS_8:4;
       end;
    end;
     while<>0(a,i,I) is_closed_on s &
     while<>0(a,i,I) is_halting_on s from WhileNHalt(A1,A5,A10,A11);
     hence while<>0(a,i,I) is_closed_on s & while<>0(a,i,I) is_halting_on s;
     assume A30: s.DataLoc(s.a,i) <> 0;
     IExec(while<>0(a,i,I),s) =IExec(while<>0(a,i,I),IExec(I,s))
       from WhileNExec(A1,A30,A5,A10,A11);
     hence thesis;
end;

begin :: An example: computing Greatest Common Divisor(Euclide algorithm)
::   by loop-invariant

:: gcd(x,y)     < x=(GBP,1) y=(GBP,2),(GBP,3)=x-y >
:: while x<>y do
:: if x>y then x=x-y else y=y-x

definition
 func GCD-Algorithm -> Program-block equals
:Def4:
     (GBP:=0) ';' (GBP,3):=(GBP,1) ';'
     SubFrom(GBP,3,GBP,2) ';'
     while<>0(GBP,3,
           if>0(GBP,3,Load SubFrom(GBP,1,GBP,2),
           Load SubFrom(GBP,2,GBP,1)) ';'
           (GBP,3):=(GBP,1) ';' SubFrom(GBP,3,GBP,2)
     );
 coherence;
end;

theorem Th21:
 for s being State of SCMPDS,I being No-StopCode shiftable Program-block,
 a,b,c be Int_position,i,d be Integer st
 card I > 0 & s.a=d & s.b > 0 & s.c > 0 & s.DataLoc(d,i)=s.b-s.c &
   (for t be State of SCMPDS st
    t.b > 0 & t.c > 0 & t.a=d & t.DataLoc(d,i)=t.b-t.c & t.b<>t.c
  holds IExec(I,t).a=d & I is_closed_on t & I is_halting_on t &
   (t.b > t.c implies IExec(I,t).b=t.b-t.c & IExec(I,t).c = t.c) &
   (t.b <= t.c implies IExec(I,t).c = t.c-t.b & IExec(I,t).b=t.b) &
   IExec(I,t).DataLoc(d,i)=IExec(I,t).b-IExec(I,t).c)
 holds
     IExec(while<>0(a,i,I),s).b = s.b gcd s.c &
     IExec(while<>0(a,i,I),s).c = s.b gcd s.c
proof
   let s be State of SCMPDS,I be No-StopCode shiftable Program-block,
  a,b,c be Int_position, i,d be Integer;
   set ci=DataLoc(s.a,i);

   assume A1: card I > 0;
   assume A2: s.a=d & s.b > 0 & s.c > 0 & s.DataLoc(d,i)=s.b-s.c;
   assume A3: for t be State of SCMPDS st
      t.b > 0 & t.c > 0 & t.a=d & t.DataLoc(d,i)=t.b-t.c & t.b<>t.c
  holds IExec(I,t).a=d & I is_closed_on t & I is_halting_on t &
     (t.b > t.c implies IExec(I,t).b=t.b-t.c & IExec(I,t).c = t.c) &
     (t.b <= t.c implies IExec(I,t).c = t.c-t.b & IExec(I,t).b=t.b) &
     IExec(I,t).DataLoc(d,i)=IExec(I,t).b-IExec(I,t).c;

     defpred P[set] means ex t be State of SCMPDS st
     t=$1 & t.b > 0 & t.c > 0 & t.b gcd t.c =s.b gcd s.c &
     t.DataLoc(d,i)=t.b-t.c;

    consider f be Function of product the Object-Kind of SCMPDS,NAT such that
A4: for s be State of SCMPDS holds (s.b = s.c implies f.s =0) &
    (s.b <> s.c implies f.s=max(abs(s.b),abs(s.c))) by Th6;
     deffunc F(State of SCMPDS) = f.$1;
A5: for t be State of SCMPDS st P[Dstate t] holds F(Dstate t)=0 iff t.ci = 0
     proof
       let t be State of SCMPDS;
       assume P[Dstate t];
         then consider v be State of SCMPDS such that
     A6: v=Dstate t & v.b > 0 & v.c > 0 & v.b gcd v.c =s.b gcd s.c &
         v.DataLoc(d,i)=v.b-v.c;
     A7: t.ci=v.b-v.c by A2,A6,SCMPDS_8:4
         .=t.b-v.c by A6,SCMPDS_8:4
         .=t.b-t.c by A6,SCMPDS_8:4;
       hereby
          assume A8: F(Dstate t)=0;
            now
            assume t.b <> t.c;
            then (Dstate t).b <> t.c by SCMPDS_8:4;
            then (Dstate t).b <> (Dstate t).c by SCMPDS_8:4;
            then A9: F(Dstate t)=max(abs((Dstate t).b),abs((Dstate t).c)) by A4
            .=max(abs(t.b),abs((Dstate t).c)) by SCMPDS_8:4
            .=max(abs(t.b),abs(t.c)) by SCMPDS_8:4;
              t.b > 0 by A6,SCMPDS_8:4;
            then abs(t.b) > 0 by ABSVALUE:6;
            hence contradiction by A8,A9,SQUARE_1:46;
          end;
         hence t.ci=0 by A7,XCMPLX_1:14;
      end;
      hereby
          assume t.ci=0;
          then t.b=t.c by A7,XCMPLX_1:15;
          then (Dstate t).b = t.c by SCMPDS_8:4;
          then (Dstate t).b = (Dstate t).c by SCMPDS_8:4;
        hence F(Dstate t)=0 by A4;
      end;
   end;
A10: P[Dstate s]
    proof
       take t=Dstate s;
       thus t=Dstate s;
       thus t.b > 0 by A2,SCMPDS_8:4;
       thus t.c > 0 by A2,SCMPDS_8:4;
       thus t.b gcd t.c = s.b gcd t.c by SCMPDS_8:4
        .=s.b gcd s.c by SCMPDS_8:4;
       thus t.DataLoc(d,i)=s.b-s.c by A2,SCMPDS_8:4
            .=t.b-s.c by SCMPDS_8:4
            .=t.b-t.c by SCMPDS_8:4;
    end;
A11:  now
         let t be State of SCMPDS;
         assume A12:P[Dstate t] & t.a=s.a & t.ci <> 0;
         then consider v be State of SCMPDS such that
     A13: v=Dstate t & v.b > 0 & v.c > 0 & v.b gcd v.c =s.b gcd s.c &
         v.DataLoc(d,i)=v.b-v.c;
     A14: t.b > 0 & t.c > 0 by A13,SCMPDS_8:4;
     A15: t.DataLoc(d,i)=v.b-v.c by A13,SCMPDS_8:4
         .=t.b-v.c by A13,SCMPDS_8:4
         .=t.b-t.c by A13,SCMPDS_8:4;
     then A16: t.b<>t.c by A2,A12,XCMPLX_1:14;
      hence IExec(I,t).a=t.a by A2,A3,A12,A14,A15;
      thus I is_closed_on t & I is_halting_on t by A2,A3,A12,A14,A15,A16;

   A17: (t.b > t.c implies IExec(I,t).b=t.b-t.c & IExec(I,t).c = t.c) &
       (t.b <= t.c implies IExec(I,t).c =t.c-t.b & IExec(I,t).b=t.b) &
       IExec(I,t).DataLoc(d,i)=IExec(I,t).b-IExec(I,t).c by A2,A3,A12,A14,A15,
A16;
       set x=IExec(I,t).b,
       y=IExec(I,t).c;
   A18: now
         per cases;
          suppose A19: t.b > t.c;
        then A20: t.b-t.c > 0 by SQUARE_1:11;
        A21: x=t.b-t.c by A2,A3,A12,A14,A15,A19;
           thus x > 0 by A2,A3,A12,A14,A15,A19,A20;
          thus y > 0 by A2,A3,A12,A14,A15,A19;
          thus x gcd y = t.b gcd t.c by A14,A17,Th4;
          hereby
    A22:      max(t.b,t.c)=t.b by A19,SQUARE_1:def 2;
             per cases by SQUARE_1:49;
             suppose max(x,y) = x;
               hence max(x,y) < max(t.b,t.c) by A14,A21,A22,SQUARE_1:29;
            suppose max(x,y) = y;
               hence max(x,y) < max(t.b,t.c) by A2,A3,A12,A14,A15,A19,A22;
          end;

        suppose A23: t.b <= t.c;
         then t.b < t.c by A16,REAL_1:def 5;
         then A24: t.c-t.b > 0 by SQUARE_1:11;
         A25: x=t.b by A2,A3,A12,A14,A15,A16,A23;
          thus x > 0 by A2,A3,A12,A14,A15,A16,A23;
         A26: y=t.c-t.b by A2,A3,A12,A14,A15,A16,A23;
         thus y > 0 by A2,A3,A12,A14,A15,A16,A23,A24;
         thus x gcd y =t.b gcd t.c by A14,A17,Th4;
         hereby
    A27:      max(t.b,t.c)=t.c by A23,SQUARE_1:def 2;
             per cases by SQUARE_1:49;
             suppose max(x,y) = y;
               hence max(x,y) < max(t.b,t.c) by A14,A26,A27,SQUARE_1:29;
            suppose max(x,y) = x;
               hence max(x,y) < max(t.b,t.c) by A16,A23,A25,A27,REAL_1:def 5;
          end;
       end;
        set It=IExec(I,t),
            t2=Dstate It,
            t1=Dstate t;

        thus F(t2) < F(t1)
        proof
            t1.b <> t.c by A16,SCMPDS_8:4;
          then t1.b <> t1.c by SCMPDS_8:4;
     then A28:  F(t1)=max(abs(t1.b),abs(t1.c)) by A4
          .=max(abs(t.b),abs(t1.c)) by SCMPDS_8:4
          .=max(abs(t.b),abs(t.c)) by SCMPDS_8:4
          .=max( t.b,abs(t.c)) by A14,ABSVALUE:def 1
          .=max(t.b,t.c) by A14,ABSVALUE:def 1;
          then F(t1) >= t.b by SQUARE_1:46;
      then A29: F(t1) > 0 by A14,AXIOMS:22;
          per cases;
          suppose t2.b=t2.c;
            hence thesis by A4,A29;
          suppose t2.b<>t2.c;
           then F(t2)=max(abs(t2.b),abs(t2.c)) by A4
          .=max(abs(x),abs(t2.c)) by SCMPDS_8:4
          .=max(abs(x),abs(y)) by SCMPDS_8:4
          .=max( x,abs(y)) by A18,ABSVALUE:def 1
          .=max(x,y) by A18,ABSVALUE:def 1;
          hence thesis by A18,A28;
       end;
       thus P[Dstate It]
       proof
            take u=Dstate It;
            thus u=Dstate It;
       thus u.b > 0 & u.c > 0 by A18,SCMPDS_8:4;
       thus u.b gcd u.c =It.b gcd u.c by SCMPDS_8:4
            .=t.b gcd t.c by A18,SCMPDS_8:4
            .=v.b gcd t.c by A13,SCMPDS_8:4
            .=s.b gcd s.c by A13,SCMPDS_8:4;
       thus u.DataLoc(d,i)=x-y by A17,SCMPDS_8:4
            .=u.b-y by SCMPDS_8:4
            .=u.b-u.c by SCMPDS_8:4;
       end;
    end;
    set s1=IExec(while<>0(a,i,I),s),
        ss=Dstate s1;
A30: F(ss)=0 & P[ss] from WhileNEnd(A1,A5,A10,A11);
     then consider w be State of SCMPDS such that
A31:   w=ss & w.b > 0 & w.c > 0 & w.b gcd w.c =s.b gcd s.c &
      w.DataLoc(d,i)=w.b-w.c;
        w.b-w.c =s1.ci by A2,A31,SCMPDS_8:4
      .=0 by A5,A30;
then A32:   w.b=w.c by XCMPLX_1:15;
then A33:   abs(w.b)=abs(w.b) hcf abs(w.c)
      .=s.b gcd s.c by A31,INT_2:def 3;
    thus IExec(while<>0(a,i,I),s).b=ss.b by SCMPDS_8:4
      .=s.b gcd s.c by A31,A33,ABSVALUE:def 1;
    thus IExec(while<>0(a,i,I),s).c =ss.c by SCMPDS_8:4
      .=s.b gcd s.c by A31,A32,A33,ABSVALUE:def 1;
end;

 set i1= GBP:=0,
     i2= (GBP,3):=(GBP,1),
     i3= SubFrom(GBP,3,GBP,2),
     j1= Load SubFrom(GBP,1,GBP,2),
     j2= Load SubFrom(GBP,2,GBP,1),
     IF= if>0(GBP,3,j1,j2),
     k1= (GBP,3):=(GBP,1),
     k2= SubFrom(GBP,3,GBP,2),
     WB= IF ';' k1 ';' k2,
     WH= while<>0(GBP,3,WB);

Lm12:
   card WB=6
proof
    thus card WB=card (IF ';' k1)+1 by SCMP_GCD:8
        .=card IF +1+1 by SCMP_GCD:8
        .=card j1+card j2 +2+1+1 by SCMPDS_6:79
        .= 1+card j2 +2+1+1 by SCMPDS_5:6
        .= 1+1+2+1+1 by SCMPDS_5:6
        .=6;
end;

Lm13:
   card WH=9
proof
   thus card WH=6+3 by Lm12,Th12
    .=9;
end;

theorem
   card GCD-Algorithm=12
proof
   thus card GCD-Algorithm=card (i1 ';' i2 ';' i3) + card WH by Def4,SCMPDS_4:
45
     .=card (i1 ';' i2) +1+ card WH by SCMP_GCD:8
     .=2+1+ 9 by Lm13,SCMP_GCD:9
     .=12;
end;

Lm14:
  for s being State of SCMPDS st s.GBP=0 holds
   (s.a3 > 0 implies IExec(WB,s).a1=s.a1-s.a2 & IExec(WB,s).a2 = s.a2) &
   (s.a3 <= 0 implies IExec(WB,s).a2=s.a2-s.a1 & IExec(WB,s).a1=s.a1) &
   IExec(WB,s).GBP=0 & IExec(WB,s).a3=IExec(WB,s).a1-IExec(WB,s).a2
proof
     let s be State of SCMPDS;
     assume A1:s.GBP=0;
     set s1=IExec(IF,s),
         s2=IExec(IF ';' k1,s),
         a=GBP;
A2:  now
        assume A3:s1.GBP=0;
then A4:     DataLoc(s1.a,3)=intpos (0+3) by SCMP_GCD:5;
then A5:     a<>DataLoc(s1.a,3) by SCMP_GCD:4,def 2;
A6:    s2.a =Exec(k1, s1).a by SCMPDS_5:46
        .=0 by A3,A5,SCMPDS_2:59;
A7:     a1<>DataLoc(s1.a,3) by A4,SCMP_GCD:4;
A8:    s2.a1 =Exec(k1, s1).a1 by SCMPDS_5:46
        .=s1.a1 by A7,SCMPDS_2:59;
A9:     a2<>DataLoc(s1.a,3) by A4,SCMP_GCD:4;
A10:    s2.a2 =Exec(k1, s1).a2 by SCMPDS_5:46
        .=s1.a2 by A9,SCMPDS_2:59;
A11:    s2.a3 =Exec(k1, s1).a3 by SCMPDS_5:46
        .=s1.DataLoc(s1.a,1) by A4,SCMPDS_2:59
        .=s1.intpos (0+1) by A3,SCMP_GCD:5;

A12:     DataLoc(s2.a,3)=intpos (0+3) by A6,SCMP_GCD:5;
then A13:     a<>DataLoc(s2.a,3) by SCMP_GCD:4,def 2;
   thus IExec(WB,s).a =Exec(k2, s2).a by SCMPDS_5:46
        .=0 by A6,A13,SCMPDS_2:62;
A14:     a1<>DataLoc(s2.a,3) by A12,SCMP_GCD:4;
    thus
A15:   IExec(WB,s).a1 =Exec(k2, s2).a1 by SCMPDS_5:46
        .=s1.a1 by A8,A14,SCMPDS_2:62;
A16:     a2<>DataLoc(s2.a,3) by A12,SCMP_GCD:4;
    thus
A17:   IExec(WB,s).a2 =Exec(k2, s2).a2 by SCMPDS_5:46
        .=s1.a2 by A10,A16,SCMPDS_2:62;
    thus IExec(WB,s).a3 =Exec(k2, s2).a3 by SCMPDS_5:46
        .=s2.a3-s2.DataLoc(s2.a,2) by A12,SCMPDS_2:62
        .=s2.a3-s2.intpos (0+2) by A6,SCMP_GCD:5
        .=IExec(WB,s).a1-IExec(WB,s).a2 by A10,A11,A15,A17;
    end;
    set s0=Initialized s,
        m1=SubFrom(GBP,1,GBP,2),
        m2=SubFrom(GBP,2,GBP,1);
A18:  s0.a=0 by A1,SCMPDS_5:40;
A19:  s0.a1=s.a1 by SCMPDS_5:40;
A20:  s0.a2=s.a2 by SCMPDS_5:40;
A21:   DataLoc(s.a,3)=intpos(0+3) by A1,SCMP_GCD:5;
A22:  now
       assume A23: s.a3 > 0;
A24:       DataLoc(s0.a,1)=intpos (0+1) by A18,SCMP_GCD:5;
then A25:       a<> DataLoc(s0.a,1) by SCMP_GCD:4,def 2;
        thus s1.a=IExec(j1,s).a by A21,A23,SCMPDS_6:87
          .=Exec(m1, s0).a by SCMPDS_5:45
          .=0 by A18,A25,SCMPDS_2:62;
        thus s1.a1=IExec(j1,s).a1 by A21,A23,SCMPDS_6:87
          .=Exec(m1, s0).a1 by SCMPDS_5:45
          .=s0.a1-s0.DataLoc(s0.a,2) by A24,SCMPDS_2:62
          .=s0.a1-s0.intpos(0+2) by A18,SCMP_GCD:5
          .=s.a1-s.a2 by A20,SCMPDS_5:40;
A26:       a2<> DataLoc(s0.a,1) by A24,SCMP_GCD:4;
        thus s1.a2=IExec(j1,s).a2 by A21,A23,SCMPDS_6:87
          .=Exec(m1, s0).a2 by SCMPDS_5:45
          .=s.a2 by A20,A26,SCMPDS_2:62;
     end;
A27:  now
       assume A28: s.a3 <= 0;
A29:       DataLoc(s0.a,2)=intpos (0+2) by A18,SCMP_GCD:5;
then A30:       a<> DataLoc(s0.a,2) by SCMP_GCD:4,def 2;
        thus s1.a=IExec(j2,s).a by A21,A28,SCMPDS_6:88
          .=Exec(m2, s0).a by SCMPDS_5:45
          .=0 by A18,A30,SCMPDS_2:62;
        thus s1.a2=IExec(j2,s).a2 by A21,A28,SCMPDS_6:88
          .=Exec(m2, s0).a2 by SCMPDS_5:45
          .=s0.a2-s0.DataLoc(s0.a,1) by A29,SCMPDS_2:62
          .=s0.a2-s0.intpos(0+1) by A18,SCMP_GCD:5
          .=s.a2-s.a1 by A20,SCMPDS_5:40;
A31:       a1<> DataLoc(s0.a,2) by A29,SCMP_GCD:4;
        thus s1.a1=IExec(j2,s).a1 by A21,A28,SCMPDS_6:88
          .=Exec(m2, s0).a1 by SCMPDS_5:45
          .=s.a1 by A19,A31,SCMPDS_2:62;
     end;
A32:  now
       per cases;
       suppose s.a3 > 0;
         hence s1.a=0 by A22;
       suppose s.a3 <= 0;
         hence s1.a=0 by A27;
      end;
      thus s.a3 > 0 implies
         IExec(WB,s).a1=s.a1-s.a2 & IExec(WB,s).a2 = s.a2 by A2,A22;
      thus s.a3 <= 0 implies
         IExec(WB,s).a2=s.a2-s.a1 & IExec(WB,s).a1 = s.a1 by A2,A27;
     thus IExec(WB,s).a=0 &
     IExec(WB,s).a3=IExec(WB,s).a1-IExec(WB,s).a2 by A2,A32;
end;

Lm15:
 for s being State of SCMPDS st s.GBP=0 & s.a1 > 0 & s.a2 > 0 &
   s.a3=s.a1-s.a2 holds
   IExec(WH,s).a1 = s.a1 gcd s.a2 & IExec(WH,s).a2 = s.a1 gcd s.a2 &
   WH is_closed_on s & WH is_halting_on s
proof
   let s be State of SCMPDS;
   set a=GBP;
   assume A1: s.a=0 & s.a1 > 0 & s.a2 > 0 & s.a3=s.a1-s.a2;
A2:  DataLoc(0,3)=intpos(0+3) by SCMP_GCD:5;
A3:  now
        let t be State of SCMPDS;
        assume A4: t.a1 > 0 & t.a2 > 0 & t.a=0 & t.DataLoc(0,3)=t.a1-t.a2 &
           t.a1<>t.a2;
     hence IExec(WB,t).a=0 by Lm14;
     thus WB is_closed_on t by SCMPDS_6:34;
     thus WB is_halting_on t by SCMPDS_6:35;
     hereby
         assume t.a1 > t.a2;
         then t.a3 > 0 by A2,A4,SQUARE_1:11;
         hence IExec(WB,t).a1=t.a1-t.a2 & IExec(WB,t).a2 = t.a2 by A4,Lm14;
     end;
     hereby
         assume t.a1 <= t.a2;
         then t.a3 <= 0 by A2,A4,REAL_2:106;
         hence IExec(WB,t).a2=t.a2-t.a1 & IExec(WB,t).a1 = t.a1 by A4,Lm14;
     end;
     thus IExec(WB,t).DataLoc(0,3)=IExec(WB,t).a1-IExec(WB,t).a2 by A2,A4,Lm14
;
   end;
   hence IExec(WH,s).a1 = s.a1 gcd s.a2 & IExec(WH,s).a2 = s.a1 gcd s.a2
     by A1,A2,Lm12,Th21;
   thus thesis by A1,A2,A3,Lm12,Th20;
end;

   set GA=i1 ';' i2 ';' i3 ';' WH;
Lm16:
 for s being State of SCMPDS st s.a1 > 0 & s.a2 > 0 holds
   IExec(GA,s).a1 = s.a1 gcd s.a2 & IExec(GA,s).a2 = s.a1 gcd s.a2 &
   GA is_closed_on s & GA is_halting_on s
proof
     let s be State of SCMPDS;
     assume A1: s.a1 > 0 & s.a2 > 0;
   set t0=Initialized s,
       t1=IExec(i1 ';' i2 ';' i3,s),
       t2=IExec(i1 ';' i2,s),
       t3=Exec(i1, t0),
       a=GBP;
A2: t3.a=0 by SCMPDS_2:57;
       a <> a1 by SCMP_GCD:4,def 2;
then A3: t3.a1=t0.a1 by SCMPDS_2:57
     .=s.a1 by SCMPDS_5:40;
       a <> a2 by SCMP_GCD:4,def 2;
then A4: t3.a2=t0.a2 by SCMPDS_2:57
     .=s.a2 by SCMPDS_5:40;
A5:  DataLoc(t3.a,3)=intpos (0+3) by A2,SCMP_GCD:5;
then A6:  a<>DataLoc(t3.a,3) by SCMP_GCD:4,def 2;
A7: t2.a=Exec(i2,t3).a by SCMPDS_5:47
     .=0 by A2,A6,SCMPDS_2:59;
A8:  a1<>DataLoc(t3.a,3) by A5,SCMP_GCD:4;
A9: t2.a1=Exec(i2,t3).a1 by SCMPDS_5:47
     .=s.a1 by A3,A8,SCMPDS_2:59;
A10:  a2<>DataLoc(t3.a,3) by A5,SCMP_GCD:4;
A11: t2.a2=Exec(i2,t3).a2 by SCMPDS_5:47
     .=s.a2 by A4,A10,SCMPDS_2:59;
A12: t2.a3=Exec(i2,t3).a3 by SCMPDS_5:47
     .=t3.DataLoc(t3.a,1) by A5,SCMPDS_2:59
     .=t3.intpos(0+1) by A2,SCMP_GCD:5
     .=s.a1 by A3;

A13:  DataLoc(t2.a,3)=intpos (0+3) by A7,SCMP_GCD:5;
then A14:  a<>DataLoc(t2.a,3) by SCMP_GCD:4,def 2;
A15: t1.a=Exec(i3,t2).a by SCMPDS_5:46
     .=0 by A7,A14,SCMPDS_2:62;
A16:  a1<>DataLoc(t2.a,3) by A13,SCMP_GCD:4;
A17: t1.a1=Exec(i3,t2).a1 by SCMPDS_5:46
     .=s.a1 by A9,A16,SCMPDS_2:62;
A18:  a2<>DataLoc(t2.a,3) by A13,SCMP_GCD:4;
A19: t1.a2=Exec(i3,t2).a2 by SCMPDS_5:46
     .=s.a2 by A11,A18,SCMPDS_2:62;
  t1.a3=Exec(i3,t2).a3 by SCMPDS_5:46
     .=t2.a3-t2.DataLoc(t2.a,2) by A13,SCMPDS_2:62
     .=t2.a3-t2.intpos(0+2) by A7,SCMP_GCD:5
     .=t1.a1-t1.a2 by A11,A12,A17,A19;
then A20: IExec(WH,t1).a1 = t1.a1 gcd t1.a2 & IExec(WH,t1).a2 = t1.a1 gcd t1.a2
&
    WH is_closed_on t1 & WH is_halting_on t1 by A1,A15,A17,A19,Lm15;

   hence IExec(GA,s).a1=s.a1 gcd s.a2 by A17,A19,SCPISORT:8;
   thus IExec(GA,s).a2=s.a1 gcd s.a2 by A17,A19,A20,SCPISORT:8;
  thus GA is_closed_on s & GA is_halting_on s by A20,SCPISORT:10;
end;

theorem      :: SCMP_GCD:18
    for s being State of SCMPDS,x, y being Integer st
  s.intpos 1 = x & s.intpos 2 = y & x > 0 & y > 0 holds
  IExec(GCD-Algorithm,s).intpos 1 = x gcd y &
  IExec(GCD-Algorithm,s).intpos 2 = x gcd y &
  GCD-Algorithm is_closed_on s & GCD-Algorithm is_halting_on s
  by Def4,Lm16;

Back to top