The Mizar article:

Insert Sort on \SCMFSA

by
Jing-Chao Chen

Received March 13, 1999

Copyright (c) 1999 Association of Mizar Users

MML identifier: SCMISORT
[ MML identifier index ]


environ

 vocabulary SCMFSA7B, AMI_1, SCMFSA_2, SCMFSA6A, SF_MASTR, AMI_3, FUNCT_1,
      RELAT_1, FUNCT_4, CAT_1, FINSUB_1, PROB_1, SCMFSA8B, SCMFSA8A, SCMFSA_4,
      CARD_1, AMI_5, RELOC, BOOLE, SCMFSA_9, FINSEQ_1, INT_1, RFINSEQ,
      SCMFSA6C, SCMFSA6B, SCM_1, SCM_HALT, FUNCT_7, UNIALG_2, CARD_3, AMI_2,
      SCMFSA8C, ARYTM_1, ABSVALUE, SCMBSORT, FINSEQ_4, SCMISORT;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
      NAT_1, CQC_LANG, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, FUNCT_7, CARD_1,
      FINSEQ_1, CARD_3, STRUCT_0, AMI_1, AMI_3, SCM_1, AMI_5, SCMFSA_2,
      SCMFSA_4, SCMFSA_5, SCMFSA6A, SEQ_1, SF_MASTR, SCMFSA6B, SCMFSA6C,
      SCMFSA7B, SCMFSA8A, SCMFSA_9, SCMFSA8B, INT_1, FINSEQ_4, SCMBSORT,
      FINSUB_1, PROB_1, SCMFSA8C, RFINSEQ, SCM_HALT, GROUP_1;
 constructors NAT_1, AMI_5, SCMFSA_5, SCM_1, SCMFSA6A, SCMFSA6B, SEQ_1,
      SCMFSA6C, SETWISEO, CQC_SIM1, SCMFSA8B, SCMFSA8C, RFINSEQ, SCM_HALT,
      SCMFSA8A, FINSEQ_4, SCMBSORT, SCMFSA_9, SFMASTR1, PROB_1, MEMBERED;
 clusters RELSET_1, FUNCT_1, AMI_1, SCMFSA_2, SCMFSA_4, SF_MASTR, SCMFSA6C,
      SCMFSA8A, FINSUB_1, SCM_HALT, SCMFSA_9, INT_1, CQC_LANG, NAT_1, FRAENKEL,
      XREAL_0, MEMBERED;
 requirements BOOLE, REAL, NUMERALS, SUBSET, ARITHM;
 definitions AMI_1;
 theorems SF_MASTR, FUNCT_1, FUNCT_7, CQC_LANG, RELAT_1, AMI_1, FUNCT_2,
      SCMFSA6A, FUNCT_4, AMI_5, FINSEQ_3, AXIOMS, ENUMSET1, AMI_3, REAL_1,
      NAT_1, TARSKI, INT_1, GRFUNC_1, RFINSEQ, SCMFSA_2, SCMFSA6B, SCMFSA7B,
      SCMFSA8B, SCMFSA8A, SCMFSA8C, SCMFSA_4, SCMFSA6C, SCM_HALT, ABSVALUE,
      FINSEQ_4, REAL_2, FINSEQ_2, CQC_THE1, SCMBSORT, SCMFSA_9, SCMFSA_5,
      SCM_1, SCMFSA9A, PARTFUN1, CARD_1, XBOOLE_0, XBOOLE_1, XCMPLX_0,
      XCMPLX_1;
 schemes NAT_1, SCMFSA_9, RECDEF_1;

begin :: Preliminaries

definition
 let i be good Instruction of SCM+FSA;
 cluster Macro i -> good;
 coherence
 proof
       i does_not_destroy intloc 0 by SCM_HALT:def 6;
     hence thesis by SCMFSA8C:99;
 end;
end;

definition
 let a be read-write Int-Location,b be Int-Location;
 cluster AddTo(a,b) -> good;
 coherence
 proof
      AddTo(a,b) does_not_destroy intloc 0 by SCMFSA7B:13;
    hence thesis by SCM_HALT:def 6;
 end;
end;

theorem Th1:  ::PR016
 for f be Function,d,r be set st d in dom f holds dom f=dom (f+*(d.-->r))
proof
  let f be Function,d,r be set;
  assume A1:d in dom f;
  thus dom f=dom (f+*(d,r)) by FUNCT_7:32
  .=dom (f+*(d.-->r)) by A1,FUNCT_7:def 3;
end;

theorem   ::PR014
   for p be programmed FinPartState of SCM+FSA,l be Instruction-Location of
  SCM+FSA, ic be Instruction of SCM+FSA st l in dom p & (ex pc be Instruction
  of SCM+FSA st pc=p.l & UsedIntLoc pc=UsedIntLoc ic) holds UsedIntLoc p
  = UsedIntLoc (p+*(l.-->ic))
proof let p be programmed FinPartState of SCM+FSA,l be Instruction-Location
  of SCM+FSA, ic be Instruction of SCM+FSA;
  set pl=p+*(l.-->ic);
  assume A1: l in dom p & (ex pc be Instruction of SCM+FSA st pc=p.l &
  UsedIntLoc pc=UsedIntLoc ic);
  then A2: pl.l=(p+*(l,ic)).l by FUNCT_7:def 3
      .=ic by A1,FUNCT_7:33;
 consider UIL being Function of the Instructions of SCM+FSA,Fin Int-Locations
  such that
A3: (for i being Instruction of SCM+FSA holds UIL.i = UsedIntLoc i) &
   UsedIntLoc p = Union (UIL * p) by SF_MASTR:def 2;
 consider UIL2 being Function of the Instructions of SCM+FSA, Fin Int-Locations
    such that
A4: (for i being Instruction of SCM+FSA holds UIL2.i = UsedIntLoc i) &
   UsedIntLoc pl = Union (UIL2 * pl) by SF_MASTR:def 2;
      for c be Element of the Instructions of SCM+FSA holds UIL.c = UIL2.c
    proof
      let c be Element of the Instructions of SCM+FSA;
      reconsider d = c as Instruction of SCM+FSA;
      thus UIL.c = UsedIntLoc d by A3
        .= UIL2.c by A4;
    end;
then A5: UIL=UIL2 by FUNCT_2:113;
    set f = UIL * p,
        g = UIL * pl;
   now
   A6: dom p = dom pl by A1,Th1;
   A7: dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1;
   then A8: rng p c= dom UIL & rng pl c= dom UIL by SCMFSA_4:1;
   then A9: dom f = dom p by RELAT_1:46;
    hence dom f = dom g by A6,A8,RELAT_1:46;
   let x be set;
   assume A10: x in dom f;
    then pl.x in rng pl by A6,A9,FUNCT_1:def 5;
    then reconsider plx = pl.x as Instruction of SCM+FSA by A7,A8;
   per cases;
   suppose x<>l;
      then not x in {l} by TARSKI:def 1;
   then not x in dom (l.-->ic) by CQC_LANG:5;
   then p.x=pl.x by FUNCT_4:12;
      hence f.x = UIL.plx by A10,FUNCT_1:22
          .= g.x by A6,A9,A10,FUNCT_1:23;
   suppose A11:x=l;
      thus f.x = UIL.(p.x) by A10,FUNCT_1:22
          .= UsedIntLoc plx by A1,A2,A3,A11
          .= UIL.plx by A4,A5
          .= g.x by A6,A9,A10,FUNCT_1:23;
 end;
  hence thesis by A3,A4,A5,FUNCT_1:9;
end;

theorem   ::PR020
   for a being Int-Location,I being Macro-Instruction holds
  if>0(a, I ';' Goto insloc 0,SCM+FSA-Stop).insloc (card I +4)
  = goto insloc (card I +4)
proof
   let a be Int-Location,I be Macro-Instruction;
   set I4=card I +4,
        Lc4=insloc I4,
        Gi= Goto insloc 0,
        SS=SCM+FSA-Stop,
        I1=I ';' Gi,
        F=if>0(a, I1, SS),
        i=a>0_goto insloc (card SS + 3),
        MM=i ';' SS ';' Goto insloc (card I1 + 1) ';' I,
        GS=Gi ';' SS;
A1: insloc 0 in dom Gi by SCMFSA8A:47;
A2: Gi.insloc 0=goto insloc 0 by SCMFSA8A:47;
then A3: Gi.insloc 0 <> halt SCM+FSA by SCMFSA_9:9;
A4: GS.insloc 0 = (Directed Gi).insloc 0 by A1,SCMFSA8A:28
    .=goto insloc 0 by A1,A2,A3,SCMFSA8A:30;
A5: card F=card I +6 by SCMFSA_9:2;
      I4 < card I + 6 by REAL_1:53;
then A6: Lc4 in dom F by A5,SCMFSA6A:15;
A7: card MM = card (i ';' SS ';' Goto insloc (card I1 + 1)) + card I
       by SCMFSA6A:61
   .= card (i ';' SS) + card Goto insloc (card I1 + 1) + card I by SCMFSA6A:61
   .= card (i ';' SS) + 1 + card I by SCMFSA8A:29
   .= card (Macro i ';' SS) + 1 + card I by SCMFSA6A:def 5
   .= card Macro i + 1 + 1 + card I by SCMFSA6A:61,SCMFSA8A:17
   .= 2 + 1 + 1 + card I by SCMFSA7B:6
   .=I4;
then A8: not Lc4 in dom MM by SCMFSA6A:15;
A9: F= i ';' SS ';' Goto insloc (card I1 + 1) ';' I1 ';' SS by SCMFSA8B:def 2
    .=MM ';' Gi ';' SS by SCMFSA6A:62
    .=MM ';' GS by SCMFSA6A:62
    .= Directed MM +* ProgramPart Relocated(GS, I4) by A7,SCMFSA6A:def 4;
then A10: dom F = dom Directed MM \/ dom ProgramPart Relocated(GS, I4)
    by FUNCT_4:def 1;
    then dom F = dom MM \/ dom ProgramPart Relocated(GS, I4) by SCMFSA6A:14;
then A11: Lc4 in dom ProgramPart Relocated(GS, I4) by A6,A8,XBOOLE_0:def 2;
A12: insloc 0 + I4 = insloc ( 0 + I4) by SCMFSA_4:def 1;
   card GS=card Gi + card SS by SCMFSA6A:61
    .=1 + 1 by SCMFSA8A:17,29
    .=2;
then A13: insloc 0 in dom GS by SCMFSA6A:15;
    then insloc 0 + I4 in { il+I4 where il is Instruction-Location of SCM+FSA:
      il in dom GS};
then A14: Lc4 in dom Shift(GS,I4) by A12,SCMFSA_4:31;
then A15: pi(Shift(GS,I4),Lc4) = Shift(GS,I4).(insloc 0 +I4) by A12,AMI_5:def 5
    .= goto insloc 0 by A4,A13,SCMFSA_4:30;

   thus F.Lc4 = (ProgramPart Relocated(GS,I4)).Lc4 by A6,A9,A10,A11,FUNCT_4:def
1
   .= IncAddr(Shift(ProgramPart(GS),I4),I4).Lc4 by SCMFSA_5:2
   .= IncAddr(Shift(GS,I4),I4).Lc4 by AMI_5:72
   .= IncAddr(goto insloc 0, I4 ) by A14,A15,SCMFSA_4:24
   .= goto insloc I4 by A12,SCMFSA_4:14;
end;

theorem   ::PR022
   for p be programmed FinPartState of SCM+FSA,l be Instruction-Location of
  SCM+FSA, ic be Instruction of SCM+FSA st l in dom p & (ex pc be Instruction
  of SCM+FSA st pc=p.l & UsedInt*Loc pc=UsedInt*Loc ic) holds UsedInt*Loc p
  = UsedInt*Loc (p+*(l.-->ic))
proof
  let p be programmed FinPartState of SCM+FSA,l be Instruction-Location
  of SCM+FSA,ic be Instruction of SCM+FSA;
  set pl=p+*(l.-->ic);
  assume A1: l in dom p & (ex pc be Instruction of SCM+FSA st pc=p.l &
  UsedInt*Loc pc=UsedInt*Loc ic);
  then A2: pl.l=(p+*(l,ic)).l by FUNCT_7:def 3
      .=ic by A1,FUNCT_7:33;
   consider UIL being Function of the Instructions of SCM+FSA,
   Fin FinSeq-Locations such that
A3: (for i being Instruction of SCM+FSA holds UIL.i = UsedInt*Loc i) &
   UsedInt*Loc p = Union (UIL * p) by SF_MASTR:def 4;
 consider UIL2 being Function of the Instructions of SCM+FSA,
   Fin FinSeq-Locations such that
A4: (for i being Instruction of SCM+FSA holds UIL2.i = UsedInt*Loc i) &
   UsedInt*Loc pl = Union (UIL2 * pl) by SF_MASTR:def 4;
      for c be Element of the Instructions of SCM+FSA holds UIL.c = UIL2.c
    proof
      let c be Element of the Instructions of SCM+FSA;
      reconsider d = c as Instruction of SCM+FSA;
      thus UIL.c = UsedInt*Loc d by A3
        .= UIL2.c by A4;
    end;
then A5: UIL=UIL2 by FUNCT_2:113;
    set f = UIL * p,
        g = UIL * pl;
   now
   A6: dom p = dom pl by A1,Th1;
   A7: dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1;
   then A8: rng p c= dom UIL & rng pl c= dom UIL by SCMFSA_4:1;
   then A9: dom f = dom p by RELAT_1:46;
    hence dom f = dom g by A6,A8,RELAT_1:46;
   let x be set;
   assume A10: x in dom f;
    then pl.x in rng pl by A6,A9,FUNCT_1:def 5;
    then reconsider plx = pl.x as Instruction of SCM+FSA by A7,A8;
   per cases;
   suppose x<>l;
      then not x in {l} by TARSKI:def 1;
   then not x in dom (l.-->ic) by CQC_LANG:5;
   then p.x=pl.x by FUNCT_4:12;
      hence f.x = UIL.plx by A10,FUNCT_1:22
          .= g.x by A6,A9,A10,FUNCT_1:23;
   suppose A11:x=l;
      thus f.x = UIL.(p.x) by A10,FUNCT_1:22
          .= UsedInt*Loc plx by A1,A2,A3,A11
          .= UIL.plx by A4,A5
          .= g.x by A6,A9,A10,FUNCT_1:23;
 end;
  hence thesis by A3,A4,A5,FUNCT_1:9;
end;

reserve s for State of SCM+FSA,
   I for Macro-Instruction,
   a for read-write Int-Location;
reserve i,j,k,n for Nat;

canceled;

theorem Th6:   ::PR026
 for s be State of SCM+FSA,I be Macro-Instruction st s.intloc 0=1 &
 IC s = insloc 0 holds
   s +* I = s +* Initialized I
proof
  let s be State of SCM+FSA,I be Macro-Instruction;
  assume A1:s.intloc 0=1 & IC s = insloc 0;
then A2: s.IC SCM+FSA = insloc 0 by AMI_1:def 15;
A3: IC SCM+FSA in dom s by AMI_5:25;
 thus s +* Initialized I = s +* (I +* Start-At insloc 0) by A1,SCMFSA8C:18
 .= s +* I +* Start-At insloc 0 by FUNCT_4:15
 .= s +* Start-At insloc 0 +* I by SCMFSA6B:14
 .= s +* (IC SCM+FSA .--> insloc 0) +* I by AMI_3:def 12
 .= s +* I by A2,A3,SCMFSA8C:6;
end;

theorem Th7:   ::PR006
 for I being Macro-Instruction,a,b being Int-Location st
 I does_not_destroy b holds while>0(a,I) does_not_destroy b
proof
    let I be Macro-Instruction,a,b be Int-Location;
    assume that A1: I does_not_destroy b;
    set J=insloc (card I +4) .--> goto insloc 0,
         Gi= Goto insloc 0,
         SS=SCM+FSA-Stop,
         F=if>0(a, I ';' Gi, SS);
A2: J does_not_destroy b by SCMFSA_9:35;
      Gi does_not_destroy b by SCMFSA8C:86;
then A3: I ';' Gi does_not_destroy b by A1,SCMFSA8C:81;
      SS does_not_destroy b by SCMFSA8C:85;
then A4: F does_not_destroy b by A3,SCMFSA8C:121;
      while>0(a,I) = F+*J by SCMFSA_9:def 2;
    hence thesis by A2,A4,SCMFSA8A:25;
end;

theorem Th8:  ::PR029
  n <= 11 implies n = 0 or n = 1 or n = 2 or n = 3 or n = 4 or n = 5
  or n = 6 or n = 7 or n = 8 or n = 9 or n=10 or n=11
proof
  assume n <= 11;
  then n <= 10+1;
  then n <= 10 or n= 11 by NAT_1:26;
  hence thesis by SCMBSORT:13;
end;

theorem Th9:   ::PR012
 for f,g be FinSequence of INT,m,n be Nat st 1<=n & n <= len f &
 1<=m & m <= len f & g=f+*(m,f/.n) +*(n,f/.m) holds
 f.m=g.n & f.n=g.m & (for k be set st k<>m & k<>n & k in dom f holds
 f.k=g.k) & f,g are_fiberwise_equipotent
proof
   let f,g be FinSequence of INT,m,n be Nat;
   assume A1: 1<=n & n <= len f &
        1<=m & m <= len f & g=f+*(m,f/.n) +*(n,f/.m);
then A2: n in dom f by FINSEQ_3:27;
A3: m in dom f by A1,FINSEQ_3:27;
A4: dom (f+*(m,f/.n))=dom f by FUNCT_7:32;
then A5: dom g =dom f by A1,FUNCT_7:32;
thus A6: g.n=f/.m by A1,A2,A4,FUNCT_7:33
       .=f.m by A1,FINSEQ_4:24;
thus A7: now per cases;
      suppose m=n;
        hence g.m=f.n by A6;
      suppose m<>n;
        hence g.m=(f+*(m,f/.n)).m by A1,FUNCT_7:34
           .=f/.n by A3,FUNCT_7:33
           .=f.n by A1,FINSEQ_4:24;
   end;
hereby let k be set;
      assume A8:k<>m & k<>n & k in dom f;
     hence g.k=(f+*(m,f/.n)).k by A1,FUNCT_7:34
           .=f.k by A8,FUNCT_7:34;
    end;
    hence f, g are_fiberwise_equipotent by A2,A3,A5,A6,A7,SCMBSORT:7;
end;

theorem Th10:
 for s being State of SCM+FSA, I being Macro-Instruction
     st I is_halting_on Initialize s holds
 (for a be Int-Location holds
     IExec(I,s).a = (Computation (Initialize s +* (I +* Start-At insloc 0))).
         (LifeSpan (Initialize s +* (I +* Start-At insloc 0))).a)
proof
   let s be State of SCM+FSA,I be Macro-Instruction;
   set s0 = Initialize s,
       s1 = s0 +* (I +* Start-At insloc 0),
       A = the Instruction-Locations of SCM+FSA;
   assume I is_halting_on s0;
then A1: s1 is halting by SCMFSA7B:def 8;
   hereby let a be Int-Location;
        not a in A by SCMFSA_2:84;
      then not a in dom s /\ A by XBOOLE_0:def 3;
  then A2: a in dom Result s1 & not a in dom (s | A) by RELAT_1:90,SCMFSA_2:66;
        s +* Initialized I = s1 by SCMFSA8A:13;
      hence IExec(I,s).a = (Result s1 +* s | A).a by SCMFSA6B:def 1
      .= (Result s1).a by A2,FUNCT_4:12
      .= (Computation s1).(LifeSpan s1).a by A1,SCMFSA6B:16;
    end;
end;

theorem Th11:  ::SCMFSA6B_28
 for s1,s2 be State of SCM+FSA,I be InitHalting Macro-Instruction st
     Initialized I c= s1 & Initialized I c= s2 &
 s1,s2 equal_outside the Instruction-Locations of SCM+FSA holds
 for k be Nat holds
     (Computation s1).k, (Computation s2).k
         equal_outside the Instruction-Locations of SCM+FSA &
     CurInstr (Computation s1).k = CurInstr (Computation s2).k
proof
   let s1,s2 be State of SCM+FSA,I be InitHalting Macro-Instruction;
   assume that
A1: Initialized I c= s1 and
A2: Initialized I c= s2 and
A3: s1,s2 equal_outside the Instruction-Locations of SCM+FSA;
A4:  I c= s1 by A1,SCM_HALT:13;
A5:  I c= s2 by A2,SCM_HALT:13;
   hereby let k be Nat;
        for m being Nat st m < k holds IC((Computation s2).m) in dom I
          by A2,SCM_HALT:def 1;
      hence (Computation s1).k, (Computation s2).k equal_outside
          the Instruction-Locations of SCM+FSA by A3,A4,A5,SCMFSA6B:21;
   then A6: IC (Computation s1).k = IC (Computation s2).k by SCMFSA6A:29;
  A7: IC (Computation s1).k in dom I by A1,SCM_HALT:def 1;
  A8: IC (Computation s2).k in dom I by A2,SCM_HALT:def 1;
      thus CurInstr (Computation s2).k
       = ((Computation s2).k).IC (Computation s2).k by AMI_1:def 17
      .= s2.IC (Computation s2).k by AMI_1:54
      .= I.IC (Computation s2).k by A5,A8,GRFUNC_1:8
      .= s1.IC (Computation s1).k by A4,A6,A7,GRFUNC_1:8
      .= ((Computation s1).k).IC (Computation s1).k by AMI_1:54
      .= CurInstr (Computation s1).k by AMI_1:def 17;
     end;
end;

theorem Th12:   ::SCMFSA6B_29
 for s1,s2 be State of SCM+FSA,I be InitHalting Macro-Instruction st
     Initialized I c= s1 & Initialized I c= s2 &
 s1,s2 equal_outside the Instruction-Locations of SCM+FSA holds
 LifeSpan s1 = LifeSpan s2 &
 Result s1, Result s2 equal_outside the Instruction-Locations of SCM+FSA
proof
   let s1,s2 be State of SCM+FSA,I be InitHalting Macro-Instruction;
   assume that
A1: Initialized I c= s1 and
A2: Initialized I c= s2 and
A3: s1,s2 equal_outside the Instruction-Locations of SCM+FSA;
A4: s1 is halting by A1,SCM_HALT:5;
A5: now let l be Nat; assume
   A6: CurInstr (Computation s2).l = halt SCM+FSA;
     CurInstr (Computation s1).l = CurInstr (Computation s2).l
      by A1,A2,A3,Th11;
      hence LifeSpan s1 <= l by A4,A6,SCM_1:def 2;
     end;
A7: CurInstr (Computation s2).LifeSpan s1
     = CurInstr (Computation s1).LifeSpan s1 by A1,A2,A3,Th11
    .= halt SCM+FSA by A4,SCM_1:def 2;
A8: s2 is halting by A2,SCM_HALT:5;
   hence LifeSpan s1 = LifeSpan s2 by A5,A7,SCM_1:def 2;
then A9: Result s2 = (Computation s2).LifeSpan s1 by A8,SCMFSA6B:16;
     Result s1 = (Computation s1).LifeSpan s1 by A4,SCMFSA6B:16;
   hence Result s1, Result s2 equal_outside
       the Instruction-Locations of SCM+FSA by A1,A2,A3,A9,Th11;
end;

theorem Th13:  ::SCMFSA6A_49
 for I be Macro-Instruction, f be FinSeq-Location holds
     not f in dom I
proof
   let I be Macro-Instruction,f be FinSeq-Location;
   assume A1: f in dom I;
      dom I c= the Instruction-Locations of SCM+FSA by AMI_3:def 13;
    hence contradiction by A1,SCMFSA_2:85;
end;

theorem Th14:   ::SCMFSA6A_48
 for I be Macro-Instruction, a be Int-Location holds
     not a in dom I
proof
   let I be Macro-Instruction,a be Int-Location;
   assume A1: a in dom I;
      dom I c= the Instruction-Locations of SCM+FSA by AMI_3:def 13;
    hence contradiction by A1,SCMFSA_2:84;
end;

theorem Th15:  ::AMI_1_46
  for N being non empty with_non-empty_elements set
  for S being halting IC-Ins-separated definite
      (non empty non void AMI-Struct over N)
  for s being State of S st (LifeSpan s) <= j & s is halting holds
   (Computation s).j = (Computation s).(LifeSpan s)
proof
  let N be non empty with_non-empty_elements set,
      S be halting IC-Ins-separated definite
      (non empty non void AMI-Struct over N),
     s be State of S;
     assume A1: (LifeSpan s) <= j & s is halting;
     then CurInstr((Computation s).(LifeSpan s)) = halt S by SCM_1:def 2;
     hence thesis by A1,AMI_1:52;
end;

begin  :: -- Basic property of while Macro ---
set D = Int-Locations \/ FinSeq-Locations;
set IL = the Instruction-Locations of SCM+FSA;
::  set D = Int-Locations U FinSeq-Locations;
::  set IL = the Instruction-Locations of SCM+FSA;

theorem Th16:     :: Th032
 for s being State of SCM+FSA, I being Macro-Instruction,
 a being read-write Int-Location
 st s.a <= 0 holds while>0(a,I) is_halting_onInit s &
  while>0(a,I) is_closed_onInit s
proof
    let s be State of SCM+FSA,I be Macro-Instruction;
    let a be read-write Int-Location;
    assume A1: s.a <= 0;
    set s0=Initialize s;
      s0.a <= 0 by A1,SCMFSA6C:3;
    then while>0(a,I) is_halting_on s0 & while>0(a,I) is_closed_on s0
    by SCMFSA_9:43;
    hence thesis by SCM_HALT:40,41;
end;

theorem     ::Th033
   for a being Int-Location, I being Macro-Instruction,
 s being State of SCM+FSA,k being Nat st
   I is_closed_onInit s & I is_halting_onInit s &
   k < LifeSpan (s +* Initialized I) &
   IC (Computation (s +* Initialized while>0(a,I))).(1 + k) =
   IC (Computation (s +* Initialized I)).k + 4 &
   (Computation (s +* Initialized while>0(a,I))).(1 + k) | D =
   (Computation (s +* Initialized I)).k | D
  holds
   IC (Computation (s +* Initialized while>0(a,I))).(1 + k+1) =
   IC (Computation (s +* Initialized I)).(k+1) + 4 &
   (Computation (s +* Initialized while>0(a,I))).(1 + k+1) | D =
   (Computation (s +* Initialized I)).(k+1) | D
proof
    let a be Int-Location,I be Macro-Instruction;
    let s be State of SCM+FSA,k be Nat;
    set s0=Initialize s,
        sw = s +* Initialized while>0(a,I),
        sI = s +* Initialized I,
        s0I= s0 +* (I +* Start-At insloc 0),
        s0w= s0 +* (while>0(a,I) +* Start-At insloc 0),
        sK1=(Computation sw).(1 + k),
        sK2= (Computation sI).k,
        l3=IC (Computation sI).k;
    assume A1: I is_closed_onInit s;
    assume A2: I is_halting_onInit s;
    assume A3: k < LifeSpan sI;
    assume A4: IC (Computation sw).(1 + k)=l3 + 4;
    assume A5: sK1 | D = sK2 | D;
A6: I is_closed_on s0 by A1,SCM_HALT:40;
A7: I is_halting_on s0 by A2,SCM_HALT:41;
A8: sI=s0I by SCMFSA8A:13;
A9: sw=s0w by SCMFSA8A:13;
   hence
     IC (Computation sw).(1 + k+1) = IC (Computation sI ).(k+1) + 4 by A3,A4,A5
,A6,A7,A8,SCMFSA_9:44;
   thus
     (Computation sw ).(1 + k+1) | D = (Computation sI).(k+1) | D by A3,A4,A5,
A6,A7,A8,A9,SCMFSA_9:44;
end;

theorem    ::Th034
   for a being Int-Location, I being Macro-Instruction,
  s being State of SCM+FSA st
   I is_closed_onInit s & I is_halting_onInit s &
   IC (Computation (s +* Initialized while>0(a,I))).(1 +
   LifeSpan (s +* Initialized I)) =
   IC (Computation (s +* Initialized I)).LifeSpan (s +* Initialized I) + 4
   holds
   CurInstr (Computation (s +* Initialized while>0(a,I))).(1 +
   LifeSpan (s +* Initialized I)) = goto insloc (card I +4)
proof
    let a be Int-Location,I be Macro-Instruction;
    let s be State of SCM+FSA;
    set s0=Initialize s,
        sw = s +* Initialized while>0(a,I),
        sI = s +* Initialized I,
        s0I= s0 +* (I +* Start-At insloc 0),
        s0w= s0 +* (while>0(a,I) +* Start-At insloc 0);
    assume A1: I is_closed_onInit s;
    assume A2: I is_halting_onInit s;
    assume A3: IC (Computation sw).(1 + LifeSpan sI) =
     IC (Computation sI).LifeSpan sI + 4;
A4: I is_closed_on s0 by A1,SCM_HALT:40;
A5: I is_halting_on s0 by A2,SCM_HALT:41;
A6: sI=s0I by SCMFSA8A:13;
  sw=s0w by SCMFSA8A:13;
   hence
        CurInstr (Computation sw).(1 + LifeSpan sI)
      = goto insloc (card I +4) by A3,A4,A5,A6,SCMFSA_9:45;
end;

theorem Th19:   ::Th036
 for s being State of SCM+FSA, I being Macro-Instruction,
 a being read-write Int-Location
 st I is_closed_onInit s & I is_halting_onInit s & s.a >0 holds
    IC (Computation (s +* Initialized while>0(a,I))).
    (LifeSpan (s +* Initialized I) + 3) = insloc 0 &
    for k being Nat st k <= LifeSpan (s +* Initialized I) + 3
    holds IC (Computation (s +* Initialized while>0(a,I))).k in
    dom while>0(a,I)
proof
    let s be State of SCM+FSA,I be Macro-Instruction;
    let a be read-write Int-Location;
    set s0=Initialize s,
        sw = s +* Initialized while>0(a,I),
        sI = s +* Initialized I,
        s0I= s0 +* (I +* Start-At insloc 0),
        s0w= s0 +* (while>0(a,I) +* Start-At insloc 0);
    assume A1: I is_closed_onInit s;
    assume A2: I is_halting_onInit s;
    assume A3: s.a >0;
A4: I is_closed_on s0 by A1,SCM_HALT:40;
A5: I is_halting_on s0 by A2,SCM_HALT:41;
A6: s0.a>0 by A3,SCMFSA6C:3;
A7: sI=s0I by SCMFSA8A:13;
A8: sw=s0w by SCMFSA8A:13;
    hence IC (Computation sw).(LifeSpan sI + 3)
    = insloc 0 by A4,A5,A6,A7,SCMFSA_9:47;
    thus for k be Nat st k <= LifeSpan sI + 3 holds
     IC (Computation sw).k in dom while>0(a,I) by A4,A5,A6,A7,A8,SCMFSA_9:47;
end;

theorem     ::SCM_9_36
   for s being State of SCM+FSA, I being Macro-Instruction,a be read-write
 Int-Location st
    I is_closed_onInit s & I is_halting_onInit s & s.a >0 holds
    for k being Nat st k <= LifeSpan (s +* Initialized I) + 3
    holds IC (Computation (s +* Initialized while>0(a,I))).k
    in dom while>0(a,I)
proof
    let s be State of SCM+FSA, I be Macro-Instruction,a be read-write
    Int-Location;
    assume A1:I is_closed_onInit s;
    assume A2:I is_halting_onInit s;
    assume A3:s.a >0;
    set s0=Initialize s,
        IA=I +* Start-At insloc 0;
      now let k be Nat;
         IC (Computation (s +* Initialized I )).k in dom I
          by A1,SCM_HALT:def 4;
       hence IC (Computation (s0 +* IA )).k in dom I by SCMFSA8A:13;
    end;
then A4: I is_closed_on s0 by SCMFSA7B:def 7;
      s +* Initialized I is halting by A2,SCM_HALT:def 5;
    then s0 +* IA is halting by SCMFSA8A:13;
then A5: I is_halting_on s0 by SCMFSA7B:def 8;
A6: s0.a > 0 by A3,SCMFSA6C:3;
    hereby let k be Nat;
       assume k <= LifeSpan (s +* Initialized I) + 3;
    then k <= LifeSpan (s0 +* IA) + 3 by SCMFSA8A:13;
       then IC (Computation (s0 +* (while>0(a,I) +* Start-At insloc 0))).k
       in dom while>0(a,I) by A4,A5,A6,SCMFSA_9:47;
       hence IC (Computation (s +* Initialized while>0(a,I))).k
       in dom while>0(a,I) by SCMFSA8A:13;
    end;
end;

theorem Th21:    ::SCM_9_37
 for s being State of SCM+FSA, I be Macro-Instruction,a be read-write
 Int-Location st
    I is_closed_onInit s & I is_halting_onInit s & s.a >0 holds
    IC (Computation (s +* Initialized while>0(a,I))).
    (LifeSpan (s +* Initialized I) + 3) = insloc 0 &
    (Computation (s +* Initialized while>0(a,I))).
    (LifeSpan (s +* Initialized I) + 3) | D =
 (Computation (s +* Initialized I)).(LifeSpan (s +* Initialized I)) | D
proof
    let s be State of SCM+FSA,I be Macro-Instruction,a be read-write
    Int-Location;
    assume A1: I is_closed_onInit s;
    assume A2: I is_halting_onInit s;
    assume A3:  s.a > 0;
    set s0=Initialize s,
        IA=I +* Start-At insloc 0;
   set s1 = s0 +* (while>0(a,I) +* Start-At insloc 0),
        s2 = (Computation s1).1,
        i = a >0_goto insloc 4 ,
        sI = s0 +* IA;

      now let k be Nat;
         IC (Computation (s +* Initialized I )).k in dom I
          by A1,SCM_HALT:def 4;
       hence IC (Computation (s0 +* IA )).k in dom I by SCMFSA8A:13;
    end;
then A4: I is_closed_on s0 by SCMFSA7B:def 7;
      s +* Initialized I is halting by A2,SCM_HALT:def 5;
    then s0 +* IA is halting by SCMFSA8A:13;
then A5: I is_halting_on s0 by SCMFSA7B:def 8;
A6: s0.a > 0 by A3,SCMFSA6C:3;

A7:  insloc 0 in dom while>0(a,I) by SCMFSA_9:10;
       while>0(a,I) c= while>0(a,I) +* Start-At insloc 0 by SCMFSA8A:9;
then A8: dom while>0(a,I) c= dom (while>0(a,I) +* Start-At insloc 0)
       by GRFUNC_1:8;
A9:   IC SCM+FSA in dom (while>0(a,I) +* Start-At insloc 0) by SF_MASTR:65;
A10:  IC s1 = s1.IC SCM+FSA by AMI_1:def 15
     .= (while>0(a,I) +* Start-At insloc 0).IC SCM+FSA by A9,FUNCT_4:14
     .= insloc 0 by SF_MASTR:66;
       s1.insloc 0 = (while>0(a,I) +* Start-At insloc 0).insloc 0
     by A7,A8,FUNCT_4:14
     .= while>0(a,I).insloc 0 by A7,SCMFSA6B:7
     .= i by SCMFSA_9:11;
then A11:  CurInstr s1 = i by A10,AMI_1:def 17;
A12:  (Computation s1).(0 + 1) = Following (Computation s1).0 by AMI_1:def 19
     .= Following s1 by AMI_1:def 19
     .= Exec(i,s1) by A11,AMI_1:def 18;
       not a in dom (while>0(a,I) +* Start-At insloc 0) & a in dom s0
       by SCMFSA6B:12,SCMFSA_2:66;
     then A13: s1.a = s0.a by FUNCT_4:12;
A14:  IC s2 = s2.IC SCM+FSA by AMI_1:def 15
     .= insloc 4 by A6,A12,A13,SCMFSA_2:97;
       (for c be Int-Location holds s2.c = s1.c) &
     for f be FinSeq-Location holds s2.f = s1.f
       by A12,SCMFSA_2:97;
then A15:  s2 | D = s1 | D by SCMFSA6A:38
     .= s0 | D by SCMFSA8A:11
     .= sI | D by SCMFSA8A:11;
    defpred P[Nat] means
       $1 <= LifeSpan sI implies
       IC (Computation s1).(1 + $1) = IC (Computation sI).$1 + 4 &
       (Computation s1).(1 + $1) | D = (Computation sI).$1 | D;
A16: P[0]
     proof assume 0 <= LifeSpan sI;
A17:    IC SCM+FSA in dom (I +* Start-At insloc 0) by SF_MASTR:65;
         IC (Computation sI).0 = IC sI by AMI_1:def 19
       .= sI.IC SCM+FSA by AMI_1:def 15
       .= (I +* Start-At insloc 0).IC SCM+FSA by A17,FUNCT_4:14
       .= insloc 0 by SF_MASTR:66;
       then IC (Computation sI).0 + 4 = insloc (0+ 4) by SCMFSA_4:def 1;
       hence IC (Computation s1).(1 + 0) = IC (Computation sI).0 + 4 &
       (Computation s1).(1 + 0) | D = (Computation sI).0 | D
        by A14,A15,AMI_1:def 19;
    end;
A18: now let k be Nat;
      assume A19: P[k];
        now assume A20: k + 1 <= LifeSpan sI;
           k + 0 < k + 1 by REAL_1:53;
then k < LifeSpan sI by A20,AXIOMS:22;
         hence
           IC (Computation s1).(1 + k+1) = IC (Computation sI).(k+1) + 4 &
         (Computation s1).(1 + k+1) | D = (Computation sI).(k+1) | D
          by A4,A5,A19,SCMFSA_9:44;
      end;
      hence P[k + 1];
    end;
    set s2=(Computation s1).(1 + LifeSpan sI);
    set loc4=insloc (card I + 4);
    set s3=(Computation s1).(1+LifeSpan sI+1);
   for k being Nat holds P[k] from Ind(A16,A18);
then A21: P[LifeSpan sI];
then A22: CurInstr s2 = goto loc4 by A4,A5,SCMFSA_9:45;
A23: s3 = Following s2 by AMI_1:def 19
    .= Exec(goto loc4,s2) by A22,AMI_1:def 18;
     then (for c be Int-Location holds s3.c = s2.c) &
     for f be FinSeq-Location holds s3.f = s2.f by SCMFSA_2:95;
then A24:  s3 | D = s2 | D by SCMFSA6A:38;
A25: loc4 in dom while>0(a,I) by SCMFSA_9:38;
A26: IC s3 = s3.IC SCM+FSA by AMI_1:def 15
    .= loc4 by A23,SCMFSA_2:95;
    set s4=(Computation s1).(1+LifeSpan sI+1+1);
      s3.loc4 = s1.loc4 by AMI_1:54
    .= (while>0(a,I) +* Start-At insloc 0).loc4 by A8,A25,FUNCT_4:14
    .= while>0(a,I).loc4 by A25,SCMFSA6B:7
    .= goto insloc 0 by SCMFSA_9:46;
then A27: CurInstr s3 = goto insloc 0 by A26,AMI_1:def 17;
A28: s4 = Following s3 by AMI_1:def 19
    .= Exec(goto insloc 0,s3) by A27,AMI_1:def 18;
     then (for c be Int-Location holds s4.c = s3.c) &
     for f be FinSeq-Location holds s4.f = s3.f by SCMFSA_2:95;
then A29:  s4 | D =s2 | D by A24,SCMFSA6A:38;
A30: IC s4 = s4.IC SCM+FSA by AMI_1:def 15
    .= insloc 0 by A28,SCMFSA_2:95;
A31: LifeSpan sI+1+1+1 = LifeSpan sI+(1+1)+1 by XCMPLX_1:1
    .=LifeSpan sI+(2+1) by XCMPLX_1:1;
A32: (Computation (s +* Initialized while>0(a,I))).
    (LifeSpan (s +* Initialized I) + 3) =(Computation s1).
    (LifeSpan (s +* Initialized I) + 3) by SCMFSA8A:13
    .=s4 by A31,SCMFSA8A:13;
 hence IC (Computation (s +* Initialized while>0(a,I))).
    (LifeSpan (s +* Initialized I) + 3) =insloc 0 by A30;
 thus (Computation (s +* Initialized while>0(a,I))).
    (LifeSpan (s +* Initialized I) + 3) | D =
(Computation (s +* Initialized I)).(LifeSpan sI) | D by A21,A29,A32,SCMFSA8A:13
    .=(Computation (s +* Initialized I)).
     (LifeSpan (s +* Initialized I)) | D by SCMFSA8A:13;
end;

theorem  ::TMP22B
   for s be State of SCM+FSA, I be InitHalting Macro-Instruction,
     a be read-write Int-Location st s.a > 0 holds
 ex s2 be State of SCM+FSA, k be Nat st
   s2 = s +* Initialized (while>0(a,I)) &
   k =LifeSpan (s +* Initialized I) + 3 &
   IC (Computation s2).k = insloc 0 &
   (for b be Int-Location holds (Computation s2).k.b = IExec(I,s).b) &
   (for f be FinSeq-Location holds (Computation s2).k.f = IExec(I,s).f)
proof
   let s be State of SCM+FSA,I be InitHalting Macro-Instruction;
   let a be read-write Int-Location;
   assume A1: s.a > 0;
   set P = while>0(a,I),
       s1 = s +* Initialized I;
   take s2 = s +* Initialized P;
   take k = LifeSpan s1 + 3;
   thus s2 = s +* Initialized P &
        k = LifeSpan s1 + 3;
    set Is=Initialize s +* (I +* Start-At insloc 0);
A2: I is_halting_onInit s by SCM_HALT:36;
    then s1 is halting by SCM_HALT:def 5;
    then Is is halting by SCMFSA8A:13;
then A3:  I is_halting_on Initialize s by SCMFSA7B:def 8;
A4:  I is_closed_onInit s by SCM_HALT:35;
   hence IC ((Computation s2).k)=insloc 0 by A1,A2,Th21;
     set s4=(Computation s2).k,
         s3=(Computation s1).(LifeSpan s1);
A5:  s3=(Computation Is).(LifeSpan s1) by SCMFSA8A:13
     .=(Computation Is).(LifeSpan Is) by SCMFSA8A:13;
     A6: s4 | D = s3 | D by A1,A2,A4,Th21;
    hereby let b be Int-Location;
      thus s4.b =(Computation Is).(LifeSpan Is).b by A5,A6,SCMFSA6A:38
      .= IExec(I,s).b by A3,Th10;
    end;
    hereby let f be FinSeq-Location;
      thus s4.f =(Computation Is).(LifeSpan Is).f by A5,A6,SCMFSA6A:38
      .= IExec(I,s).f by A3,SCMFSA8C:87;
    end;
end;


definition
let s,I,a;
    deffunc U(Nat, Element of product the Object-Kind of SCM+FSA) =
     (Computation ($2 +* Initialized while>0(a,I))).
         (LifeSpan ($2+* Initialized I) + 3);
func StepWhile>0(a,s,I) -> Function of NAT,product the Object-Kind of SCM+FSA
  means
:Def1:
   it.0 = s qua Element of (product the Object-Kind of SCM+FSA)
qua non empty set & for i being Nat
  holds it.(i+1)=(Computation (it.i +* Initialized while>0(a,I))).
      (LifeSpan (it.i +* Initialized I) + 3);
 existence
  proof
   thus ex f being Function of NAT,product the Object-Kind of SCM+FSA st
   f.0 = s qua Element of (product the Object-Kind of SCM+FSA)
qua non empty set & for i being Nat holds f.(i+1)= U(i,f.i)
   from LambdaRecExD;
  end;
 uniqueness
proof let F1,F2 be Function of NAT,product the Object-Kind of SCM+FSA
      such that
A1: F1.0 = s & for i being Nat holds F1.(i+1)= U(i,F1.i) and
A2: F2.0 = s & for i being Nat holds F2.(i+1)= U(i,F2.i);
    thus F1 = F2 from LambdaRecUnD(A1,A2);
 end;
end;

canceled 2;

theorem   ::Th039
   StepWhile>0(a,s,I).(k+1)=StepWhile>0(a,StepWhile>0(a,s,I).k,I).1
proof
    set sk=StepWhile>0(a,s,I).k;
    set sk0=StepWhile>0(a,sk,I).0;
  sk0=sk by Def1;
    hence StepWhile>0(a,s,I).(k+1) =
(Computation (sk0 +* Initialized while>0(a,I))).
    (LifeSpan (sk0 +* Initialized I) + 3) by Def1
    .=StepWhile>0(a,sk,I).(0+1) by Def1
    .=StepWhile>0(a,sk,I).1;
end;

theorem Th26:  ::Th040
  for I being Macro-Instruction,a being read-write Int-Location,
   s being State of SCM+FSA holds
   StepWhile>0(a,s,I).(0+1)=(Computation (s +* Initialized while>0(a,I))).
   (LifeSpan (s+* Initialized I) + 3)
proof
    let I be Macro-Instruction,a be read-write Int-Location,
    s be State of SCM+FSA;
    thus StepWhile>0(a,s,I).(0+1)=(Computation (StepWhile>0(a,s,I).0 +*
    Initialized while>0(a,I))).(LifeSpan (StepWhile>0(a,s,I).0 +*
      Initialized I) + 3) by Def1
    .=(Computation (s +* Initialized while>0(a,I)))
      .(LifeSpan (StepWhile>0(a,s,I).0+* Initialized I) + 3) by Def1
    .=(Computation (s +* Initialized while>0(a,I)))
     .(LifeSpan (s+* Initialized I) + 3) by Def1;
end;

theorem Th27:  ::Th041
for I be Macro-Instruction,a be read-write Int-Location,
  s be State of SCM+FSA,k,n be Nat st
  IC StepWhile>0(a,s,I).k =insloc 0 & StepWhile>0(a,s,I).k=
  (Computation (s +* Initialized while>0(a,I))).n &
  StepWhile>0(a,s,I).k.intloc 0=1
  holds
  StepWhile>0(a,s,I).k = StepWhile>0(a,s,I).k +* Initialized while>0(a,I) &
  StepWhile>0(a,s,I).(k+1)=(Computation (s +* Initialized while>0(a,I))).
  (n +(LifeSpan (StepWhile>0(a,s,I).k +* Initialized I) + 3))
proof
    let I be Macro-Instruction,a be read-write Int-Location,
    s be State of SCM+FSA,k,n be Nat;
    set s1 = s +* Initialized while>0(a,I);
    set sk=StepWhile>0(a,s,I).k,
        s0k=Initialize sk,
        At0=while>0(a,I) +* Start-At insloc 0,
        s2=s0k +* At0,
        s3=sk +* Initialized while>0(a,I);
    assume A1:IC sk =insloc 0;
    assume A2:sk =(Computation s1).n;
    assume A3:sk.intloc 0=1;
A4: IC SCM+FSA in dom At0 by SF_MASTR:65;
A5: IC s3 = IC s2 by SCMFSA8A:13
    .= s2.IC SCM+FSA by AMI_1:def 15
    .= At0.IC SCM+FSA by A4,FUNCT_4:14
    .= IC sk by A1,SF_MASTR:66;
A6:  s3 | D = s2 | D by SCMFSA8A:13
     .= s0k | D by SCMFSA8A:11
     .= sk | D by A1,A3,SCMFSA8C:14;
   sk | IL =s1 | IL by A2,SCMFSA6B:17;
    then s3 | IL = sk | IL by SCMFSA_9:27;hence
  s3=sk by A5,A6,SCMFSA_9:29;
    hence
      StepWhile>0(a,s,I).(k+1)=
(Computation sk).(LifeSpan (sk +* Initialized I) + 3) by Def1
    .=(Computation s1).(n +(LifeSpan (sk +* Initialized I) + 3)) by A2,AMI_1:51
;
end;

theorem    :: Th042
    for I be Macro-Instruction,a be read-write Int-Location,
    s be State of SCM+FSA st
     ex f being Function of product the Object-Kind of SCM+FSA,NAT st
      (for k being Nat holds ( f.(StepWhile>0(a,s,I).k) <> 0 implies
      f.(StepWhile>0(a,s,I).(k+1)) < f.(StepWhile>0(a,s,I).k) &
      I is_closed_onInit StepWhile>0(a,s,I).k &
      I is_halting_onInit StepWhile>0(a,s,I).k) &
      (StepWhile>0(a,s,I).(k+1)).intloc 0=1 &
      ( f.(StepWhile>0(a,s,I).k)=0 iff (StepWhile>0(a,s,I).k).a <= 0 ) )
     holds
     while>0(a,I) is_halting_onInit s & while>0(a,I) is_closed_onInit s
proof
    let I be Macro-Instruction,a be read-write Int-Location,s be State
    of SCM+FSA;
    given f be Function of product the Object-Kind of SCM+FSA,NAT
    such that A1:for k be Nat holds
      (f.(StepWhile>0(a,s,I).k) <> 0 implies
      f.(StepWhile>0(a,s,I).(k+1)) < f.(StepWhile>0(a,s,I).k) &
      I is_closed_onInit StepWhile>0(a,s,I).k &
      I is_halting_onInit StepWhile>0(a,s,I).k) &
      (StepWhile>0(a,s,I).(k+1)).intloc 0=1 &
      ( f.(StepWhile>0(a,s,I).k)=0 iff (StepWhile>0(a,s,I).k).a <= 0);
    deffunc F(Nat) = f.(StepWhile>0(a,s,I).$1);
    set IniI=Initialized I,
        Iwhile=Initialized while>0(a,I),
        s1 = s +* Iwhile;
A2: F(0) =f.s by Def1;
A3: for k holds ( F(k+1) < F(k) or F(k) = 0 ) by A1;
    consider m being Nat such that
A4: F(m)=0 and
A5: for n st F(n) =0 holds m <= n from MinIndex(A2,A3);
A6: now let i be Nat;
       assume i<m;
       then F(i)<>0 by A5;
       hence
         I is_closed_onInit StepWhile>0(a,s,I).i &
       I is_halting_onInit StepWhile>0(a,s,I).i by A1;
    end;
    defpred P[Nat] means
      $1+1 <= m implies
        ex k st StepWhile>0(a,s,I).($1+1)=(Computation s1).k;
A7:  P[0]
     proof assume 0+1 <= m;
       take n=(LifeSpan (s +* IniI) + 3);
       thus StepWhile>0(a,s,I).(0+1)=(Computation s1).n by Th26;
    end;
A8: IC SCM+FSA in dom Iwhile by SCMFSA6A:24;
A9: now let k be Nat;
       assume A10: P[k];
         now assume A11: (k+1)+ 1 <= m;
            k + 0 < k+ (1+ 1) by REAL_1:53;
          then k < (k+1) +1 by XCMPLX_1:1;
then A12:       k < m by A11,AXIOMS:22;
          A13: (k+1)+ 0 < (k+ 1)+ 1 by REAL_1:53;
          set sk=StepWhile>0(a,s,I).k,
              sk1=StepWhile>0(a,s,I).(k+1);
          consider n be Nat such that
A14:       sk1 = (Computation s1).n by A10,A11,A13,AXIOMS:22;
A15:       sk1= (Computation (sk +* Iwhile)).
          (LifeSpan (sk +* IniI ) + 3) by Def1;
A16:       I is_closed_onInit sk & I is_halting_onInit sk by A6,A12;
            F(k) <> 0 by A5,A12;
          then sk.a > 0 by A1;
then A17:       IC sk1 =insloc 0 by A15,A16,Th19;
A18:       sk1.intloc 0=1 by A1;
          take m=n +(LifeSpan (sk1 +* IniI ) + 3);
          thus StepWhile>0(a,s,I).((k+1)+1)=(Computation s1).m
            by A14,A17,A18,Th27;
       end;
       hence P[k+1];
    end;
A19: for k being Nat holds P[k] from Ind(A7,A9);
      now per cases;
       suppose m=0;
         then (StepWhile>0(a,s,I).0).a <= 0 by A1,A4;
         then s.a <= 0 by Def1;
         hence while>0(a,I) is_halting_onInit s &
         while>0(a,I) is_closed_onInit s
         by Th16;
       suppose A20:m<>0;
         then consider i being Nat such that
A21:      m=i+1 by NAT_1:22;
A22:     i<m by A21,REAL_1:69;
         set si=StepWhile>0(a,s,I).i,
             sm=StepWhile>0(a,s,I).m,
             sm1=sm +* Iwhile,
             sm2=sm +*(while>0(a,I) +* Start-At (insloc 0));
         consider n being Nat such that
A23:     sm = (Computation s1).n by A19,A21;
A24:      sm.a <= 0 by A1,A4;
A25:     sm= (Computation (si +* Iwhile)).
           (LifeSpan (si +* IniI) + 3) by A21,Def1;
A26:     I is_closed_onInit si & I is_halting_onInit si by A6,A22;
           i < m by A21,NAT_1:38;
         then F(i) <> 0 by A5;
         then si.a > 0 by A1;
then A27:     IC sm =insloc 0 by A25,A26,Th19;
           (StepWhile>0(a,s,I).(i+1)).intloc 0 = 1 by A1;
then A28:     sm1=sm2 by A21,SCMFSA8C:18;
then A29:     IC sm2 = sm1.IC SCM+FSA by AMI_1:def 15
         .= Iwhile.IC SCM+FSA by A8,FUNCT_4:14
         .= IC sm by A27,SCMFSA6A:46;
A30:     sm2 | D = sm | D by SCMFSA8A:11;
      sm | IL =s1 | IL by A23,SCMFSA6B:17;
then sm2 | IL = sm | IL by A28,SCMFSA_9:27;
then A31:     sm1=sm by A28,A29,A30,SCMFSA_9:29;
           while>0(a,I) is_halting_onInit sm by A24,Th16;
         then sm1 is halting by SCM_HALT:def 5;
         then consider j being Nat such that
A32:      CurInstr((Computation sm).j) = halt SCM+FSA by A31,AMI_1:def 20;
           CurInstr (Computation s1).(n+j) = halt SCM+FSA by A23,A32,AMI_1:51;
         then s1 is halting by AMI_1:def 20;
         hence while>0(a,I) is_halting_onInit s by SCM_HALT:def 5;
         set p=(LifeSpan (s+* IniI) + 3);
           now let q be Nat;
A33:         0<m by A20,NAT_1:19;
            per cases;
            suppose A34: q <= p;
A35:           StepWhile>0(a,s,I).0=s by Def1;
                F(0) <> 0 by A5,A33;
then A36:           s.a > 0 by A1,A35;
                I is_closed_onInit s & I is_halting_onInit s by A6,A33,A35;
              hence IC (Computation s1).q in dom while>0(a,I) by A34,A36,Th19;
            suppose A37: q > p;
              defpred P2[Nat] means
                $1<=m & $1<>0 & (ex k st StepWhile>0(a,s,I).$1=
                (Computation s1).k & k <= q);
A38:           for i be Nat st P2[i] holds i <= m;
A39:           now
                 take k=p;
                 thus StepWhile>0(a,s,I).1=(Computation s1).k & k <= q
                 by A37,Th26;
              end;
                0+1 < m +1 by A33,REAL_1:53;
then 1 <= m by NAT_1:38;
then A40:          ex t being Nat st P2[t] by A39;
                ex k st P2[k] & for i st P2[i] holds i <= k
               from Max(A38,A40);
              then consider t being Nat such that
A41:           P2[t] & for i st P2[i] holds i <= t;
                now per cases;
                 suppose t=m;
                   then consider r being Nat such that
A42:                sm=(Computation s1).r & r <= q by A41;
                   consider x being Nat such that
A43:                q = r+x by A42,NAT_1:28;
A44:                (Computation s1).q = (Computation sm1).x by A31,A42,A43,
AMI_1:51;
                     while>0(a,I) is_closed_onInit sm by A24,Th16;
                   hence IC (Computation s1).q in dom while>0(a,I) by A44,
SCM_HALT:def 4;
                 suppose t<>m;
then A45:                t < m by A41,REAL_1:def 5;
                   consider y being Nat such that
A46:                t=y+1 by A41,NAT_1:22;
A47:                StepWhile>0(a,s,I).t.intloc 0=1 by A1,A46;
                   consider z being Nat such that
A48:                StepWhile>0(a,s,I).t=(Computation s1).z & z <= q by A41;
                     y+ 0 < t by A46,REAL_1:53;
then A49:                y < m by A41,AXIOMS:22;
                   set Dy=StepWhile>0(a,s,I).y;
                   set Dt=StepWhile>0(a,s,I).t;
A50:                Dt= (Computation (Dy +* Iwhile)).
                    (LifeSpan (Dy +* IniI) + 3) by A46,Def1;
A51:                I is_closed_onInit Dy & I is_halting_onInit Dy by A6,A49;
                     F(y) <> 0 by A5,A49;
                   then Dy.a > 0 by A1;
then A52:                IC Dt =insloc 0 by A50,A51,Th19;
                   set z2=z +(LifeSpan (Dt +* IniI) + 3);
A53:                now assume A54: z2 <= q;
A55:                    now take k=z2;thus
                            StepWhile>0(a,s,I).(t+1)=(Computation s1).k & k <=q
                          by A47,A48,A52,A54,Th27;
                       end;
                      t+1 <= m by A45,NAT_1:38;
                       then t+1 <= t by A41,A55;
                       hence contradiction by REAL_1:69;
                   end;
                   consider w be Nat such that
A56:                q = z+w by A48,NAT_1:28;
A57:                w < LifeSpan (Dt +* IniI) + 3 by A53,A56,AXIOMS:24;
A58:                (Computation s1).q = (Computation Dt ).w by A48,A56,AMI_1:
51
                   .= (Computation (Dt +* Iwhile)).w
                      by A47,A48,A52,Th27;
A59:                I is_closed_onInit Dt & I is_halting_onInit Dt by A6,A45;
                     F(t) <> 0 by A5,A45;
                   then Dt.a > 0 by A1;
                   hence IC (Computation s1).q in dom while>0(a,I)
                    by A57,A58,A59,Th19;
              end;
              hence IC (Computation s1).q in dom while>0(a,I);
         end;
         hence while>0(a,I) is_closed_onInit s by SCM_HALT:def 4;
    end;
    hence thesis;
end;

theorem Th29:   :: W_halt1
  for I be good InitHalting Macro-Instruction,a be read-write Int-Location
    st (for s be State of SCM+FSA holds
    (s.a > 0 implies IExec(I, s).a < s.a ))
    holds while>0(a,I) is InitHalting
proof
    let I be good InitHalting Macro-Instruction,a be read-write Int-Location;
    assume A1:for s be State of SCM+FSA holds
     (s.a > 0 implies IExec(I, s).a < s.a );
    defpred P[Nat] means
      for t be State of SCM+FSA st t.a <= $1 holds
       while>0(a,I) is_halting_onInit t;
A2:  P[0] by Th16;
A3: now let k be Nat;
      assume A4:P[k];
        now let t be State of SCM+FSA;
         assume A5:t.a <= k+1;
         per cases;
         suppose t.a<>k+1;
           then t.a < k+1 by A5,REAL_1:def 5;
           then t.a <= k by INT_1:20;
           hence while>0(a,I) is_halting_onInit t by A4;
         suppose A6:t.a=k+1;
         then A7: t.a > 0 by NAT_1:19;
         A8: I is_closed_onInit t by SCM_HALT:35;
         A9: I is_halting_onInit t by SCM_HALT:36;
             set Iwhile=Initialized while>0(a,I),
                 tW0=t +* Iwhile,
                 t1=t +* Initialized I,
                 Wt=(Computation tW0).((LifeSpan t1)+ 3),
                 A = the Instruction-Locations of SCM+FSA,
                It=(Computation t1).(LifeSpan t1);
         A10: IC Wt=insloc 0 &
             Wt | D = It | D by A7,A8,A9,Th21;
         A11: t1 is halting by A9,SCM_HALT:def 5;
             set l0=intloc 0;
               not l0 in A by SCMFSA_2:84;
             then not l0 in dom t /\ A by XBOOLE_0:def 3;
         then A12: l0 in dom Result t1 & not l0 in dom (t | A)
              by RELAT_1:90,SCMFSA_2:66;
         A13: Wt.l0 =It.l0 by A10,SCMFSA6A:38
             .=(Result t1).l0 by A11,SCMFSA6B:16
             .=(Result t1 +* t | A).l0 by A12,FUNCT_4:12
             .=IExec(I,t).l0 by SCMFSA6B:def 1
             .=1 by SCM_HALT:17;
        A14: Iwhile c= tW0 by FUNCT_4:26;
               while>0(a,I) c= Iwhile by SCMFSA6A:26;
             then while>0(a,I) c= tW0 by A14,XBOOLE_1:1;
             then while>0(a,I) c= Wt by AMI_3:38;
             then Wt +* while>0(a,I) = Wt by AMI_5:10;
         then A15: Wt +* Iwhile = Wt by A10,A13,Th6;
               not a in A by SCMFSA_2:84;
             then not a in dom t /\ A by XBOOLE_0:def 3;
         then A16: a in dom Result t1 & not a in dom (t | A)
              by RELAT_1:90,SCMFSA_2:66;
                Wt.a =It.a by A10,SCMFSA6A:38
             .=(Result t1).a by A11,SCMFSA6B:16
             .=(Result t1 +* t | A).a by A16,FUNCT_4:12
             .=IExec(I,t).a by SCMFSA6B:def 1;
            then Wt.a < k+1 by A1,A6,A7;
            then Wt.a <= k by INT_1:20;
          then while>0(a,I) is_halting_onInit Wt by A4;
          then A17: Wt +* Iwhile is halting by SCM_HALT:def 5;
            now
           consider m be Nat such that
       A18: CurInstr((Computation Wt).m) = halt SCM+FSA by A15,A17,AMI_1:def 20
;
           take mm=((LifeSpan t1)+ 3)+m;
           thus CurInstr((Computation tW0).mm) = halt SCM+FSA
           by A18,AMI_1:51;
          end;
        then tW0 is halting by AMI_1:def 20;
       hence while>0(a,I) is_halting_onInit t by SCM_HALT:def 5;
     end;
     hence P[k+1];
  end;
A19: for k be Nat holds P[k] from Ind(A2,A3);
    now let t be State of SCM+FSA;
    per cases;
    suppose t.a<=0;
     hence while>0(a,I) is_halting_onInit t by Th16;
    suppose t.a>0;
      then reconsider n=t.a as Nat by INT_1:16;
        P[n] by A19;
      hence while>0(a,I) is_halting_onInit t;
  end;
  hence thesis by SCM_HALT:36;
end;

theorem Th30:   :: W_halt2
  for I be good InitHalting Macro-Instruction,a be read-write Int-Location
    st (for s be State of SCM+FSA holds
    IExec(I, s).a < s.a or IExec(I, s).a <= 0)
    holds while>0(a,I) is InitHalting
proof
    let I be good InitHalting Macro-Instruction,a be read-write Int-Location;
    assume A1:for s be State of SCM+FSA holds
        IExec(I, s).a < s.a or IExec(I, s).a <= 0;
      now let t be State of SCM+FSA;
        assume A2: t.a > 0;
        per cases by A1;
         suppose IExec(I, t).a < t.a;
           hence IExec(I, t).a < t.a;
         suppose IExec(I, t).a <= 0;
           hence IExec(I, t).a < t.a by A2;
    end;
    hence thesis by Th29;
end;

definition let D be set,
 f be Function of D,INT, d be Element of D;
 redefine func f.d -> Integer;
 coherence
  proof
     per cases;
     suppose D is non empty;
     then reconsider D as non empty set;
     reconsider d as Element of D;
     reconsider f as Function of D,INT;
       f.d is Integer;
     hence thesis;
     suppose D is empty;
     then f = {} by PARTFUN1:57;
     hence f.d is Integer by CARD_1:51,FUNCT_1:def 4,RELAT_1:60;
  end;
end;

theorem    :: W_halt3
   for I be good InitHalting Macro-Instruction,a be read-write Int-Location
   st ex f being Function of (product the Object-Kind of SCM+FSA),INT st
    (for s,t be State of SCM+FSA
    holds (f.s > 0 implies f.IExec(I, s) < f.s )
     & (s|D=t|D implies f.s=f.t) & ( f.s <= 0 iff s.a <= 0 ) )
   holds while>0(a,I) is InitHalting
proof
    let I be good InitHalting Macro-Instruction,a be read-write Int-Location;
    given f be Function of product the Object-Kind of SCM+FSA,INT
    such that A1: (for s,t be State of SCM+FSA holds (f.s > 0
    implies f.IExec(I, s) < f.s ) & (s|D=t|D implies f.s=f.t) &
    ( f.s <= 0 iff s.a <= 0 ) );
    defpred P[Nat] means
      for t be State of SCM+FSA st f.t <= $1 holds
       while>0(a,I) is_halting_onInit t;
A2: P[0]
    proof let t be State of SCM+FSA;
      assume f.t <= 0;
      then t.a <= 0 by A1;
      hence while>0(a,I) is_halting_onInit t by Th16;
    end;
A3: now let k be Nat;
      assume A4:P[k];
        now let t be State of SCM+FSA;
         assume A5:f.t <= k+1;
         per cases;
         suppose f.t<>k+1;
           then f.t < k+1 by A5,REAL_1:def 5;
           then f.t <= k by INT_1:20;
           hence while>0(a,I) is_halting_onInit t by A4;
         suppose A6:f.t=k+1;
         then A7: f.t > 0 by NAT_1:19;
         then A8: not t.a <= 0 by A1;
         A9: I is_closed_onInit t by SCM_HALT:35;
         A10: I is_halting_onInit t by SCM_HALT:36;
             set Iwhile=Initialized while>0(a,I),
                 tW0=t +* Iwhile,
                 t1=t +* Initialized I,
                 Wt=(Computation tW0).((LifeSpan t1)+ 3),
                 A = the Instruction-Locations of SCM+FSA,
                It=(Computation t1).(LifeSpan t1);
         A11: IC Wt=insloc 0 &
             Wt | D = It | D by A8,A9,A10,Th21;
         A12: t1 is halting by A10,SCM_HALT:def 5;
             set l0=intloc 0;
               not l0 in A by SCMFSA_2:84;
             then not l0 in dom t /\ A by XBOOLE_0:def 3;
         then A13: l0 in dom Result t1 & not l0 in dom (t | A)
              by RELAT_1:90,SCMFSA_2:66;
         A14: Wt.l0 =It.l0 by A11,SCMFSA6A:38
             .=(Result t1).l0 by A12,SCMFSA6B:16
             .=(Result t1 +* t | A).l0 by A13,FUNCT_4:12
             .=IExec(I,t).l0 by SCMFSA6B:def 1
             .=1 by SCM_HALT:17;
        A15: Iwhile c= tW0 by FUNCT_4:26;
               while>0(a,I) c= Iwhile by SCMFSA6A:26;
             then while>0(a,I) c= tW0 by A15,XBOOLE_1:1;
             then while>0(a,I) c= Wt by AMI_3:38;
             then Wt +* while>0(a,I) = Wt by AMI_5:10;
         then A16: Wt +* Iwhile = Wt by A11,A14,Th6;
               Wt | D =(Result t1) | D by A11,A12,SCMFSA6B:16
             .=(Result t1 +* t | A)|D by SCMFSA8C:35
             .=IExec(I,t) | D by SCMFSA6B:def 1;
             then f.Wt=f.IExec(I,t) by A1;
            then f.Wt < k+1 by A1,A6,A7;
            then f.Wt <= k by INT_1:20;
          then while>0(a,I) is_halting_onInit Wt by A4;
          then A17: Wt +* Iwhile is halting by SCM_HALT:def 5;
            now
           consider m be Nat such that
       A18: CurInstr((Computation Wt).m) = halt SCM+FSA by A16,A17,AMI_1:def 20
;
           take mm=((LifeSpan t1)+ 3)+m;
           thus CurInstr((Computation tW0).mm) = halt SCM+FSA
           by A18,AMI_1:51;
          end;
        then tW0 is halting by AMI_1:def 20;
       hence while>0(a,I) is_halting_onInit t by SCM_HALT:def 5;
     end;
     hence P[k+1];
  end;
A19: for k be Nat holds P[k] from Ind(A2,A3);
    now let t be State of SCM+FSA;
    per cases;
    suppose f.t<=0;
     then t.a <= 0 by A1;
     hence while>0(a,I) is_halting_onInit t by Th16;
    suppose f.t>0;
      then reconsider n=f.t as Nat by INT_1:16;
        P[n] by A19;
      hence while>0(a,I) is_halting_onInit t;
  end;
  hence thesis by SCM_HALT:36;
end;

theorem Th32:  ::WG002
 for s be State of SCM+FSA, I be Macro-Instruction,
     a be read-write Int-Location st s.a <= 0 holds
 IExec(while>0(a,I),s) | (Int-Locations \/ FinSeq-Locations) =
     (Initialize s) | (Int-Locations \/ FinSeq-Locations)
proof
   let s be State of SCM+FSA, I be Macro-Instruction,
   a be read-write Int-Location;
   set Is=Initialize s;
   assume s.a <= 0;
then A1: Is.a <= 0 by SCMFSA6C:3;
    set A = the Instruction-Locations of SCM+FSA;
    set s1 = Is +* (while>0(a,I) +* Start-At insloc 0);
    set s2 = (Computation s1).1;
    set s3 = (Computation s1).2;
    set s4 = (Computation s1).3;
    set s5 = (Computation s1).4;
    set C1 = Computation s1;
    set i = a >0_goto insloc 4;
A2: insloc 0 in dom while>0(a,I) by SCMFSA_9:10;
      while>0(a,I) c= while>0(a,I) +* Start-At insloc 0 by SCMFSA8A:9;
then A3: dom while>0(a,I) c= dom (while>0(a,I) +* Start-At insloc 0)
       by GRFUNC_1:8;
A4:  IC SCM+FSA in dom (while>0(a,I) +* Start-At insloc 0) by SF_MASTR:65;
A5: IC s1 = s1.IC SCM+FSA by AMI_1:def 15
    .= (while>0(a,I) +* Start-At insloc 0).IC SCM+FSA by A4,FUNCT_4:14
    .= insloc 0 by SF_MASTR:66;
    s1.insloc 0 = (while>0(a,I) +* Start-At insloc 0).insloc 0 by A2,A3,FUNCT_4
:14
  .= while>0(a,I).insloc 0 by A2,SCMFSA6B:7
  .= i by SCMFSA_9:11;
then A6: CurInstr s1 = i by A5,AMI_1:def 17;
A7: (Computation s1).(0 + 1) = Following (Computation s1).0 by AMI_1:def 19
    .= Following s1 by AMI_1:def 19
    .= Exec(i,s1) by A6,AMI_1:def 18;
      not a in dom (while>0(a,I) +* Start-At insloc 0) & a in dom Is
       by SCMFSA6B:12,SCMFSA_2:66;
    then A8: s1.a = Is.a by FUNCT_4:12;
A9: IC C1.1 = C1.1.IC SCM+FSA by AMI_1:def 15
    .= Next insloc 0 by A1,A5,A7,A8,SCMFSA_2:97
    .= insloc (0 + 1) by SCMFSA_2:32;
A10: insloc 1 in dom while>0(a,I) by SCMFSA_9:10;
      C1.1.insloc 1 = s1.insloc 1 by AMI_1:54
    .= (while>0(a,I) +* Start-At insloc 0).insloc 1 by A3,A10,FUNCT_4:14
    .= while>0(a,I).insloc 1 by A10,SCMFSA6B:7
    .= goto insloc 2 by SCMFSA_9:11;
then A11: CurInstr C1.1 = goto insloc 2 by A9,AMI_1:def 17;
A12: (Computation s1).(1 + 1) = Following s2 by AMI_1:def 19
    .= Exec(goto insloc 2,s2) by A11,AMI_1:def 18;
A13: insloc 2 in dom while>0(a,I) by SCMFSA_9:37;

A14: IC s3 = s3.IC SCM+FSA by AMI_1:def 15
    .= insloc 2 by A12,SCMFSA_2:95;
      s3.insloc 2 = s1.insloc 2 by AMI_1:54
    .= (while>0(a,I) +* Start-At insloc 0).insloc 2 by A3,A13,FUNCT_4:14
    .= while>0(a,I).insloc 2 by A13,SCMFSA6B:7
    .= goto insloc 3 by SCMFSA_9:41;
then A15:  CurInstr s3 = goto insloc 3 by A14,AMI_1:def 17;
A16: (Computation s1).(2 + 1) = Following s3 by AMI_1:def 19
    .= Exec(goto insloc 3,s3) by A15,AMI_1:def 18;
A17: insloc 3 in dom while>0(a,I) by SCMFSA_9:37;
     set loc5= insloc (card I +5);
A18:  IC s4 = s4.IC SCM+FSA by AMI_1:def 15
    .= insloc 3 by A16,SCMFSA_2:95;
      s4.insloc 3 = s1.insloc 3 by AMI_1:54
    .= (while>0(a,I) +* Start-At insloc 0).insloc 3 by A3,A17,FUNCT_4:14
    .= while>0(a,I).insloc 3 by A17,SCMFSA6B:7
    .= goto loc5 by SCMFSA_9:40;
then A19: CurInstr s4 = goto loc5 by A18,AMI_1:def 17;
A20: (Computation s1).(3 + 1) = Following s4 by AMI_1:def 19
    .= Exec(goto loc5,s4) by A19,AMI_1:def 18;

A21: loc5 in dom while>0(a,I) by SCMFSA_9:38;

A22:  IC s5 = s5.IC SCM+FSA by AMI_1:def 15
     .= loc5 by A20,SCMFSA_2:95;
       s5.loc5 = s1.loc5 by AMI_1:54
     .= (while>0(a,I) +* Start-At insloc 0).loc5 by A3,A21,FUNCT_4:14
     .= while>0(a,I).loc5 by A21,SCMFSA6B:7
     .= halt SCM+FSA by SCMFSA_9:39;
then A23:  CurInstr s5 = halt SCM+FSA by A22,AMI_1:def 17;
then A24: s1 is halting by AMI_1:def 20;
A25: Is +* Initialized while>0(a,I) =
   Initialize Is +* (while>0(a,I) +* Start-At insloc 0) by SCMFSA8A:13
   .=s1 by SCMFSA8C:15;
     now let k be Nat;
      assume A26: CurInstr (Computation s1).k = halt SCM+FSA;
        CurInstr (Computation s1).0 = i by A6,AMI_1:def 19;
      then A27: k <> 0 by A26,SCMFSA_9:8;
      A28: k <> 1 by A11,A26,SCMFSA_9:9;
      A29: k <> 2 by A15,A26,SCMFSA_9:9;
           goto loc5 <> halt SCM+FSA by SCMFSA_9:9;
         then 3<k by A19,A26,A27,A28,A29,CQC_THE1:4;
       hence 3+1<=k by INT_1:20;
   end;
then A30: LifeSpan s1 = 4 by A23,A24,SCM_1:def 2;
      Is.intloc 0=1 & IC Is = insloc 0 by SCMFSA6C:3;
    then s1=Is+*while>0(a,I) by A25,Th6;
then A31: Is,s1 equal_outside A by SCMFSA6A:27;
A32: now let a be Int-Location;
      thus Is.a = s1.a by A31,SCMFSA6A:30
           .=s2.a by A7,SCMFSA_2:97
           .=s3.a by A12,SCMFSA_2:95
           .=s4.a by A16,SCMFSA_2:95
           .=s5.a by A20,SCMFSA_2:95;
   end;
A33: now let f be FinSeq-Location;
      thus Is.f = s1.f by A31,SCMFSA6A:31
           .=s2.f by A7,SCMFSA_2:97
           .=s3.f by A12,SCMFSA_2:95
           .=s4.f by A16,SCMFSA_2:95
           .=s5.f by A20,SCMFSA_2:95;
   end;
  thus
     IExec(while>0(a,I),s) | D = IExec(while>0(a,I),Is) | D by SCMFSA8C:17
   .= (Result (Is +* Initialized while>0(a,I)) +* Is | A) | D by SCMFSA6B:def 1
   .= (Result s1) | D by A25,SCMFSA8C:35
   .= s5 | D by A24,A30,SCMFSA6B:16
   .= Is | D by A32,A33,SCMFSA6A:38;
end;

theorem Th33:  ::WG004
 for s be State of SCM+FSA, I be good InitHalting Macro-Instruction,
    a be read-write Int-Location st s.a > 0 & while>0(a,I) is InitHalting
   holds
   IExec(while>0(a,I),s) | (Int-Locations \/ FinSeq-Locations) =
   IExec(while>0(a,I),IExec(I,s)) | (Int-Locations \/ FinSeq-Locations)
proof
   let s be State of SCM+FSA,I be good InitHalting Macro-Instruction,
   a be read-write Int-Location;
   assume A1:s.a > 0 & while>0(a,I) is InitHalting;
   set ps = s | the Instruction-Locations of SCM+FSA,
       sI = s +* Initialized I,
       Iwhile= Initialized while>0(a,I),
       sW = s +* Iwhile,
       s3 = (Computation sI).(LifeSpan sI) +* Iwhile,
       m1 = LifeSpan sI,
       m3 = LifeSpan s3,
       CI = Computation sI,
       CW = Computation sW,
       C3 = Computation s3;
      set A = the Instruction-Locations of SCM+FSA;

   Initialized I c= sI by FUNCT_4:26;
then A2: sI is halting by AMI_1:def 26;
A3: Iwhile c= sW by FUNCT_4:26;
A4:Iwhile is halting by A1,SCM_HALT:def 2;
then A5: sW is halting by A3,AMI_1:def 26;
A6: Iwhile c= s3 by FUNCT_4:26;
then A7: s3 is halting by A4,AMI_1:def 26;

A8: dom ps = dom s /\ A by RELAT_1:90
   .= (Int-Locations \/ FinSeq-Locations \/ {IC SCM+FSA} \/ A) /\
 A by SCMFSA6A:34
   .= A by XBOOLE_1:21;
     CI.m1, CI.m1 +* ps equal_outside dom ps by FUNCT_7:31;
  then CI.m1 +* Iwhile, CI.m1 +* ps +* Iwhile equal_outside dom ps
  by SCMFSA6A:11;
then A9: CI.m1 +* ps +* Iwhile, CI.m1 +*Iwhile equal_outside dom ps
   by FUNCT_7:28;
    Result (IExec(I,s) +* Iwhile),Result s3 equal_outside A
  proof
  A10: Iwhile c= IExec(I,s) +* Iwhile by FUNCT_4:26;
        IExec(I,s) = Result (s +* Initialized I) +* ps by SCMFSA6B:def 1
      .= CI.m1 +* ps by A2,SCMFSA6B:16;
      hence thesis by A1,A6,A8,A9,A10,Th12;
  end;
then A11: Result (IExec(I,s) +* Iwhile) +* ps = Result s3 +* ps
                           by A8,SCMFSA6A:13;
    set mW=LifeSpan sW;
      mW <= (m1+3+m3) + mW by NAT_1:29;
then A12: mW <= m1+3+(m3+mW) by XCMPLX_1:1;
A13: IExec(while>0(a,I),s)
    = Result (s +* Iwhile) +* ps by SCMFSA6B:def 1
   .= CW.mW +* ps by A5,SCMFSA6B:16
   .= CW.(m1+3+(m3+ mW)) +* ps by A5,A12,Th15;
    IExec(I,s) | A = (Result (s +* Initialized I) +* ps) | A by SCMFSA6B:def 1
   .= ps by SCMFSA6A:40;
then A14: IExec(while>0(a,I),IExec(I,s))
    = Result (IExec(I,s) +* Iwhile) +* ps by SCMFSA6B:def 1
   .= C3.m3 +* ps by A7,A11,SCMFSA6B:16;

A15: (Computation CW.(m1 + 3)).(m3+mW) | D = C3.m3 | D
   proof
     set Cm3=CW.(m1 + 3);
     A16: I is_closed_onInit s by SCM_HALT:35;
     A17: I is_halting_onInit s by SCM_HALT:36;
     then A18: IC Cm3=insloc 0 by A1,A16,Th21;
     then A19: IC Cm3=IC s3 by A6,SCMFSA6B:34;
     A20: Cm3 | D =CI.m1 | D by A1,A16,A17,Th21
         .=(CI.m1 +* while>0(a,I)) | D by SCMFSA8C:34;
         reconsider Wg=while>0(a,I) as good InitHalting Macro-Instruction
         by A1;
           Wg is keepInt0_1;
     then A21: Cm3.intloc 0 =1 by A3,SCM_HALT:def 3;
           while>0(a,I) c= Iwhile by SCMFSA6A:26;
         then while>0(a,I) c= sW by A3,XBOOLE_1:1;
         then while>0(a,I) c= CW.(m1+3) by AMI_3:38;
         then Cm3 +* while>0(a,I) = Cm3 by AMI_5:10;
         then Cm3 +* Iwhile = Cm3 by A18,A21,Th6;
     then A22: Iwhile c= Cm3 by FUNCT_4:26;
     A23: now let f be FinSeq-Location;
           A24: not f in dom Iwhile by SCMFSA6A:49;
           A25: not f in dom while>0(a,I) by Th13;
           thus s3.f = CI.m1.f by A24,FUNCT_4:12
              .=(CI.m1 +* while>0(a,I)).f by A25,FUNCT_4:12
              .=Cm3.f by A20,SCMFSA6A:38;
         end;
        now let b be Int-Location;
           per cases;
           suppose b <> intloc 0;
             then A26: not b in dom Iwhile by SCMFSA6A:48;
             A27: not b in dom while>0(a,I) by Th14;
             thus s3.b = CI.m1.b by A26,FUNCT_4:12
               .=(CI.m1 +* while>0(a,I)).b by A27,FUNCT_4:12
               .=Cm3.b by A20,SCMFSA6A:38;
           suppose b = intloc 0;
             hence s3.b=Cm3.b by A6,A21,SCM_HALT:7;
         end;
     then A28: Cm3,s3 equal_outside A by A19,A23,SCMFSA6A:28;
     then A29: LifeSpan Cm3 = m3 by A1,A6,A22,Th12;
     A30: Result Cm3,Result s3 equal_outside A by A1,A6,A22,A28,Th12;
     A31: Cm3 is halting by A4,A22,AMI_1:def 26;
       (LifeSpan Cm3) <= (LifeSpan Cm3) + mW by NAT_1:29;
    hence (Computation Cm3).(m3+mW) | D =
(Computation Cm3).(LifeSpan Cm3) | D by A29,A31,Th15
        .=(Result Cm3) | D by A31,SCMFSA6B:16
        .=(Result s3) | D by A30,SCMFSA6A:39
        .=C3.m3 | D by A7,SCMFSA6B:16;
   end;
   thus IExec(while>0(a,I),s) | D = IExec(while>0(a,I),IExec(I,s)) | D
   proof
A32:    dom ps misses D by A8,SCMFSA_2:13,14,XBOOLE_1:70;
      hence IExec(while>0(a,I),s) | D
       = CW.(m1 + 3 + (m3+ mW)) | D by A13,AMI_5:7
      .= C3.m3 | D by A15,AMI_1:51
      .= IExec(while>0(a,I),IExec(I,s)) | D by A14,A32,AMI_5:7;
    end;
end;

theorem Th34:  ::WG006
 for s be State of SCM+FSA, I be Macro-Instruction,
     f be FinSeq-Location,a be read-write Int-Location st s.a <= 0 holds
     IExec(while>0(a,I),s).f=s.f
proof
     let s be State of SCM+FSA,I be Macro-Instruction,
     f be FinSeq-Location,a be read-write Int-Location;
     assume A1: s.a <= 0;
       f in FinSeq-Locations by SCMFSA_2:10;
then A2:  f in D by XBOOLE_0:def 2;
    hence
      IExec(while>0(a,I),s).f=(IExec(while>0(a,I),s) | D).f by FUNCT_1:72
     .= ((Initialize s) | D).f by A1,Th32
     .= (Initialize s).f by A2,FUNCT_1:72
     .= s.f by SCMFSA6C:3;
end;

theorem Th35:  ::WG008
 for s be State of SCM+FSA, I be Macro-Instruction,
     b be Int-Location,a be read-write Int-Location st s.a <= 0 holds
     IExec(while>0(a,I),s).b=(Initialize s).b
proof
     let s be State of SCM+FSA,I be Macro-Instruction,
     b be Int-Location,a be read-write Int-Location;
     assume A1: s.a <= 0;
       b in Int-Locations by SCMFSA_2:9;
then A2:  b in D by XBOOLE_0:def 2;
     hence
       IExec(while>0(a,I),s).b=(IExec(while>0(a,I),s) | D).b by FUNCT_1:72
     .= ((Initialize s) | D).b by A1,Th32
     .= (Initialize s).b by A2,FUNCT_1:72;
end;

theorem Th36:  ::WG010
 for s be State of SCM+FSA, I be good InitHalting Macro-Instruction,
     f be FinSeq-Location,a be read-write Int-Location st
     s.a > 0 & while>0(a,I) is InitHalting holds
     IExec(while>0(a,I),s).f =IExec(while>0(a,I),IExec(I,s)).f
proof
     let s be State of SCM+FSA,I be good InitHalting Macro-Instruction,
     f be FinSeq-Location,a be read-write Int-Location;
     assume A1: s.a > 0 & while>0(a,I) is InitHalting;
       f in FinSeq-Locations by SCMFSA_2:10;
then A2:  f in D by XBOOLE_0:def 2;
   then IExec(while>0(a,I),s).f=(IExec(while>0(a,I),s) | D).f by FUNCT_1:72
   .=(IExec(while>0(a,I),IExec(I,s)) | D).f by A1,Th33;
   hence thesis by A2,FUNCT_1:72;
end;

theorem Th37:  ::WG012
 for s be State of SCM+FSA, I be good InitHalting Macro-Instruction,
     b be Int-Location,a be read-write Int-Location st
     s.a > 0 & while>0(a,I) is InitHalting holds
     IExec(while>0(a,I),s).b =IExec(while>0(a,I),IExec(I,s)).b
proof
     let s be State of SCM+FSA,I be good InitHalting Macro-Instruction,
     b be Int-Location,a be read-write Int-Location;
     assume A1: s.a > 0 & while>0(a,I) is InitHalting;
       b in Int-Locations by SCMFSA_2:9;
then A2:  b in D by XBOOLE_0:def 2;
     then IExec(while>0(a,I),s).b=(IExec(while>0(a,I),s) | D).b by FUNCT_1:72
     .=(IExec(while>0(a,I),IExec(I,s)) | D).b by A1,Th33;
     hence thesis by A2,FUNCT_1:72;
end;

begin   ::  - Insert Sort Algorithm -
set a0 = intloc 0;
set a1 = intloc 1;
set a2 = intloc 2;
set a3 = intloc 3;
set a4 = intloc 4;
set a5 = intloc 5;
set a6 = intloc 6;
set initializeWorkMem= (a2:= a0) ';' (a3:= a0) ';'
                   (a4:= a0) ';' (a5:= a0) ';' (a6:= a0);
:: set a0 = intloc 0;
:: set a1 = intloc 1;
:: set a2 = intloc 2;
:: set a3 = intloc 3;
:: set a4 = intloc 4;
:: set a5 = intloc 5;
:: set a6 = intloc 6;
:: set initializeWorkMem= (a2:= a0) ';' (a3:= a0) ';'
::                  (a4:= a0) ';' (a5:= a0) ';' (a6:= a0);

definition
 let f be FinSeq-Location;
 func insert-sort f -> Macro-Instruction means
:Def2:  ::def1
   it=
   initializeWorkMem ';'
       (a1:=len f) ';'
       SubFrom(a1,a0) ';'
       Times(a1,
          ((a2:=len f) ';' SubFrom(a2,a1) ';' (a3 := a2) ';'
          AddTo(a3,a0) ';' (a6:=(f,a3)) ';' SubFrom(a4,a4)) ';'
          while>0(a2, (a5:=(f,a2)) ';' SubFrom(a5,a6) ';'
               if>0(a5,Macro SubFrom(a2,a2),
                    AddTo(a4,a0) ';' SubFrom(a2,a0))
          ) ';'
          Times(a4,
               (a2:=a3) ';'
               SubFrom(a3,a0) ';'
               (a5:=(f,a2)) ';'
               (a6:=(f,a3)) ';'
               ((f,a2):=a6) ';'((f,a3):=a5)
          )
       );
  correctness;
end;

definition
 func Insert-Sort-Algorithm -> Macro-Instruction means
:Def3:  ::def2
  it = insert-sort fsloc 0;
  correctness;
end;

theorem Th38:   ::IS002
 for f being FinSeq-Location holds
  UsedIntLoc (insert-sort f) = {a0,a1,a2,a3,a4,a5,a6}
proof
  let f be FinSeq-Location;
  set i1= a2:=a3,
       i2= SubFrom(a3,a0),
       i3= a5:=(f,a2),
       i4= a6:=(f,a3),
       i5= (f,a2):=a6,
       i6= (f,a3):=a5,
       body3= i1 ';' i2 ';' i3 ';' i4 ';' i5 ';' i6,
       Ui123=UsedIntLoc (i1 ';' i2 ';'i3 ),
       Ui12=UsedIntLoc (i1 ';' i2 ),
       Ub3=UsedIntLoc body3;
A1: Ub3 = {a3,a5} \/ {a2,a0,a6}
   proof thus
      Ub3 = (UsedIntLoc (i1 ';' i2 ';'i3 ';'i4 ';' i5 ))
         \/ UsedIntLoc i6 by SF_MASTR:34
     .= (UsedIntLoc (i1 ';' i2 ';'i3 ';'i4 ';' i5 )) \/ {a3,a5} by SF_MASTR:21
     .= (UsedIntLoc (i1 ';' i2 ';'i3 ';' i4)) \/ (UsedIntLoc i5) \/ {a3,a5}
         by SF_MASTR:34
     .= (UsedIntLoc (i1 ';' i2 ';'i3 ';' i4)) \/ {a2,a6} \/ {a3,a5}
         by SF_MASTR:21
     .= Ui123 \/ (UsedIntLoc i4) \/ {a2,a6} \/ {a3,a5} by SF_MASTR:34
     .= Ui123 \/ {a6,a3} \/ {a2,a6} \/ {a3,a5} by SF_MASTR:21
     .= Ui123 \/ ({a6,a3} \/ {a2,a6}) \/ {a3,a5} by XBOOLE_1:4
     .= Ui123 \/ {a6,a3,a2,a6} \/ {a3,a5} by ENUMSET1:45
     .= Ui123 \/ {a6,a6,a2,a3} \/ {a3,a5} by ENUMSET1:107
     .= Ui123 \/ {a6,a2,a3} \/ {a3,a5} by ENUMSET1:71
     .= Ui123 \/ ({a6,a2} \/ {a3}) \/ {a3,a5} by ENUMSET1:43
     .= Ui123 \/ {a6,a2} \/ {a3} \/ {a3,a5} by XBOOLE_1:4
     .= Ui123 \/ {a6,a2} \/ ({a3} \/ {a3,a5}) by XBOOLE_1:4
     .= Ui123 \/ {a6,a2} \/ {a3,a3,a5} by ENUMSET1:42
     .= Ui123 \/ {a6,a2} \/ {a3,a5} by ENUMSET1:70
     .= Ui12 \/ (UsedIntLoc i3) \/ {a6,a2} \/ {a3,a5} by SF_MASTR:34
     .= Ui12 \/ {a5,a2} \/ {a6,a2} \/ {a3,a5} by SF_MASTR:21
     .= Ui12 \/ ({a5,a2} \/ {a6,a2}) \/ {a3,a5} by XBOOLE_1:4
     .= Ui12 \/ {a5,a2,a6,a2} \/ {a3,a5} by ENUMSET1:45
     .= Ui12 \/ {a2,a2,a6,a5} \/ {a3,a5} by ENUMSET1:123
     .= Ui12 \/ {a2,a6,a5} \/ {a3,a5} by ENUMSET1:71
     .= Ui12 \/ ({a2,a6} \/ {a5}) \/ {a3,a5} by ENUMSET1:43
     .= Ui12 \/ {a2,a6} \/ {a5} \/ {a3,a5} by XBOOLE_1:4
     .= Ui12 \/ {a2,a6} \/ ({a5} \/ {a3,a5}) by XBOOLE_1:4
     .= Ui12 \/ {a2,a6} \/ {a5,a3,a5} by ENUMSET1:43
     .= Ui12 \/ {a2,a6} \/ {a5,a5,a3} by ENUMSET1:98
     .= Ui12 \/ {a2,a6} \/ {a5,a3} by ENUMSET1:70
     .= (UsedIntLoc i1) \/ (UsedIntLoc i2) \/ {a2,a6} \/ {a5,a3} by SF_MASTR:35
     .= {a2,a3} \/ (UsedIntLoc i2) \/ {a2,a6} \/ {a5,a3} by SF_MASTR:18
     .= {a2,a3} \/ {a3,a0} \/ {a2,a6} \/ {a5,a3} by SF_MASTR:18
     .= {a2,a3,a3,a0} \/ {a2,a6} \/ {a5,a3} by ENUMSET1:45
     .= {a3,a3,a2,a0} \/ {a2,a6} \/ {a5,a3} by ENUMSET1:116
     .= {a3,a2,a0} \/ {a2,a6} \/ {a5,a3} by ENUMSET1:71
     .= {a3} \/ {a2,a0} \/ {a2,a6} \/ {a5,a3} by ENUMSET1:42
     .= {a3} \/ ({a2,a0} \/ {a2,a6}) \/ {a5,a3} by XBOOLE_1:4
     .= {a3} \/ {a2,a0,a2,a6} \/ {a5,a3} by ENUMSET1:45
     .= {a3} \/ {a2,a2,a0,a6} \/ {a5,a3} by ENUMSET1:104
     .= {a3} \/ {a2,a0,a6} \/ {a5,a3} by ENUMSET1:71
     .= {a3} \/ {a5,a3} \/ {a2,a0,a6} by XBOOLE_1:4
     .= {a3,a5,a3} \/ {a2,a0,a6} by ENUMSET1:43
     .= {a3,a3,a5} \/ {a2,a0,a6} by ENUMSET1:98
     .= {a3,a5} \/ {a2,a0,a6} by ENUMSET1:70;
   end;
     set k2= a2:= a0,
          k3= a3:= a0,
          k4= a4:= a0,
          k5= a5:= a0;
A2:  UsedIntLoc initializeWorkMem = {a0} \/ {a2,a3,a4,a5,a6}
   proof thus
       UsedIntLoc initializeWorkMem = UsedIntLoc (k2 ';' k3 ';' k4 ';' k5)
     \/ UsedIntLoc (a6:= a0) by SF_MASTR:34
    .= UsedIntLoc (k2 ';' k3 ';' k4 ';' k5) \/ {a6,a0} by SF_MASTR:18
    .= UsedIntLoc (k2 ';' k3 ';' k4 ) \/ UsedIntLoc k5 \/ {a6,a0}
        by SF_MASTR:34
    .= UsedIntLoc (k2 ';' k3 ';' k4 ) \/ {a5,a0} \/ {a6,a0} by SF_MASTR:18
    .= UsedIntLoc (k2 ';' k3 ) \/ UsedIntLoc k4 \/ {a5,a0} \/
 {a6,a0} by SF_MASTR:34
    .= UsedIntLoc (k2 ';' k3 ) \/ {a4,a0} \/ {a5,a0} \/ {a6,a0} by SF_MASTR:18
    .= UsedIntLoc k2 \/ UsedIntLoc k3 \/ {a4,a0} \/ {a5,a0} \/ {a6,a0}
       by SF_MASTR:35
    .= UsedIntLoc k2 \/ {a3,a0} \/ {a4,a0} \/ {a5,a0} \/
 {a6,a0} by SF_MASTR:18
    .= {a2,a0} \/ {a3,a0} \/ {a4,a0} \/ {a5,a0} \/ {a6,a0} by SF_MASTR:18
    .= {a2,a0} \/ {a3,a0} \/ {a4,a0} \/ ({a5,a0} \/ {a6,a0}) by XBOOLE_1:4
    .= {a2,a0} \/ {a3,a0} \/ {a4,a0} \/ {a0,a5,a6} by SCMBSORT:32
    .= {a0,a2,a3} \/ {a4,a0} \/ {a0,a5,a6} by SCMBSORT:32
    .= {a0,a2,a3} \/ {a4,a0} \/ ({a0} \/ {a5,a6}) by ENUMSET1:42
    .= {a0,a2,a3} \/ {a4,a0} \/ {a0} \/ {a5,a6} by XBOOLE_1:4
    .= {a0,a2,a3} \/ ({a4,a0} \/ {a0}) \/ {a5,a6} by XBOOLE_1:4
    .= {a0,a2,a3} \/ {a4,a0,a0} \/ {a5,a6} by ENUMSET1:43
    .= {a0,a2,a3} \/ ({a0,a0} \/ {a4}) \/ {a5,a6} by ENUMSET1:42
    .= {a0,a2,a3} \/ {a0,a0} \/ {a4} \/ {a5,a6} by XBOOLE_1:4
    .= {a0,a0,a0,a2,a3} \/ {a4} \/ {a5,a6} by ENUMSET1:48
    .= {a0,a2,a3} \/ {a4} \/ {a5,a6} by ENUMSET1:78
    .= {a0,a2,a3,a4} \/ {a5,a6} by ENUMSET1:46
    .= {a0,a2,a3,a4,a5,a6} by ENUMSET1:54
    .= {a0} \/ {a2,a3,a4,a5,a6} by ENUMSET1:51;
  end;
    set m0=SubFrom(a2,a2),
        m1=Macro m0,
        m2=AddTo(a4,a0),
        m3=SubFrom(a2,a0),
        IF=if>0(a5, m1, m2 ';' m3),
        UIF = UsedIntLoc IF;
A3:  UIF = {a2,a5} \/ {a4,a0}
   proof thus
       UIF = {a5} \/ UsedIntLoc (m1) \/ UsedIntLoc(m2 ';' m3) by SCMBSORT:29
     .= {a5} \/ UsedIntLoc m0 \/ UsedIntLoc(m2 ';' m3) by SF_MASTR:32
     .= {a5} \/ {a2,a2} \/ UsedIntLoc(m2 ';' m3) by SF_MASTR:18
     .= {a5} \/ {a2,a2} \/ (UsedIntLoc m2 \/ UsedIntLoc m3) by SF_MASTR:35
     .= {a5} \/ {a2,a2} \/ ({a4,a0} \/ UsedIntLoc m3) by SF_MASTR:18
     .= {a5} \/ {a2,a2} \/ ({a4,a0} \/ {a2,a0}) by SF_MASTR:18
     .= {a5} \/ {a2} \/ ({a4,a0} \/ {a2,a0}) by ENUMSET1:69
     .= {a5} \/ {a2} \/ {a2,a0} \/ {a4,a0} by XBOOLE_1:4
     .= {a2,a5} \/ {a2,a0} \/ {a4,a0} by ENUMSET1:41
     .= {a2,a5,a2,a0} \/ {a4,a0} by ENUMSET1:45
     .= {a2,a2,a5,a0} \/ {a4,a0} by ENUMSET1:104
     .= {a2,a5,a0} \/ {a4,a0} by ENUMSET1:71
     .= {a2,a5,a0,a4,a0} by ENUMSET1:49
     .= {a2} \/ {a5,a0,a4,a0} by ENUMSET1:47
     .= {a2} \/ {a0,a0,a4,a5} by ENUMSET1:123
     .= {a2} \/ {a0,a4,a5} by ENUMSET1:71
     .= {a2,a0,a4,a5} by ENUMSET1:44
     .= {a2,a5,a4,a0} by ENUMSET1:107
     .= {a2,a5} \/ {a4,a0} by ENUMSET1:45;
   end;
   set n1=a5:=(f,a2),
        n2=SubFrom(a5,a6),
        body2=n1 ';'n2 ';' IF,
        Ub2=UsedIntLoc body2;
A4: Ub2 = {a5,a2,a6,a4,a0}
  proof thus
      Ub2 = UsedIntLoc (n1 ';'n2) \/ UIF by SF_MASTR:31
    .= UsedIntLoc n1 \/ UsedIntLoc n2 \/ UIF by SF_MASTR:35
    .= {a2,a5} \/ UsedIntLoc n2 \/ UIF by SF_MASTR:21
    .= {a2,a5} \/ {a5,a6} \/ UIF by SF_MASTR:18
    .= {a2,a5,a5,a6} \/ UIF by ENUMSET1:45
    .= {a5,a5,a2,a6} \/ UIF by ENUMSET1:116
    .= {a5,a2,a6} \/ ({a2,a5} \/ {a4,a0}) by A3,ENUMSET1:71
    .= {a5,a2,a6} \/ {a2,a5} \/ {a4,a0} by XBOOLE_1:4
    .= {a2,a5,a5,a2,a6} \/ {a4,a0} by ENUMSET1:48
    .= {a2,a5,a5,a2} \/ {a6} \/ {a4,a0} by ENUMSET1:50
    .= {a2,a2,a5,a5} \/ {a6} \/ {a4,a0} by ENUMSET1:107
    .= {a2,a5,a5} \/ {a6} \/ {a4,a0} by ENUMSET1:71
    .= {a5,a5,a2} \/ {a6} \/ {a4,a0} by ENUMSET1:102
    .= {a5,a2} \/ {a6} \/ {a4,a0} by ENUMSET1:70
    .= {a5,a2,a6} \/ {a4,a0} by ENUMSET1:43
    .= {a5,a2,a6,a4,a0} by ENUMSET1:49;
   end;
    set T3=Times(a4,body3),
        t1=a2:=len f,
        t2=SubFrom(a2,a1),
        t3=a3 := a2,
        t4=AddTo(a3,a0),
        t5=a6:=(f,a3),
        t6=SubFrom(a4,a4),
        Wg=while>0(a2,body2),
        t16=t1 ';' t2 ';' t3 ';' t4 ';' t5 ';' t6,
        body1=t16 ';' Wg ';' T3,
        Ub1 =UsedIntLoc body1,
        Ut1_6=UsedIntLoc t16;
A5:   Ut1_6={a3,a2,a1} \/ {a6,a4,a0}
  proof thus
      Ut1_6=UsedIntLoc (t1 ';' t2 ';' t3 ';' t4 ';' t5 ) \/ UsedIntLoc t6
        by SF_MASTR:34
      .=UsedIntLoc (t1 ';' t2 ';' t3 ';' t4 ';' t5 ) \/ {a4,a4} by SF_MASTR:18
      .=UsedIntLoc (t1 ';' t2 ';' t3 ';' t4) \/ UsedIntLoc t5 \/ {a4,a4}
          by SF_MASTR:34
      .=UsedIntLoc (t1 ';' t2 ';' t3 ';' t4) \/ {a3,a6} \/ {a4,a4}
          by SF_MASTR:21
      .=UsedIntLoc (t1 ';' t2 ';' t3) \/ UsedIntLoc t4 \/ {a3,a6} \/ {a4,a4}
          by SF_MASTR:34
      .=UsedIntLoc (t1 ';' t2 ';' t3) \/ {a3,a0} \/ {a3,a6} \/ {a4,a4}
          by SF_MASTR:18
      .=UsedIntLoc (t1 ';' t2) \/ UsedIntLoc t3 \/ {a3,a0} \/ {a3,a6} \/
 {a4,a4}
          by SF_MASTR:34
      .=UsedIntLoc (t1 ';' t2) \/ {a3,a2} \/ {a3,a0} \/ {a3,a6} \/ {a4,a4}
          by SF_MASTR:18
      .=UsedIntLoc t1 \/ UsedIntLoc t2 \/ {a3,a2} \/ {a3,a0} \/ {a3,a6} \/
 {a4,a4}
          by SF_MASTR:35
      .={a2} \/ UsedIntLoc t2 \/ {a3,a2} \/ {a3,a0} \/ {a3,a6} \/ {a4,a4}
          by SF_MASTR:22
      .={a2} \/ {a2,a1} \/ {a3,a2} \/ {a3,a0} \/ {a3,a6} \/
 {a4,a4} by SF_MASTR:18
      .={a2,a2,a1} \/ {a3,a2} \/ {a3,a0} \/ {a3,a6} \/ {a4,a4} by ENUMSET1:42
      .={a2,a1} \/ {a3,a2} \/ {a3,a0} \/ {a3,a6} \/ {a4,a4} by ENUMSET1:70
      .={a2,a1,a3,a2} \/ {a3,a0} \/ {a3,a6} \/ {a4,a4} by ENUMSET1:45
      .={a2,a2,a3,a1} \/ {a3,a0} \/ {a3,a6} \/ {a4,a4} by ENUMSET1:107
      .={a2,a3,a1} \/ {a3,a0} \/ {a3,a6} \/ {a4,a4} by ENUMSET1:71
      .={a2,a3,a1,a3,a0} \/ {a3,a6} \/ {a4,a4} by ENUMSET1:49
      .={a2,a3,a1,a3} \/ {a0} \/ {a3,a6} \/ {a4,a4} by ENUMSET1:50
      .={a3,a3,a1,a2} \/ {a0} \/ {a3,a6} \/ {a4,a4} by ENUMSET1:123
      .={a3,a1,a2} \/ {a0} \/ {a3,a6} \/ {a4,a4} by ENUMSET1:71
      .={a3,a1,a2} \/ {a0} \/ {a3,a6} \/ {a4} by ENUMSET1:69
      .={a3,a1,a2} \/ {a3,a6} \/ {a0} \/ {a4} by XBOOLE_1:4
      .={a3,a1,a2,a3,a6} \/ {a0} \/ {a4} by ENUMSET1:49
      .={a3,a1,a2,a3} \/ {a6} \/ {a0} \/ {a4} by ENUMSET1:50
      .={a3,a3,a2,a1} \/ {a6} \/ {a0} \/ {a4} by ENUMSET1:107
      .={a3,a2,a1} \/ {a6} \/ {a0} \/ {a4} by ENUMSET1:71
      .={a3,a2,a1} \/ ({a6} \/ {a0}) \/ {a4} by XBOOLE_1:4
      .={a3,a2,a1} \/ {a6,a0} \/ {a4} by ENUMSET1:41
      .={a3,a2,a1} \/ ({a6,a0} \/ {a4}) by XBOOLE_1:4
      .={a3,a2,a1} \/ {a6,a0,a4} by ENUMSET1:43
      .={a3,a2,a1} \/ {a6,a4,a0} by ENUMSET1:98;
   end;
A6: Ub1 ={a0,a1,a2,a3,a4,a5,a6}
 proof
    thus
      Ub1 = UsedIntLoc (t16 ';' Wg) \/ UsedIntLoc T3 by SF_MASTR:31
    .= UsedIntLoc (t16 ';' Wg) \/ (Ub3 \/ {a4,a0}) by SCMBSORT:31
    .= Ut1_6 \/ UsedIntLoc Wg \/ (Ub3 \/ {a4,a0}) by SF_MASTR:31
    .= Ut1_6 \/ ({a5,a2,a6,a4,a0} \/ {a2}) \/ (Ub3 \/
 {a4,a0}) by A4,SCMFSA9A:30
    .= Ut1_6 \/ {a2,a5,a2,a6,a4,a0} \/ (Ub3 \/ {a4,a0}) by ENUMSET1:51
    .= Ut1_6 \/ ({a2,a5,a2,a6} \/ {a4,a0}) \/ (Ub3 \/ {a4,a0}) by ENUMSET1:54
    .= Ut1_6 \/ ({a2,a2,a5,a6} \/ {a4,a0}) \/ (Ub3 \/ {a4,a0}) by ENUMSET1:104
    .= Ut1_6 \/ ({a2,a5,a6} \/ {a4,a0}) \/ (Ub3 \/ {a4,a0}) by ENUMSET1:71
    .= Ut1_6 \/ {a2,a5,a6,a4,a0} \/ (Ub3 \/ {a4,a0}) by ENUMSET1:49
    .= Ut1_6 \/ ({a6,a4,a0} \/ {a2,a5}) \/ (Ub3 \/ {a4,a0}) by ENUMSET1:48
    .= {a3,a2,a1} \/ {a6,a4,a0} \/ {a6,a4,a0} \/ {a2,a5} \/ (Ub3 \/
 {a4,a0}) by A5,XBOOLE_1:4
    .= {a3,a2,a1} \/ ({a6,a4,a0} \/ {a6,a4,a0}) \/ {a2,a5} \/ (Ub3 \/ {a4,a0})
         by XBOOLE_1:4
    .= {a3,a2,a1} \/ {a6,a4,a0} \/ {a2,a5} \/ ({a3,a5} \/ ({a2,a0,a6} \/
 {a4,a0}))
        by A1,XBOOLE_1:4
    .= {a3,a2,a1} \/ {a6,a4,a0} \/ {a2,a5} \/ ({a3,a5} \/ {a2,a0,a6,a4,a0})
      by ENUMSET1:49
    .= {a3,a2,a1} \/ {a6,a4,a0} \/ {a2,a5} \/ ({a3,a5} \/ ({a2} \/
 {a0,a6,a4,a0}))
      by ENUMSET1:47
    .= {a3,a2,a1} \/ {a6,a4,a0} \/ {a2,a5} \/ ({a3,a5} \/ ({a2} \/
 {a0,a0,a4,a6}))
      by ENUMSET1:107
    .= {a3,a2,a1} \/ {a6,a4,a0} \/ {a2,a5} \/ ({a3,a5} \/ ({a2} \/ {a0,a4,a6}))
      by ENUMSET1:71
    .= {a3,a2,a1} \/ {a6,a4,a0} \/ {a2,a5} \/ ({a3,a5} \/ {a2,a0,a4,a6})
      by ENUMSET1:44
    .= {a3,a2,a1} \/ {a6,a4,a0} \/ {a2,a5} \/
 {a3,a5,a2,a0,a4,a6} by ENUMSET1:52
    .= {a3,a2,a1} \/ {a0,a4,a6} \/ {a5,a2} \/
 {a3,a5,a2,a0,a4,a6} by ENUMSET1:102
    .= {a3,a2,a1} \/ ({a0,a4,a6} \/ {a5,a2}) \/ {a3,a5,a2,a0,a4,a6}
        by XBOOLE_1:4
    .= {a3,a2,a1} \/ {a5,a2,a0,a4,a6} \/ {a3,a5,a2,a0,a4,a6} by ENUMSET1:48
    .= {a3,a2,a1} \/ {a5,a2,a0,a4,a6} \/ ({a5,a2,a0,a4,a6} \/ {a3})
     by ENUMSET1:51
    .= {a3,a2,a1} \/ {a5,a2,a0,a4,a6} \/ {a5,a2,a0,a4,a6} \/ {a3} by XBOOLE_1:4
    .= {a3,a2,a1} \/ ({a5,a2,a0,a4,a6} \/ {a5,a2,a0,a4,a6}) \/ {a3} by XBOOLE_1
:4
    .= {a3,a2,a1,a5,a2,a0,a4,a6} \/ {a3} by ENUMSET1:64
    .= {a3,a2,a1,a5,a2} \/ {a0,a4,a6} \/ {a3} by ENUMSET1:66
    .= {a3} \/ {a2,a1,a5,a2} \/ {a0,a4,a6} \/ {a3} by ENUMSET1:47
    .= {a3} \/ {a2,a2,a5,a1} \/ {a0,a4,a6} \/ {a3} by ENUMSET1:107
    .= {a3} \/ {a2,a5,a1} \/ {a0,a4,a6} \/ {a3} by ENUMSET1:71
    .= {a3,a2,a5,a1} \/ {a0,a4,a6} \/ {a3} by ENUMSET1:44
    .= {a1,a5,a2,a3} \/ {a0,a4,a6} \/ {a3} by ENUMSET1:125
    .= {a1,a5,a2,a3,a0,a4,a6} \/ {a3} by ENUMSET1:59
    .= {a1} \/ {a5,a2,a3,a0,a4,a6} \/ {a3} by ENUMSET1:56
    .= {a1} \/ ({a5,a2,a3,a0,a4} \/ {a6}) \/ {a3} by ENUMSET1:55
    .= {a1} \/ {a5,a2,a3,a0,a4} \/ {a6} \/ {a3} by XBOOLE_1:4
    .= {a1} \/ {a5,a2,a3,a0,a4} \/ {a3} \/ {a6} by XBOOLE_1:4
    .= {a1} \/ ({a5,a2,a3,a0,a4} \/ {a3}) \/ {a6} by XBOOLE_1:4
    .= {a1} \/ {a5,a2,a3,a0,a4,a3} \/ {a6} by ENUMSET1:55
    .= {a1} \/ ({a5,a2} \/ {a3,a0,a4,a3}) \/ {a6} by ENUMSET1:52
    .= {a1} \/ ({a5,a2} \/ {a3,a3,a4,a0}) \/ {a6} by ENUMSET1:107
    .= {a1} \/ ({a5,a2} \/ {a3,a4,a0}) \/ {a6} by ENUMSET1:71
    .= {a1} \/ {a5,a2,a3,a4,a0} \/ {a6} by ENUMSET1:48
    .= {a1} \/ ({a0} \/ {a5,a2,a3,a4}) \/ {a6} by ENUMSET1:50
    .= {a1} \/ {a0} \/ {a5,a2,a3,a4} \/ {a6} by XBOOLE_1:4
    .= {a0,a1} \/ {a5,a2,a3,a4} \/ {a6} by ENUMSET1:41
    .= {a0,a1} \/ {a2,a3,a4,a5} \/ {a6} by ENUMSET1:111
    .= {a0,a1,a2,a3,a4,a5} \/ {a6} by ENUMSET1:52
    .= {a0,a1,a2,a3,a4,a5,a6} by ENUMSET1:61;
  end;
   set WM=initializeWorkMem,
       j1=a1:=len f,
       j2=SubFrom(a1,a0),
       Uj1= UsedIntLoc (WM ';' j1);
   thus UsedIntLoc (insert-sort f)
     = UsedIntLoc (WM ';' j1 ';' j2 ';' Times(a1,body1)) by Def2
    .= UsedIntLoc (WM ';' j1 ';' j2) \/ UsedIntLoc Times(a1,body1)
        by SF_MASTR:31
    .= UsedIntLoc (WM ';' j1 ';' j2) \/ (Ub1 \/ {a1,a0}) by SCMBSORT:31
    .= Uj1 \/ UsedIntLoc j2 \/ (Ub1 \/ {a1,a0}) by SF_MASTR:34
    .= Uj1 \/ {a1,a0} \/ (Ub1 \/ {a1,a0}) by SF_MASTR:18
    .= Uj1 \/ {a1,a0} \/ {a1,a0} \/ Ub1 by XBOOLE_1:4
    .= Uj1 \/ ({a1,a0} \/ {a1,a0}) \/ Ub1 by XBOOLE_1:4
    .= UsedIntLoc WM \/ UsedIntLoc j1 \/ {a1,a0} \/ Ub1 by SF_MASTR:34
    .= {a2,a3,a4,a5,a6} \/ {a0} \/ {a1} \/ {a1,a0} \/ Ub1 by A2,SF_MASTR:22
    .= {a2,a3,a4,a5,a6} \/ ({a0} \/ {a1}) \/ {a1,a0} \/ Ub1 by XBOOLE_1:4
    .= {a2,a3,a4,a5,a6} \/ {a1,a0} \/ {a1,a0} \/ Ub1 by ENUMSET1:41
    .= {a2,a3,a4,a5,a6} \/ ({a1,a0} \/ {a1,a0}) \/ Ub1 by XBOOLE_1:4
    .= {a0,a1,a2,a3,a4,a5,a6} \/ {a0,a1,a2,a3,a4,a5,a6} by A6,ENUMSET1:57
    .= {a0,a1,a2,a3,a4,a5,a6};
end;

theorem Th39:    ::IS004
 for f being FinSeq-Location holds
  UsedInt*Loc (insert-sort f) = {f}
proof
  let f be FinSeq-Location;
  set i1= a2:=a3,
       i2= SubFrom(a3,a0),
       i3= a5:=(f,a2),
       i4= a6:=(f,a3),
       i5= (f,a2):=a6,
       i6= (f,a3):=a5,
       body3= i1 ';' i2 ';' i3 ';' i4 ';' i5 ';' i6,
       Ub3=UsedInt*Loc body3;
A1: Ub3 = {f}
   proof thus
      Ub3 = UsedInt*Loc (i1 ';' i2 ';'i3 ';'i4 ';' i5 )
         \/ UsedInt*Loc i6 by SF_MASTR:50
    .= UsedInt*Loc (i1 ';' i2 ';'i3 ';'i4 ';' i5 ) \/ {f} by SF_MASTR:37
    .= UsedInt*Loc (i1 ';' i2 ';'i3 ';'i4) \/ UsedInt*Loc i5 \/ {f}
       by SF_MASTR:50
    .= UsedInt*Loc (i1 ';' i2 ';'i3 ';'i4) \/ {f} \/ {f} by SF_MASTR:37
    .= UsedInt*Loc (i1 ';' i2 ';'i3) \/ UsedInt*Loc i4 \/ {f} \/ {f}
       by SF_MASTR:50
    .= UsedInt*Loc (i1 ';' i2 ';'i3) \/ {f} \/ {f} \/ {f} by SF_MASTR:37
    .= UsedInt*Loc (i1 ';' i2) \/ UsedInt*Loc i3 \/ {f} \/ {f} \/ {f}
      by SF_MASTR:50
    .= UsedInt*Loc (i1 ';' i2) \/ {f} \/ {f} \/ {f} \/ {f} by SF_MASTR:37
    .= UsedInt*Loc i1 \/ UsedInt*Loc i2 \/ {f} \/ {f} \/ {f} \/ {f}
      by SF_MASTR:51
    .= {} \/ UsedInt*Loc i2 \/ {f} \/ {f} \/ {f} \/ {f} by SF_MASTR:36
    .= {} \/ {f} \/ {f} \/ {f} \/ {f} by SF_MASTR:36
    .= {f};
   end;
     set k2= a2:= a0,
          k3= a3:= a0,
          k4= a4:= a0,
          k5= a5:= a0;
A2:  UsedInt*Loc initializeWorkMem = UsedInt*Loc (k2 ';' k3 ';' k4 ';' k5)
     \/ UsedInt*Loc (a6:= a0) by SF_MASTR:50
    .= UsedInt*Loc (k2 ';' k3 ';' k4 ';' k5) \/ {} by SF_MASTR:36
    .= UsedInt*Loc (k2 ';' k3 ';' k4) \/ UsedInt*Loc k5 by SF_MASTR:50
    .= UsedInt*Loc (k2 ';' k3 ';' k4) \/ {} by SF_MASTR:36
    .= UsedInt*Loc (k2 ';' k3 ) \/ UsedInt*Loc k4 by SF_MASTR:50
    .= UsedInt*Loc (k2 ';' k3 ) \/ {} by SF_MASTR:36
    .= UsedInt*Loc k2 \/ UsedInt*Loc k3 by SF_MASTR:51
    .= UsedInt*Loc k2 \/ {} by SF_MASTR:36
    .= {} by SF_MASTR:36;
    set m0=SubFrom(a2,a2),
        m1=Macro m0,
        m2=AddTo(a4,a0),
        m3=SubFrom(a2,a0),
        IF=if>0(a5, m1, m2 ';' m3),
        UIF = UsedInt*Loc IF;
A3:  UIF = {}
   proof thus
       UIF = UsedInt*Loc m1 \/ UsedInt*Loc (m2 ';' m3) by SCMBSORT:35
     .= UsedInt*Loc m0 \/ UsedInt*Loc (m2 ';' m3) by SF_MASTR:48
     .= {} \/ UsedInt*Loc (m2 ';' m3) by SF_MASTR:36
     .= {} \/ (UsedInt*Loc m2 \/ UsedInt*Loc m3) by SF_MASTR:51
     .= {} \/ ({} \/ UsedInt*Loc m3) by SF_MASTR:36
     .= {} by SF_MASTR:36;
   end;
   set n1=a5:=(f,a2),
        n2=SubFrom(a5,a6),
        body2=n1 ';'n2 ';' IF,
        Ub2=UsedInt*Loc body2;
A4: Ub2 = {f}
  proof thus
      Ub2 = UsedInt*Loc (n1 ';'n2) \/ UIF by SF_MASTR:47
    .= UsedInt*Loc n1 \/ UsedInt*Loc n2 \/ UIF by SF_MASTR:51
    .= {f} \/ UsedInt*Loc n2 \/ UIF by SF_MASTR:37
    .= {f} \/ {} by A3,SF_MASTR:36
    .= {f};
  end;
    set T3=Times(a4,body3),
        t1=a2:=len f,
        t2=SubFrom(a2,a1),
        t3=a3 := a2,
        t4=AddTo(a3,a0),
        t5=a6:=(f,a3),
        t6=SubFrom(a4,a4),
        Wg=while>0(a2,body2),
        t16=t1 ';' t2 ';' t3 ';' t4 ';' t5 ';' t6,
        body1=t16 ';' Wg ';' T3,
        Ub1 =UsedInt*Loc body1,
        Ut1_6 =UsedInt*Loc t16;
A5:   Ut1_6={f}
  proof thus
      Ut1_6= UsedInt*Loc (t1 ';'t2 ';' t3 ';' t4 ';' t5) \/ UsedInt*Loc t6
       by SF_MASTR:50
    .= UsedInt*Loc (t1 ';'t2 ';' t3 ';' t4 ';' t5) \/ {} by SF_MASTR:36
    .= UsedInt*Loc (t1 ';'t2 ';' t3 ';' t4) \/ UsedInt*Loc t5 \/ {}
        by SF_MASTR:50
    .= UsedInt*Loc (t1 ';'t2 ';' t3 ';' t4) \/ {f} \/ {} by SF_MASTR:37
    .= UsedInt*Loc (t1 ';'t2 ';' t3) \/ UsedInt*Loc t4 \/ {f} \/ {}
         by SF_MASTR:50
    .= UsedInt*Loc (t1 ';'t2 ';' t3) \/ {} \/ {f} \/ {} by SF_MASTR:36
    .= UsedInt*Loc (t1 ';'t2) \/ UsedInt*Loc t3 \/ {} \/ {f} \/
 {} by SF_MASTR:50
    .= UsedInt*Loc (t1 ';'t2) \/ {} \/ {} \/ {f} \/ {} by SF_MASTR:36
    .= UsedInt*Loc t1 \/ UsedInt*Loc t2 \/ {} \/ {} \/ {f} \/ {} by SF_MASTR:51
    .= {f} \/ UsedInt*Loc t2 \/ {} \/ {} \/ {f} \/ {} by SF_MASTR:38
    .= {f} \/ {f} \/ {} by SF_MASTR:36
    .= {f};
  end;
A6: Ub1 ={f}
 proof thus
      UsedInt*Loc body1 = UsedInt*Loc (t16 ';' Wg ) \/ UsedInt*Loc T3
      by SF_MASTR:47
    .= UsedInt*Loc (t16 ';' Wg) \/ {f} by A1,SCMBSORT:37
    .= UsedInt*Loc t16 \/ UsedInt*Loc Wg \/ {f} by SF_MASTR:47
    .= {f} \/ {f} by A4,A5,SCMFSA9A:31
    .= {f};
    end;
   set WM=initializeWorkMem,
       j1=a1:=len f,
       j2=SubFrom(a1,a0);
   thus UsedInt*Loc (insert-sort f)
     = UsedInt*Loc (WM ';' j1 ';' j2 ';' Times(a1,body1)) by Def2
    .= UsedInt*Loc (WM ';' j1 ';' j2) \/ UsedInt*Loc Times(a1,body1)
        by SF_MASTR:47
    .= UsedInt*Loc (WM ';' j1 ';' j2) \/ {f} by A6,SCMBSORT:37
    .= UsedInt*Loc (WM ';' j1) \/ UsedInt*Loc j2 \/ {f} by SF_MASTR:50
    .= UsedInt*Loc (WM ';' j1) \/ {} \/ {f} by SF_MASTR:36
    .= UsedInt*Loc WM \/ UsedInt*Loc j1 \/ {} \/ {f} by SF_MASTR:50
    .= {f} \/ {f} by A2,SF_MASTR:38
    .= {f};
end;

theorem Th40:  :: IS007
 for k1,k2,k3,k4 being Instruction of SCM+FSA holds
     card( k1 ';' k2 ';' k3 ';' k4) =8
proof
    let k1,k2,k3,k4 be Instruction of SCM+FSA;
    thus card( k1 ';' k2 ';' k3 ';' k4)
     =card( k1 ';' k2 ';' k3 ';' Macro k4) by SCMFSA6A:def 6
    .= card (k1 ';' k2 ';' k3) + card Macro k4 by SCMFSA6A:61
    .= card (k1 ';' k2 ';' k3)+ 2 by SCMFSA7B:6
    .= 6 + 2 by SCMBSORT:45
    .= 8;
end;

theorem Th41:  :: IS009
 for k1,k2,k3,k4,k5 being Instruction of SCM+FSA holds
     card( k1 ';' k2 ';' k3 ';' k4 ';'k5) =10
proof
    let k1,k2,k3,k4,k5 be Instruction of SCM+FSA;
    thus card( k1 ';' k2 ';' k3 ';' k4 ';'k5)
     =card( k1 ';' k2 ';' k3 ';' k4 ';' Macro k5) by SCMFSA6A:def 6
    .= card (k1 ';' k2 ';' k3 ';' k4)+ card Macro k5 by SCMFSA6A:61
    .= card (k1 ';' k2 ';' k3 ';' k4)+ 2 by SCMFSA7B:6
    .= 8+ 2 by Th40
    .= 10;
end;

theorem Th42:  :: IS010
 for f being FinSeq-Location holds card (insert-sort f) = 82
proof
  let f be FinSeq-Location;
  set i1= a2:=a3,
       i2= SubFrom(a3,a0),
       i3= a5:=(f,a2),
       i4= a6:=(f,a3),
       i5= (f,a2):=a6,
       i6= (f,a3):=a5,
       body3= i1 ';' i2 ';' i3 ';' i4 ';' i5 ';' i6;
A1: card body3 = card (i1 ';' i2 ';' i3 ';' i4 ';' i5 ';' Macro i6)
     by SCMFSA6A:def 6
     .= card (i1 ';' i2 ';' i3 ';' i4 ';' i5) + card Macro i6
      by SCMFSA6A:61
     .=10 + card Macro i6 by Th41
     .=10+2 by SCMFSA7B:6
     .=12;
    set m1=Macro SubFrom(a2,a2),
        m2=AddTo(a4,a0),
        m3=SubFrom(a2,a0),
        IF=if>0(a5, m1, m2 ';' m3);
A2:  card IF = card m1 + card (m2 ';' m3)+ 4 by SCMFSA8B:15
       .= 2 + card (m2 ';' m3)+ 4 by SCMFSA7B:6
       .= 2 + card (Macro m2 ';' Macro m3)+ 4 by SCMFSA6A:def 7
       .= 2 + (card Macro m2 + card Macro m3)+ 4 by SCMFSA6A:61
       .= 2 + (2 + card Macro m3)+ 4 by SCMFSA7B:6
       .= 2 + (2 + 2)+ 4 by SCMFSA7B:6
       .= 10;
   set n1=a5:=(f,a2),
        n2=SubFrom(a5,a6),
        body2=n1 ';'n2 ';' IF;
A3:    card body2 = card (n1 ';'n2) + card IF by SCMFSA6A:61
        .= card (Macro n1 ';' Macro n2) + card IF by SCMFSA6A:def 7
        .= card Macro n1 + card Macro n2 + card IF by SCMFSA6A:61
        .= 2 + card Macro n2 + card IF by SCMFSA7B:6
        .= 2 + 2 + 10 by A2,SCMFSA7B:6
        .= 14;
    set T3=Times(a4,body3),
        t1=a2:=len f,
        t2=SubFrom(a2,a1),
        t3=a3 := a2,
        t4=AddTo(a3,a0),
        t5=a6:=(f,a3),
        t6=SubFrom(a4,a4),
        Wg=while>0(a2,body2),
        t16=t1 ';' t2 ';' t3 ';' t4 ';' t5 ';' t6,
        body1=t16 ';' Wg ';' T3;
A4:  card body1 = card (t16 ';' Wg) + card T3 by SCMFSA6A:61
      .= card t16 + card Wg + card T3 by SCMFSA6A:61
      .= card (t1 ';' t2 ';' t3 ';' t4 ';' t5 ';' Macro t6)
          + card Wg + card T3 by SCMFSA6A:def 6
      .= card (t1 ';' t2 ';' t3 ';' t4 ';' t5) + card Macro t6
          + card Wg + card T3 by SCMFSA6A:61
      .= 10 + card Macro t6 + card Wg + card T3 by Th41
      .= 10 + 2 + card Wg + card T3 by SCMFSA7B:6
      .= 10 + 2 + (14 + 6) + card T3 by A3,SCMFSA_9:5
      .= 10 + 2 + (14 + 6) + (12+12) by A1,SCMBSORT:44
      .= 56;
   set WM=initializeWorkMem,
       j1=a1:=len f,
       j2=SubFrom(a1,a0);
  thus card (insert-sort f)
     = card (WM ';' j1 ';' j2 ';' Times(a1,body1)) by Def2
     .= card (WM ';' j1 ';' j2 ) + card Times(a1,body1) by SCMFSA6A:61
     .= card (WM ';' j1 ';' j2 ) + (56+12) by A4,SCMBSORT:44
     .= card (WM ';' j1 ';' Macro j2 ) + (56+12) by SCMFSA6A:def 6
     .= card (WM ';' j1) + card Macro j2 + (56+12) by SCMFSA6A:61
     .= card (WM ';' j1) + 2 + (56+12) by SCMFSA7B:6
     .= card (WM ';' Macro j1) + 2 + (56+12) by SCMFSA6A:def 6
     .= card WM + card Macro j1 + 2 + (56+12) by SCMFSA6A:61
     .= card WM + 2 + 2 + (56+12) by SCMFSA7B:6
     .= 10 + 2 + 2 + 68 by Th41
     .= 82;
end;

theorem Th43:   :: IS012
 for f being FinSeq-Location, k being Nat st
   k < 82 holds insloc k in dom (insert-sort f)
proof
    let f be FinSeq-Location, k be Nat;
    assume A1: k < 82;
      card (insert-sort f) = 82 by Th42;
    hence thesis by A1,SCMFSA6A:15;
end;

Lm1:  ::Lem02
  for s being State of SCM+FSA st Insert-Sort-Algorithm c= s holds
     s.insloc 0= a2:=a0 &
     s.insloc 1= goto insloc 2 &
     s.insloc 2= a3:=a0 &
     s.insloc 3= goto insloc 4 &
     s.insloc 4= a4:=a0 &
     s.insloc 5= goto insloc 6 &
     s.insloc 6= a5:=a0 &
     s.insloc 7= goto insloc 8 &
     s.insloc 8= a6:=a0 &
     s.insloc 9= goto insloc 10 &
     s.insloc 10= a1:=len fsloc 0 &
     s.insloc 11= goto insloc 12
proof
   set f0=fsloc 0,
       TT=Times(a1,
          ((a2:=len f0) ';' SubFrom(a2,a1) ';' (a3 := a2) ';'
          AddTo(a3,a0) ';' (a6:=(f0,a3)) ';' SubFrom(a4,a4)) ';'
          while>0(a2, (a5:=(f0,a2)) ';' SubFrom(a5,a6) ';'
               if>0(a5,Macro SubFrom(a2,a2),
                    AddTo(a4,a0) ';' SubFrom(a2,a0))
          ) ';'
          Times(a4,
               (a2:=a3) ';'
               SubFrom(a3,a0) ';'
               (a5:=(f0,a2)) ';'
               (a6:=(f0,a3)) ';'
               ((f0,a2):=a6) ';'((f0,a3):=a5)
          )
       );
     set q=Insert-Sort-Algorithm,
         q0=insert-sort f0;
     let s be State of SCM+FSA such that
A1:  q c= s;
     A2: q=q0 by Def3;
A3:  now let i be Nat;
       assume i< 82;
       then insloc i in dom q0 by Th43;
       hence q0.insloc i= s.insloc i by A1,A2,GRFUNC_1:8;
     end;
     set W2=a2:= a0,
         W3=a3:= a0,
         W4=a4:= a0,
         W5=a5:= a0,
         W6=a6:= a0,
         W7=a1:=len f0,
         W8=SubFrom(a1,a0),
         T8= W8 ';' TT,

         T7=W7 ';' T8,
         T6=W6 ';' T7,
         T5=W5 ';' T6,
         T4=W4 ';' T5,
         T3=W3 ';' T4,

         X3=W2 ';' W3,
         X4=X3 ';' W4,
         X5=X4 ';' W5,
         X6=X5 ';' W6;
A4:  q0=X6 ';' W7 ';' W8 ';' TT by Def2
     .=X6 ';' W7 ';' T8 by SCMFSA6A:64;
then A5:  q0=X5 ';' W6 ';' T7 by SCMFSA6A:64;
then A6:  q0=X4 ';' W5 ';' T6 by SCMFSA6A:64;
then A7:  q0=X3 ';' W4 ';' T5 by SCMFSA6A:64;
then A8:  q0=W2 ';' W3 ';' T4 by SCMFSA6A:64;
     then q0=W2 ';' T3 by SCMFSA6A:68;
then A9:  q0=Macro W2 ';' T3 by SCMFSA6A:def 5;
A10:  q0=Macro W2 ';' Macro W3 ';' T4 by A8,SCMFSA6A:def 7
      .=Macro W2 ';' W3 ';' T4 by SCMFSA6A:def 6;
       dom Macro W2 = {insloc 0, insloc 1} by SCMFSA7B:4;
then A11:  insloc 0 in dom Macro W2 & insloc 1 in dom Macro W2 by TARSKI:def 2;
A12:  W2 <> halt SCM+FSA by SCMBSORT:49;
     thus s.insloc 0=q0.insloc 0 by A3
    .= (Directed Macro W2).insloc 0 by A9,A11,SCMFSA8A:28
    .= W2 by A12,SCMFSA7B:7;
     thus s.insloc 1=q0.insloc 1 by A3
    .= (Directed Macro W2).insloc 1 by A9,A11,SCMFSA8A:28
    .= goto insloc 2 by SCMFSA7B:8;
A13:  card Macro W2=2 by SCMFSA7B:6;
     thus s.insloc 2=q0.insloc 2 by A3
    .= W3 by A10,A13,SCMBSORT:51;
     thus s.insloc 3=q0.insloc (2+1) by A3
     .=goto insloc (2+2) by A10,A13,SCMBSORT:51
     .=goto insloc 4;
A14:  card X3=card (Macro W2 ';' Macro W3) by SCMFSA6A:def 7
     .= card Macro W2 + card Macro W3 by SCMFSA6A:61
     .= 2 + card Macro W3 by SCMFSA7B:6
     .= 2 + 2 by SCMFSA7B:6
     .=4;
     thus s.insloc 4=q0.insloc 4 by A3
    .= W4 by A7,A14,SCMBSORT:51;
     thus s.insloc 5=q0.insloc (4+1) by A3
     .=goto insloc (4+2) by A7,A14,SCMBSORT:51
     .=goto insloc 6;
A15:  card X4=6 by SCMBSORT:45;
     thus s.insloc 6=q0.insloc 6 by A3
    .= W5 by A6,A15,SCMBSORT:51;
     thus s.insloc 7=q0.insloc (6+1) by A3
     .=goto insloc (6+2) by A6,A15,SCMBSORT:51
     .=goto insloc 8;
A16:  card X5=card (X4 ';' Macro W5) by SCMFSA6A:def 6
     .= 6 + card Macro W5 by A15,SCMFSA6A:61
     .= 6 + 2 by SCMFSA7B:6
     .=8;
     thus s.insloc 8=q0.insloc 8 by A3
    .= W6 by A5,A16,SCMBSORT:51;
     thus s.insloc 9=q0.insloc (8+1) by A3
     .=goto insloc (8+2) by A5,A16,SCMBSORT:51
     .=goto insloc 10;
A17:  card X6=card (X5 ';' Macro W6) by SCMFSA6A:def 6
     .= 8 + card Macro W6 by A16,SCMFSA6A:61
     .= 8 + 2 by SCMFSA7B:6
     .= 10;
     thus s.insloc 10=q0.insloc 10 by A3
    .= W7 by A4,A17,SCMBSORT:52;
     thus s.insloc 11=q0.insloc (10+1) by A3
     .=goto insloc (10+2) by A4,A17,SCMBSORT:52
     .=goto insloc 12;
end;

set f0=fsloc 0;
set b1=intloc (0+1),b2=intloc (1+1),b3=intloc (2+1),b4=intloc (3+1),
     b5=intloc (4+1),b6=intloc (5+1);

set i1= b2:=b3,
     i2= SubFrom(b3,a0),
     i3= b5:=(f0,b2),
     i4= b6:=(f0,b3),
     i5= (f0,b2):=b6,
     i6= (f0,b3):=b5,
     body3= i1 ';' i2 ';' i3 ';' i4 ';' i5 ';' i6,
     w2= b2:= a0,
     w3= b3:= a0,
     w4= b4:= a0,
     w5= b5:= a0,
     w6= b6:= a0,
     T3=Times(b4,body3),
     m0=SubFrom(b2,b2),
     m1=Macro m0,
     m2=AddTo(b4,a0),
     m3=SubFrom(b2,a0),
     IF=if>0(b5, m1, m2 ';' m3),
     n1=b5:=(f0,b2),
     n2=SubFrom(b5,b6),
     body2=n1 ';'n2 ';' IF,
     t1=b2:=len f0,
     t2=SubFrom(b2,b1),
     t3=b3:= b2,
     t4=AddTo(b3,a0),
     t5=b6:=(f0,b3),
     t6=SubFrom(b4,b4),
     Wg=while>0(b2,body2),
     t16=t1 ';' t2 ';' t3 ';' t4 ';' t5 ';' t6,
     body1=t16 ';' Wg ';' T3,
     WM=initializeWorkMem,
     j1=b1:=len f0,
     j2=SubFrom(b1,a0);

Lm2:   ::Lem04
  for s being State of SCM+FSA st Insert-Sort-Algorithm c= s &
   s starts_at insloc 0 holds
   (for k being Nat st k>0 & k<12 holds
   (Computation s).k.IC SCM+FSA = insloc k &
   (Computation s).k.a0=s.a0 & (Computation s).k.fsloc 0=s.fsloc 0)
   &
   (Computation s).11.a1=len(s.fsloc 0) &
   (Computation s).11.a2=s.a0 & (Computation s).11.a3=s.a0 &
   (Computation s).11.a4=s.a0 & (Computation s).11.a5=s.a0 &
   (Computation s).11.a6=s.a0
proof
   let s be State of SCM+FSA such that
A1:  Insert-Sort-Algorithm c= s and
A2:  s starts_at insloc 0;
     set Cs= Computation s;
A3:  Cs.0 = s by AMI_1:def 19;
then A4:  IC Cs.0 = insloc 0 by A2,AMI_3:def 14;
then A5:  Cs.(0+1) = Exec(s.insloc 0,Cs.0) by AMI_1:55
    .= Exec(a2:=a0,Cs.0) by A1,Lm1;
then A6: Cs.1.IC SCM+FSA = Next IC Cs.0 by SCMFSA_2:89
     .= insloc (0+1) by A4,SCMFSA_2:32
     .= insloc 1;
then A7: IC Cs.1= insloc 1 by AMI_1:def 15;
A8:  Cs.1.a2 =s.a0 by A3,A5,SCMFSA_2:89;
     A9: a2<>a0 by SCMFSA_2:16;
then A10: Cs.1.a0 =s.a0 by A3,A5,SCMFSA_2:89;
A11: Cs.1.(fsloc 0) =s.(fsloc 0) by A3,A5,SCMFSA_2:89;

A12:  Cs.(1+1) = Exec(s.insloc 1,Cs.1) by A7,AMI_1:55
    .= Exec(goto insloc 2,Cs.1) by A1,Lm1;
then Cs.2.IC SCM+FSA = insloc 2 by SCMFSA_2:95;
then A13:  IC Cs.2= insloc 2 by AMI_1:def 15;
A14: Cs.2.a0 =s.a0 by A10,A12,SCMFSA_2:95;
A15: Cs.2.(fsloc 0) =s.(fsloc 0) by A11,A12,SCMFSA_2:95;
A16: Cs.2.a2 =s.a0 by A8,A12,SCMFSA_2:95;

A17:  Cs.(2+1) = Exec(s.insloc 2,Cs.2) by A13,AMI_1:55
    .= Exec(a3:=a0,Cs.2) by A1,Lm1;
then A18: Cs.3.IC SCM+FSA = Next IC Cs.2 by SCMFSA_2:89
     .= insloc (2+1) by A13,SCMFSA_2:32
     .= insloc 3;
then A19: IC Cs.3= insloc 3 by AMI_1:def 15;
A20: Cs.3.a3 =s.a0 by A14,A17,SCMFSA_2:89;
    A21: a3<>a0 by SCMFSA_2:16;
then A22: Cs.3.a0 =s.a0 by A14,A17,SCMFSA_2:89;
A23: Cs.3.(fsloc 0) =s.(fsloc 0) by A15,A17,SCMFSA_2:89;
      a2<>a3 by SCMFSA_2:16;
then A24: Cs.3.a2 =s.a0 by A16,A17,SCMFSA_2:89;

A25:  Cs.(3+1) = Exec(s.insloc 3,Cs.3) by A19,AMI_1:55
    .= Exec(goto insloc 4,Cs.3) by A1,Lm1;
then Cs.4.IC SCM+FSA = insloc 4 by SCMFSA_2:95;
then A26: IC Cs.4= insloc 4 by AMI_1:def 15;
A27: Cs.4.a0 =s.a0 by A22,A25,SCMFSA_2:95;
A28: Cs.4.(fsloc 0) =s.(fsloc 0) by A23,A25,SCMFSA_2:95;
A29: Cs.4.a2 =s.a0 by A24,A25,SCMFSA_2:95;
A30: Cs.4.a3 =s.a0 by A20,A25,SCMFSA_2:95;

A31:  Cs.(4+1) = Exec(s.insloc 4,Cs.4) by A26,AMI_1:55
    .= Exec(a4:=a0,Cs.4) by A1,Lm1;
then A32: Cs.5.IC SCM+FSA = Next IC Cs.4 by SCMFSA_2:89
     .= insloc (4+1) by A26,SCMFSA_2:32
     .= insloc 5;
then A33: IC Cs.5= insloc 5 by AMI_1:def 15;
A34: Cs.5.a4 =s.a0 by A27,A31,SCMFSA_2:89;
    A35: a4<>a0 by SCMFSA_2:16;
then A36: Cs.5.a0 =s.a0 by A27,A31,SCMFSA_2:89;
A37: Cs.5.(fsloc 0) =s.(fsloc 0) by A28,A31,SCMFSA_2:89;
      a2<>a4 by SCMFSA_2:16;
then A38: Cs.5.a2 =s.a0 by A29,A31,SCMFSA_2:89;
      a3<>a4 by SCMFSA_2:16;
then A39: Cs.5.a3 =s.a0 by A30,A31,SCMFSA_2:89;

A40:  Cs.(5+1) = Exec(s.insloc 5,Cs.5) by A33,AMI_1:55
    .= Exec(goto insloc 6,Cs.5) by A1,Lm1;
then Cs.6.IC SCM+FSA = insloc 6 by SCMFSA_2:95;
then A41: IC Cs.6= insloc 6 by AMI_1:def 15;
A42:  Cs.6.a0 =s.a0 by A36,A40,SCMFSA_2:95;
A43:  Cs.6.(fsloc 0) =s.(fsloc 0) by A37,A40,SCMFSA_2:95;
A44: Cs.6.a2 =s.a0 by A38,A40,SCMFSA_2:95;
A45: Cs.6.a3 =s.a0 by A39,A40,SCMFSA_2:95;
A46: Cs.6.a4 =s.a0 by A34,A40,SCMFSA_2:95;

A47:  Cs.(6+1) = Exec(s.insloc 6,Cs.6) by A41,AMI_1:55
    .= Exec(a5:=a0,Cs.6) by A1,Lm1;
then A48: Cs.7.IC SCM+FSA = Next IC Cs.6 by SCMFSA_2:89
     .= insloc (6+1) by A41,SCMFSA_2:32
     .= insloc 7;
then A49: IC Cs.7= insloc 7 by AMI_1:def 15;
A50: Cs.7.a5 =s.a0 by A42,A47,SCMFSA_2:89;
    A51: a5<>a0 by SCMFSA_2:16;
then A52: Cs.7.a0 =s.a0 by A42,A47,SCMFSA_2:89;
A53: Cs.7.(fsloc 0) =s.(fsloc 0) by A43,A47,SCMFSA_2:89;
      a2<>a5 by SCMFSA_2:16;
then A54: Cs.7.a2 =s.a0 by A44,A47,SCMFSA_2:89;
      a3<>a5 by SCMFSA_2:16;
then A55: Cs.7.a3 =s.a0 by A45,A47,SCMFSA_2:89;
      a4<>a5 by SCMFSA_2:16;
then A56: Cs.7.a4 =s.a0 by A46,A47,SCMFSA_2:89;

A57:  Cs.(7+1) = Exec(s.insloc 7,Cs.7) by A49,AMI_1:55
    .= Exec(goto insloc 8,Cs.7) by A1,Lm1;
then Cs.8.IC SCM+FSA = insloc 8 by SCMFSA_2:95;
then A58: IC Cs.8= insloc 8 by AMI_1:def 15;
A59: Cs.8.a0 =s.a0 by A52,A57,SCMFSA_2:95;
A60: Cs.8.(fsloc 0) =s.(fsloc 0) by A53,A57,SCMFSA_2:95;
A61: Cs.8.a2 =s.a0 by A54,A57,SCMFSA_2:95;
A62: Cs.8.a3 =s.a0 by A55,A57,SCMFSA_2:95;
A63: Cs.8.a4 =s.a0 by A56,A57,SCMFSA_2:95;
A64: Cs.8.a5 =s.a0 by A50,A57,SCMFSA_2:95;

A65:  Cs.(8+1) = Exec(s.insloc 8,Cs.8) by A58,AMI_1:55
    .= Exec(a6:=a0,Cs.8) by A1,Lm1;
then A66: Cs.9.IC SCM+FSA = Next IC Cs.8 by SCMFSA_2:89
     .= insloc (8+1) by A58,SCMFSA_2:32
     .= insloc 9;
then A67: IC Cs.9= insloc 9 by AMI_1:def 15;
A68: Cs.9.a6 =s.a0 by A59,A65,SCMFSA_2:89;
    A69: a6<>a0 by SCMFSA_2:16;
then A70: Cs.9.a0 =s.a0 by A59,A65,SCMFSA_2:89;
A71: Cs.9.(fsloc 0) =s.(fsloc 0) by A60,A65,SCMFSA_2:89;
      a2<>a6 by SCMFSA_2:16;
then A72: Cs.9.a2 =s.a0 by A61,A65,SCMFSA_2:89;
      a3<>a6 by SCMFSA_2:16;
then A73: Cs.9.a3 =s.a0 by A62,A65,SCMFSA_2:89;
      a4<>a6 by SCMFSA_2:16;
then A74: Cs.9.a4 =s.a0 by A63,A65,SCMFSA_2:89;
      a5<>a6 by SCMFSA_2:16;
then A75: Cs.9.a5 =s.a0 by A64,A65,SCMFSA_2:89;

A76:  Cs.(9+1) = Exec(s.insloc 9,Cs.9) by A67,AMI_1:55
    .= Exec(goto insloc 10,Cs.9) by A1,Lm1;
then Cs.10.IC SCM+FSA = insloc 10 by SCMFSA_2:95;
then A77: IC Cs.10= insloc 10 by AMI_1:def 15;
A78: Cs.10.a0 =s.a0 by A70,A76,SCMFSA_2:95;
A79: Cs.10.(fsloc 0) =s.(fsloc 0) by A71,A76,SCMFSA_2:95;
A80: Cs.10.a2 =s.a0 by A72,A76,SCMFSA_2:95;
A81: Cs.10.a3 =s.a0 by A73,A76,SCMFSA_2:95;
A82: Cs.10.a4 =s.a0 by A74,A76,SCMFSA_2:95;
A83: Cs.10.a5 =s.a0 by A75,A76,SCMFSA_2:95;
A84: Cs.10.a6 =s.a0 by A68,A76,SCMFSA_2:95;

A85:  Cs.(10+1) = Exec(s.insloc 10,Cs.10) by A77,AMI_1:55
    .= Exec(a1:=len fsloc 0,Cs.10) by A1,Lm1;
then A86: Cs.11.IC SCM+FSA = Next IC Cs.10 by SCMFSA_2:100
     .= insloc (10+1) by A77,SCMFSA_2:32
     .= insloc 11;
    A87: a1<>a0 by SCMFSA_2:16;

  hereby let k be Nat;
       assume A88:k>0 & k<12;
        then k<11+1;
        then A89: k<=11 by NAT_1:38;
     set c1=(Computation s).k.IC SCM+FSA,
         d1= insloc k,
         c2=(Computation s).k.a0,
         d2=s.a0,
         c3=(Computation s).k.fsloc 0,
         d3=s.fsloc 0;
     per cases by A88,A89,Th8;
     suppose k = 1;
              hence c1=d1 & c2=d2 & c3=d3 by A3,A5,A6,A9,SCMFSA_2:89;
     suppose k = 2;
              hence c1=d1 & c2=d2 & c3=d3 by A10,A11,A12,SCMFSA_2:95;
     suppose k = 3;
              hence c1=d1 & c2=d2 & c3=d3 by A14,A15,A17,A18,A21,SCMFSA_2:89;
     suppose k = 4;
              hence c1=d1 & c2=d2 & c3=d3 by A22,A23,A25,SCMFSA_2:95;
     suppose k = 5;
              hence c1=d1 & c2=d2 & c3=d3 by A27,A28,A31,A32,A35,SCMFSA_2:89;
     suppose k = 6;
              hence c1=d1 & c2=d2 & c3=d3 by A36,A37,A40,SCMFSA_2:95;
     suppose k = 7;
              hence c1=d1 & c2=d2 & c3=d3 by A42,A43,A47,A48,A51,SCMFSA_2:89;
     suppose k = 8;
              hence c1=d1 & c2=d2 & c3=d3 by A52,A53,A57,SCMFSA_2:95;
     suppose k = 9;
              hence c1=d1 & c2=d2 & c3=d3 by A59,A60,A65,A66,A69,SCMFSA_2:89;
     suppose k = 10;
              hence c1=d1 & c2=d2 & c3=d3 by A70,A71,A76,SCMFSA_2:95;
     suppose k = 11;
              hence c1=d1 & c2=d2 & c3=d3 by A78,A79,A85,A86,A87,SCMFSA_2:100;
end;

thus Cs.11.a1 =len(s.fsloc 0) by A79,A85,SCMFSA_2:100;
      a2<>a1 by SCMFSA_2:16;
hence Cs.11.a2 =s.a0 by A80,A85,SCMFSA_2:100;
      a3<>a1 by SCMFSA_2:16;
hence Cs.11.a3 =s.a0 by A81,A85,SCMFSA_2:100;
      a4<>a1 by SCMFSA_2:16;
hence Cs.11.a4 =s.a0 by A82,A85,SCMFSA_2:100;
      a5<>a1 by SCMFSA_2:16;
hence Cs.11.a5 =s.a0 by A83,A85,SCMFSA_2:100;
      a6<>a1 by SCMFSA_2:16;
hence Cs.11.a6 =s.a0 by A84,A85,SCMFSA_2:100;
end;

Lm3:   ::Lem19
 for s be State of SCM+FSA holds
         (s.b5>0 implies IExec(IF,s).b2 =0) &
         (s.b5<=0 implies IExec(IF,s).b2 =s.b2-1)
proof
  let s be State of SCM+FSA;
  set s0=Initialize s,
      s1=Exec(m2, s0);
  hereby
     assume s.b5 > 0;
  hence IExec(IF,s).b2 = IExec(m1,s).b2 by SCM_HALT:54
       .=Exec(m0,Initialize s).b2 by SCMFSA6C:6
       .=s0.b2-s0.b2 by SCMFSA_2:91
       .=0 by XCMPLX_1:14;
  end;
   b2<>b4 by SCMFSA_2:16;
then A1: s1.b2=s0.b2 by SCMFSA_2:90
    .=s.b2 by SCMFSA6C:3;
A2: s1.a0=s0.a0 by SCMFSA_2:90
    .=1 by SCMFSA6C:3;
    hereby
      assume s.b5 <= 0;
      hence IExec(IF,s).b2 = IExec(m2 ';' m3, s).b2 by SCM_HALT:54
          .=Exec(m3,s1).b2 by SCMFSA6C:9
          .=s.b2-1 by A1,A2,SCMFSA_2:91;
   end;
end;

Lm4:  ::LemB2
for s be State of SCM+FSA holds
     IExec(body2,s).b2<s.b2 or IExec(body2,s).b2<=0
proof let s be State of SCM+FSA;
    set s0=Initialize s,
        s1=Exec(n1,s0),
        s2=IExec(n1 ';'n2,s);
A1: b5<>b2 by SCMFSA_2:16;
A2:  s2.b2=Exec(n2,s1).b2 by SCMFSA6C:9
     .=s1.b2 by A1,SCMFSA_2:91
     .=s0.b2 by A1,SCMFSA_2:98
     .=s.b2 by SCMFSA6C:3;
     per cases;
     suppose A3:s2.b5>0;
          IExec(body2,s).b2=IExec(IF,s2).b2 by SCM_HALT:30
        .=0 by A3,Lm3;
       hence thesis;
     suppose A4:s2.b5<=0;
         IExec(body2,s).b2=IExec(IF,s2).b2 by SCM_HALT:30
       .=s.b2-1 by A2,A4,Lm3;
       hence thesis by INT_1:26;
end;

then Lm5:   ::Lem08
  while>0(b2,body2) is good InitHalting Macro-Instruction by Th30;

Lm6:   ::Lem05
   body3 does_not_destroy b4
proof
         b4 <> b2 by SCMFSA_2:16;
then A1:    i1 does_not_destroy b4 by SCMFSA7B:12;
         b4 <> b3 by SCMFSA_2:16;
then A2:    i2 does_not_destroy b4 by SCMFSA7B:14;
         b4 <> b5 by SCMFSA_2:16;
then A3:    i3 does_not_destroy b4 by SCMFSA7B:20;
         b4 <> b6 by SCMFSA_2:16;
then A4:    i4 does_not_destroy b4 by SCMFSA7B:20;
A5:    i5 does_not_destroy b4 by SCMFSA7B:21;
A6:    i6 does_not_destroy b4 by SCMFSA7B:21;
         i1 ';' i2 does_not_destroy b4 by A1,A2,SCMFSA8C:84;
       then i1 ';' i2 ';' i3 does_not_destroy b4 by A3,SCMFSA8C:83;
       then i1 ';' i2 ';' i3 ';' i4 does_not_destroy b4 by A4,SCMFSA8C:83;
       then i1 ';' i2 ';' i3 ';' i4 ';' i5 does_not_destroy b4
           by A5,SCMFSA8C:83;
       hence thesis by A6,SCMFSA8C:83;
end;

Lm7:   ::Lem09
   body3 does_not_destroy b1
proof
         b1 <> b2 by SCMFSA_2:16;
then A1:    i1 does_not_destroy b1 by SCMFSA7B:12;
         b1 <> b3 by SCMFSA_2:16;
then A2:    i2 does_not_destroy b1 by SCMFSA7B:14;
         b1 <> b5 by SCMFSA_2:16;
then A3:    i3 does_not_destroy b1 by SCMFSA7B:20;
         b1 <> b6 by SCMFSA_2:16;
then A4:    i4 does_not_destroy b1 by SCMFSA7B:20;
A5:    i5 does_not_destroy b1 by SCMFSA7B:21;
A6:    i6 does_not_destroy b1 by SCMFSA7B:21;
         i1 ';' i2 does_not_destroy b1 by A1,A2,SCMFSA8C:84;
       then i1 ';' i2 ';' i3 does_not_destroy b1 by A3,SCMFSA8C:83;
       then i1 ';' i2 ';' i3 ';' i4 does_not_destroy b1 by A4,SCMFSA8C:83;
       then i1 ';' i2 ';' i3 ';' i4 ';' i5 does_not_destroy b1
           by A5,SCMFSA8C:83;
       hence thesis by A6,SCMFSA8C:83;
end;

Lm8:   ::Lem10
      body2 does_not_destroy b1
proof
A1:   b1 <> b5 by SCMFSA_2:16;
then A2:   n1 does_not_destroy b1 by SCMFSA7B:20;
A3:   n2 does_not_destroy b1 by A1,SCMFSA7B:14;
A4:   b1 <> b2 by SCMFSA_2:16;
      then m0 does_not_destroy b1 by SCMFSA7B:14;
then A5:   m1 does_not_destroy b1 by SCMFSA8C:77;
     b1 <> b4 by SCMFSA_2:16;
then A6:   m2 does_not_destroy b1 by SCMFSA7B:13;
     m3 does_not_destroy b1 by A4,SCMFSA7B:14;
      then m2 ';' m3 does_not_destroy b1 by A6,SCMFSA8C:84;
then A7:   IF does_not_destroy b1 by A5,SCMFSA8C:121;
        n1 ';' n2 does_not_destroy b1 by A2,A3,SCMFSA8C:84;
      hence thesis by A7,SCMFSA8C:81;
end;

Lm9:   ::Lem12
   body1 does_not_destroy b1
proof
A1:    b1 <> b2 by SCMFSA_2:16;
then A2:    t1 does_not_destroy b1 by SCMFSA7B:22;
A3:    t2 does_not_destroy b1 by A1,SCMFSA7B:14;
A4:    b1 <> b3 by SCMFSA_2:16;
then A5:    t3 does_not_destroy b1 by SCMFSA7B:12;
A6:    t4 does_not_destroy b1 by A4,SCMFSA7B:13;
         b1 <> b6 by SCMFSA_2:16;
then A7:    t5 does_not_destroy b1 by SCMFSA7B:20;
A8:    b1 <> b4 by SCMFSA_2:16;
then A9:    t6 does_not_destroy b1 by SCMFSA7B:14;
A10:    Wg does_not_destroy b1 by Lm8,Th7;
A11:    T3 does_not_destroy b1 by A8,Lm7,SCMBSORT:3;
         t1 ';' t2 does_not_destroy b1 by A2,A3,SCMFSA8C:84;
       then t1 ';' t2 ';' t3 does_not_destroy b1 by A5,SCMFSA8C:83;
       then t1 ';' t2 ';' t3 ';' t4 does_not_destroy b1 by A6,SCMFSA8C:83;
       then t1 ';' t2 ';' t3 ';' t4 ';' t5 does_not_destroy b1
            by A7,SCMFSA8C:83;
       then t16 does_not_destroy b1 by A9,SCMFSA8C:83;
       then t16 ';' Wg does_not_destroy b1 by A10,SCMFSA8C:81;
       hence thesis by A11,SCMFSA8C:81;
end;

Lm10:   ::Lem13
    Times(b4,body3) is good InitHalting Macro-Instruction
proof
         Initialized Times(b4,body3) is halting by Lm6,SCM_HALT:76;
       hence thesis by SCM_HALT:def 2;
end;

Lm11:   ::Lem15
    body1 is good InitHalting Macro-Instruction
proof
      reconsider WT=Wg as good InitHalting Macro-Instruction by Lm4,Th30;
      reconsider TT=T3 as good InitHalting Macro-Instruction by Lm10;
      reconsider t14=t1 ';' t2 ';' t3 ';' t4 as good InitHalting
      Macro-Instruction;
      reconsider t16=t14 ';' t5 ';' t6 as good InitHalting
      Macro-Instruction;
        t16 ';' WT ';' TT is good InitHalting;
      hence thesis;
end;

Lm12:   ::Lem16
  Times(b1,body1) is good InitHalting Macro-Instruction
proof
        Initialized Times(b1,body1) is halting by Lm9,Lm11,SCM_HALT:76;
      hence thesis by SCM_HALT:def 2;
end;

theorem Th44:    ::IS014
  insert-sort (fsloc 0) is keepInt0_1 InitHalting
proof
   reconsider T1 =Times(b1,body1)
     as good InitHalting Macro-Instruction by Lm12;
     WM= w2 ';' w3 ';' w4 ';' w5 ';' w6;
   then reconsider WM as keepInt0_1 InitHalting Macro-Instruction;
     insert-sort f0 = WM ';' j1 ';' j2 ';' T1 by Def2;
   hence thesis;
end;

Lm13:   ::Lem18
 for s be State of SCM+FSA holds IExec(IF,s).f0=s.f0
proof
  let s be State of SCM+FSA;
  set s0=Initialize s;
   per cases;
   suppose s.b5 >0;
       hence IExec(IF,s).f0 = IExec(m1,s).f0 by SCM_HALT:54
           .=Exec(m0,s0).f0 by SCMFSA6C:6
           .=s0.f0 by SCMFSA_2:91
           .=s.f0 by SCMFSA6C:3;
    suppose s.b5 <= 0;
      hence IExec(IF,s).f0 = IExec(m2 ';' m3, s).f0 by SCM_HALT:54
         .=Exec(m3,Exec(m2, s0)).f0 by SCMFSA6C:10
         .=Exec(m2, s0).f0 by SCMFSA_2:91
         .=s0.f0 by SCMFSA_2:90
         .=s.f0 by SCMFSA6C:3;
end;

Lm14:   ::Lem17
 for s be State of SCM+FSA holds
         (s.b5>0 implies IExec(IF,s).b4 =s.b4) &
         (s.b5<=0 implies IExec(IF,s).b4 =s.b4+1)
proof
  let s be State of SCM+FSA;
  set s0=Initialize s;
A1: b2<>b4 by SCMFSA_2:16;
  hereby
     assume s.b5 > 0;
     hence IExec(IF,s).b4 = IExec(m1,s).b4 by SCM_HALT:54
       .=Exec(m0,s0).b4 by SCMFSA6C:6
       .=s0.b4 by A1,SCMFSA_2:91
       .=s.b4 by SCMFSA6C:3;
  end;
  hereby
    assume s.b5 <= 0;
    hence IExec(IF,s).b4 = IExec(m2 ';' m3, s).b4 by SCM_HALT:54
     .=Exec(m3,Exec(m2, s0)).b4 by SCMFSA6C:9
     .=Exec(m2, s0).b4 by A1,SCMFSA_2:91
     .=s0.b4+s0.a0 by SCMFSA_2:90
     .=s0.b4+1 by SCMFSA6C:3
     .=s.b4+1 by SCMFSA6C:3;
  end;
end;

Lm15:   ::Lem20
 for a be read-write Int-Location,s be State of SCM+FSA st a<>b4 & a<>b2
    holds IExec(IF,s).a = s.a
proof
  let a be read-write Int-Location,s be State of SCM+FSA;
  assume A1:a<>b4 & a<> b2;
  set s1=Exec(m2, Initialize s),
      s2=IExec(m2 ';' m3, s);
A2: s1.a= (Initialize s).a by A1,SCMFSA_2:90
   .=s.a by SCMFSA6C:3;
A3: s2.a=Exec(m3,s1).a by SCMFSA6C:9
   .=s.a by A1,A2,SCMFSA_2:91;
   per cases;
   suppose s.b5 >0;
     hence IExec(IF,s).a = IExec(m1,s).a by SCM_HALT:54
           .=Exec(m0,Initialize s).a by SCMFSA6C:6
           .=(Initialize s).a by A1,SCMFSA_2:91
           .=s.a by SCMFSA6C:3;
    suppose s.b5 <= 0;
     hence IExec(IF,s).a =s.a by A3,SCM_HALT:54;
end;

Lm16:  ::Lem36
for t be State of SCM+FSA st t.b2 >= 1 & t.b2 <= len(t.f0)
 holds
       IExec(body2,t).b3=t.b3 & IExec(body2,t).b6=t.b6 &
       IExec(body2,t).f0=t.f0 &
       ex x1 be Integer st x1=t.f0.(t.b2) &
       ( x1-t.b6>0 implies IExec(body2,t).b2=0 &
         IExec(body2,t).b4=t.b4 ) &
       ( x1-t.b6<=0 implies IExec(body2,t).b2=t.b2-1 &
        IExec(body2,t).b4=t.b4+1 )
proof let s be State of SCM+FSA;
    assume A1:s.b2 >= 1 & s.b2 <= len(s.f0);
    set s0=Initialize s,
        s1=Exec(n1,s0),
        s2=IExec(n1 ';'n2,s);
A2:  b4<>b3 by SCMFSA_2:16;
A3:  b2<>b3 by SCMFSA_2:16;
A4:  b5<>b3 by SCMFSA_2:16;
 thus IExec(body2,s).b3=IExec(IF,s2).b3 by SCM_HALT:30
     .=s2.b3 by A2,A3,Lm15
     .=Exec(n2,s1).b3 by SCMFSA6C:9
     .=s1.b3 by A4,SCMFSA_2:91
     .=s0.b3 by A4,SCMFSA_2:98
     .=s.b3 by SCMFSA6C:3;
A5:  b4<>b6 by SCMFSA_2:16;
A6:  b2<>b6 by SCMFSA_2:16;
A7:  b5<>b6 by SCMFSA_2:16;
then A8:   s1.b6=s0.b6 by SCMFSA_2:98
     .=s.b6 by SCMFSA6C:3;
thus IExec(body2,s).b6=IExec(IF,s2).b6 by SCM_HALT:30
     .=s2.b6 by A5,A6,Lm15
     .=Exec(n2,s1).b6 by SCMFSA6C:9
     .=s.b6 by A7,A8,SCMFSA_2:91;
 thus IExec(body2,s).f0=IExec(IF,s2).f0 by SCM_HALT:31
     .=s2.f0 by Lm13
     .=Exec(n2,s1).f0 by SCMFSA6C:10
     .=s1.f0 by SCMFSA_2:91
     .=s0.f0 by SCMFSA_2:98
     .=s.f0 by SCMFSA6C:3;
A9:  b5<>b2 by SCMFSA_2:16;
A10:  s2.b2=Exec(n2,s1).b2 by SCMFSA6C:9
     .=s1.b2 by A9,SCMFSA_2:91
     .=s0.b2 by A9,SCMFSA_2:98
     .=s.b2 by SCMFSA6C:3;
A11:  b5<>b4 by SCMFSA_2:16;
A12:  s2.b4=Exec(n2,s1).b4 by SCMFSA6C:9
     .=s1.b4 by A11,SCMFSA_2:91
     .=s0.b4 by A11,SCMFSA_2:98
     .=s.b4 by SCMFSA6C:3;
A13:  s.b2>= 0 by A1,AXIOMS:22;
then A14:  abs(s.b2)=s.b2 by ABSVALUE:def 1;
     reconsider k1=s.b2 as Nat by A13,INT_1:16;
    k1 in dom (s.f0) by A1,FINSEQ_3:27;
     then s.f0.k1 in INT by FINSEQ_2:13;
     then reconsider n=s.f0.k1 as Integer by INT_1:12;
A15:  (s.f0)/.k1=n by A1,FINSEQ_4:24;
A16:  s1.b5=(s0.f0)/.(abs(s0.b2)) by SCMBSORT:8
     .=(s0.f0)/.(abs(s.b2)) by SCMFSA6C:3
     .=n by A14,A15,SCMFSA6C:3;
A17:  s2.b5=Exec(n2,s1).b5 by SCMFSA6C:9
     .=n-s.b6 by A8,A16,SCMFSA_2:91;
     take n;
     thus n=s.f0.(s.b2);
     hereby
        assume A18: n-s.b6>0;
        thus IExec(body2,s).b2=IExec(IF,s2).b2 by SCM_HALT:30
              .=0 by A17,A18,Lm3;
        thus IExec(body2,s).b4=IExec(IF,s2).b4 by SCM_HALT:30
              .=s.b4 by A12,A17,A18,Lm14;
      end;
     hereby
        assume A19: n-s.b6<=0;
        thus IExec(body2,s).b2=IExec(IF,s2).b2 by SCM_HALT:30
              .=s.b2-1 by A10,A17,A19,Lm3;
        thus IExec(body2,s).b4=IExec(IF,s2).b4 by SCM_HALT:30
              .=s.b4+1 by A12,A17,A19,Lm14;
     end;
end;

Lm17:  ::Lem29
  for k be Nat,s be State of SCM+FSA st s.b2=k & s.b2<=len(s.f0)
  holds s.f0=IExec(Wg,s).f0 & s.b6=IExec(Wg,s).b6 & s.b3=IExec(Wg,s).b3 &
    (k=0 or ex n be Nat,x1 be Integer
 st n=IExec(Wg,s).b4-s.b4 & n<=k & (k-n>=1 implies x1=s.f0.(k-n) & x1 >= s.b6)
       & (for i be Nat st i>k-n & i<k+1 holds ex x2 be Integer st
       x2=s.f0.i & x2 <= s.b6))
proof
   defpred P[Nat] means
   for s be State of SCM+FSA st s.b2=$1 & s.b2<=len(s.f0) holds
    IExec(Wg,s).f0=s.f0 & IExec(Wg,s).b6=s.b6 & IExec(Wg,s).b3=s.b3 &
    ($1=0 or ex n be Nat,x1 be Integer
 st n=IExec(Wg,s).b4-s.b4 & n<=$1 & ($1-n>=1 implies x1=s.f0.($1-n) & x1 >=
 s.b6)
    & (for i be Nat st i>$1-n & i<$1+1 holds ex x2 be Integer st
       x2=s.f0.i & x2 <= s.b6));
A1: P[0]
    proof let s be State of SCM+FSA;
      set s0=Initialize s;
      assume A2: s.b2=0 & s.b2<=len(s.f0);
      hence IExec(Wg,s).f0=s.f0 by Th34;
      thus IExec(Wg,s).b6=s0.b6 by A2,Th35
        .=s.b6 by SCMFSA6C:3;
      thus IExec(Wg,s).b3=s0.b3 by A2,Th35
        .=s.b3 by SCMFSA6C:3;
      thus
        0=0 or ex n be Nat,x1 be Integer
  st n=IExec(Wg,s).b4-s.b4 & n<=0 & (0-n>=1 implies x1=s.f0.(0-n) & x1 >= s.b6)
       & (for i be Nat st i>0-n & i<0+1 holds ex x2 be Integer st
       x2=s.f0.i & x2 <= s.b6);
   end;
A3: now let k be Nat;
      assume A4:P[k];
        now let s be State of SCM+FSA;
        assume A5: s.b2=k+1 & s.b2<=len(s.f0);
        then A6: s.b2>0 by NAT_1:19;
        then A7: s.b2 >= 1+0 by INT_1:20;
        set bs=IExec(body2,s),
            bs0=Initialize bs;
           consider m be Integer such that
       A8: m=s.f0.(s.b2) &
       ( m-s.b6>0 implies bs.b2=0 & bs.b4=s.b4) &
       ( m-s.b6<=0 implies bs.b2=s.b2-1 & bs.b4=s.b4+1) by A5,A7,Lm16;
       per cases;
       suppose A9:m-s.b6>0;
       thus IExec(Wg,s).f0=IExec(Wg,bs).f0 by A6,Lm5,Th36
         .=bs.f0 by A8,A9,Th34
         .=s.f0 by A5,A7,Lm16;
       thus IExec(Wg,s).b6=IExec(Wg,bs).b6 by A6,Lm5,Th37
         .=bs0.b6 by A8,A9,Th35
         .=bs.b6 by SCMFSA6C:3
         .=s.b6 by A5,A7,Lm16;
       thus IExec(Wg,s).b3=IExec(Wg,bs).b3 by A6,Lm5,Th37
         .=bs0.b3 by A8,A9,Th35
         .=bs.b3 by SCMFSA6C:3
         .=s.b3 by A5,A7,Lm16;
         A10: IExec(Wg,s).b4=IExec(Wg,bs).b4 by A6,Lm5,Th37
         .=bs0.b4 by A8,A9,Th35
         .=s.b4 by A8,A9,SCMFSA6C:3;
         now
          take n=0;
         take x1=m;
        thus n=IExec(Wg,s).b4-s.b4 by A10,XCMPLX_1:14;
        thus n<=k+1 by NAT_1:18;
        thus k+1-n>=1 implies x1=s.f0.(k+1-n) &
        x1>=0+s.b6 by A5,A8,A9,REAL_1:84;
        thus for i be Nat st i>k+1-n & i<k+1+1 holds ex x2 be Integer st
           x2=s.f0.i & x2 <= s.b6 by INT_1:20;
        end;
        hence (k+1)=0 or ex n be Nat,x1 be Integer st n=IExec(Wg,s).b4-s.b4
         & n<=k+1 & (k+1-n>=1 implies x1=s.f0.(k+1-n) & x1 >= s.b6)
         & (for i be Nat st i>k+1-n & i<k+1+1 holds ex x2 be Integer st
         x2=s.f0.i & x2 <= s.b6);

    suppose A11:m-s.b6<=0;
        then A12: bs.b2=k by A5,A8,XCMPLX_1:26;
        A13: bs.f0=s.f0 by A5,A7,Lm16;
              bs.b2<k+1 by A12,REAL_1:69;
            then A14: bs.b2<=len(s.f0) by A5,AXIOMS:22;
        A15: bs.f0=s.f0 by A5,A7,Lm16;
        A16: bs.b6=s.b6 by A5,A7,Lm16;
       thus IExec(Wg,s).f0=IExec(Wg,bs).f0 by A6,Lm5,Th36
            .=s.f0 by A4,A12,A13,A14;
       thus IExec(Wg,s).b6=IExec(Wg,bs).b6 by A6,Lm5,Th37
            .=s.b6 by A4,A12,A13,A14,A16;
       thus IExec(Wg,s).b3=IExec(Wg,bs).b3 by A6,Lm5,Th37
            .=bs.b3 by A4,A12,A13,A14
            .=s.b3 by A5,A7,Lm16;
       hereby
          per cases;
          suppose k<>0;
            then consider n be Nat,x1 be Integer such that
        A17:n=IExec(Wg,bs).b4-bs.b4 & n<=k &
             (k-n>=1 implies x1=bs.f0.(k-n) & x1 >= bs.b6)
            & (for i be Nat st i>k-n & i<k+1 holds ex x2 be Integer st
            x2=bs.f0.i & x2 <= bs.b6) by A4,A12,A13,A14;
          A18: IExec(Wg,s).b4=IExec(Wg,bs).b4 by A6,Lm5,Th37
          .=s.b4+1+n by A8,A11,A17,XCMPLX_1:27
          .=s.b4+(1+n) by XCMPLX_1:1;
          now
          take n1=1+n;
       A19: k+1-n1=k-n by XCMPLX_1:32;
          take y1=x1;
          thus n1=IExec(Wg,s).b4-s.b4 by A18,XCMPLX_1:26;
          thus n1<=k+1 by A17,AXIOMS:24;
          thus k+1-n1>=1 implies y1=s.f0.(k+1-n1) &
            y1 >=s.b6 by A5,A7,A15,A17,Lm16,XCMPLX_1:32;
            now let i be Nat;
            assume A20:i>k+1-n1 & i<k+1+1;
            per cases;
            suppose A21: i=k+1;
                  take x2=m;
                  thus x2=s.f0.i by A5,A8,A21;
                    x2<=0+s.b6 by A11,REAL_1:86;
                  hence x2<=s.b6;
            suppose A22: i<>k+1;
                   i<=k+1 by A20,INT_1:20;
                 then i<k+1 by A22,REAL_1:def 5;
               then consider y2 be Integer such that
             A23: y2=bs.f0.i & y2 <= bs.b6 by A17,A19,A20;
                take x2=y2;
                thus x2=s.f0.i by A5,A7,A23,Lm16;
                thus x2<=s.b6 by A5,A7,A23,Lm16;
          end;
          hence for i be Nat st i>k+1-n1 & i<k+1+1 holds
          ex x2 be Integer st x2=s.f0.i & x2 <= s.b6;
        end;
        hence k+1=0 or ex n be Nat,x1 be Integer st n=IExec(Wg,s).b4-s.b4 &
       n<=k+1 & (k+1-n>=1 implies x1=s.f0.(k+1-n) & x1 >= s.b6)
         & (for i be Nat st i>k+1-n & i<k+1+1 holds ex x2 be Integer st
         x2=s.f0.i & x2 <= s.b6);

       suppose A24:k=0;
           A25: IExec(Wg,s).b4=IExec(Wg,bs).b4 by A6,Lm5,Th37
            .=bs0.b4 by A5,A8,A24,Th35
            .=s.b4+1 by A8,A11,SCMFSA6C:3;
           now
              take n1=1;
              take x1=0;
              thus n1=IExec(Wg,s).b4-s.b4 by A25,XCMPLX_1:26;
              thus n1<=k+1 by A24;
              thus k+1-n1>=1 implies x1=s.f0.(k+1-n1) & x1 >= s.b6 by A24;
              hereby let i be Nat;
                  assume A26:i>k+1-n1 & i<k+1+1;
               then A27:i>=0+1 by A24,INT_1:20;
                  A28: i<=1 by A24,A26,INT_1:20;
                  take x2=m;
               thus x2=s.f0.i by A5,A8,A24,A27,A28,AXIOMS:21;
                    x2<=0+s.b6 by A11,REAL_1:86;
                  hence x2<=s.b6;
              end;
         end;
          hence k+1=0 or ex n be Nat,x1 be Integer st n=IExec(Wg,s).b4-s.b4
      & n<=k+1 & (k+1-n>=1 implies x1=s.f0.(k+1-n) & x1 >= s.b6)
           & (for i be Nat st i>k+1-n & i<k+1+1 holds ex x2 be Integer st
          x2=s.f0.i & x2 <= s.b6);
        end;
      end;
      hence P[k+1];
    end;
     for k be Nat holds P[k] from Ind(A1,A3);
   hence thesis;
end;

Lm18:  ::Lem32
for s be State of SCM+FSA holds
       IExec(body3,s).b3=s.b3-1 &
       IExec(body3,s).f0=s.f0+*(abs(s.b3),(s.f0)/.(abs((s.b3-1))))
         +*(abs((s.b3-1)),(s.f0)/.(abs(s.b3)))
proof let s be State of SCM+FSA;
    set s0=Initialize s,
        s1=Exec(i1,s0),
        s2=IExec(i1 ';' i2,s),
        s3=IExec(i1 ';' i2 ';' i3,s),
        s4=IExec(i1 ';' i2 ';' i3 ';' i4,s),
        s5=IExec(i1 ';' i2 ';' i3 ';' i4 ';' i5,s),
        s6=IExec(body3,s);
A1:  b6<>b3 by SCMFSA_2:16;
A2: b5<>b3 by SCMFSA_2:16;
A3: b2<>b3 by SCMFSA_2:16;
A4:  s1.a0=s0.a0 by SCMFSA_2:89
     .=1 by SCMFSA6C:3;
A5:  s3.b3=Exec(i3,s2).b3 by SCMFSA6C:7
     .=s2.b3 by A2,SCMFSA_2:98
     .=Exec(i2,s1).b3 by SCMFSA6C:9
     .=s1.b3-s1.a0 by SCMFSA_2:91
     .=s0.b3-s1.a0 by A3,SCMFSA_2:89
     .=s.b3-1 by A4,SCMFSA6C:3;
A6:  s5.b3=Exec(i5,s4).b3 by SCMFSA6C:7
     .=s4.b3 by SCMFSA_2:99
     .=Exec(i4,s3).b3 by SCMFSA6C:7
     .=s.b3-1 by A1,A5,SCMFSA_2:98;
thus s6.b3=Exec(i6,s5).b3 by SCMFSA6C:7
     .=s.b3-1 by A6,SCMFSA_2:99;
A7: s2.f0=Exec(i2,s1).f0 by SCMFSA6C:10
    .=s1.f0 by SCMFSA_2:91
    .=s0.f0 by SCMFSA_2:89
    .=s.f0 by SCMFSA6C:3;
A8:  s3.f0=Exec(i3,s2).f0 by SCMFSA6C:8
    .=s.f0 by A7,SCMFSA_2:98;
A9: s4.f0=Exec(i4,s3).f0 by SCMFSA6C:8
    .=s.f0 by A8,SCMFSA_2:98;
A10: b6<>b2 by SCMFSA_2:16;
A11: b5<>b2 by SCMFSA_2:16;
A12:  s2.b2=Exec(i2,s1).b2 by SCMFSA6C:9
     .=s1.b2 by A3,SCMFSA_2:91
     .=s0.b3 by SCMFSA_2:89
     .=s.b3 by SCMFSA6C:3;
A13:  s4.b2=Exec(i4,s3).b2 by SCMFSA6C:7
     .=s3.b2 by A10,SCMFSA_2:98
     .=Exec(i3,s2).b2 by SCMFSA6C:7
     .=s.b3 by A11,A12,SCMFSA_2:98;
A14:  s4.b6=Exec(i4,s3).b6 by SCMFSA6C:7
     .=(s.f0)/.(abs((s.b3-1))) by A5,A8,SCMBSORT:8;
A15: b6<>b5 by SCMFSA_2:16;
A16:  s5.b5=Exec(i5,s4).b5 by SCMFSA6C:7
     .=s4.b5 by SCMFSA_2:99
     .=Exec(i4,s3).b5 by SCMFSA6C:7
     .=s3.b5 by A15,SCMFSA_2:98
     .=Exec(i3,s2).b5 by SCMFSA6C:7
     .=(s.f0)/.(abs(s.b3)) by A7,A12,SCMBSORT:8;
A17:  s5.f0=Exec(i5,s4).f0 by SCMFSA6C:8
    .=s.f0+*(abs(s.b3),(s.f0)/.abs(s.b3-1)) by A9,A13,A14,SCMBSORT:9;
thus s6.f0=Exec(i6,s5).f0 by SCMFSA6C:8
    .=s.f0+*(abs(s.b3),(s.f0)/.abs(s.b3-1))
      +*(abs((s.b3-1)),(s.f0)/.abs(s.b3)) by A6,A16,A17,SCMBSORT:9;
end;

Lm19:  ::Lem31
  for k be Nat,s be State of SCM+FSA st s.b4=k & k<s.b3 & s.b3<=len(s.f0)
  holds (s.f0, IExec(T3,s).f0 are_fiberwise_equipotent) &
     IExec(T3,s).b3=s.b3-k & IExec(T3,s).f0.(s.b3-k)=s.f0.(s.b3) &
     (for i be Nat st s.b3-k<i & i<=s.b3 holds IExec(T3,s).f0.i=s.f0.(i-1))
     & (for i be Nat st s.b3<i & i<=len(s.f0) holds IExec(T3,s).f0.i=s.f0.i)
     & (for i be Nat st 1<=i & i<s.b3-k holds IExec(T3,s).f0.i=s.f0.i)
proof
     defpred P[Nat] means
    for s be State of SCM+FSA st s.b4=$1 & $1<s.b3 & s.b3<=len(s.f0)
  holds (s.f0, IExec(T3,s).f0 are_fiberwise_equipotent) &
     IExec(T3,s).b3=s.b3-$1 & IExec(T3,s).f0.(s.b3-$1)=s.f0.(s.b3) &
     (for i be Nat st s.b3-$1<i & i<=s.b3 holds IExec(T3,s).f0.i=s.f0.(i-1))
    & (for i be Nat st s.b3<i & i<=len(s.f0) holds IExec(T3,s).f0.i=s.f0.i)
    & (for i be Nat st 1<=i & i<s.b3-$1 holds IExec(T3,s).f0.i=s.f0.i);
A1:P[0]
  proof let s be State of SCM+FSA;
   assume A2:s.b4=0 & 0<s.b3 & s.b3<=len(s.f0);
      hence s.f0, IExec(T3,s).f0 are_fiberwise_equipotent by SCM_HALT:80;
      thus IExec(T3,s).b3=(Initialize s).b3 by A2,SCM_HALT:81
      .=s.b3-0 by SCMFSA6C:3;
      thus IExec(T3,s).f0.(s.b3-0)=s.f0.(s.b3) by A2,SCM_HALT:80;
      thus for i be Nat st s.b3-0<i & i<=s.b3 holds
           IExec(T3,s).f0.i=s.f0.(i-1);
      thus for i be Nat st s.b3<i & i<=len(s.f0) holds
        IExec(T3,s).f0.i=s.f0.i by A2,SCM_HALT:80;
      thus for i be Nat st 1<=i & i<s.b3-0
        holds IExec(T3,s).f0.i=s.f0.i by A2,SCM_HALT:80;
  end;
A3:now let k be Nat;
     assume A4:P[k];
     set s_4=SubFrom(b4,a0);
       now let s be State of SCM+FSA;
        assume A5: s.b4=k+1 & k+1<s.b3 & s.b3<=len(s.f0);
         then A6: s.b4>0 by NAT_1:19;
         set b3s=IExec(body3 ';'s_4,s),
             bds=IExec(body3,s);
      A7: b3s.b4=Exec(s_4,bds).b4 by SCMFSA6C:7
         .=bds.b4-bds.a0 by SCMFSA_2:91
         .=bds.b4-1 by SCMFSA6B:35
         .=(Initialize s).b4-1 by Lm6,SCMFSA8C:91
         .=k+1-1 by A5,SCMFSA6C:3
         .=k by XCMPLX_1:26;
      A8: b4<>b3 by SCMFSA_2:16;
       A9: b3s.b3=Exec(s_4,bds).b3 by SCMFSA6C:7
         .=bds.b3 by A8,SCMFSA_2:91
         .=s.b3-1 by Lm18;
          A10: k+1-1<s.b3-1 by A5,REAL_1:54;
       then A11:k<s.b3-1 by XCMPLX_1:26;
       A12:k<b3s.b3 by A9,A10,XCMPLX_1:26;
       A13:b3s.f0=Exec(s_4,bds).f0 by SCMFSA6C:8
         .=bds.f0 by SCMFSA_2:91;
           k+1>=0 by NAT_1:18;
      then A14: s.b3>=0 by A5,AXIOMS:22;
      then reconsider m=s.b3 as Nat by INT_1:16;
      A15: abs(s.b3)=m by A14,ABSVALUE:def 1;
      A16:k>=0 by NAT_1:18;
      then A17:s.b3-1>=0 by A11,AXIOMS:22;
      then reconsider n=s.b3-1 as Nat by INT_1:16;
      A18:abs(s.b3-1)=n by A17,ABSVALUE:def 1;
      A19: 0+1<=k+1 by A16,AXIOMS:24;
      then A20: 1<=m by A5,AXIOMS:22;
           k+1+1<=m by A5,INT_1:20;
         then k+1+1-1<=n by REAL_1:49;
         then k+1<=n by XCMPLX_1:26;
     then A21: 1<=n by A19,AXIOMS:22;
       n<s.b3 by INT_1:26;
     then A22: n<=len(s.f0) by A5,AXIOMS:22;
     A23: bds.f0=s.f0+*(m,(s.f0)/.n) +*(n,(s.f0)/.m) by A15,A18,Lm18;
        set ff=s.f0, gg=bds.f0;
     A24: ff.m=gg.n & ff.n=gg.m &
        (for k be set st k<>m & k<>n & k in dom ff holds ff.k=gg.k) &
        ff,gg are_fiberwise_equipotent by A5,A20,A21,A22,A23,Th9;
     A25:ff,b3s.f0 are_fiberwise_equipotent by A5,A13,A20,A21,A22,A23,Th9;
     A26:len ff=len (b3s.f0) by A13,A24,RFINSEQ:16;
          n<=len(b3s.f0) by A22,A25,RFINSEQ:16;
    then A27: (b3s.f0,IExec(T3,b3s).f0 are_fiberwise_equipotent) &
       IExec(T3,b3s).b3=b3s.b3-k & IExec(T3,b3s).f0.(b3s.b3-k)
        =b3s.f0.(b3s.b3) & (for i be Nat st b3s.b3-k<i & i<=b3s.b3 holds
       IExec(T3,b3s).f0.i=b3s.f0.(i-1)) & (for i be Nat st b3s.b3<i &
       i<=len(b3s.f0) holds IExec(T3,b3s).f0.i=b3s.f0.i) & (for i be Nat
       st 1<=i & i<b3s.b3-k holds IExec(T3,b3s).f0.i=b3s.f0.i)
             by A4,A7,A9,A12;
     IExec(T3,s).f0=IExec(T3,b3s).f0 by A6,Lm6,SCM_HALT:82;
    hence ff,IExec(T3,s).f0 are_fiberwise_equipotent by A25,A27,RFINSEQ:2;
    A28: b3s.b3-k=s.b3+(-1-k) by A9,XCMPLX_1:158
       .=s.b3+ (-(k+1)) by XCMPLX_1:161
       .=s.b3-(k+1) by XCMPLX_0:def 8;
    hence IExec(T3,s).b3=s.b3-(k+1) by A6,A27,Lm6,SCM_HALT:83;
    thus IExec(T3,s).f0.(s.b3-(k+1))=s.f0.(s.b3) by A6,A9,A13,A24,A27,A28,Lm6,
SCM_HALT:82;
    hereby let i be Nat;
        assume A29: s.b3-(k+1)<i & i<=s.b3;
        per cases;
        suppose A30:i=s.b3;
           then A31:b3s.b3<i by A9,INT_1:26;
           thus IExec(T3,s).f0.i=IExec(T3,b3s).f0.i
               by A6,Lm6,SCM_HALT:82
           .=s.f0.(i-1) by A4,A5,A7,A9,A12,A13,A22,A24,A26,A30,A31;
        suppose i<>s.b3;
        then i<s.b3 by A29,REAL_1:def 5;
           then A32: i+1<=s.b3 by INT_1:20;
        then A33: i<=s.b3-1 by REAL_1:84;
        A34: i<=b3s.b3 by A9,A32,REAL_1:84;
        A35: i-1<i by INT_1:26;
        then A36: i-1<s.b3 by A29,AXIOMS:22;
              k+1-(k+1)<s.b3-(k+1) by A5,REAL_1:54;
            then 0<s.b3-(k+1) by XCMPLX_1:14;
        then A37: 1+0<=s.b3-(k+1) by INT_1:20;
             s.b3-(k+1)+1<=i by A29,INT_1:20;
           then s.b3-(k+1)+1-1<=i-1 by REAL_1:49;
           then s.b3-(k+1)<=i-1 by XCMPLX_1:26;
        then A38: 1<=i-1 by A37,AXIOMS:22;
            then 0<=i-1 by AXIOMS:22;
            then reconsider i1=i-1 as Nat by INT_1:16;
              i1<=len (s.f0) by A5,A36,AXIOMS:22;
        then A39: i1 in dom ff by A38,FINSEQ_3:27;
       thus IExec(T3,s).f0.i=IExec(T3,b3s).f0.i
               by A6,Lm6,SCM_HALT:82
           .=bds.f0.(i-1) by A4,A7,A9,A12,A13,A22,A26,A28,A29,A34
           .=s.f0.(i-1) by A5,A20,A21,A22,A23,A29,A33,A35,A39,Th9;
     end;
     hereby let i be Nat;
       assume A40:s.b3<i & i<=len(s.f0);
          s.b3-1<s.b3 by INT_1:26;
     then A41:b3s.b3<i by A9,A40,AXIOMS:22;
     A42: n<>i by A40,INT_1:26;
     A43: k+1<i by A5,A40,AXIOMS:22;
           1<=k+1 by NAT_1:29;
         then 1<=i by A43,AXIOMS:22;
     then A44: i in dom ff by A40,FINSEQ_3:27;
     thus IExec(T3,s).f0.i=IExec(T3,b3s).f0.i
               by A6,Lm6,SCM_HALT:82
          .=bds.f0.i by A4,A7,A9,A12,A13,A22,A26,A40,A41
          .=s.f0.i by A5,A20,A21,A22,A23,A40,A42,A44,Th9;
     end;
      hereby let i be Nat;
        assume A45:1<=i & i<s.b3-(k+1);
      then A46:i<s.b3-1-k by XCMPLX_1:36;
      A47:i<b3s.b3-k by A9,A45,XCMPLX_1:36;
          0<=k by NAT_1:18;
       then A48: s.b3-1-k<=s.b3-1-0 by REAL_1:92;
      then A49: i<s.b3-1 by A46,AXIOMS:22;
         A50: s.b3-1<s.b3 by INT_1:26;
      then A51: i<s.b3 by A49,AXIOMS:22;
      A52: i<>m by A46,A48,A50,AXIOMS:22;
            i<=len (s.f0) by A5,A51,AXIOMS:22;
      then A53: i in dom ff by A45,FINSEQ_3:27;
      thus IExec(T3,s).f0.i=IExec(T3,b3s).f0.i
                   by A6,Lm6,SCM_HALT:82
          .=bds.f0.i by A4,A7,A9,A12,A13,A22,A26,A45,A47
          .=s.f0.i by A5,A20,A21,A22,A23,A46,A48,A52,A53,Th9;
     end;
    end;
    hence P[k+1];
  end;
    for k be Nat holds P[k] from Ind(A1,A3);
  hence thesis;
end;

Lm20:  ::Lem28
 for s be State of SCM+FSA holds IExec(t16,s).b2=len(s.f0) - s.b1 &
 IExec(t16,s).b3=len(s.f0) - s.b1+1 & IExec(t16,s).f0=s.f0 &
 IExec(t16,s).b4=0 & IExec(t16,s).b6=(s.f0)/.(abs((len(s.f0)-s.b1+1)))
proof let s be State of SCM+FSA;
    set s0=Initialize s,
        s1=Exec(t1,s0),
        s2=IExec(t1 ';' t2,s),
        s3=IExec(t1 ';' t2 ';' t3,s),
        s4=IExec(t1 ';' t2 ';' t3 ';' t4,s),
        s5=IExec(t1 ';' t2 ';' t3 ';' t4 ';' t5,s),
        s6=IExec(t16,s);
A1: b4<>b3 by SCMFSA_2:16;
A2: b4<>b2 by SCMFSA_2:16;
A3: b6<>b4 by SCMFSA_2:16;
A4: b6<>b3 by SCMFSA_2:16;
A5: b6<>b2 by SCMFSA_2:16;
A6: b2<>b3 by SCMFSA_2:16;
A7: b2<>b1 by SCMFSA_2:16;
A8:  s3.a0=1 by SCMFSA6B:35;
A9:  s2.b2=Exec(t2,s1).b2 by SCMFSA6C:9
     .=s1.b2-s1.b1 by SCMFSA_2:91
     .=len(s0.f0)-s1.b1 by SCMFSA_2:100
     .=len(s0.f0)-s0.b1 by A7,SCMFSA_2:100
     .=len(s.f0)-s0.b1 by SCMFSA6C:3
     .=len(s.f0)-s.b1 by SCMFSA6C:3;
thus s6.b2=Exec(t6,s5).b2 by SCMFSA6C:7
     .=s5.b2 by A2,SCMFSA_2:91
     .=Exec(t5,s4).b2 by SCMFSA6C:7
     .=s4.b2 by A5,SCMFSA_2:98
     .=Exec(t4,s3).b2 by SCMFSA6C:7
     .=s3.b2 by A6,SCMFSA_2:90
     .=Exec(t3,s2).b2 by SCMFSA6C:7
     .=len(s.f0)-s.b1 by A6,A9,SCMFSA_2:89;

A10:  s4.b3=Exec(t4,s3).b3 by SCMFSA6C:7
     .=s3.b3+1 by A8,SCMFSA_2:90
     .=Exec(t3,s2).b3+1 by SCMFSA6C:7
     .=len(s.f0)-s.b1+1 by A9,SCMFSA_2:89;
thus s6.b3=Exec(t6,s5).b3 by SCMFSA6C:7
     .=s5.b3 by A1,SCMFSA_2:91
     .=Exec(t5,s4).b3 by SCMFSA6C:7
     .=len(s.f0)-s.b1+1 by A4,A10,SCMFSA_2:98;

A11:  s4.f0=Exec(t4,s3).f0 by SCMFSA6C:8
     .=s3.f0 by SCMFSA_2:90
     .=Exec(t3,s2).f0 by SCMFSA6C:8
     .=s2.f0 by SCMFSA_2:89
     .=Exec(t2,s1).f0 by SCMFSA6C:10
     .=s1.f0 by SCMFSA_2:91
     .=s0.f0 by SCMFSA_2:100
     .=s.f0 by SCMFSA6C:3;

thus s6.f0=Exec(t6,s5).f0 by SCMFSA6C:8
     .=s5.f0 by SCMFSA_2:91
     .=Exec(t5,s4).f0 by SCMFSA6C:8
     .=s.f0 by A11,SCMFSA_2:98;
thus s6.b4=Exec(t6,s5).b4 by SCMFSA6C:7
     .=s5.b4-s5.b4 by SCMFSA_2:91
     .=0 by XCMPLX_1:14;

thus s6.b6=Exec(t6,s5).b6 by SCMFSA6C:7
     .=s5.b6 by A3,SCMFSA_2:91
     .=Exec(t5,s4).b6 by SCMFSA6C:7
     .=(s.f0)/.(abs((len(s.f0)-s.b1+1))) by A10,A11,SCMBSORT:8;
end;

set T1=Times(b1,body1);
Lm21:
 for s be State of SCM+FSA st s.b1=len (s.f0) -1 holds
    (s.f0, IExec(T1,s).f0 are_fiberwise_equipotent) &
    (for i,j be Nat st i>=1 & j<=len (s.f0) & i<j
     for x1,x2 be Integer st x1 =IExec(T1,s).f0.i &
        x2=IExec(T1,s).f0.j holds x1 >= x2)
proof
    let s be State of SCM+FSA;
    assume A1: s.b1=len (s.f0)-1;
    reconsider t14=t1 ';' t2 ';' t3 ';' t4 as good InitHalting
    Macro-Instruction;
    reconsider t16=t14 ';' t5 ';' t6 as good InitHalting Macro-Instruction;
    reconsider Wt=Wg as good InitHalting Macro-Instruction by Lm4,Th30;
    A2: t16 ';' Wt is good InitHalting Macro-Instruction;
    per cases;
    suppose A3:len (s.f0)<=1;
      then len (s.f0)-1<=0 by REAL_2:106;
      hence s.f0, IExec(T1,s).f0 are_fiberwise_equipotent by A1,Lm11,SCM_HALT:
80;
        now let i,j be Nat;
          assume A4:i>=1 & j<=len (s.f0) & i<j;
          then j<=1 & i<j by A3,AXIOMS:22;
          hence contradiction by A4,AXIOMS:22;
      end;
      hence thesis;
    suppose A5:len (s.f0)>1;
     defpred P[Nat] means
     for t be State of SCM+FSA st t.b1=$1 & t.b1<=len(t.f0)-1 holds
     ((for i,j be Nat st i>=1 & j<=len(t.f0)-t.b1 & i<j
        for x1,x2 be Integer st x1 =t.f0.i & x2=t.f0.j holds x1 >= x2)
     implies
      (t.f0, IExec(T1,t).f0 are_fiberwise_equipotent) &
      (for i,j be Nat st i>=1 & j<=len(t.f0) & i<j
        for x1,x2 be Integer st x1 =IExec(T1,t).f0.i & x2=IExec(T1,t).f0.j
           holds x1 >= x2));
A6: P[0]
    proof let t be State of SCM+FSA;
       assume A7:t.b1=0 & t.b1 <= len (t.f0)-1;
     then IExec(T1,t).f0=t.f0 by Lm11,SCM_HALT:80;
       hence
           (for i,j be Nat st i>=1 & j<=len(t.f0)-t.b1 & i<j
            for x1,x2 be Integer st x1 =t.f0.i & x2=t.f0.j holds x1 >= x2)
            implies
        (t.f0, IExec(T1,t).f0 are_fiberwise_equipotent) &
        for i,j being Nat st
           (i>=1 & j<=len(t.f0) & i<j) holds
           for x1,x2 being Integer st
           x1 =IExec(T1,t).f0.i & x2=IExec(T1,t).f0.j
           holds x1 >= x2 by A7;
    end;
A8: now let k be Nat;
     assume A9:P[k];
       now let t be State of SCM+FSA;
        assume A10: t.b1=k+1 & t.b1<=len(t.f0)-1;
         set B_1=SubFrom(b1,a0),
             IB=IExec(body1 ';' B_1,t);
         A11: t.b1>0 by A10,NAT_1:19;
         then A12: IB.b1=k+1-1 by A10,Lm9,Lm11,SCM_HALT:79
             .=k by XCMPLX_1:26;
        set IW=IExec(t16 ';' Wg,t),
            ts=IExec(t16,t);
         A13: ts.f0=t.f0 by Lm20;
         A14:len(t.f0)+ -(len (t.f0)-1)=len(t.f0)-(len (t.f0)-1)
           by XCMPLX_0:def 8
            .=1 by XCMPLX_1:18;
         A15: ts.b2=len(t.f0)-t.b1 by Lm20;
               len(t.f0)<len(t.f0)+t.b1 by A11,REAL_1:69;
             then A16: len(t.f0)-t.b1<len(t.f0)+t.b1-t.b1 by REAL_1:54;
         then A17: len(t.f0)-t.b1<len(t.f0) by XCMPLX_1:26;
               ts.b2<len(t.f0) by A15,A16,XCMPLX_1:26;
         then A18:ts.b2<=len(ts.f0) by Lm20;
                -(len (t.f0)-1) <= -t.b1 by A10,REAL_1:50;
             then len(t.f0)+ -(len (t.f0)-1)<=len(t.f0)+-t.b1 by AXIOMS:24;
        then A19:1<=len(t.f0)-t.b1 by A14,XCMPLX_0:def 8;
            then 0<=len(t.f0)-t.b1 by AXIOMS:22;
        then reconsider k1=len(t.f0)-t.b1 as Nat by INT_1:16;
        A20: ts.b2=k1 by Lm20;
             0<k1 by A19,AXIOMS:22;
        then consider n be Nat,x1 be Integer such that
        A21: n=IExec(Wg,ts).b4-ts.b4 & n<=k1 & (k1-n>=1
              implies x1=ts.f0.(k1-n) & x1 >= ts.b6) & (for i be
              Nat st i>k1-n & i<k1+1 holds ex x2 be Integer st
              x2=ts.f0.i & x2 <= ts.b6) by A15,A18,Lm17;
       A22: IW.f0=IExec(Wg,ts).f0 by Lm5,SCM_HALT:31
             .=t.f0 by A13,A17,A20,Lm17;
       A23: IB.f0=Exec(B_1,IExec(body1,t)).f0 by Lm11,SCM_HALT:34
             .=IExec(body1,t).f0 by SCMFSA_2:91
             .=IExec(T3,IW).f0 by A2,Lm10,SCM_HALT:31;
         IExec(Wg,ts).b4=n+ts.b4 by A21,XCMPLX_1:27;
       then A24: IW.b4=n+ts.b4 by Lm5,SCM_HALT:30
           .=n+0 by Lm20
           .=n;
       A25: IW.b3=IExec(Wg,ts).b3 by Lm5,SCM_HALT:30
           .=ts.b3 by A13,A17,A20,Lm17
           .=k1+1 by Lm20;
           A26: k1<k1+1 by REAL_1:69;
       then A27: n<k1+1 by A21,AXIOMS:22;
       A28: n<IW.b3 by A21,A25,A26,AXIOMS:22;
             n-n<k1+1-n by A27,REAL_1:54;
       then A29: 0<k1+1-n by XCMPLX_1:14;
       A30: len(t.f0)-t.b1+1<=len(t.f0) by A17,INT_1:20;
       A31: IW.b3<=len(IW.f0) by A17,A22,A25,INT_1:20;
             k1+1>0 by NAT_1:19;
       then A32: 1+0<=k1+1 by INT_1:20;
             0<=k1+1 by NAT_1:18;
       then A33: abs((k1+1))=k1+1 by ABSVALUE:def 1;
           k1+1 in dom (t.f0) by A30,A32,FINSEQ_3:27;
         then t.f0.(k1+1) in INT by FINSEQ_2:13;
       then reconsider n3=t.f0.(k1+1) as Integer by INT_1:12;
       A34: ts.b6=(t.f0)/.(k1+1) by A33,Lm20
           .=n3 by A30,A32,FINSEQ_4:24;
       then A35: k1-n>=1 implies x1=t.f0.(k1-n) &
            x1 >= n3 by A21,Lm20;
         set mm=k1+1-n;
A36: IExec(T3,IW).f0.mm=IW.f0.(k1+1) by A22,A24,A25,A27,A30,Lm19;
    A37: IW.f0,IExec(T3,IW).f0 are_fiberwise_equipotent by A22,A24,A25,A27,A30,
Lm19;
         IW.f0, IB.f0 are_fiberwise_equipotent by A22,A23,A24,A25,A28,A30,Lm19;
          then A38: len(IB.f0)=len(t.f0) by A22,RFINSEQ:16;
                IB.b1<t.b1 by A10,A12,REAL_1:69;
              then A39: IB.b1<=len(IB.f0)-1 by A10,A38,AXIOMS:22;
       hereby
          assume A40: for i,j be Nat st i>=1 & j<=len(t.f0)-t.b1 & i<j
           for x1,x2 be Integer st x1 =t.f0.i & x2=t.f0.j holds x1 >= x2;
           A41: now
               let i,j be Nat;
               assume A42:i>=1 & j<=len(IB.f0)-IB.b1 & i<j;
               let y1,y2 be Integer;
               assume A43:y1 =IB.f0.i & y2=IB.f0.j;
            A44: len(IB.f0)-IB.b1=len(t.f0)+1-t.b1 by A10,A12,A38,XCMPLX_1:32
               .=k1+1 by XCMPLX_1:29;
            then A45:j-1<=k1 by A42,REAL_1:86;
               A46:1<=j by A42,AXIOMS:22;
                 n>=0 by NAT_1:18;
               then A47: k1+1-n<=k1+1-0 by REAL_1:92;
                then k1-n+1<=k1+1 by XCMPLX_1:29;
            then A48: k1-n<=k1 by REAL_1:53;
                 A49: 1-1<=i-1 by A42,REAL_1:49;
                 then reconsider i1=i-1 as Nat by INT_1:16;
            A50: i-1<j-1 by A42,REAL_1:54;
                 then 0<=j-1 by A49,AXIOMS:22;
                then reconsider j1=j-1 as Nat by INT_1:16;
               per cases by AXIOMS:21;
               suppose A51:i<mm;
                   then A52: y1=t.f0.i by A22,A23,A24,A25,A27,A31,A42,A43,Lm19;
                   hereby per cases by AXIOMS:21;
                     suppose A53:j<mm;
                     then j<k1+1 by A47,AXIOMS:22;
                   then A54:j<=k1 by INT_1:20;
                       y2=t.f0.j by A22,A23,A24,A25,A27,A31,A43,A46,A53,Lm19;
                    hence y1 >= y2 by A40,A42,A52,A54;
                     suppose A55:j>mm;
                     then mm+1<=j by INT_1:20;
                     then mm<=j1 by REAL_1:84;
                  then A56:i<j1 by A51,AXIOMS:22;
                       y2=t.f0.j1 by A22,A23,A24,A25,A27,A31,A42,A43,A44,A55,
Lm19;
                    hence y1 >= y2 by A40,A42,A45,A52,A56;
                     suppose A57: j=mm;
                 then A58: y2=t.f0.(k1+1) by A22,A23,A24,A25,A28,A30,A43,Lm19;
                       i<k1-n+1 by A51,XCMPLX_1:29;
                 then A59: i<=k1-n by INT_1:20;
                 then A60: 1<=k1-n by A42,AXIOMS:22;
                     hereby
                         0<=k1-n by A60,AXIOMS:22;
                       then reconsider kn=k1-n as Nat by INT_1:16;
                 A61:   t.f0.kn=x1 by A21,A42,A59,Lm20,AXIOMS:22;
                       per cases;
                       suppose i=kn;
                        hence y1>=y2 by A21,A22,A23,A24,A25,A27,A30,A34,A42,A43
,A51,A58,A61,Lm19;
                       suppose i<>kn;
                          then i<kn by A59,REAL_1:def 5;
                          then y1>=x1 by A35,A40,A42,A48,A52,AXIOMS:22;
                          hence y1 >= y2 by A21,A22,A23,A34,A36,A42,A43,A57,A59
,AXIOMS:22;
                     end;
                   end;
               suppose A62:i>mm;
                   i<=k1+1 by A42,A44,AXIOMS:22;
                then A63: y1=t.f0.i1 by A22,A23,A24,A25,A27,A31,A43,A62,Lm19;
                   mm<j by A42,A62,AXIOMS:22;
                then A64: y2=t.f0.j1 by A22,A23,A24,A25,A27,A31,A42,A43,A44,
Lm19;
                      mm+1<=i by A62,INT_1:20;
                    then 0<i1 by A29,REAL_1:84;
                    then 1+0<=i1 by INT_1:20;
                hence y1 >= y2 by A40,A45,A50,A63,A64;
               suppose A65:i=mm;
                then A66: y2=t.f0.j1 by A22,A23,A24,A25,A28,A31,A42,A43,A44,
Lm19;
                      k1<k1+1 by REAL_1:69;
                then A67:j1<k1+1 by A45,AXIOMS:22;
                A68:mm-1=k1-n+1-1 by XCMPLX_1:29
                 .=k1-n by XCMPLX_1:26;
                    mm-1<j1 by A42,A65,REAL_1:54;
                  then consider yy be Integer such that
                A69: yy=t.f0.j1 & yy <= n3 by A13,A21,A34,A67,A68;
                  thus y1 >= y2 by A22,A23,A24,A25,A28,A31,A43,A65,A66,A69,Lm19
;
           end;
       then A70: (IB.f0, IExec(T1,IB).f0 are_fiberwise_equipotent) &
           (for i,j be Nat st i>=1 & j<=len(IB.f0) & i<j
           for x1,x2 be Integer st x1 =IExec(T1,IB).f0.i &
           x2=IExec(T1,IB).f0.j holds x1 >= x2) by A9,A12,A39;
       A71: IExec(T1,t).f0=IExec(T1,IB).f0 by A11,Lm9,Lm11,SCM_HALT:82;
          hence t.f0, IExec(T1,t).f0 are_fiberwise_equipotent by A22,A23,A37,
A70,RFINSEQ:2;
          let i,j be Nat;
            assume A72:i>=1 & j<=len(t.f0) & i<j;
              let x1,x2 be Integer;
            assume A73:x1=IExec(T1,t).f0.i & x2=IExec(T1,t).f0.j;
              j<=len(IB.f0) by A22,A23,A37,A72,RFINSEQ:16;
             hence x1>=x2 by A9,A12,A39,A41,A71,A72,A73;
      end;
    end;
    hence P[k+1];
    end;
      1-1<len(s.f0)-1 by A5,REAL_1:54
;
    then reconsider m=len(s.f0)-1 as Nat by INT_1:16;
      for k be Nat holds P[k] from Ind(A6,A8);
    then A74: P[m];
then A75: (for i,j be Nat st i>=1 & j<=len(s.f0)-s.b1 & i<j
        for x1,x2 be Integer st x1 =s.f0.i & x2=s.f0.j holds x1 >= x2)
     implies
      (s.f0, IExec(T1,s).f0 are_fiberwise_equipotent) &
      (for i,j be Nat st i>=1 & j<=len(s.f0) & i<j
        for x1,x2 be Integer st x1 =IExec(T1,s).f0.i & x2=IExec(T1,s).f0.j
           holds x1 >= x2) by A1;
     A76: now let i,j be Nat;
         assume A77:i>=1 & j<=len(s.f0)-s.b1 & i<j;
           then j<=1 by A1,XCMPLX_1:18;
         hence contradiction by A77,AXIOMS:22;
     end;
then A78: for i,j be Nat st i>=1 & j<=len(s.f0)-s.b1 & i<j
        for x1,x2 be Integer st x1 =s.f0.i & x2=s.f0.j holds x1 >= x2;
     thus s.f0, IExec(T1,s).f0 are_fiberwise_equipotent by A75,A76;
     thus thesis by A1,A74,A78;
end;

theorem Th45:   ::IS016
for s be State of SCM+FSA holds
    (s.f0, IExec(insert-sort f0,s).f0 are_fiberwise_equipotent) &
    (for i,j be Nat st i>=1 & j<=len (s.f0) & i<j
     for x1,x2 be Integer st x1 =IExec(insert-sort f0,s).f0.i &
        x2=IExec(insert-sort f0,s).f0.j holds x1 >= x2)
proof let s be State of SCM+FSA;
      set WJ=w2 ';' w3 ';' w4 ';' w5 ';' w6 ';' j1 ';' j2,
      s0=Initialize s,
      s1=Exec(w2, s0),
      s2=IExec(w2 ';' w3, s),
      s3=IExec(w2 ';' w3 ';' w4,s),
      s4=IExec(w2 ';' w3 ';' w4 ';' w5,s),
      s5=IExec(w2 ';' w3 ';' w4 ';' w5 ';' w6,s),
      s6=IExec(w2 ';' w3 ';' w4 ';' w5 ';' w6 ';' j1,s),
      s7=IExec(WJ,s);
A1:  s5.f0 =Exec(w6, s4).f0 by SCMFSA6C:8
     .=s4.f0 by SCMFSA_2:89
     .=Exec(w5, s3).f0 by SCMFSA6C:8
     .=s3.f0 by SCMFSA_2:89
     .=Exec(w4, s2).f0 by SCMFSA6C:8
     .=s2.f0 by SCMFSA_2:89
     .=Exec(w3, s1).f0 by SCMFSA6C:10
     .=s1.f0 by SCMFSA_2:89
     .=s0.f0 by SCMFSA_2:89
     .=s.f0 by SCMFSA6C:3;
A2:  s6.f0 =Exec(j1, s5).f0 by SCMFSA6C:8
     .=s.f0 by A1,SCMFSA_2:100;
A3:  IExec(WJ,s).f0 =Exec(j2, s6).f0 by SCMFSA6C:8
     .=s.f0 by A2,SCMFSA_2:91;
A4:  s6.b1=Exec(j1, s5).b1 by SCMFSA6C:7
    .=len (s7.f0) by A1,A3,SCMFSA_2:100;
A5:  s7.b1=Exec(j2, s6).b1 by SCMFSA6C:7
     .=s6.b1-s6.a0 by SCMFSA_2:91
     .=len (s7.f0) - 1 by A4,SCM_HALT:17;
A6:  IExec(insert-sort f0,s).f0=IExec(WJ ';' T1,s).f0 by Def2
     .=IExec(T1,s7).f0 by Lm12,SCM_HALT:31;
     hence s.f0, IExec(insert-sort f0,s).f0 are_fiberwise_equipotent by A3,A5,
Lm21;
     let i,j be Nat;
     assume i>=1 & j<=len (s.f0) & i<j;
     hence thesis by A3,A5,A6,Lm21;
end;

theorem Th46:    ::IS018
 for i being Nat, s being State of SCM+FSA,w being FinSequence of INT
  st Initialized Insert-Sort-Algorithm +* ((fsloc 0) .--> w) c= s
  holds IC (Computation s).i in dom Insert-Sort-Algorithm
proof
   set IS=Insert-Sort-Algorithm,
       Ii=Initialized IS;
   let i be Nat, s be State of SCM+FSA,w be FinSequence of INT;
   set x=((fsloc 0) .--> w);
   assume A1: Ii +* x c= s;
     dom Ii misses dom x by SCMBSORT:46;
   then Ii c= Ii +* x by FUNCT_4:33;
then A2:Ii c= s by A1,XBOOLE_1:1;
     IS is InitHalting Macro-Instruction by Def3,Th44;
   hence thesis by A2,SCM_HALT:def 1;
end;

theorem Th47:   ::IS020
  for s be State of SCM+FSA,t be FinSequence of INT st
  Initialized Insert-Sort-Algorithm +*(fsloc 0 .--> t) c= s
  holds ex u being FinSequence of REAL
    st t,u are_fiberwise_equipotent & u is non-increasing &
     u is FinSequence of INT & (Result s).(fsloc 0) = u
proof
  let s be State of SCM+FSA,t be FinSequence of INT;
  set Ia=Insert-Sort-Algorithm,
      p=Initialized Ia,
      x=fsloc 0 .--> t,
      z=IExec(insert-sort f0,s).f0;
  assume A1: p+*x c= s;
      dom x = { f0} by CQC_LANG:5;
then A2: f0 in dom x by TARSKI:def 1;
 then f0 in dom (p+*x) by FUNCT_4:13;
then A3: s.f0=(p+*x).f0 by A1,GRFUNC_1:8
    .=x.f0 by A2,FUNCT_4:14
    .=t by CQC_LANG:6;
A4: (s.f0, z are_fiberwise_equipotent) &
    (for i,j be Nat st i>=1 & j<=len (s.f0) & i<j
     for x1,x2 be Integer st x1 =z.i & x2=z.j holds x1 >= x2) by Th45;
     reconsider u=z as FinSequence of REAL by SCMBSORT:38;
     take u;
     thus t, u are_fiberwise_equipotent by A3,Th45;
A5:  dom (s.f0) = dom u by A4,RFINSEQ:16;
       now let i,j be Nat;
        assume A6:i in dom u & j in dom u & i<j;
        then A7: i>=1 by FINSEQ_3:27;
        A8: j<=len (s.f0) by A5,A6,FINSEQ_3:27;
        A9: z.i in INT & z.j in INT by A6,FINSEQ_2:13;
            then reconsider y1=z.i as Integer by INT_1:12;
            reconsider y2=z.j as Integer by A9,INT_1:12;
           y1 >= y2 by A6,A7,A8,Th45;
           hence u.i>=u.j;
     end;
     hence u is non-increasing by RFINSEQ:32;
     thus u is FinSequence of INT;
       dom p misses dom x by SCMBSORT:46;
     then p c=p+*x by FUNCT_4:33;
     then p c= s by A1,XBOOLE_1:1;
  then s=s+*p by AMI_5:10;
    hence (Result s ).f0 =IExec(Ia,s).f0 by SCMBSORT:57
    .=u by Def3;
end;

theorem Th48:    ::IS022
 for w being FinSequence of INT holds
  Initialized Insert-Sort-Algorithm +* ((fsloc 0) .--> w) is autonomic
proof
     let w be FinSequence of INT;
     set p=Initialized Insert-Sort-Algorithm +* ((fsloc 0) .--> w),
         q=Insert-Sort-Algorithm;
A1: for s1,s2 being State of SCM+FSA,i st p c= s1 & p c= s2 & i <= 10
     holds
      (Computation s1).i.intloc 0 = (Computation s2).i.intloc 0 &
      (Computation s1).i.IC SCM+FSA = (Computation s2).i.IC SCM+FSA &
      (Computation s1).i.fsloc 0 = (Computation s2).i.fsloc 0
    proof
      let s1,s2 be State of SCM+FSA,i;
      assume A2: p c= s1 & p c=s2 & i <= 10;
      set Cs1=Computation s1, Cs2=Computation s2;
A3:    Cs1.0 = s1 & Cs2.0 = s2 by AMI_1:def 19;
A4:  p starts_at insloc 0 by SCMBSORT:47;
then A5:  s1 starts_at insloc 0 by A2,AMI_3:49;
A6:  s2 starts_at insloc 0 by A2,A4,AMI_3:49;
A7:  q c= s1 & q c=s2 by A2,SCMBSORT:53;

A8:  s1.intloc 0 =1 by A2,SCMBSORT:54
     .= s2.intloc 0 by A2,SCMBSORT:54;
A9:  s1.fsloc 0 =w by A2,SCMBSORT:54
     .=s2.fsloc 0 by A2,SCMBSORT:54;
A10:  IC s1 = insloc 0 by A5,AMI_3:def 14
     .= IC s2 by A6,AMI_3:def 14;
     per cases by A2,SCMBSORT:13;
     suppose A11:i = 0;
       hence Cs1.i.intloc 0 = Cs2.i.intloc 0 by A3,A8;
       thus (Cs1.i).IC SCM+FSA = IC s2 by A3,A10,A11,AMI_1:def 15
       .= (Cs2.i).IC SCM+FSA by A3,A11,AMI_1:def 15;
       thus Cs1.i.fsloc 0 = Cs2.i.fsloc 0 by A3,A9,A11;
     suppose A12:i = 1;
       hence Cs1.i.intloc 0 = s1.intloc 0 by A5,A7,Lm2
          .= Cs2.i.intloc 0 by A6,A7,A8,A12,Lm2;
       thus (Cs1.i).IC SCM+FSA = insloc 1 by A5,A7,A12,Lm2
       .= (Cs2.i).IC SCM+FSA by A6,A7,A12,Lm2;
       thus Cs1.i.fsloc 0 = s1.fsloc 0 by A5,A7,A12,Lm2
          .= Cs2.i.fsloc 0 by A6,A7,A9,A12,Lm2;
     suppose A13:i = 2;
       hence Cs1.i.intloc 0 = s1.intloc 0 by A5,A7,Lm2
          .= Cs2.i.intloc 0 by A6,A7,A8,A13,Lm2;
       thus (Cs1.i).IC SCM+FSA = insloc 2 by A5,A7,A13,Lm2
       .= (Cs2.i).IC SCM+FSA by A6,A7,A13,Lm2;
       thus Cs1.i.fsloc 0 = s1.fsloc 0 by A5,A7,A13,Lm2
          .= Cs2.i.fsloc 0 by A6,A7,A9,A13,Lm2;
     suppose A14:i = 3;
       hence Cs1.i.intloc 0 = s1.intloc 0 by A5,A7,Lm2
          .= Cs2.i.intloc 0 by A6,A7,A8,A14,Lm2;
       thus (Cs1.i).IC SCM+FSA = insloc 3 by A5,A7,A14,Lm2
       .= (Cs2.i).IC SCM+FSA by A6,A7,A14,Lm2;
       thus Cs1.i.fsloc 0 = s1.fsloc 0 by A5,A7,A14,Lm2
          .= Cs2.i.fsloc 0 by A6,A7,A9,A14,Lm2;
     suppose A15:i = 4;
       hence Cs1.i.intloc 0 = s1.intloc 0 by A5,A7,Lm2
          .= Cs2.i.intloc 0 by A6,A7,A8,A15,Lm2;
       thus (Cs1.i).IC SCM+FSA = insloc 4 by A5,A7,A15,Lm2
       .= (Cs2.i).IC SCM+FSA by A6,A7,A15,Lm2;
       thus Cs1.i.fsloc 0 = s1.fsloc 0 by A5,A7,A15,Lm2
          .= Cs2.i.fsloc 0 by A6,A7,A9,A15,Lm2;
     suppose A16:i = 5;
       hence Cs1.i.intloc 0 = s1.intloc 0 by A5,A7,Lm2
          .= Cs2.i.intloc 0 by A6,A7,A8,A16,Lm2;
       thus (Cs1.i).IC SCM+FSA = insloc 5 by A5,A7,A16,Lm2
       .= (Cs2.i).IC SCM+FSA by A6,A7,A16,Lm2;
       thus Cs1.i.fsloc 0 = s1.fsloc 0 by A5,A7,A16,Lm2
          .= Cs2.i.fsloc 0 by A6,A7,A9,A16,Lm2;
    suppose A17:i = 6;
       hence Cs1.i.intloc 0 = s1.intloc 0 by A5,A7,Lm2
          .= Cs2.i.intloc 0 by A6,A7,A8,A17,Lm2;
       thus (Cs1.i).IC SCM+FSA = insloc 6 by A5,A7,A17,Lm2
       .= (Cs2.i).IC SCM+FSA by A6,A7,A17,Lm2;
       thus Cs1.i.fsloc 0 = s1.fsloc 0 by A5,A7,A17,Lm2
          .= Cs2.i.fsloc 0 by A6,A7,A9,A17,Lm2;
    suppose A18:i = 7;
       hence Cs1.i.intloc 0 = s1.intloc 0 by A5,A7,Lm2
          .= Cs2.i.intloc 0 by A6,A7,A8,A18,Lm2;
       thus (Cs1.i).IC SCM+FSA = insloc 7 by A5,A7,A18,Lm2
       .= (Cs2.i).IC SCM+FSA by A6,A7,A18,Lm2;
       thus Cs1.i.fsloc 0 = s1.fsloc 0 by A5,A7,A18,Lm2
          .= Cs2.i.fsloc 0 by A6,A7,A9,A18,Lm2;
    suppose A19:i = 8;
       hence Cs1.i.intloc 0 = s1.intloc 0 by A5,A7,Lm2
          .= Cs2.i.intloc 0 by A6,A7,A8,A19,Lm2;
       thus (Cs1.i).IC SCM+FSA = insloc 8 by A5,A7,A19,Lm2
       .= (Cs2.i).IC SCM+FSA by A6,A7,A19,Lm2;
       thus Cs1.i.fsloc 0 = s1.fsloc 0 by A5,A7,A19,Lm2
          .= Cs2.i.fsloc 0 by A6,A7,A9,A19,Lm2;
    suppose A20:i = 9;
       hence Cs1.i.intloc 0 = s1.intloc 0 by A5,A7,Lm2
          .= Cs2.i.intloc 0 by A6,A7,A8,A20,Lm2;
       thus (Cs1.i).IC SCM+FSA = insloc 9 by A5,A7,A20,Lm2
       .= (Cs2.i).IC SCM+FSA by A6,A7,A20,Lm2;
       thus Cs1.i.fsloc 0 = s1.fsloc 0 by A5,A7,A20,Lm2
          .= Cs2.i.fsloc 0 by A6,A7,A9,A20,Lm2;
    suppose A21:i = 10;
       hence Cs1.i.intloc 0 = s1.intloc 0 by A5,A7,Lm2
          .= Cs2.i.intloc 0 by A6,A7,A8,A21,Lm2;
       thus (Cs1.i).IC SCM+FSA = insloc 10 by A5,A7,A21,Lm2
       .= (Cs2.i).IC SCM+FSA by A6,A7,A21,Lm2;
       thus Cs1.i.fsloc 0 = s1.fsloc 0 by A5,A7,A21,Lm2
          .= Cs2.i.fsloc 0 by A6,A7,A9,A21,Lm2;
   end;
    set UD={fsloc 0,a0,a1,a2,a3,a4,a5,a6},
        Us=UsedInt*Loc q \/ UsedIntLoc q;
A22: UsedInt*Loc q = UsedInt*Loc insert-sort fsloc 0 by Def3
    .={fsloc 0} by Th39;
    A23: UsedIntLoc q = UsedIntLoc insert-sort fsloc 0 by Def3
    .={a0,a1,a2,a3,a4,a5,a6} by Th38;
then A24: Us = UD by A22,ENUMSET1:62;
A25:   for i being Nat,s1,s2 being State of SCM+FSA
       st 11 <= i & p c= s1 & p c= s2
       holds (Computation s1).i | Us = (Computation s2).i | Us &
    (Computation s1).i.IC SCM+FSA = (Computation s2).i.IC SCM+FSA
    proof
     let i be Nat,s1,s2 be State of SCM+FSA such that
A26:  11 <= i and
A27:  p c= s1 and
A28:  p c= s2;
     set Cs11=(Computation s1).11, Cs21=(Computation s2).11;
A29:   p starts_at insloc 0 by SCMBSORT:47;
then A30:   s1 starts_at insloc 0 by A27,AMI_3:49;
A31:   s2 starts_at insloc 0 by A28,A29,AMI_3:49;
A32:   q c= s1 by A27,SCMBSORT:53;
A33:   q c= s2 by A28,SCMBSORT:53;
A34:  s1.intloc 0 =1 by A27,SCMBSORT:54
     .= s2.intloc 0 by A28,SCMBSORT:54;
A35:  s1.fsloc 0 =w by A27,SCMBSORT:54
     .=s2.fsloc 0 by A28,SCMBSORT:54;
A36:   Us c= dom(Cs11) by SCMBSORT:56;
A37:   Us c= dom(Cs21) by SCMBSORT:56;
        now
        let x be set;
        assume x in Us;
        then A38: x in UD by A22,A23,ENUMSET1:62;
      per cases by A38,ENUMSET1:38;
      suppose A39: x = fsloc 0;
        hence Cs11.x =s1.fsloc 0 by A30,A32,Lm2
        .=Cs21.x by A31,A33,A35,A39,Lm2;
      suppose A40: x = a0;
        hence Cs11.x =s1.a0 by A30,A32,Lm2
        .=Cs21.x by A31,A33,A34,A40,Lm2;
      suppose A41: x = a1;
        hence Cs11.x=len(s1.fsloc 0) by A30,A32,Lm2
        .=Cs21.x by A31,A33,A35,A41,Lm2;
      suppose A42: x = a2;
        hence Cs11.x=s1.a0 by A30,A32,Lm2
        .=Cs21.x by A31,A33,A34,A42,Lm2;
      suppose A43: x = a3;
        hence Cs11.x=s1.a0 by A30,A32,Lm2
        .=Cs21.x by A31,A33,A34,A43,Lm2;
      suppose A44: x = a4;
        hence Cs11.x=s1.a0 by A30,A32,Lm2
        .=Cs21.x by A31,A33,A34,A44,Lm2;
      suppose A45: x = a5;
        hence Cs11.x=s1.a0 by A30,A32,Lm2
        .=Cs21.x by A31,A33,A34,A45,Lm2;
      suppose A46: x = a6;
        hence Cs11.x=s1.a0 by A30,A32,Lm2
        .=Cs21.x by A31,A33,A34,A46,Lm2;
     end;
then A47:  Cs11 | Us = Cs21 | Us by A36,A37,SCMFSA6A:9;
A48:  Cs11.IC SCM+FSA = insloc 11 by A30,A32,Lm2
     .=Cs21.IC SCM+FSA by A31,A33,Lm2;
A49:  for i holds IC (Computation s1).i in dom q by A27,Th46;
       for i holds IC (Computation s2).i in dom q by A28,Th46;
     hence thesis by A26,A32,A33,A47,A48,A49,SCMBSORT:26;
   end;
    set DD={intloc 0,IC SCM+FSA,fsloc 0};
A50: dom p = dom q \/ DD by SCMBSORT:42;
      now
      let s1,s2 be State of SCM+FSA,i;
      assume A51: p c= s1 & p c=s2;
      set Cs1i=(Computation s1).i, Cs2i=(Computation s2).i;
        q c= s1 & q c=s2 by A51,SCMBSORT:53;
then A52:   Cs1i | dom q = Cs2i| dom q by SCMBSORT:22;
A53:   DD c= dom Cs1i by SCMBSORT:55;
A54:   DD c= dom Cs2i by SCMBSORT:55;
    Cs1i | DD = Cs2i| DD
      proof
A55:     intloc 0 in Us by A24,ENUMSET1:39;
A56:     fsloc 0 in Us by A24,ENUMSET1:39;
A57:     Us c= dom(Cs1i) by SCMBSORT:56;
A58:     Us c= dom(Cs2i) by SCMBSORT:56;
A59:     i>10 implies 10+1 < i+1 by REAL_1:53;
          now let x be set;
         assume A60: x in DD;
         per cases by A60,ENUMSET1:13;
         suppose A61: x=intloc 0;
              now per cases;
             suppose i<=10;
              hence Cs1i.x=Cs2i.x by A1,A51,A61;
             suppose i>10;
              then 11 <= i by A59,NAT_1:38;
              then Cs1i | Us = Cs2i | Us by A25,A51;
              hence Cs1i.x=Cs2i.x by A55,A57,A58,A61,SCMFSA6A:9;
           end;
           hence Cs1i.x=Cs2i.x;
         suppose A62: x=IC SCM+FSA;
              now per cases;
             suppose i<=10;
              hence Cs1i.x=Cs2i.x by A1,A51,A62;
             suppose i>10;
              then 11 <= i by A59,NAT_1:38;
              hence Cs1i.x=Cs2i.x by A25,A51,A62;
           end;
           hence Cs1i.x=Cs2i.x;
         suppose A63: x=fsloc 0;
              now per cases;
             suppose i<=10;
              hence Cs1i.x=Cs2i.x by A1,A51,A63;
             suppose i>10;
              then 11 <= i by A59,NAT_1:38;
              then Cs1i | Us = Cs2i | Us by A25,A51;
              hence Cs1i.x=Cs2i.x by A56,A57,A58,A63,SCMFSA6A:9;
           end;
           hence Cs1i.x=Cs2i.x;
         end;
         hence thesis by A53,A54,SCMFSA6A:9;
      end;
      hence Cs1i| dom p = Cs2i | dom p by A50,A52,AMI_3:20;
    end;
    then for s1,s2 being State of SCM+FSA st p c= s1 & p c= s2
    for i holds (Computation s1).i|dom p = (Computation s2).i|dom p;
    hence thesis by AMI_1:def 25;
end;

theorem    :: IS026
   Initialized Insert-Sort-Algorithm computes Sorting-Function
proof let x be set;
  assume x in dom Sorting-Function;
     then consider w being FinSequence of INT such that
A1:  x = fsloc 0 .--> w by SCMBSORT:60;
     reconsider s = x as FinPartState of SCM+FSA by A1;
   set p = Initialized Insert-Sort-Algorithm;
A2:  dom s = { fsloc 0 } by A1,CQC_LANG:5;
     take s;
thus x = s;
A3:  p +* s is autonomic by A1,Th48;
A4:  dom p misses dom s by A1,SCMBSORT:46;
     A5: now let t be State of SCM+FSA;
       assume A6:p+*s c= t;
        set bf=insert-sort fsloc 0;
          p c=p+*s by A4,FUNCT_4:33;
        then p c= t by A6,XBOOLE_1:1;
then A7:     Initialized bf c=t by Def3;
          Initialized bf is halting by Th44,SCM_HALT:def 2;
       hence t is halting by A7,AMI_1:def 26;
     end;
     then A8: p +* s is halting by AMI_1:def 26;
   thus
   p +* s is pre-program of SCM+FSA by A1,A5,Th48,AMI_1:def 26;
     consider z being FinSequence of REAL such that
A9:  w,z are_fiberwise_equipotent & z is non-increasing &
     z is FinSequence of INT &
     Sorting-Function.s = fsloc 0 .--> z by A1,SCMBSORT:61;
     consider t being State of SCM+FSA such that
A10:  p +* s c= t by AMI_3:39;
     consider u being FinSequence of REAL such that
A11:  w,u are_fiberwise_equipotent & u is non-increasing &
     u is FinSequence of INT & (Result t).(fsloc 0) = u by A1,A10,Th47;
       u,z are_fiberwise_equipotent by A9,A11,RFINSEQ:2;
then A12:  u=z by A9,A11,RFINSEQ:36;
       fsloc 0 in the carrier of SCM+FSA;
then fsloc 0 in dom Result t by AMI_3:36;
then A13:  Sorting-Function.s c= Result t by A9,A11,A12,AMI_3:27;
       s c= p +* s by FUNCT_4:26;
then A14:  dom s c= dom(p +* s) by RELAT_1:25;
     A15: dom(fsloc 0 .--> z) = { fsloc 0 } by CQC_LANG:5;
       Result(p +* s) = (Result t)|dom(p +* s) by A3,A8,A10,AMI_1:def 28;
 hence Sorting-Function.s c= Result(p +* s) by A2,A9,A13,A14,A15,AMI_3:21;
end;

Back to top