The Mizar article:

The Construction and Shiftability of Program Blocks for SCMPDS

by
Jing-Chao Chen

Received June 15, 1999

Copyright (c) 1999 Association of Mizar Users

MML identifier: SCMPDS_4
[ MML identifier index ]


environ

 vocabulary AMI_3, CAT_1, AMI_1, SCMPDS_2, SCMFSA_7, SCMPDS_3, RELAT_1,
      FINSET_1, FUNCT_1, CARD_1, TARSKI, AMI_5, BOOLE, RELOC, FUNCT_4, INT_1,
      SCMFSA6A, AMI_2, FUNCT_7, SCMPDS_1, ABSVALUE, NAT_1, ARYTM_1, SCMFSA6B,
      FUNCOP_1, SCMPDS_4;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0,
      RELAT_1, FUNCT_1, FUNCT_4, INT_1, NAT_1, CQC_LANG, FINSET_1, STRUCT_0,
      AMI_1, AMI_2, AMI_3, AMI_5, FUNCT_7, SCMPDS_1, SCMPDS_2, GROUP_1,
      SCMFSA_4, SCMPDS_3, CARD_1;
 constructors DOMAIN_1, NAT_1, AMI_5, FUNCT_7, SCMPDS_1, SCMFSA_4, SCMPDS_3,
      WELLORD2, MEMBERED;
 clusters AMI_1, INT_1, FUNCT_1, RELSET_1, XBOOLE_0, SCMPDS_2, FUNCT_7,
      PRELAMB, SCMFSA_4, SCMPDS_3, FRAENKEL, XREAL_0, MEMBERED, NUMBERS,
      ORDINAL2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, AMI_1, AMI_3, SCMPDS_3, FUNCT_7, XBOOLE_0;
 theorems AMI_1, AMI_3, NAT_1, CQC_LANG, TARSKI, FUNCT_4, FUNCT_1, ZFMISC_1,
      INT_1, RELAT_1, AMI_5, SCMPDS_2, AMI_2, FUNCT_2, FUNCT_7, SCMPDS_3,
      CARD_1, PRE_CIRC, WELLORD2, ENUMSET1, SCMFSA_2, CARD_3, ABSVALUE,
      SCMFSA6A, GRFUNC_1, CARD_2, AXIOMS, SCM_1, SCMFSA6B, FINSEQ_1, XBOOLE_0,
      XBOOLE_1, XCMPLX_0, XCMPLX_1;
 schemes NAT_1, DOMAIN_1, FUNCT_7, ZFREFLE1;

begin :: Definition of a program block and its basic properties

definition
  mode Program-block is initial programmed FinPartState of SCMPDS;
end;

reserve l, m, n for Nat,
        i,j,k for Instruction of SCMPDS,
        I,J,K for Program-block;

definition let i;
 func Load i -> Program-block equals
:Def1: (inspos 0).--> i;
 coherence
  proof set I = (inspos 0).--> i;
A1:  dom I = {inspos 0} by CQC_LANG:5;
    reconsider I as finite Function;
    reconsider I as FinPartState of SCMPDS;
      I is initial programmed
     proof
      thus I is initial
       proof let m,n such that
A2:      inspos n in dom I and
A3:      m < n;
           inspos n = inspos 0 by A1,A2,TARSKI:def 1;
         then n = 0 by SCMPDS_3:31;
         hence inspos m in dom I by A3,NAT_1:18;
       end;
      thus dom I c= the Instruction-Locations of SCMPDS
       by A1,ZFMISC_1:37;
     end;
   hence thesis;
  end;
 correctness;
end;

definition let i;
 cluster Load i -> non empty;
 coherence
  proof
      Load i = (inspos 0) .--> i by Def1;
   hence Load i is non empty;
  end;
end;

theorem Th1:  ::SCMFSA6A=SCMPDS_4,Th15
 for P being Program-block, n holds
  n < card P iff inspos n in dom P
 proof let P be Program-block, n;
   deffunc U(Nat) = inspos $1;
   set A = { m : U(m) in dom P};
A1: now let x be set;
    assume
A2:   x in dom P;
       dom P c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
     then consider n such that
A3:    x = inspos n by A2,SCMPDS_3:32;
    take n;
    thus x = U(n) by A3;
   end;
A4: for n,m st U(n) = U(m) holds n = m by SCMPDS_3:31;
A5:  dom P,A are_equipotent from CardMono(A1,A4);
   defpred X[Nat] means U($1) in dom P;
   set A = { m : X[m] };
A6: A is Subset of NAT from SubsetD;
     now let n,m such that
A7: n in A and
A8: m < n;
       ex l st l = n & inspos l in dom P by A7;
     then inspos m in dom P by A8,SCMPDS_3:def 5;
    hence m in A;
   end;
   then reconsider A as Cardinal by A6,FUNCT_7:22;
A9: Card n = n & Card card P = card P by FINSEQ_1:78;
A10: Card A = A by CARD_1:def 5;
  hereby assume n < card P;
    then Card n in Card card P by CARD_1:73;
    then n in card dom P by A9,PRE_CIRC:21;
    then n in Card A by A5,CARD_1:21;
    then ex m st m = n & inspos m in dom P by A10;
   hence inspos n in dom P;
  end;
  assume inspos n in dom P;
   then n in Card A by A10;
   then n in card dom P by A5,CARD_1:21;
   then Card n in Card card P by A9,PRE_CIRC:21;
  hence n < card P by CARD_1:73;
 end;

definition let I be initial FinPartState of SCMPDS;
 cluster ProgramPart I -> initial;
 coherence
  proof let m,n such that
A1: inspos n in dom ProgramPart I and
A2: m < n;
      ProgramPart I c= I by AMI_5:63;
    then dom ProgramPart I c= dom I by RELAT_1:25;
    then inspos m in dom I by A1,A2,SCMPDS_3:def 5;
   hence inspos m in dom ProgramPart I by AMI_5:73;
  end;
end;

theorem Th2:   ::S6A02,Th16
 dom I misses dom Shift(J,card I)
proof
A1:  dom Shift(J,card I) = { inspos(l+card I):inspos l in dom J }
     by SCMPDS_3:def 7;
 assume dom I meets dom Shift(J,card I);
  then consider x being set such that
A2: x in dom I and
A3: x in { inspos(l+card I):inspos l in dom J } by A1,XBOOLE_0:3;
   consider l such that
A4: x = inspos(l+card I) and inspos l in dom J by A3;
    l+card I < card I by A2,A4,Th1;
 hence contradiction by NAT_1:29;
end;

theorem Th3:    :: S6A03,Th17
for I being programmed FinPartState of SCMPDS
 holds card Shift(I,m) = card I
proof let I be programmed FinPartState of SCMPDS;
  set B = { l:inspos l in dom I };
  deffunc U(Nat) = inspos $1;
A1: for x being set st x in dom I ex d being Nat st x = U(d)
     proof let x be set;
A2:     dom I c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
      assume x in dom I;
      hence thesis by A2,SCMPDS_3:32;
     end;
A3: for d1,d2 being Nat st U(d1) = U(d2) holds d1=d2 by SCMPDS_3:31;
  deffunc V(Nat) = inspos($1+m);
  defpred NC[set] means not contradiction;
  defpred X[Nat] means inspos $1 in dom I;
  set B = { l: U(l) in dom I },
      C = { V(l): l in { n: X[n] } & NC[l] },
      D = { V(l): l in B },
      E = { inspos(l+m):inspos l in dom I };
A4: dom I,B are_equipotent from CardMono(A1,A3);
  set B = { l: X[l] };
      B is Subset of NAT from SubsetD;
then A5: B c= NAT;
  set B = { l:inspos l in dom I };
A6: now let d1,d2 be Nat;
     assume V(d1) = V(d2);
      then d1+m = d2+m by SCMPDS_3:31;
     hence d1 = d2 by XCMPLX_1:2;
    end;
A7: C c= E
     proof let e be set;
      assume e in C;
       then consider l such that
A8:     e =V(l) and
A9:     l in { n: X[n] } & NC[l];
       ex n st n=l & X[n] by A9;
      hence e in E by A8;
     end;
A10: E c= D
     proof let e be set;
      assume e in E;
       then consider l such that
A11:     e = inspos(l+m) and
A12:     inspos l in dom I;
       l in B by A12;
      hence e in D by A11;
     end;
A13: D c= C
     proof let e be set;
      assume e in D;
       then ex l st e = V(l) & l in B;
      hence e in C;
     end;
   then E c= C by A10,XBOOLE_1:1;
   then
A14:  C = E by A7,XBOOLE_0:def 10;
   then
A15:  C = D by A10,A13,XBOOLE_0:def 10;
A16: B,D are_equipotent from CardMono'(A5,A6);
    dom Shift(I,m) = E by SCMPDS_3:def 7;
  then A17: dom Shift(I,m),dom I are_equipotent by A4,A14,A15,A16,WELLORD2:22;
 thus card Shift(I,m) = card dom Shift(I,m) by PRE_CIRC:21
      .= card dom I by A17,CARD_1:21
     .= card I by PRE_CIRC:21;
end;

theorem Th4:   :: S6A04,Th20
for I,J being FinPartState of SCMPDS holds
 ProgramPart(I +* J) = ProgramPart I +* ProgramPart J
proof let I,J be FinPartState of SCMPDS;
A1: ProgramPart I = I|the Instruction-Locations of SCMPDS &
   ProgramPart J = J|the Instruction-Locations of SCMPDS
                  by AMI_5:def 6;
 thus ProgramPart(I +* J) = (I +* J)|the Instruction-Locations of SCMPDS
                  by AMI_5:def 6
     .= ProgramPart I +* ProgramPart J by A1,AMI_5:6;
end;

theorem    ::Th21
  for I,J being FinPartState of SCMPDS holds
 Shift(ProgramPart(I +* J),n) =
    Shift(ProgramPart I,n) +* Shift(ProgramPart J,n)
proof let I,J be FinPartState of SCMPDS;
 thus
       Shift(ProgramPart(I +* J),n) = Shift(ProgramPart I +* ProgramPart J,n)
     by Th4
    .= Shift(ProgramPart I,n) +* Shift(ProgramPart J,n) by SCMPDS_3:41;
end;

reserve a,b,c for Int_position,
        s,s1,s2 for State of SCMPDS,
        k1,k2 for Integer;

definition let I;
 func Initialized I -> FinPartState of SCMPDS equals
:Def2: I +* Start-At(inspos 0);
 coherence;
 correctness;
end;

theorem Th6:   ::S6A06,Th23
 InsCode i in {0,1,4,5,6} or Exec(i,s).IC SCMPDS = Next IC s
proof
 assume not InsCode i in {0,1,4,5,6};
  then A1: InsCode i <> 0 & InsCode i <> 1 & InsCode i <> 4 & InsCode i <> 5
    & InsCode i <> 6 by ENUMSET1:24;
A2: InsCode i <= 13 by SCMPDS_2:15;
 per cases by A1,A2,SCMPDS_3:1;
 suppose InsCode i = 2;
  then ex a,k1 st i = a:=k1 by SCMPDS_2:37;
 hence Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:57;
 suppose InsCode i = 3;
  then ex a,k1 st i = saveIC(a,k1) by SCMPDS_2:38;
 hence Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:71;
 suppose InsCode i = 7;
  then ex a,k1,k2 st i = (a,k1) := k2 by SCMPDS_2:42;
 hence Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:58;
 suppose InsCode i = 8;
  then ex a,k1,k2 st i = AddTo(a,k1,k2) by SCMPDS_2:43;
 hence Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:60;
 suppose InsCode i = 9;
  then ex a,b,k1,k2 st i = AddTo(a,k1,b,k2) by SCMPDS_2:44;
  hence Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:61;
 suppose InsCode i = 10;
  then ex a,b,k1,k2 st i = SubFrom(a,k1,b,k2) by SCMPDS_2:45;
 hence Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:62;
 suppose InsCode i = 11;
  then ex a,b,k1,k2 st i = MultBy(a,k1,b,k2) by SCMPDS_2:46;
 hence Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:63;
 suppose InsCode i = 12;
  then ex a,b,k1,k2 st i = Divide(a,k1,b,k2) by SCMPDS_2:47;
 hence Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:64;
 suppose InsCode i = 13;
  then ex a,b,k1,k2 st i = (a,k1):=(b,k2) by SCMPDS_2:48;
 hence Exec(i,s).IC SCMPDS = Next IC s by SCMPDS_2:59;
end;

theorem Th7:   :: Th24 SF_65
 IC SCMPDS in dom Initialized I
proof
A1: dom Initialized I
      = dom(I +* Start-At(inspos 0)) by Def2
     .= dom I \/ dom Start-At(inspos 0)
            by FUNCT_4:def 1;
    dom Start-At(inspos 0) = { IC SCMPDS } by AMI_3:34;
  then IC SCMPDS in dom Start-At(inspos 0) by TARSKI:def 1;
 hence thesis by A1,XBOOLE_0:def 2;
end;

theorem    :: S6A08
   IC Initialized I = inspos 0
proof
    dom Start-At(inspos 0) = { IC SCMPDS } by AMI_3:34;
then A1: IC SCMPDS in dom Start-At(inspos 0) by TARSKI:def 1;
   IC SCMPDS in dom Initialized I by Th7;
 hence IC Initialized I = (Initialized I).IC SCMPDS by AMI_3:def 16
    .= (I +* Start-At(inspos 0)).IC SCMPDS by Def2
    .= (Start-At inspos 0).IC SCMPDS by A1,FUNCT_4:14
    .= inspos 0 by AMI_3:50;
end;

theorem Th9:   :: Th26
 I c= Initialized I
proof set A = the Instruction-Locations of SCMPDS;
A1: Initialized I = I +* Start-At(inspos 0) by Def2;
  dom I c= A by AMI_3:def 13;
then A2: not IC SCMPDS in dom I by AMI_1:48;
      dom Start-At(inspos 0) = { IC SCMPDS } by AMI_3:34;
    then dom I misses dom (Start-At (inspos 0)) by A2,ZFMISC_1:56;
 hence thesis by A1,FUNCT_4:33;
end;

canceled;

theorem Th11:  :: Th28
 for s1,s2 being State of SCMPDS
   st IC s1 = IC s2 & for a being Int_position holds s1.a = s2.a
  holds s1,s2 equal_outside the Instruction-Locations of SCMPDS
proof set A = the Instruction-Locations of SCMPDS;
 let s1,s2 be State of SCMPDS such that
A1: IC s1 = IC s2 and
A2: for a being Int_position holds s1.a = s2.a;
     not IC SCMPDS in A by AMI_1:48;
   then {IC SCMPDS} misses A by ZFMISC_1:56;
then A3: {IC SCMPDS } \/ SCM-Data-Loc misses A by SCMPDS_2:10,XBOOLE_1:70;
A4: (the carrier of SCMPDS) \ A
        = {IC SCMPDS } \/ SCM-Data-Loc \ A by SCMPDS_3:5,XBOOLE_1:40
       .= {IC SCMPDS } \/ SCM-Data-Loc by A3,XBOOLE_1:83;
A5: dom s1 \ A c= dom s1 by XBOOLE_1:36;
A6: dom(s1|(dom s1 \ A)) = dom s1 /\ (dom s1 \ A) by RELAT_1:90
       .= dom s1 \ A by A5,XBOOLE_1:28
       .= {IC SCMPDS } \/ SCM-Data-Loc by A4,AMI_3:36;
A7: dom s2 \ A c= dom s2 by XBOOLE_1:36;
A8: dom(s2|(dom s2 \ A)) = dom s2 /\ (dom s2 \ A) by RELAT_1:90
       .= dom s2 \ A by A7,XBOOLE_1:28
       .= {IC SCMPDS } \/ SCM-Data-Loc by A4,AMI_3:36;
    now let x be set;
   assume
A9:  x in {IC SCMPDS } \/ SCM-Data-Loc;
   per cases by A9,XBOOLE_0:def 2;
   suppose x in {IC SCMPDS};
then A10:  x = IC SCMPDS by TARSKI:def 1;
   thus (s1|(dom s1 \ A)).x = s1.x by A6,A9,FUNCT_1:70
        .= IC s1 by A10,AMI_1:def 15
        .= s2.x by A1,A10,AMI_1:def 15
        .= (s2|(dom s2 \ A)).x by A8,A9,FUNCT_1:70;
   suppose x in SCM-Data-Loc;
then A11: x is Int_position by SCMPDS_2:9;
   thus (s1|(dom s1 \ A)).x = s1.x by A6,A9,FUNCT_1:70
        .= s2.x by A2,A11
        .= (s2|(dom s2 \ A)).x by A8,A9,FUNCT_1:70;
  end;
 hence s1|(dom s1 \ A) = s2|(dom s2 \ A) by A6,A8,FUNCT_1:9;
end;

canceled;

theorem Th13:  :: Th30
 s1,s2 equal_outside the Instruction-Locations of SCMPDS implies
  for a being Int_position holds s1.a = s2.a
proof set IL = the Instruction-Locations of SCMPDS;
 assume
A1: s1,s2 equal_outside IL;
  let a be Int_position;
A2: a in dom s1 by SCMPDS_2:49;
A3: a in dom s2 by SCMPDS_2:49;
      a in SCM-Data-Loc by SCMPDS_2:def 2;
then A4:  not a in IL by SCMPDS_2:10,XBOOLE_0:3;
    then a in dom s1 \ IL by A2,XBOOLE_0:def 4;
then A5: a in dom s1 /\ (dom s1 \ IL) by A2,XBOOLE_0:def 3;
      a in dom s2 \ IL by A3,A4,XBOOLE_0:def 4;
then A6: a in dom s2 /\ (dom s2 \ IL) by A3,XBOOLE_0:def 3;
 thus s1.a = (s1|(dom s1 \ IL)).a by A5,FUNCT_1:71
         .= (s2|(dom s2 \ IL)).a by A1,FUNCT_7:def 2
         .= s2.a by A6,FUNCT_1:71;
end;

theorem Th14:  :: Lm1
    s1,s2 equal_outside the Instruction-Locations of SCMPDS implies
     s1.DataLoc(s1.a,k1)=s2.DataLoc(s2.a,k1)
proof assume
A1: s1,s2 equal_outside the Instruction-Locations of SCMPDS;
    hence s1.DataLoc(s1.a,k1)=s1.DataLoc(s2.a,k1) by Th13
    .=s2.DataLoc(s2.a,k1) by A1,Th13;
end;

theorem Th15:   ::Th32
 s1,s2 equal_outside the Instruction-Locations of SCMPDS implies
  Exec(i,s1),Exec(i,s2) equal_outside the Instruction-Locations of SCMPDS
proof assume
A1: s1,s2 equal_outside the Instruction-Locations of SCMPDS;
A2: InsCode i <= 13 by SCMPDS_2:15;
A3: IC s1 = IC s2 by A1,SCMFSA6A:29;
    per cases by A2,SCMPDS_3:1;
    suppose InsCode i = 0;
    then consider k1 such that
A4:  i = goto k1 by SCMPDS_2:35;
A5:  now let a;
        thus Exec(i, s1).a = s1.a by A4,SCMPDS_2:66
        .=s2.a by A1,Th13
        .=Exec(i, s2).a by A4,SCMPDS_2:66;
     end;
       IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
        .= ICplusConst(s1,k1) by A4,SCMPDS_2:66
        .= ICplusConst(s2,k1) by A3,SCMPDS_3:2
        .= Exec(i,s2).IC SCMPDS by A4,SCMPDS_2:66
        .= IC Exec(i,s2) by AMI_1:def 15;
      hence Exec(i,s1),Exec(i,s2)
      equal_outside the Instruction-Locations of SCMPDS by A5,Th11;

    suppose InsCode i = 1;
    then consider a such that
A6:   i = return a by SCMPDS_2:36;
A7: now let b;
         per cases;
         suppose A8:a=b;
          hence Exec(i, s1).b= s1.DataLoc(s1.a,RetSP) by A6,SCMPDS_2:70
          .=s2.DataLoc(s2.a,RetSP) by A1,Th14
          .=Exec(i,s2).b by A6,A8,SCMPDS_2:70;
         suppose A9:a<>b;
          hence Exec(i, s1).b = s1.b by A6,SCMPDS_2:70
          .=s2.b by A1,Th13
          .=Exec(i,s2).b by A6,A9,SCMPDS_2:70;
      end;
        IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
        .= 2*(abs(s1.DataLoc(s1.a,RetIC)) div 2)+4 by A6,SCMPDS_2:70
        .= 2*(abs(s1.DataLoc(s2.a,RetIC)) div 2)+4 by A1,Th13
        .= 2*(abs(s2.DataLoc(s2.a,RetIC)) div 2)+4 by A1,Th13
        .= Exec(i,s2).IC SCMPDS by A6,SCMPDS_2:70
        .= IC Exec(i,s2) by AMI_1:def 15;
         hence thesis by A7,Th11;

    suppose InsCode i = 2;
    then consider a,k1 such that
A10:   i = a := k1 by SCMPDS_2:37;
A11:  now let b;
         per cases;
         suppose A12:a=b;
          hence Exec(i, s1).b= k1 by A10,SCMPDS_2:57
          .=Exec(i,s2).b by A10,A12,SCMPDS_2:57;
         suppose A13:a<>b;
          hence Exec(i,s1).b = s1.b by A10,SCMPDS_2:57
          .=s2.b by A1,Th13
          .=Exec(i,s2).b by A10,A13,SCMPDS_2:57;
     end;
        IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
        .= Next IC s2 by A3,A10,SCMPDS_2:57
        .= Exec(i,s2).IC SCMPDS by A10,SCMPDS_2:57
        .= IC Exec(i,s2) by AMI_1:def 15;
      hence thesis by A11,Th11;

    suppose InsCode i = 3;
    then consider a,k1 such that
A14:   i = saveIC(a,k1) by SCMPDS_2:38;
A15:  now let b;
         per cases;
         suppose A16:b=DataLoc(s1.a,k1);
          then A17:b=DataLoc(s2.a,k1) by A1,Th13;
          thus Exec(i, s1).b=IC s2 by A3,A14,A16,SCMPDS_2:71
          .=Exec(i,s2).b by A14,A17,SCMPDS_2:71;
         suppose A18:b<>DataLoc(s1.a,k1);
          then A19:b<>DataLoc(s2.a,k1) by A1,Th13;
          thus Exec(i,s1).b = s1.b by A14,A18,SCMPDS_2:71
          .=s2.b by A1,Th13
          .=Exec(i,s2).b by A14,A19,SCMPDS_2:71;
       end;
        IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
        .= Next IC s2 by A3,A14,SCMPDS_2:71
        .= Exec(i,s2).IC SCMPDS by A14,SCMPDS_2:71
        .= IC Exec(i,s2) by AMI_1:def 15;
      hence thesis by A15,Th11;

    suppose InsCode i = 4;
    then consider a,k1,k2 such that
A20:   i = (a,k1)<>0_goto k2 by SCMPDS_2:39;
A21:  now let a;
        thus Exec(i, s1).a = s1.a by A20,SCMPDS_2:67
        .=s2.a by A1,Th13
        .=Exec(i, s2).a by A20,SCMPDS_2:67;
     end;
       now
        per cases;
        suppose A22: s1.DataLoc(s1.a,k1) <> 0;
         then A23: s2.DataLoc(s2.a,k1) <> 0 by A1,Th14;
       thus IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
        .= ICplusConst(s1,k2) by A20,A22,SCMPDS_2:67
        .= ICplusConst(s2,k2) by A3,SCMPDS_3:2
        .= Exec(i,s2).IC SCMPDS by A20,A23,SCMPDS_2:67
        .= IC Exec(i,s2) by AMI_1:def 15;
        suppose A24: s1.DataLoc(s1.a,k1) = 0;
         then A25: s2.DataLoc(s2.a,k1) = 0 by A1,Th14;
       thus IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
        .= Next IC s2 by A3,A20,A24,SCMPDS_2:67
        .= Exec(i,s2).IC SCMPDS by A20,A25,SCMPDS_2:67
        .= IC Exec(i,s2) by AMI_1:def 15;
     end;
     hence thesis by A21,Th11;

    suppose InsCode i = 5;
    then consider a,k1,k2 such that
A26:   i = (a,k1)<=0_goto k2 by SCMPDS_2:40;
A27:  now let a;
        thus Exec(i, s1).a = s1.a by A26,SCMPDS_2:68
        .=s2.a by A1,Th13
        .=Exec(i, s2).a by A26,SCMPDS_2:68;
     end;
       now
        per cases;
        suppose A28: s1.DataLoc(s1.a,k1) <= 0;
         then A29: s2.DataLoc(s2.a,k1) <= 0 by A1,Th14;
       thus IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
        .= ICplusConst(s1,k2) by A26,A28,SCMPDS_2:68
        .= ICplusConst(s2,k2) by A3,SCMPDS_3:2
        .= Exec(i,s2).IC SCMPDS by A26,A29,SCMPDS_2:68
        .= IC Exec(i,s2) by AMI_1:def 15;
        suppose A30: s1.DataLoc(s1.a,k1) > 0;
         then A31: s2.DataLoc(s2.a,k1) > 0 by A1,Th14;
       thus IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
        .= Next IC s2 by A3,A26,A30,SCMPDS_2:68
        .= Exec(i,s2).IC SCMPDS by A26,A31,SCMPDS_2:68
        .= IC Exec(i,s2) by AMI_1:def 15;
     end;
     hence thesis by A27,Th11;

    suppose InsCode i = 6;
    then consider a,k1,k2 such that
A32:   i = (a,k1)>=0_goto k2 by SCMPDS_2:41;
A33:  now let a;
        thus Exec(i, s1).a = s1.a by A32,SCMPDS_2:69
        .=s2.a by A1,Th13
        .=Exec(i, s2).a by A32,SCMPDS_2:69;
     end;
       now
        per cases;
        suppose A34: s1.DataLoc(s1.a,k1) >= 0;
         then A35: s2.DataLoc(s2.a,k1) >= 0 by A1,Th14;
       thus IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
        .= ICplusConst(s1,k2) by A32,A34,SCMPDS_2:69
        .= ICplusConst(s2,k2) by A3,SCMPDS_3:2
        .= Exec(i,s2).IC SCMPDS by A32,A35,SCMPDS_2:69
        .= IC Exec(i,s2) by AMI_1:def 15;
        suppose A36: s1.DataLoc(s1.a,k1) < 0;
         then A37: s2.DataLoc(s2.a,k1) < 0 by A1,Th14;
       thus IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
        .= Next IC s2 by A3,A32,A36,SCMPDS_2:69
        .= Exec(i,s2).IC SCMPDS by A32,A37,SCMPDS_2:69
        .= IC Exec(i,s2) by AMI_1:def 15;
     end;
     hence thesis by A33,Th11;

    suppose InsCode i = 7;
    then consider a,k1,k2 such that
A38:   i = (a,k1) := k2 by SCMPDS_2:42;
A39:  now let b;
         per cases;
         suppose A40:DataLoc(s1.a,k1)=b;
         then A41: DataLoc(s2.a,k1)=b by A1,Th13;
          thus Exec(i, s1).b= k2 by A38,A40,SCMPDS_2:58
          .=Exec(i,s2).b by A38,A41,SCMPDS_2:58;
         suppose A42:DataLoc(s1.a,k1)<>b;
         then A43: DataLoc(s2.a,k1)<>b by A1,Th13;
          thus Exec(i,s1).b = s1.b by A38,A42,SCMPDS_2:58
          .=s2.b by A1,Th13
          .=Exec(i,s2).b by A38,A43,SCMPDS_2:58;
     end;
        IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
        .= Next IC s2 by A3,A38,SCMPDS_2:58
        .= Exec(i,s2).IC SCMPDS by A38,SCMPDS_2:58
        .= IC Exec(i,s2) by AMI_1:def 15;
      hence thesis by A39,Th11;

    suppose InsCode i = 8;
    then consider a,k1,k2 such that
A44:   i = AddTo(a,k1,k2) by SCMPDS_2:43;
A45:  now let b;
         per cases;
         suppose A46:DataLoc(s1.a,k1)=b;
         then A47: DataLoc(s2.a,k1)=b by A1,Th13;
          thus Exec(i, s1).b= s1.DataLoc(s1.a,k1)+k2 by A44,A46,SCMPDS_2:60
          .= s2.DataLoc(s2.a,k1)+k2 by A1,Th14
          .=Exec(i,s2).b by A44,A47,SCMPDS_2:60;
         suppose A48:DataLoc(s1.a,k1)<>b;
         then A49: DataLoc(s2.a,k1)<>b by A1,Th13;
          thus Exec(i,s1).b = s1.b by A44,A48,SCMPDS_2:60
          .=s2.b by A1,Th13
          .=Exec(i,s2).b by A44,A49,SCMPDS_2:60;
     end;
        IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
        .= Next IC s2 by A3,A44,SCMPDS_2:60
        .= Exec(i,s2).IC SCMPDS by A44,SCMPDS_2:60
        .= IC Exec(i,s2) by AMI_1:def 15;
      hence thesis by A45,Th11;

    suppose InsCode i = 9;
    then consider a,b,k1,k2 such that
A50:   i = AddTo(a,k1,b,k2) by SCMPDS_2:44;
A51:  now let c;
         per cases;
         suppose A52:DataLoc(s1.a,k1)=c;
         then A53: DataLoc(s2.a,k1)=c by A1,Th13;
          thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)+s1.DataLoc(s1.b,k2)
             by A50,A52,SCMPDS_2:61
          .= s2.DataLoc(s2.a,k1)+s1.DataLoc(s1.b,k2) by A1,Th14
          .= s2.DataLoc(s2.a,k1)+s2.DataLoc(s2.b,k2) by A1,Th14
          .=Exec(i,s2).c by A50,A53,SCMPDS_2:61;
         suppose A54:DataLoc(s1.a,k1)<>c;
         then A55: DataLoc(s2.a,k1)<>c by A1,Th13;
          thus Exec(i,s1).c = s1.c by A50,A54,SCMPDS_2:61
          .=s2.c by A1,Th13
          .=Exec(i,s2).c by A50,A55,SCMPDS_2:61;
     end;
        IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
        .= Next IC s2 by A3,A50,SCMPDS_2:61
        .= Exec(i,s2).IC SCMPDS by A50,SCMPDS_2:61
        .= IC Exec(i,s2) by AMI_1:def 15;
      hence thesis by A51,Th11;

    suppose InsCode i = 10;
    then consider a,b,k1,k2 such that
A56:   i = SubFrom(a,k1,b,k2) by SCMPDS_2:45;
A57:  now let c;
         per cases;
         suppose A58:DataLoc(s1.a,k1)=c;
         then A59: DataLoc(s2.a,k1)=c by A1,Th13;
          thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)-s1.DataLoc(s1.b,k2)
             by A56,A58,SCMPDS_2:62
          .= s2.DataLoc(s2.a,k1)-s1.DataLoc(s1.b,k2) by A1,Th14
          .= s2.DataLoc(s2.a,k1)-s2.DataLoc(s2.b,k2) by A1,Th14
          .=Exec(i,s2).c by A56,A59,SCMPDS_2:62;
         suppose A60:DataLoc(s1.a,k1)<>c;
         then A61: DataLoc(s2.a,k1)<>c by A1,Th13;
          thus Exec(i,s1).c = s1.c by A56,A60,SCMPDS_2:62
          .=s2.c by A1,Th13
          .=Exec(i,s2).c by A56,A61,SCMPDS_2:62;
     end;
        IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
        .= Next IC s2 by A3,A56,SCMPDS_2:62
        .= Exec(i,s2).IC SCMPDS by A56,SCMPDS_2:62
        .= IC Exec(i,s2) by AMI_1:def 15;
      hence thesis by A57,Th11;

    suppose InsCode i = 11;
    then consider a,b,k1,k2 such that
A62:   i = MultBy(a,k1,b,k2) by SCMPDS_2:46;
A63:  now let c;
         per cases;
         suppose A64:DataLoc(s1.a,k1)=c;
         then A65: DataLoc(s2.a,k1)=c by A1,Th13;
          thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)*s1.DataLoc(s1.b,k2)
             by A62,A64,SCMPDS_2:63
          .= s2.DataLoc(s2.a,k1)*s1.DataLoc(s1.b,k2) by A1,Th14
          .= s2.DataLoc(s2.a,k1)*s2.DataLoc(s2.b,k2) by A1,Th14
          .=Exec(i,s2).c by A62,A65,SCMPDS_2:63;
         suppose A66:DataLoc(s1.a,k1)<>c;
         then A67: DataLoc(s2.a,k1)<>c by A1,Th13;
          thus Exec(i,s1).c = s1.c by A62,A66,SCMPDS_2:63
          .=s2.c by A1,Th13
          .=Exec(i,s2).c by A62,A67,SCMPDS_2:63;
     end;
        IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
        .= Next IC s2 by A3,A62,SCMPDS_2:63
        .= Exec(i,s2).IC SCMPDS by A62,SCMPDS_2:63
        .= IC Exec(i,s2) by AMI_1:def 15;
      hence thesis by A63,Th11;

    suppose InsCode i = 12;
    then consider a,b,k1,k2 such that
A68:   i = Divide(a,k1,b,k2) by SCMPDS_2:47;
A69:  now let c;
         per cases;
         suppose A70:DataLoc(s1.b,k2)=c;
         then A71: DataLoc(s2.b,k2)=c by A1,Th13;
          thus Exec(i, s1).c = s1.DataLoc(s1.a,k1) mod s1.DataLoc(s1.b,k2)
             by A68,A70,SCMPDS_2:64
          .= s2.DataLoc(s2.a,k1) mod s1.DataLoc(s1.b,k2) by A1,Th14
          .= s2.DataLoc(s2.a,k1) mod s2.DataLoc(s2.b,k2) by A1,Th14
          .= Exec(i,s2).c by A68,A71,SCMPDS_2:64;
         suppose A72:DataLoc(s1.b,k2)<>c;
         then A73: DataLoc(s2.b,k2)<>c by A1,Th13;
           hereby
             per cases;
             suppose A74:DataLoc(s1.a,k1)<>c;
             then A75: DataLoc(s2.a,k1)<>c by A1,Th13;
            thus Exec(i, s1).c = s1.c by A68,A72,A74,SCMPDS_2:64
                .=s2.c by A1,Th13
                .=Exec(i,s2).c by A68,A73,A75,SCMPDS_2:64;
             suppose A76:DataLoc(s1.a,k1)=c;
              then A77: DataLoc(s2.a,k1)=c by A1,Th13;
             thus Exec(i, s1).c = s1.DataLoc(s1.a,k1) div s1.DataLoc(s1.b,k2)
               by A68,A72,A76,SCMPDS_2:64
             .= s2.DataLoc(s2.a,k1) div s1.DataLoc(s1.b,k2) by A1,Th14
             .= s2.DataLoc(s2.a,k1) div s2.DataLoc(s2.b,k2) by A1,Th14
             .= Exec(i,s2).c by A68,A73,A77,SCMPDS_2:64;
           end;
     end;
        IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
        .= Next IC s2 by A3,A68,SCMPDS_2:64
        .= Exec(i,s2).IC SCMPDS by A68,SCMPDS_2:64
        .= IC Exec(i,s2) by AMI_1:def 15;
      hence thesis by A69,Th11;

    suppose InsCode i = 13;
    then consider a,b,k1,k2 such that
A78:   i = (a,k1):=(b,k2) by SCMPDS_2:48;
A79:  now let c;
         per cases;
         suppose A80:DataLoc(s1.a,k1)=c;
         then A81: DataLoc(s2.a,k1)=c by A1,Th13;
          thus Exec(i, s1).c = s1.DataLoc(s1.b,k2) by A78,A80,SCMPDS_2:59
          .= s2.DataLoc(s2.b,k2) by A1,Th14
          .=Exec(i,s2).c by A78,A81,SCMPDS_2:59;
         suppose A82:DataLoc(s1.a,k1)<>c;
         then A83: DataLoc(s2.a,k1)<>c by A1,Th13;
          thus Exec(i,s1).c = s1.c by A78,A82,SCMPDS_2:59
          .=s2.c by A1,Th13
          .=Exec(i,s2).c by A78,A83,SCMPDS_2:59;
     end;
        IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
        .= Next IC s2 by A3,A78,SCMPDS_2:59
        .= Exec(i,s2).IC SCMPDS by A78,SCMPDS_2:59
        .= IC Exec(i,s2) by AMI_1:def 15;
      hence thesis by A79,Th11;
end;

theorem
   (Initialized I)|the Instruction-Locations of SCMPDS = I
proof
A1: Initialized I = I +* Start-At(inspos 0) by Def2;
A2: dom I c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
A3: not IC SCMPDS in the Instruction-Locations of SCMPDS by AMI_1:48;
     dom Start-At(inspos 0) = { IC SCMPDS } by AMI_3:34;
 then dom Start-At(inspos 0) misses the Instruction-Locations of SCMPDS
       by A3,ZFMISC_1:56;
 hence (Initialized I)|the Instruction-Locations of SCMPDS = I
      by A1,A2,AMI_5:13;
end;

theorem Th17:   :: SF2_16
 for k1,k2 be Nat st k1 <> k2 holds DataLoc(k1,0) <> DataLoc(k2,0)
 proof let k1,k2 be Nat;
   assume A1:k1<>k2;
   assume A2:DataLoc(k1,0) = DataLoc(k2,0);
A3: k1 >= 0 & k2 >= 0 by NAT_1:18;
     DataLoc(k1,0)= 2*abs(k1+0)+1 & DataLoc(k2,0)= 2*abs(k2+0)+1
   by SCMPDS_2:def 4;
   then 2*abs(k1)=2*abs(k2) by A2,XCMPLX_1:2;
   then abs(k1)=abs(k2) by XCMPLX_1:5;
   then k1=abs(k2) by A3,ABSVALUE:def 1;
   hence contradiction by A1,A3,ABSVALUE:def 1;
 end;

theorem Th18:  :: SF2_19:
 for dl being Int_position ex i being Nat
  st dl = DataLoc(i,0)
 proof
  let dl be Int_position;
      dl in SCM-Data-Loc by SCMPDS_2:def 2;
   then consider i being Nat such that
A1: dl = 2*i+1 by AMI_2:def 2;
   take i;
     i >= 0 by NAT_1:18;
   hence dl =2*abs(i+0)+1 by A1,ABSVALUE:def 1
    .=DataLoc(i,0) by SCMPDS_2:def 4;
end;

scheme SCMPDSEx{ F(set) -> Instruction of SCMPDS,
                 G(set) -> Integer,
                 I() -> Instruction-Location of SCMPDS }:
 ex S being State of SCMPDS st IC S = I() &
  for i being Nat holds
    S.inspos i = F(i) & S.DataLoc(i,0) = G(i)
proof
 defpred P[set,set] means ex m st
   $1 = IC SCMPDS & $2 = I() or
   $1 = inspos m & $2 = F(m) or
   $1 = DataLoc(m,0) & $2 = G(m);
  set S1={IC SCMPDS },
      S2=SCM-Data-Loc,
      S3=the Instruction-Locations of SCMPDS;
A1: for e being set st e in the carrier of SCMPDS
     ex u being set st P[e,u]
   proof let e be set;
    assume e in the carrier of SCMPDS;
    then A2: e in S1 \/ S2 or e in S3 by SCMPDS_3:5,XBOOLE_0:def 2;
       now per cases by A2,XBOOLE_0:def 2;
      case e in S1;
       hence e = IC SCMPDS by TARSKI:def 1;
      case e in S2;
        then e is Int_position by SCMPDS_2:9;
        hence ex m st e = DataLoc(m,0) by Th18;
      case e in S3;
       hence ex m st e = inspos m by SCMPDS_3:32;
     end;
     then consider m such that
A3:  e = IC SCMPDS or e = inspos m or e = DataLoc(m,0);
    per cases by A3;
    suppose
A4:   e = IC SCMPDS;
     take u = I(); thus P[e,u] by A4;
    suppose
A5:   e = inspos m;
     take u = F(m); thus P[e,u] by A5;
    suppose
A6:   e = DataLoc(m,0);
     take u = G(m); thus P[e,u] by A6;
   end;
  consider f being Function such that
A7: dom f = the carrier of SCMPDS and
A8: for e being set st e in the carrier of SCMPDS holds P[e,f.e]
                         from NonUniqFuncEx(A1);
A9: dom the Object-Kind of SCMPDS = the carrier of SCMPDS by FUNCT_2:def 1;
    now let x be set;
   assume
A10: x in dom the Object-Kind of SCMPDS;
     then A11: x in S1 \/ S2 or x in S3 by A9,SCMPDS_3:5,XBOOLE_0:def 2;
   consider m such that
A12: x = IC SCMPDS & f.x = I() or
    x = inspos m & f.x = F(m) or
    x = DataLoc(m,0) & f.x = G(m) by A8,A9,A10;
   per cases by A11,XBOOLE_0:def 2;
    suppose x in S2;
     then A13: x is Int_position by SCMPDS_2:9;
    then (the Object-Kind of SCMPDS).x = ObjectKind DataLoc(m,0) by A12,AMI_1:
def 6,SCMPDS_2:52,53
        .= INT by SCMPDS_2:13;
   hence f.x in (the Object-Kind of SCMPDS).x by A12,A13,INT_1:12,SCMPDS_2:52,
53;
    suppose x in S1;
then A14:    x = IC SCMPDS by TARSKI:def 1;
    then (the Object-Kind of SCMPDS).x = ObjectKind IC SCMPDS by AMI_1:def 6
       .= the Instruction-Locations of SCMPDS by AMI_1:def 11;
   hence f.x in (the Object-Kind of SCMPDS).x by A12,A14,AMI_1:48,SCMPDS_2:52;
    suppose A15: x in the Instruction-Locations of SCMPDS;
    then (the Object-Kind of SCMPDS).x = ObjectKind inspos m by A12,AMI_1:48,
def 6,SCMPDS_2:53
        .= the Instructions of SCMPDS by AMI_1:def 14;
   hence f.x in (the Object-Kind of SCMPDS).x by A12,A15,AMI_1:48,SCMPDS_2:53;
  end;
  then reconsider f as State of SCMPDS by A7,A9,CARD_3:18;
 take f;
  consider m such that
A16: IC SCMPDS = IC SCMPDS & f.IC SCMPDS = I() or
    IC SCMPDS = inspos m & f.IC SCMPDS = F(m) or
    IC SCMPDS = DataLoc(m,0) & f.IC SCMPDS = G(m) by A8;
 thus IC f = I() by A16,AMI_1:48,def 15,SCMPDS_2:52;
 let i be Nat;
  consider m such that
A17: inspos i = IC SCMPDS & f.inspos i = I() or
    inspos i = inspos m & f.inspos i = F(m) or
    inspos i = DataLoc(m,0) & f.inspos i = G(m) by A8;
  thus f.inspos i = F(i) by A17,AMI_1:48,SCMPDS_2:53,SCMPDS_3:31;
  consider m such that
A18: DataLoc(i,0) = IC SCMPDS & f.DataLoc(i,0) = I() or
    DataLoc(i,0) = inspos m & f.DataLoc(i,0) = F(m) or
    DataLoc(i,0) = DataLoc(m,0) & f.DataLoc(i,0) = G(m) by A8;
 thus f.DataLoc(i,0) = G(i) by A18,Th17,SCMPDS_2:52,53;
end;

theorem    :: Th34
  for s being State of SCMPDS holds
     dom s = {IC SCMPDS} \/ SCM-Data-Loc \/
         the Instruction-Locations of SCMPDS by AMI_3:36,SCMPDS_3:5;

theorem    :: T12'
   for s being State of SCMPDS, x being set st x in dom s holds
     x is Int_position or x = IC SCMPDS or
     x is Instruction-Location of SCMPDS
 proof
   let s be State of SCMPDS;
   let x be set;
   set S1={IC SCMPDS},
       S2=SCM-Data-Loc,
       S3=the Instruction-Locations of SCMPDS;
A1:dom s = S1 \/ S2 \/ S3 by AMI_3:36,SCMPDS_3:5;
   assume x in dom s;
   then x in S1 \/ S2 or x in S3 by A1,XBOOLE_0:def 2;
   then x in S1 or x in S2 or x in S3 by XBOOLE_0:def 2;
   hence thesis by SCMPDS_2:9,TARSKI:def 1;
end;

theorem     :: T29
   for s1,s2 being State of SCMPDS holds
     (for l being Instruction-Location of SCMPDS holds s1.l = s2.l)
 iff s1 | the Instruction-Locations of SCMPDS =
     s2 | the Instruction-Locations of SCMPDS
 proof
   let s1,s2 be State of SCMPDS;
A1: the Instruction-Locations of SCMPDS c= dom s1 by SCMFSA_2:3;
A2: the Instruction-Locations of SCMPDS c= dom s2 by SCMFSA_2:3;
     (for l being Instruction-Location of SCMPDS holds s1.l = s2.l) iff
   (for l being set st l in the Instruction-Locations of SCMPDS
       holds s1.l = s2.l);
   hence thesis by A1,A2,SCMFSA6A:9;
end;

theorem  :: T32
   for i being Instruction-Location of SCMPDS holds
     not i in SCM-Data-Loc
by SCMPDS_2:10,XBOOLE_0:3;

theorem Th23:    :: Th38
 for s1,s2 being State of SCMPDS holds
     (for a being Int_position holds s1.a = s2.a)
 iff s1 | SCM-Data-Loc = s2 | SCM-Data-Loc
 proof
   let s1,s2 be State of SCMPDS;
   set T1={IC SCMPDS},
       T2=SCM-Data-Loc,
       T3=the Instruction-Locations of SCMPDS;
A1: T1 \/ T2 \/ T3=T2 \/ (T1 \/ T3) by XBOOLE_1:4;
     dom s1 = T1 \/ T2 \/ T3 by AMI_3:36,SCMPDS_3:5;
then A2: T2 c= dom s1 by A1,XBOOLE_1:7;
     dom s2 = T1 \/ T2 \/ T3 by AMI_3:36,SCMPDS_3:5;
then A3: T2 c= dom s2 by A1,XBOOLE_1:7;
A4: now
      assume A5:for a being Int_position holds s1.a = s2.a;
      hereby let x be set;
       assume x in SCM-Data-Loc;
       then x is Int_position by SCMPDS_2:9;
       hence s1.x=s2.x by A5;
     end;
    end;
     now
      assume A6:for x be set st x in SCM-Data-Loc holds s1.x = s2.x;
      hereby let a be Int_position;
         a in SCM-Data-Loc by SCMPDS_2:def 2;
       hence s1.a=s2.a by A6;
      end;
   end;
   hence thesis by A2,A3,A4,SCMFSA6A:9;
end;

theorem     :: T19
   for s1,s2 being State of SCMPDS st
     s1,s2 equal_outside the Instruction-Locations of SCMPDS holds
     s1 | SCM-Data-Loc = s2 | SCM-Data-Loc
 proof
   let s1,s2 be State of SCMPDS;
   assume s1,s2 equal_outside the Instruction-Locations of SCMPDS;
 then for a being Int_position holds s1.a = s2.a by Th13;
    hence thesis by Th23;
end;

theorem     :: T21
   for s,ss being State of SCMPDS, A being set holds
     (ss +* s | A) | A = s | A
 proof
   let s,ss be State of SCMPDS;
   let A be set;
A1: dom s = the carrier of SCMPDS by AMI_3:36;
A2: dom (ss +* s | A) = dom ss \/ dom (s | A) by FUNCT_4:def 1
   .= dom ss \/ (dom s /\ A) by RELAT_1:90
   .= (the carrier of SCMPDS) \/ (the carrier of SCMPDS) /\ A by A1,AMI_3:36
   .= the carrier of SCMPDS by XBOOLE_1:22;
A3: dom s /\ A c= dom s by XBOOLE_1:17;
A4: now let x be set;
      assume A5: x in dom s /\ A;
      then x in dom (s | A) by RELAT_1:90;
      hence (ss +* s | A).x = (s | A).x by FUNCT_4:14
      .= s.x by A5,FUNCT_1:71;
     end;
   thus (ss +* s | A) | A
    = (ss +* s | A) | (dom s /\ A) by A1,A2,SCMFSA6A:10
   .= s | (dom s /\ A) by A1,A2,A3,A4,SCMFSA6A:9
   .= s | A by SCMFSA6A:10;
 end;

theorem    :: T18
   for I,J being Program-block holds
     I,J equal_outside the Instruction-Locations of SCMPDS
 proof
   let I,J be Program-block;
     dom I c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
   then dom I \ the Instruction-Locations of SCMPDS = {} by XBOOLE_1:37;
then A1: dom (I | (dom I \ the Instruction-Locations of SCMPDS)) = {} by
SCMFSA6A:8;
     dom J c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
   then dom J \ the Instruction-Locations of SCMPDS = {} by XBOOLE_1:37;
then A2: dom (J | (dom J \ the Instruction-Locations of SCMPDS)) = {} by
SCMFSA6A:8;
     for x be set st x in {} holds
      (I | (dom I \ the Instruction-Locations of SCMPDS)).x =
          (J | (dom J \ the Instruction-Locations of SCMPDS)).x;
   then I | (dom I \ the Instruction-Locations of SCMPDS) =
       J | (dom J \ the Instruction-Locations of SCMPDS) by A1,A2,FUNCT_1:9;
   hence I,J equal_outside the Instruction-Locations of SCMPDS
       by FUNCT_7:def 2;
end;

theorem Th27:   :: Th43
 for I being Program-block holds
     dom Initialized I = dom I \/ {IC SCMPDS}
proof
   let I be Program-block;
   thus dom Initialized I
    = dom(I +* Start-At(inspos 0)) by Def2
   .= dom I \/ dom Start-At(inspos 0) by FUNCT_4:def 1
   .= dom I \/ {IC SCMPDS} by AMI_3:34;
end;

theorem Th28:   :: Th44
 for I being Program-block, x being set st x in dom Initialized I holds
     x in dom I or x = IC SCMPDS
proof
   let I be Program-block;
   let x be set;
A1: dom Initialized I = dom I \/ {IC SCMPDS} by Th27;
   assume x in dom Initialized I;
   then x in dom I or x in {IC SCMPDS} by A1,XBOOLE_0:def 2;
   hence x in dom I or x = IC SCMPDS by TARSKI:def 1;
end;

theorem Th29:    :: Th46
 for I being Program-block holds
     (Initialized I).IC SCMPDS = inspos 0
proof
   let I be Program-block;
      IC SCMPDS in {IC SCMPDS} by TARSKI:def 1;
then A1: IC SCMPDS in dom Start-At inspos 0 by AMI_3:34;
   thus (Initialized I).IC SCMPDS
    = (I +* (Start-At (inspos 0))).IC SCMPDS by Def2
   .= (Start-At (inspos 0)).IC SCMPDS by A1,FUNCT_4:14
   .= (IC SCMPDS .--> inspos 0).IC SCMPDS by AMI_3:def 12
   .= inspos 0 by CQC_LANG:6;
end;

theorem Th30:  :: Th47
  for I being Program-block holds not IC SCMPDS in dom I
proof
   let I be Program-block;
   dom I c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
   hence not IC SCMPDS in dom I by AMI_1:48;
end;

theorem Th31:  :: Th48
 for I being Program-block, a being Int_position holds
     not a in dom Initialized I
proof
   let I be Program-block;
   let a be Int_position;
   assume a in dom Initialized I;
   then A1: a in dom I \/ {IC SCMPDS} by Th27;
   per cases by A1,XBOOLE_0:def 2;
   suppose A2: a in dom I;
      dom I c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
    hence contradiction by A2,SCMPDS_2:53;
   suppose a in {IC SCMPDS};
    then a = IC SCMPDS by TARSKI:def 1;
    hence contradiction by SCMPDS_2:52;
end;

reserve x for set;

theorem Th32:   ::TN32
 x in dom I implies I.x = (I +* Start-At inspos n).x
proof assume
A1: x in dom I;
   A2: dom I c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
A3: dom Start-At inspos n = {IC SCMPDS} by AMI_3:34;
     x <> IC SCMPDS by A1,A2,AMI_1:48;
   then not x in dom Start-At inspos n by A3,TARSKI:def 1;
 hence thesis by FUNCT_4:12;
end;

theorem Th33:  :: Th50
 for I being Program-block, x being set st x in dom I holds
     I.x = (Initialized I).x
proof
   let I be Program-block, x be set;
   assume A1: x in dom I;
   thus (Initialized I).x
    = (I +* Start-At(inspos 0)).x by Def2
   .= I.x by A1,Th32;
end;

theorem Th34:   :: Th51
 for I,J being Program-block
 for s being State of SCMPDS st Initialized J c= s holds
     s +* Initialized I = s +* I
 proof
   let I,J be Program-block;
   let s be State of SCMPDS;
   set s1 = s +* I;
   assume A1: Initialized J c= s;
then A2: dom Initialized J c= dom s by GRFUNC_1:8;
     dom J \/ dom Initialized I
    = dom J \/ (dom I \/ {IC SCMPDS}) by Th27
   .= dom J \/ {IC SCMPDS} \/ dom I by XBOOLE_1:4
   .= dom Initialized J \/ dom I by Th27;
   then dom J \/ dom Initialized I c= dom s \/ dom I by A2,XBOOLE_1:13;
   then dom J \/ dom Initialized I c= dom s1 by FUNCT_4:def 1;
then A3: dom Initialized I c= dom s1 by XBOOLE_1:11;
   A4: now let x be set;
      assume A5: x in dom Initialized I;
      per cases by A5,Th28;
      suppose A6: x in dom I;
       hence (Initialized I).x = I.x by Th33
         .= s1.x by A6,FUNCT_4:14;
  suppose A7: x = IC SCMPDS;
  then A8: not x in dom I by Th30;
  A9: x in dom Initialized J by A7,Th7;
       thus (Initialized I).x = inspos 0 by A7,Th29
       .= (Initialized J).x by A7,Th29
       .= s.x by A1,A9,GRFUNC_1:8
       .= s1.x by A8,FUNCT_4:12;
     end;
A10: dom (s +* I) = dom s \/ dom I by FUNCT_4:def 1;
A11: dom (s +* Initialized I) = dom s \/ dom Initialized I by FUNCT_4:def 1;
     I c= Initialized I by Th9;
then A12: dom I c= dom Initialized I by GRFUNC_1:8;
then A13: dom (s +* I) c= dom (s +* Initialized I) by A10,A11,XBOOLE_1:9;
     dom (s +* Initialized I) c= dom s \/ (dom s \/ dom I)
       by A3,A10,A11,XBOOLE_1:9;
   then dom (s +* Initialized I) c= dom s \/ dom s \/ dom I by XBOOLE_1:4;
then A14: dom (s +* Initialized I) = dom (s +* I) by A10,A13,XBOOLE_0:def 10;
     now let x be set;
      assume x in dom (s +* Initialized I);
      per cases;
      suppose A15: x in dom Initialized I;
       hence (s +* Initialized I).x = (Initialized I).x by FUNCT_4:14
       .= (s +* I).x by A4,A15;
      suppose A16: not x in dom Initialized I;
    then A17: not x in dom I by A12;
       thus (s +* Initialized I).x = s.x by A16,FUNCT_4:12
       .= (s +* I).x by A17,FUNCT_4:12;
     end;
   hence s +* Initialized I = s +* I by A14,FUNCT_1:9;
end;

theorem
   for I,J being Program-block
 for s being State of SCMPDS st Initialized J c= s holds
     Initialized I c= s +* I
 proof
   let I,J be Program-block;
   let s be State of SCMPDS;
   assume Initialized J c= s;
   then s +* Initialized I = s +* I by Th34;
   hence Initialized I c= s +* I by FUNCT_4:26;
 end;

theorem
   for I,J being Program-block
 for s being State of SCMPDS holds
     s +* Initialized I, s +* Initialized J
         equal_outside the Instruction-Locations of SCMPDS
proof
   let I,J be Program-block;
   let s be State of SCMPDS;
A1: IC SCMPDS in dom Initialized I & IC SCMPDS in dom Initialized J
        by Th7;
A2: IC (s +* Initialized J) = (s +* Initialized J).IC SCMPDS by AMI_1:def 15
   .= (Initialized J).IC SCMPDS by A1,FUNCT_4:14
   .= inspos 0 by Th29
   .= (Initialized I).IC SCMPDS by Th29
   .= (s +* Initialized I).IC SCMPDS by A1,FUNCT_4:14
   .= IC (s +* Initialized I) by AMI_1:def 15;
   now let a be Int_position;
   A3: not a in dom Initialized I by Th31;
         not a in dom Initialized J by Th31;
       hence (s +* Initialized J).a = s.a by FUNCT_4:12
       .= (s +* Initialized I).a by A3,FUNCT_4:12;
     end;
   hence thesis by A2,Th11;
end;

begin :: Combining two consecutive blocks into one program block

definition let I,J be Program-block;
 func I ';' J -> Program-block equals
:Def3:  I +* Shift(J, card I);
 coherence
  proof set P = I +* Shift(J,card I);
       P is initial
     proof let m,n such that
A1:     inspos n in dom P and
A2:     m < n;
        set D = {inspos(l+card I): inspos l in dom J };
         dom Shift(J,card I) = D by SCMPDS_3:def 7;
then A3:    dom P = dom I \/ D by FUNCT_4:def 1;
      per cases by A1,A3,XBOOLE_0:def 2;
       suppose inspos n in dom I;
             then inspos m in dom I by A2,SCMPDS_3:def 5;
          hence inspos m in dom P by A3,XBOOLE_0:def 2;
       suppose inspos n in D;
        then consider l such that
A4:      inspos n = inspos(l+card I) and
A5:      inspos l in dom J;
A6:      n = l+card I by A4,SCMPDS_3:31;
          now per cases;
         case m < card I;
          then inspos m in dom I by Th1;
         hence inspos m in dom P by A3,XBOOLE_0:def 2;
         case m >= card I;
         then consider l1 being Nat such that
A7:      m = card I + l1 by NAT_1:28;
           l1 < l by A2,A6,A7,AXIOMS:24;
         then inspos l1 in dom J by A5,SCMPDS_3:def 5;
        hence inspos m in D by A7;
       end;
      hence inspos m in dom P by A3,XBOOLE_0:def 2;
     end;
   hence thesis;
  end;
 correctness;
end;

theorem Th37:
 for I,J being Program-block, l being Instruction-Location of SCMPDS
  st l in dom I holds (I ';' J).l = I.l
proof let I,J be Program-block, l be Instruction-Location of SCMPDS such
 that
A1: l in dom I;
A2: now assume l in dom Shift(J,card I);
       then l in { inspos(m+card I):inspos m in dom J } by SCMPDS_3:def 7;
      then consider m such that
A3:   l = inspos(m+card I) and inspos m in dom J;
         m + card I < card I by A1,A3,Th1;
       hence contradiction by NAT_1:29;
   end;
   thus (I ';' J).l = ( I +* Shift(J, card I)).l by Def3
    .= I.l by A2,FUNCT_4:12;
end;

theorem Th38:
 for I,J being Program-block, l being Instruction-Location of SCMPDS
  st l in dom J holds (I ';' J).(l+card I)= J.l
proof let I,J be Program-block, l be Instruction-Location of SCMPDS such
 that
A1: l in dom J;
    consider n such that
A2: l=inspos n by SCMPDS_3:32;
      inspos(n+card I) in { inspos(m+card I):inspos m in dom J } by A1,A2;
    then inspos(n+card I) in dom Shift(J,card I) by SCMPDS_3:def 7;
then A3: l+card I in dom Shift(J,card I) by A2,SCMPDS_3:def 3;
    thus (I ';' J).(l+card I) = ( I +* Shift(J, card I)).(l+card I) by Def3
    .= Shift(J, card I).(l+card I) by A3,FUNCT_4:14
    .=J.l by A1,SCMPDS_3:37;
end;

theorem Th39:   :: Th56
 for I,J being Program-block holds
     dom I c= dom (I ';' J)
proof
   let I,J be Program-block;
   I ';' J = I +* Shift(J,card I) by Def3;
    then dom (I ';' J) = dom I \/ dom Shift(J,card I)
       by FUNCT_4:def 1;
   hence dom I c= dom (I ';' J) by XBOOLE_1:7;
end;

theorem
   for I,J being Program-block holds
     I c= I ';' J
proof
   let I,J be Program-block;
A1: I ';' J = I +* Shift(J,card I) by Def3;
A2: dom I c= dom (I ';' J) by Th39;
     now let x be set;
      assume A3: x in dom I;
        dom I misses dom Shift(J,card I) by Th2;
      then not x in dom Shift(J,card I) by A3,XBOOLE_0:3;
      hence I.x = (I ';' J).x by A1,FUNCT_4:12;
    end;
    hence I c= I ';' J by A2,GRFUNC_1:8;
end;

theorem
   for I,J being Program-block holds
     I +* (I ';' J) = (I ';' J)
proof
   let I,J be Program-block;
A1: dom I c= dom (I ';' J) by Th39;
A2: dom (I +* (I ';' J)) = dom I \/ dom (I ';' J) by FUNCT_4:def 1
    .= dom (I ';' J) by A1,XBOOLE_1:12;
     for x be set st x in dom (I ';' J) holds
      (I +* (I ';' J)).x = (I ';' J).x by FUNCT_4:14;
   hence I +* (I ';' J) = (I ';' J) by A2,FUNCT_1:9;
end;

theorem
   for I,J being Program-block holds
     Initialized I +* (I ';' J) = Initialized (I ';' J)
 proof
   let I,J be Program-block;
     dom I c= dom (I ';' J) by Th39;
then A1: dom I \/ dom (I ';' J) = dom (I ';' J) by XBOOLE_1:12;
A2: dom (Initialized I+*(I ';' J))
    = dom Initialized I \/ dom (I ';' J) by FUNCT_4:def 1
   .= dom I \/ {IC SCMPDS} \/ dom (I ';' J) by Th27
   .= dom I \/ dom (I ';' J) \/ {IC SCMPDS} by XBOOLE_1:4
   .= dom Initialized (I ';' J) by A1,Th27;
     now let x be set;
      assume A3: x in dom Initialized (I ';' J);
      per cases by A3,Th28;
      suppose A4: x in dom (I ';' J);
       then x <> IC SCMPDS by Th30;
       then not x in {IC SCMPDS} by TARSKI:def 1;
  then A5:  not x in dom Start-At inspos 0 by AMI_3:34;
       thus (Initialized I+*(I ';' J)).x
        = (I ';' J).x by A4,FUNCT_4:14
       .= ((I ';' J) +* Start-At(inspos 0)).x by A5,FUNCT_4:12
       .= (Initialized (I ';' J)).x by Def2;
      suppose A6: x = IC SCMPDS;
       then not x in dom (I ';' J) by Th30;
       hence (Initialized I+*(I ';' J)).x
        = (Initialized I).x by FUNCT_4:12
       .= inspos 0 by A6,Th29
       .= (Initialized (I ';' J)).x by A6,Th29;
     end;
   hence Initialized I +* (I ';' J) = Initialized (I ';' J) by A2,FUNCT_1:9;
end;

begin :: Combining a block and a instruction into one program block

definition let i, J;
 func i ';' J -> Program-block equals
:Def4:  Load i ';' J;
 correctness;
end;

definition let I, j;
 func I ';' j -> Program-block equals
:Def5:  I ';' Load j;
 correctness;
end;

definition let i,j;
 func i ';' j -> Program-block equals
:Def6:  Load i ';' Load j;
 correctness;
end;

theorem Th43:  :: Th59
 i ';' j = Load i ';' j
proof
 thus i ';' j = Load i ';' Load j by Def6
   .= Load i ';' j by Def5;
end;

theorem Th44:   :: Th60
  i ';' j = i ';' Load j
 proof
  thus i ';' j = Load i ';' Load j by Def6
      .= i ';' Load j by Def4;
 end;

theorem Th45:   :: Th61
 card(I ';' J) = card I + card J
proof
A1: card dom(I ';' J) = card(I ';' J) &
  card dom I = card I & card dom J = card J by PRE_CIRC:21;
A2: card dom Shift(J, card I)
       = card Shift(J, card I) by PRE_CIRC:21
      .= card J by Th3
      .= card dom J by PRE_CIRC:21;
A3: dom(I ';' J)
      = dom(I +* Shift(J, card I)) by Def3
     .= dom I \/ dom Shift(J, card I) by FUNCT_4:def 1;
    dom I misses dom Shift(J,card I) by Th2;
  hence card(I ';' J) = card I + card J by A1,A2,A3,CARD_2:53;
end;

theorem Th46:  :: Th62
 I ';' J ';' K = I ';' (J ';' K)
proof
A1: Shift(J ';' K, card I)
     = Shift(J +* Shift(K, card J), card I) by Def3
    .= Shift(J,card I) +* Shift(Shift(K, card J), card I) by SCMPDS_3:41
    .= Shift(J,card I) +* Shift(K, card J+card I) by SCMPDS_3:39
    .= Shift(J,card I) +* Shift(K, card ( I ';'J)) by Th45;
  thus I ';' J ';' K
       = (I ';' J) +* Shift(K, card(I ';' J)) by Def3
      .= I +* Shift(J, card I) +* Shift(K, card(I ';' J)) by Def3
      .= I +* Shift(J ';' K, card I) by A1,FUNCT_4:15
      .= I ';' (J ';' K) by Def3;
end;

theorem Th47:  :: Th63
 I ';' J ';' k = I ';' (J ';' k)
proof
 thus I ';' J ';' k = I ';' J ';' Load k by Def5
       .= I ';' (J ';' Load k) by Th46
       .= I ';' (J ';' k) by Def5;
end;

theorem
   I ';' j ';' K = I ';' (j ';' K)
proof
 thus I ';' j ';' K = I ';' Load j ';' K by Def5
       .= I ';' (Load j ';' K) by Th46
       .= I ';' (j ';' K) by Def4;
end;

theorem
   I ';' j ';' k = I ';' (j ';' k)
proof
 thus I ';' j ';' k = I ';' Load j ';' k by Def5
         .= I ';' (Load j ';' k) by Th47
         .= I ';' (j ';' k) by Th43;
end;

theorem Th50:  :: Th66
 i ';' J ';' K = i ';' (J ';' K)
proof
 thus i ';' J ';' K = Load i ';' J ';' K by Def4
       .= Load i ';' (J ';' K) by Th46
       .= i ';' (J ';' K) by Def4;
end;

theorem
   i ';' J ';' k = i ';' (J ';' k)
proof
 thus i ';' J ';' k = Load i ';' J ';' k by Def4
       .= Load i ';' (J ';' k) by Th47
       .= i ';' (J ';' k) by Def4;
end;

theorem Th52:   :: Th68
 i ';' j ';' K = i ';' (j ';' K)
proof
 thus i ';' j ';' K = i ';' Load j ';' K by Th44
       .= i ';' (Load j ';' K) by Th50
       .= i ';' (j ';' K) by Def4;
end;

theorem
   i ';' j ';' k = i ';' (j ';' k)
proof
 thus i ';' j ';' k = i ';' j ';' Load k by Def5
       .= i ';' (j ';' Load k) by Th52
       .= i ';' (j ';' k) by Th44;
end;

theorem Th54:   :: SFM Th64:
  dom I misses dom Start-At inspos n
proof
A1: dom Start-At inspos n = {IC SCMPDS} by AMI_3:34;
A2: dom I c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
  assume dom I /\ dom (Start-At inspos n) <> {};
       then consider x being set such that
   A3: x in dom I /\ dom (Start-At inspos n) by XBOOLE_0:def 1;
         x in dom I & x in dom (Start-At inspos n) by A3,XBOOLE_0:def 3;
       then IC SCMPDS in dom I by A1,TARSKI:def 1;
    hence contradiction by A2,AMI_1:48;
end;

theorem   :: TN55
   Start-At inspos 0 c= Initialized I
proof
   Initialized I = I +* Start-At(inspos 0) by Def2;
 hence thesis by FUNCT_4:26;
end;

theorem Th56:  ::TN56
 I +* Start-At inspos n c= s implies I c= s
proof assume
A1: I +* Start-At inspos n c= s;
    dom I misses dom Start-At inspos n by Th54;
  then I +* Start-At inspos n = I \/ Start-At inspos n by FUNCT_4:32;
 hence thesis by A1,XBOOLE_1:11;
end;

theorem    ::S6B_5
   Initialized I c= s implies I c= s
proof assume
      Initialized I c= s;
    then I +* Start-At inspos 0 c= s by Def2;
    hence thesis by Th56;
end;

theorem Th58:  ::TN58
 (I +* Start-At inspos n)|the Instruction-Locations of SCMPDS = I
proof
A1: dom I c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
   the Instruction-Locations of SCMPDS misses dom Start-At inspos n
 proof
  assume not thesis; then consider x being set such that
A2:  x in the Instruction-Locations of SCMPDS & x in dom Start-At inspos n
       by XBOOLE_0:3;
     dom Start-At inspos n = {IC SCMPDS} by AMI_3:34;
   then x = IC SCMPDS by A2,TARSKI:def 1;
  hence contradiction by A2,AMI_1:48;
 end;
 then (I +* Start-At inspos n)|the Instruction-Locations of SCMPDS
  = I | the Instruction-Locations of SCMPDS by AMI_5:7;
 hence thesis by A1,RELAT_1:97;
end;

 reserve l,l1,loc for Instruction-Location of SCMPDS;

theorem Th59:   ::TN59
 not a in dom Start-At l
proof assume
A1: a in dom Start-At l;
    dom Start-At l = {IC SCMPDS} by AMI_3:34;
  then a = IC SCMPDS by A1,TARSKI:def 1;
 hence contradiction by SCMPDS_2:52;
end;

theorem
   not l1 in dom Start-At l
proof assume
A1: l1 in dom Start-At l;
    dom Start-At l = {IC SCMPDS} by AMI_3:34;
  then l1 = IC SCMPDS by A1,TARSKI:def 1;
 hence contradiction by AMI_1:48;
end;

theorem     ::TN61
   not a in dom (I+*Start-At l)
proof assume
     a in dom (I+*Start-At l);
   then a in dom I \/ dom Start-At l by FUNCT_4:def 1;
   then A1: a in dom I or a in dom Start-At l by XBOOLE_0:def 2;
   A2: dom I c= the Instruction-Locations of SCMPDS by AMI_3:def 13;
     a in SCM-Data-Loc by SCMPDS_2:def 2;
 hence contradiction by A1,A2,Th59,SCMPDS_2:10,XBOOLE_0:3;
end;

theorem    ::TN62
   s+*I+*Start-At inspos 0 = s+*Start-At inspos 0+*I
proof
A1:  dom I misses dom Start-At inspos 0 by Th54;
then I+*Start-At inspos 0 = I \/ Start-At inspos 0 by FUNCT_4:32
                         .= Start-At inspos 0 +* I by A1,FUNCT_4:32;
hence s+*I+*Start-At inspos 0
   = s+*(Start-At inspos 0+*I) by FUNCT_4:15
  .= s+*Start-At inspos 0+*I by FUNCT_4:15;
end;

definition
 let s be State of SCMPDS, li be Int_position, k be Integer;
 redefine func s+*(li,k) -> State of SCMPDS;
 coherence proof
A1:  dom(s+*(li,k)) = dom s by FUNCT_7:32;
A2:  dom s = dom the Object-Kind of SCMPDS by CARD_3:18;
      now let x be set;
     assume
A3:    x in dom the Object-Kind of SCMPDS;
     per cases;
     suppose
A4:    x = li;
      then A5:     (s+*(li,k)).x = k by A2,A3,FUNCT_7:33;
         (the Object-Kind of SCMPDS).x
           = ObjectKind li by A4,AMI_1:def 6
          .= INT by SCMPDS_2:13;
     hence (s+*(li,k)).x in (the Object-Kind of SCMPDS).x by A5,INT_1:12;
     suppose x <> li;
      then (s+*(li,k)).x = s.x by FUNCT_7:34;
     hence (s+*(li,k)).x in (the Object-Kind of SCMPDS).x by A3,CARD_3:18;
    end;
   hence s+*(li,k) is State of SCMPDS by A1,A2,CARD_3:18;
 end;
end;

begin :: The notions of paraclosed,parahalting and their basic properties

definition let I be Program-block;
 func stop(I) -> Program-block equals
:Def7:  I ';' SCMPDS-Stop;
 coherence;
end;

definition let I be Program-block, s be State of SCMPDS;
 func IExec(I,s) -> State of SCMPDS equals
      Result(s+*Initialized stop(I))
    +* s|the Instruction-Locations of SCMPDS;
 coherence by AMI_5:82;
end;

definition let I be Program-block;
 attr I is paraclosed means
:Def9: for s being State of SCMPDS, n being Nat
    st Initialized stop(I) c= s
   holds IC (Computation s).n in dom stop(I);

 attr I is parahalting means
:Def10: Initialized stop(I) is halting;
end;

Lm1:
  Load halt SCMPDS is parahalting
proof
  set m = Load halt SCMPDS,
      m0= stop (m),
      m1 = Initialized m0;
  let s;
  assume
A1: m1 c= s;
A2: m1 = m0 +* (Start-At inspos 0) by Def2;
   dom(Start-At inspos 0) = {IC SCMPDS} by AMI_3:34;
then A3: IC SCMPDS in dom (Start-At inspos 0) by TARSKI:def 1;
then A4: IC SCMPDS in dom m1 by A2,FUNCT_4:13;
A5: m = (inspos 0).--> halt SCMPDS by Def1;
then A6: m.inspos 0 = halt SCMPDS by CQC_LANG:6;
   dom m={inspos 0} by A5,CQC_LANG:5;
then A7: inspos 0 in dom m by TARSKI:def 1;
A8: m0= m ';' SCMPDS-Stop by Def7;
then A9: m0= m +* Shift(SCMPDS-Stop,card m) by Def3;
      dom m0 misses dom (Start-At inspos 0) by Th54;
then A10: m0 c= m1 by A2,FUNCT_4:33;
A11: inspos 0 in dom m0 by A7,A9,FUNCT_4:13;
then A12: inspos 0 in dom m1 by A2,FUNCT_4:13;
A13: IC m1 = m1.IC SCMPDS by A4,AMI_3:def 16
        .= (Start-At inspos 0).IC SCMPDS by A2,A3,FUNCT_4:14
        .= inspos 0 by AMI_3:50;
  take 0;
  thus CurInstr((Computation s).0) = CurInstr s by AMI_1:def 19
     .= s.IC s by AMI_1:def 17
     .= s.IC m1 by A1,A4,AMI_5:60
     .= m1.inspos 0 by A1,A12,A13,GRFUNC_1:8
     .= m0.inspos 0 by A10,A11,GRFUNC_1:8
     .= halt SCMPDS by A6,A7,A8,Th37;
end;

definition
 cluster parahalting Program-block;
 existence by Lm1;
end;

theorem Th63:    ::TN63
 for I being parahalting Program-block
   st Initialized stop I c= s holds s is halting
proof
 let I be parahalting Program-block; assume
A1: Initialized stop I c= s;
      Initialized stop I is halting by Def10;
    hence s is halting by A1,AMI_1:def 26;
end;

definition let I be parahalting Program-block;
 cluster Initialized stop(I) -> halting;
  coherence
  proof
  let s be State of SCMPDS;
   assume Initialized stop I c= s;
   hence s is halting by Th63;
  end;
end;

definition
 let la,lb be Instruction-Location of SCMPDS;
 let a, b be Instruction of SCMPDS;
 redefine func (la,lb) --> (a,b) -> FinPartState of SCMPDS;
 coherence
proof
       ObjectKind la = the Instructions of SCMPDS &
     ObjectKind lb = the Instructions of SCMPDS by AMI_1:def 14;
    hence thesis by AMI_1:58;
  end;
end;

canceled;

theorem Th65:
    IC s <> Next IC s
proof
   assume A1: IC s = Next IC s;
   consider mj be Element of SCM-Instr-Loc such that
A2: mj = IC s & Next mj = Next IC s by SCMPDS_2:def 19;
      mj+0=mj+2 by A1,A2,AMI_2:def 15;
    hence contradiction by XCMPLX_1:2;
end;

theorem Th66:    ::TN66
 s2 +*((IC s2,Next IC s2) --> (goto 1, goto -1)) is not halting
proof set m=(IC s2,Next IC s2) --> (goto 1, goto -1),
          s1 = s2 +* m;
A1: dom m = {IC s2,Next IC s2} by FUNCT_4:65;
then A2: IC s2 in dom m & Next IC s2 in dom m by TARSKI:def 2;
   IC s2<>Next IC s2 by Th65;
then A3: m.(IC s2) = goto 1 & m.(Next IC s2)=goto -1 by FUNCT_4:66;
A4: IC SCMPDS <> IC s2 by AMI_1:48;
   IC SCMPDS <> Next IC s2 by AMI_1:48;
then A5: not IC SCMPDS in dom m by A1,A4,TARSKI:def 2;
   defpred X[Nat] means
    IC((Computation s1).$1) = IC s1 or IC((Computation s1).$1) = Next IC s1;
A6: X[0] by AMI_1:def 19;
A7: IC s1 = s1.IC SCMPDS by AMI_1:def 15
       .= s2.IC SCMPDS by A5,FUNCT_4:12
       .= IC s2 by AMI_1:def 15;

   now let n;
    set Cn=(Computation s1).n;
    assume
A8:   IC Cn = IC s1 or IC Cn = Next IC s1;
      per cases by A8;
      case A9:IC Cn = IC s1;
A10:   CurInstr( Cn )
          = Cn.IC Cn by AMI_1:def 17
         .= s1.IC s1 by A9,AMI_1:54
         .= goto 1 by A2,A3,A7,FUNCT_4:14;
    thus IC ((Computation s1).(n+1))
            = IC Following Cn by AMI_1:def 19
           .= IC Exec(goto 1,Cn) by A10,AMI_1:def 18
           .= Exec(goto 1,Cn).IC SCMPDS by AMI_1:def 15
           .= ICplusConst(Cn,1) by SCMPDS_2:66
           .= Next IC s1 by A9,SCMPDS_3:20;
      case A11:IC Cn = Next IC s1;
A12:   CurInstr((Computation s1).n)
          = Cn.IC Cn by AMI_1:def 17
         .= s1.(Next IC s1) by A11,AMI_1:54
         .= goto -1 by A2,A3,A7,FUNCT_4:14;
        consider j be Nat such that
A13:     j = IC Cn & ICplusConst(Cn,-1)=abs(j-2+2*(-1))+2
             by SCMPDS_2:def 20;
        consider mj be Element of SCM-Instr-Loc such that
A14:      mj = IC s1 & Next mj = Next IC s1 by SCMPDS_2:def 19;
        consider i be Nat such that
A15:     IC s1=2*i+2 by SCMPDS_2:1,def 1;
A16:     j=2*i+2+2 by A11,A13,A14,A15,AMI_2:def 15
        .=2*i+(2+2) by XCMPLX_1:1;
A17:     2*i >= 0 by NAT_1:18;
    thus IC((Computation s1).(n+1))
            = IC Following Cn by AMI_1:def 19
           .= IC Exec(goto -1,Cn ) by A12,AMI_1:def 18
           .= Exec(goto -1,Cn ).IC SCMPDS by AMI_1:def 15
           .=abs(j-2+ -(2*1))+2 by A13,SCMPDS_2:66
           .=abs(j+ -2 + -2)+2 by XCMPLX_0:def 8
           .=abs(j+ (-2 + -2))+2 by XCMPLX_1:1
           .=abs(2*i+4 + -4 )+2 by A16
           .=abs(2*i)+2 by XCMPLX_1:137
           .=IC s1 by A15,A17,ABSVALUE:def 1;
   end;
then A18: for n st X[n] holds X[n+1];
A19: for n holds X[n] from Ind(A6,A18);
 let n;
   per cases by A19;
   suppose IC((Computation s1).n) = IC s1;
       then CurInstr((Computation s1).n)
          = ((Computation s1).n).IC s1 by AMI_1:def 17
         .= s1.IC s1 by AMI_1:54
         .= goto 1 by A2,A3,A7,FUNCT_4:14;
       hence CurInstr((Computation s1).n) <> halt SCMPDS by SCMPDS_2:85;
   suppose IC((Computation s1).n) = Next IC s1;
        then CurInstr((Computation s1).n)
          = ((Computation s1).n).Next IC s1 by AMI_1:def 17
         .= s1.Next IC s1 by AMI_1:54
         .= goto -1 by A2,A3,A7,FUNCT_4:14;
       hence CurInstr((Computation s1).n) <> halt SCMPDS by SCMPDS_2:85;
end;

theorem Th67:   ::Th21
 s1,s2 equal_outside the Instruction-Locations of SCMPDS &
  I c= s1 & I c= s2 &
  (for m st m < n holds IC ((Computation s2).m) in dom I)
 implies
 for m st m <= n holds
  (Computation s1).m, (Computation s2 ).m equal_outside
     the Instruction-Locations of SCMPDS
proof assume that
A1: s1,s2 equal_outside the Instruction-Locations of SCMPDS and
A2: I c= s1 and
A3: I c= s2 and
A4: for m st m < n holds IC((Computation s2).m) in dom I;
   defpred X[Nat] means $1 <= n implies
  (Computation s1).$1, (Computation s2 ).$1 equal_outside
     the Instruction-Locations of SCMPDS;
     (Computation s1).0 = s1 & (Computation s2 ).0 = s2 by AMI_1:def 19;
then A5: X[0] by A1;
A6: for m st X[m] holds X[m+1]
    proof let m such that
A7: m <= n implies
     (Computation s1).m, (Computation s2 ).m equal_outside
       the Instruction-Locations of SCMPDS;
A8:   (Computation s1).(m+1) = Following((Computation s1).m) by AMI_1:def 19
      .= Exec(CurInstr((Computation s1).m),(Computation s1).m)
         by AMI_1:def 18;
A9:   (Computation s2).(m+1) = Following((Computation s2).m) by AMI_1:def 19
      .= Exec(CurInstr((Computation s2).m),(Computation s2).m)
         by AMI_1:def 18;
    assume A10: m+1 <= n;
then m < n by NAT_1:38;
then A11:   IC((Computation s2).m) in dom I by A4;
A12:   IC ((Computation s1).m) = IC ((Computation s2).m)
     by A7,A10,NAT_1:38,SCMFSA6A:29;
       CurInstr((Computation s1).m)
          = ((Computation s1).m).IC ((Computation s1).m) by AMI_1:def 17
         .= s1.IC((Computation s1).m) by AMI_1:54
         .= I.IC((Computation s1).m) by A2,A11,A12,GRFUNC_1:8
         .= s2.IC((Computation s2).m) by A3,A11,A12,GRFUNC_1:8
         .= ((Computation s2).m).IC ((Computation s2).m) by AMI_1:54
         .= CurInstr((Computation s2).m) by AMI_1:def 17;
    hence (Computation s1).(m+1), (Computation s2 ).(m+1) equal_outside
     the Instruction-Locations of SCMPDS by A7,A8,A9,A10,Th15,NAT_1:38;
   end;
 thus for m holds X[m] from Ind(A5,A6);
end;

theorem Th68:
 for s being State of SCMPDS,l being Instruction-Location of SCMPDS
  holds l in dom s
proof
    let s be State of SCMPDS,l be Instruction-Location of SCMPDS;
     l in {IC SCMPDS} \/ SCM-Data-Loc \/ the Instruction-Locations of SCMPDS
   by XBOOLE_0:def 2;
   hence l in dom s by AMI_3:36,SCMPDS_3:5;
end;

reserve l1,l2 for Instruction-Location of SCMPDS,
         i1,i2 for Instruction of SCMPDS;

theorem Th69:
    s +*((l1,l2) --> (i1, i2)) = s +* (l1,i1) +* (l2,i2)
proof
    A1: l1 in dom s by Th68;
          l2 in dom s by Th68;
    then A2: l2 in dom (s +* (l1,i1)) by FUNCT_7:32;
    thus s +*((l1,l2) --> (i1, i2))
       =s +* ((l1 .--> i1) +* (l2 .--> i2)) by AMI_1:18
      .=s +* (l1 .--> i1) +* (l2 .--> i2) by FUNCT_4:15
      .=s +* (l1,i1) +* (l2 .--> i2) by A1,FUNCT_7:def 3
      .=s +* (l1,i1) +* (l2,i2) by A2,FUNCT_7:def 3;
end;

theorem Th70:
 Next inspos n = inspos(n+1)
 proof
A1: inspos n = il.n & inspos(n+1) = il.(n+1) by SCMPDS_3:def 2;
    consider l be Element of SCM-Instr-Loc such that
A2: l = inspos n and
A3: Next l = Next inspos n by SCMPDS_2:def 19;
    thus Next inspos n=Next il.n by A1,A2,A3,AMI_3:6
    .=inspos(n+1) by A1,AMI_3:54;
end;

theorem Th71:
    not IC s in dom I implies not Next IC s in dom I
proof
    assume A1: not IC s in dom I;
    consider m be Nat such that
A2: IC s=inspos m by SCMPDS_3:32;
A3: m >= card I by A1,A2,Th1;
A4: Next IC s=inspos(m+1) by A2,Th70;
      m+1 >= m by NAT_1:29;
    then m+1 >= card I by A3,AXIOMS:22;
    hence thesis by A4,Th1;
end;

definition
 cluster parahalting -> paraclosed Program-block;
 coherence proof
  let I be Program-block; assume
A1: I is parahalting;
  let s be State of SCMPDS, n be Nat;
 assume
A2: Initialized stop(I) c= s;
   defpred X[Nat] means not IC (Computation s).$1 in dom stop(I);
 assume not IC (Computation s).n in dom stop(I);
then A3: ex n st X[n];
  consider n such that
A4: X[n] and
A5: for m st X[m] holds n <= m from Min(A3);
A6: not Next IC (Computation s).n in dom stop(I) by A4,Th71;
   set s2 = (Computation s).n,
       Ig = ((IC s2,Next IC s2) --> (goto 1, goto -1)),
       s0 = s +* Ig,
       s1 = s2 +* Ig,
       t1= s +* (IC s2,goto 1),
       t2= t1 +* (Next IC s2,goto -1),
       t3= s2 +* (IC s2,goto 1),
       t4= t3 +* (Next IC s2,goto -1),
       IL=the Instruction-Locations of SCMPDS;
   set IAt = stop(I) +* Start-At inspos 0;
     dom stop(I) misses dom Start-At inspos 0 by Th54;
then A7: stop I c= IAt by FUNCT_4:33;
A8: Initialized stop(I) = IAt by Def2;
then A9: IAt is halting by A1,Def10;
     (IAt) | IL = stop I by Th58;
then A10:  dom stop (I) = dom(IAt) /\ IL
        by RELAT_1:90;
then A11: not IC s2 in dom IAt by A4,XBOOLE_0:def 3;
A12: not Next IC s2 in dom IAt by A6,A10,XBOOLE_0:def 3;
      IAt c= t1 by A2,A8,A11,SCMFSA6A:1;
    then IAt c= t2 by A12,SCMFSA6A:1;
then A13: IAt c= s0 by Th69;
then A14: s0 is halting by A9,AMI_1:def 26;
A15: s,t1 equal_outside IL by SCMFSA6A:3;
    t1,t2 equal_outside IL by SCMFSA6A:3;
  then s,t2 equal_outside IL by A15,FUNCT_7:29;
  then s,s0 equal_outside IL by Th69;
then A16: s0,s equal_outside IL by FUNCT_7:28;
A17: stop I c= s0 by A7,A13,XBOOLE_1:1;
A18: stop I c= s by A2,A7,A8,XBOOLE_1:1;
   for m st m < n holds IC((Computation s).m) in dom stop I by A5;
then A19: (Computation s0).n,s2 equal_outside IL by A16,A17,A18,Th67;
A20: s2,t3 equal_outside IL by SCMFSA6A:3;
     t3,t4 equal_outside IL by SCMFSA6A:3;
   then s2,t4 equal_outside IL by A20,FUNCT_7:29;
   then s2,s1 equal_outside IL by Th69;
then A21: (Computation s0).n, s1 equal_outside IL by A19,FUNCT_7:29;
        s| IL = s2 | IL by SCMFSA6B:17;
      then t1 | IL = t3 | IL by SCMFSA6A:5;
      then t2 | IL = t4 | IL by SCMFSA6A:5;
      then s0 | IL = t4 | IL by Th69;
  then s0 | IL = s1 | IL by Th69;
    then (Computation s0).n | IL = s1 | IL by SCMFSA6B:17;
then A22: (Computation s0).n = s1 by A21,SCMFSA6A:2;
    s1 is not halting by Th66;
 hence contradiction by A14,A22,SCM_1:27;
 end;
end;

theorem Th72:   :: SCMFSA8A_15
     dom SCMPDS-Stop = {inspos 0} by CQC_LANG:5,SCMPDS_3:def 6;

theorem    ::S8A_16
    inspos 0 in dom SCMPDS-Stop & SCMPDS-Stop.inspos 0 = halt SCMPDS
   by Th72,CQC_LANG:6,SCMPDS_3:def 6,TARSKI:def 1;

theorem Th74:
     card SCMPDS-Stop = 1
 proof
   thus card SCMPDS-Stop = card dom SCMPDS-Stop by PRE_CIRC:21
   .= 1 by Th72,CARD_1:79;
end;

theorem Th75: ::Th26 T9
 inspos 0 in dom stop (I)
proof
     card stop I =card (I ';' SCMPDS-Stop) by Def7
   .=card I + 1 by Th45,Th74;
   then 1 <= card stop I by NAT_1:29;
   then 0 < card stop I by AXIOMS:22;
   hence thesis by Th1;
end;

theorem Th76:
 for p being programmed FinPartState of SCMPDS,k being Nat,
 il be Instruction-Location of SCMPDS st il in dom p holds
 il+k in dom Shift(p,k)
proof
  let p be programmed FinPartState of SCMPDS,k be Nat,
  il be Instruction-Location of SCMPDS;
  assume A1: il in dom p;
   dom Shift(p,k) = { loc+k : loc in dom p} by SCMPDS_3:38;
  hence thesis by A1;
end;

begin :: Shiftability of program blocks and instructions

definition
 let i be Instruction of SCMPDS;
 let n be Nat;
 pred i valid_at n means
:Def11:  (InsCode i= 0 implies ex k1 st i = goto k1 & n+k1 >= 0) &
   (InsCode i= 4 implies ex a,k1,k2 st i = (a,k1)<>0_goto k2 & n+k2 >= 0 ) &
   (InsCode i= 5 implies ex a,k1,k2 st i = (a,k1)<=0_goto k2 & n+k2 >= 0 ) &
   (InsCode i= 6 implies ex a,k1,k2 st i = (a,k1)>=0_goto k2 & n+k2 >= 0);
end;

reserve l for Nat;

theorem Th77:
  for i be Instruction of SCMPDS,m,n be Nat st i valid_at m & m <= n
 holds i valid_at n
proof
  let i be Instruction of SCMPDS,m,n be Nat;
  assume A1:i valid_at m & m <= n;
A2: now
     assume InsCode i= 0;
       then consider k1 such that
    A3: i=goto k1 & m+k1 >= 0 by A1,Def11;
    take k1;
    thus i=goto k1 by A3;
    thus n+k1 >= 0 by A1,A3,AXIOMS:24;
  end;
A4: now
     assume InsCode i= 4;
       then consider a,k1,k2 such that
    A5: i = (a,k1)<>0_goto k2 & m+k2 >= 0 by A1,Def11;
    take a,k1,k2;
    thus i = (a,k1)<>0_goto k2 by A5;
    thus n+k2 >= 0 by A1,A5,AXIOMS:24;
  end;
A6: now
     assume InsCode i= 5;
       then consider a,k1,k2 such that
    A7: i = (a,k1)<=0_goto k2 & m+k2 >= 0 by A1,Def11;
    take a,k1,k2;
    thus i = (a,k1)<=0_goto k2 by A7;
    thus n+k2 >= 0 by A1,A7,AXIOMS:24;
  end;
  now
     assume InsCode i= 6;
       then consider a,k1,k2 such that
    A8: i = (a,k1)>=0_goto k2 & m+k2 >= 0 by A1,Def11;
    take a,k1,k2;
    thus i = (a,k1)>=0_goto k2 by A8;
    thus n+k2 >= 0 by A1,A8,AXIOMS:24;
  end;
  hence thesis by A2,A4,A6,Def11;
end;

definition let IT be FinPartState of SCMPDS;
 attr IT is shiftable means
:Def12: for n,i st inspos n in dom IT & i=IT.(inspos n) holds
      InsCode i <> 1 & InsCode i <> 3 &   :: return  and save
      i valid_at n;
end;

Lm2:
  Load halt SCMPDS is shiftable
proof
  set m = Load halt SCMPDS;
A1: m = (inspos 0).--> halt SCMPDS by Def1;
then A2: m.inspos 0 = halt SCMPDS by CQC_LANG:6;
A3: dom m={inspos 0} by A1,CQC_LANG:5;
      now let n,i;
       assume A4:inspos n in dom m & i=m.(inspos n);
       then A5: inspos n= inspos 0 by A3,TARSKI:def 1;
then A6:    InsCode i =0 by A2,A4,SCMPDS_2:21,93;
       thus InsCode i <> 1 by A2,A4,A5,SCMPDS_2:21,93;
       thus InsCode i <> 3 by A2,A4,A5,SCMPDS_2:21,93;
         ex k1 st i = goto k1 & n+k1 >= 0
       proof
          take 0;
          thus i=goto 0 by A1,A4,A5,CQC_LANG:6,SCMPDS_2:93;
          thus n+0>=0 by A5,SCMPDS_3:31;
       end;
       hence i valid_at n by A6,Def11;
    end;
    hence thesis by Def12;
end;

definition
 cluster parahalting shiftable Program-block;
 existence by Lm1,Lm2;
end;

definition let i be Instruction of SCMPDS;
 attr i is shiftable means
:Def13: InsCode i = 2 or InsCode i > 6;
end;

definition
 cluster shiftable Instruction of SCMPDS;
 existence
  proof
   take i=DataLoc(0,0):=1;
   InsCode i=2 by SCMPDS_2:23;
    hence thesis by Def13;
  end;
end;

definition
 let a,k1;
 cluster a := k1 -> shiftable;
 coherence
 proof
       InsCode (a:=k1)=2 by SCMPDS_2:23;
     hence thesis by Def13;
 end;
end;

definition
 let a,k1,k2;
 cluster (a,k1) := k2 -> shiftable;
 coherence
 proof
       InsCode ((a,k1) := k2)=7 by SCMPDS_2:28;
     hence thesis by Def13;
 end;
end;

definition
 let a,k1,k2;
 cluster AddTo(a,k1,k2) -> shiftable;
 coherence
 proof
       InsCode AddTo(a,k1,k2)=8 by SCMPDS_2:29;
     hence thesis by Def13;
 end;
end;

definition
 let a,b,k1,k2;
 cluster AddTo(a,k1,b,k2) -> shiftable;
 coherence
 proof
       InsCode AddTo(a,k1,b,k2)=9 by SCMPDS_2:30;
     hence thesis by Def13;
 end;

cluster SubFrom(a,k1,b,k2) -> shiftable;
 coherence
 proof
       InsCode SubFrom(a,k1,b,k2)=10 by SCMPDS_2:31;
     hence thesis by Def13;
 end;

cluster MultBy(a,k1,b,k2) -> shiftable;
 coherence
 proof
       InsCode MultBy(a,k1,b,k2)=11 by SCMPDS_2:32;
     hence thesis by Def13;
 end;

cluster Divide(a,k1,b,k2) -> shiftable;
 coherence
 proof
       InsCode Divide(a,k1,b,k2)=12 by SCMPDS_2:33;
     hence thesis by Def13;
 end;

cluster (a,k1) := (b,k2) -> shiftable;
 coherence
 proof
       InsCode (a,k1) := (b,k2)=13 by SCMPDS_2:34;
     hence thesis by Def13;
 end;
end;

definition
 let I,J be shiftable Program-block;
 cluster I ';' J -> shiftable;
 coherence
 proof
     set IJ=I ';' J;
A1: I ';' J = I +* Shift(J,card I) by Def3;
     now let n,i such that
A2:    inspos n in dom IJ and
A3:    i=IJ.(inspos n);
       set D = {inspos(l+card I): inspos l in dom J };
         dom Shift(J,card I) = D by SCMPDS_3:def 7;
then A4:    dom IJ = dom I \/ D by A1,FUNCT_4:def 1;
      per cases by A2,A4,XBOOLE_0:def 2;
       suppose A5:inspos n in dom I;
           then I.inspos n=i by A3,Th37;
         hence InsCode i <> 1 & InsCode i <> 3 & i valid_at n by A5,Def12;
       suppose inspos n in D;
        then consider l such that
A6:      inspos n = inspos(l+card I) and
A7:      inspos l in dom J;
A8:      J.inspos l=IJ.(inspos l+card I) by A7,Th38
         .=i by A3,A6,SCMPDS_3:def 3;
         hence InsCode i <> 1 & InsCode i <> 3 by A7,Def12;
           l <= l+card I by NAT_1:29;
then A9:      l <= n by A6,SCMPDS_3:31;
           i valid_at l by A7,A8,Def12;
         hence i valid_at n by A9,Th77;
   end;
   hence thesis by Def12;
 end;
end;

definition
 let i be shiftable Instruction of SCMPDS;
 cluster Load i -> shiftable;
 coherence
 proof
    set p=Load i;
     now let n,j such that
A1:    inspos n in dom p and
A2:    j=p.inspos n;
A3:    p=inspos 0 .--> i by Def1;
       then dom p = { inspos 0 } by CQC_LANG:5;
       then inspos n = inspos 0 by A1,TARSKI:def 1;
       then A4: j=i by A2,A3,CQC_LANG:6;
then A5:    InsCode j=2 or InsCode j > 6 by Def13;
       thus InsCode j <> 1 by A4,Def13;
       thus InsCode j <> 3 by A4,Def13;
A6:    InsCode j <> 0 by A4,Def13;
A7:    InsCode j <> 4 by A4,Def13;
     InsCode j <> 5 by A4,Def13;
       hence j valid_at n by A5,A6,A7,Def11;
     end;
     hence thesis by Def12;
  end;
end;

definition
  let i be shiftable Instruction of SCMPDS,
      J be shiftable Program-block;
 cluster i ';' J -> shiftable;
 coherence
 proof
       i ';' J=Load i ';' J by Def4;
     hence thesis;
 end;
end;

definition
 let I be shiftable Program-block,
     j be shiftable Instruction of SCMPDS;
 cluster I ';' j -> shiftable;
 coherence
 proof
       I ';' j=I ';' Load j by Def5;
     hence thesis;
 end;
end;

definition
 let i,j be shiftable Instruction of SCMPDS;
 cluster i ';' j -> shiftable;
 coherence
 proof
       i ';' j=Load i ';' Load j by Def6;
     hence thesis;
 end;
end;

definition
 cluster SCMPDS-Stop -> parahalting shiftable;
 coherence by Def1,Lm1,Lm2,SCMPDS_3:def 6;
end;

definition
 let I be shiftable Program-block;
 cluster stop I -> shiftable;
 coherence
 proof
      stop I= I ';' SCMPDS-Stop by Def7;
    hence thesis;
 end;
end;

theorem
    for I being shiftable Program-block,k1 be Integer st
  card I + k1 >= 0 holds I ';' goto k1 is shiftable
proof
  let I be shiftable Program-block,k1 be Integer;
  assume A1: card I + k1 >= 0;
   set J= Load goto k1;
   set Ig=I ';' goto k1;
A2:  Ig=I ';' J by Def5;
then A3:  Ig=I +* Shift(J,card I) by Def3;
     now let n,i such that
A4:    inspos n in dom Ig and
A5:    i=Ig.(inspos n);
       set D = {inspos(l+card I): inspos l in dom J };
         dom Shift(J,card I) = D by SCMPDS_3:def 7;
then A6:    dom Ig = dom I \/ D by A3,FUNCT_4:def 1;
      per cases by A4,A6,XBOOLE_0:def 2;
       suppose A7:inspos n in dom I;
           then I.inspos n=i by A2,A5,Th37;
         hence InsCode i <> 1 & InsCode i <> 3 & i valid_at n by A7,Def12;
       suppose inspos n in D;
        then consider l such that
A8:      inspos n = inspos(l+card I) and
A9:      inspos l in dom J;
A10:    J=inspos 0 .--> goto k1 by Def1;
       then dom J = { inspos 0 } by CQC_LANG:5;
then A11:    inspos l = inspos 0 by A9,TARSKI:def 1;
then A12:    goto k1 =J.inspos l by A10,CQC_LANG:6
       .=Ig.(inspos l+card I) by A2,A9,Th38
       .=i by A5,A8,SCMPDS_3:def 3;
       hence InsCode i <> 1 & InsCode i <> 3 by SCMPDS_2:21;
         inspos n= inspos(0+card I) by A8,A11,SCMPDS_3:31;
then A13:    n+k1 >=0 by A1,SCMPDS_3:31;
     InsCode i <> 4 & InsCode i <> 5 & InsCode i <> 6 by A12,SCMPDS_2:21;
       hence i valid_at n by A12,A13,Def11;
    end;
   hence thesis by Def12;
end;

definition
 let n be Nat;
 cluster Load goto n -> shiftable;
 coherence
 proof
   set k1=n;
   set J= Load goto k1;
     now let n,i such that
A1:    inspos n in dom J and
A2:    i=J.inspos n;
A3:    J=inspos 0 .--> goto k1 by Def1;
       then dom J = { inspos 0 } by CQC_LANG:5;
then inspos n = inspos 0 by A1,TARSKI:def 1;
then A4:    goto k1 =i by A2,A3,CQC_LANG:6;
       hence InsCode i <> 1 & InsCode i <> 3 by SCMPDS_2:21;
A5:    n+k1 >=0 by NAT_1:18;
     InsCode i <> 4 & InsCode i <> 5 & InsCode i <> 6 by A4,SCMPDS_2:21;
       hence i valid_at n by A4,A5,Def11;
    end;
   hence thesis by Def12;
  end;
end;

theorem
    for I being shiftable Program-block,k1,k2 be Integer,a be Int_position st
  card I + k2 >= 0 holds I ';' (a,k1)<>0_goto k2 is shiftable
proof
  let I be shiftable Program-block,k1,k2 be Integer,a be Int_position;
  assume A1: card I + k2 >= 0;
   set ii= (a,k1)<>0_goto k2,
       J= Load ii;
   set Ig=I ';' ii;
A2:  Ig=I ';' J by Def5;
then A3:  Ig=I +* Shift(J,card I) by Def3;
     now let n,i such that
A4:    inspos n in dom Ig and
A5:    i=Ig.(inspos n);
       set D = {inspos(l+card I): inspos l in dom J };
         dom Shift(J,card I) = D by SCMPDS_3:def 7;
then A6:    dom Ig = dom I \/ D by A3,FUNCT_4:def 1;
      per cases by A4,A6,XBOOLE_0:def 2;
       suppose A7:inspos n in dom I;
           then I.inspos n=i by A2,A5,Th37;
         hence InsCode i <> 1 & InsCode i <> 3 & i valid_at n by A7,Def12;
       suppose inspos n in D;
        then consider l such that
A8:      inspos n = inspos(l+card I) and
A9:      inspos l in dom J;
A10:    J=inspos 0 .--> ii by Def1;
       then dom J = { inspos 0 } by CQC_LANG:5;
then A11:    inspos l = inspos 0 by A9,TARSKI:def 1;
then A12:    ii=J.inspos l by A10,CQC_LANG:6
       .=Ig.(inspos l+card I) by A2,A9,Th38
       .=i by A5,A8,SCMPDS_3:def 3;
       hence InsCode i <> 1 & InsCode i <> 3 by SCMPDS_2:25;
         inspos n= inspos(0+card I) by A8,A11,SCMPDS_3:31;
then A13:    n+k2 >=0 by A1,SCMPDS_3:31;
     InsCode i <> 0 & InsCode i <> 5 & InsCode i <> 6 by A12,SCMPDS_2:25;
       hence i valid_at n by A12,A13,Def11;
    end;
   hence thesis by Def12;
end;

definition
  let k1 be Integer,a be Int_position,n be Nat;
  cluster Load (a,k1)<>0_goto n -> shiftable;
  coherence
  proof
   set k2=n;
   set ii= (a,k1)<>0_goto k2,
       J= Load ii;
     now let n,i such that
A1:    inspos n in dom J and
A2:    i=J.inspos n;
A3:    J=inspos 0 .--> ii by Def1;
       then dom J = { inspos 0 } by CQC_LANG:5;
then inspos n = inspos 0 by A1,TARSKI:def 1;
then A4:    ii =i by A2,A3,CQC_LANG:6;
       hence InsCode i <> 1 & InsCode i <> 3 by SCMPDS_2:25;
A5:    n+k2 >=0 by NAT_1:18;
     InsCode i <> 0 & InsCode i <> 5 & InsCode i <> 6 by A4,SCMPDS_2:25;
       hence i valid_at n by A4,A5,Def11;
    end;
   hence thesis by Def12;
   end;
end;

theorem
    for I being shiftable Program-block,k1,k2 be Integer,a be Int_position st
  card I + k2 >= 0 holds I ';' (a,k1)<=0_goto k2 is shiftable
proof
  let I be shiftable Program-block,k1,k2 be Integer,a be Int_position;
  assume A1: card I + k2 >= 0;
   set ii= (a,k1)<=0_goto k2,
       J= Load ii;
   set Ig=I ';' ii;
A2:  Ig=I ';' J by Def5;
then A3:  Ig=I +* Shift(J,card I) by Def3;
     now let n,i such that
A4:    inspos n in dom Ig and
A5:    i=Ig.(inspos n);
       set D = {inspos(l+card I): inspos l in dom J };
         dom Shift(J,card I) = D by SCMPDS_3:def 7;
then A6:    dom Ig = dom I \/ D by A3,FUNCT_4:def 1;
      per cases by A4,A6,XBOOLE_0:def 2;
       suppose A7:inspos n in dom I;
           then I.inspos n=i by A2,A5,Th37;
         hence InsCode i <> 1 & InsCode i <> 3 & i valid_at n by A7,Def12;
       suppose inspos n in D;
        then consider l such that
A8:      inspos n = inspos(l+card I) and
A9:      inspos l in dom J;
A10:    J=inspos 0 .--> ii by Def1;
       then dom J = { inspos 0 } by CQC_LANG:5;
then A11:    inspos l = inspos 0 by A9,TARSKI:def 1;
then A12:    ii =J.inspos l by A10,CQC_LANG:6
       .=Ig.(inspos l+card I) by A2,A9,Th38
       .=i by A5,A8,SCMPDS_3:def 3;
       hence InsCode i <> 1 & InsCode i <> 3 by SCMPDS_2:26;
         inspos n= inspos(0+card I) by A8,A11,SCMPDS_3:31;
then A13:    n+k2 >=0 by A1,SCMPDS_3:31;
     InsCode i <> 0 & InsCode i <> 4 & InsCode i <> 6 by A12,SCMPDS_2:26;
       hence i valid_at n by A12,A13,Def11;
    end;
   hence thesis by Def12;
end;

definition
  let k1 be Integer,a be Int_position,n be Nat;
  cluster Load (a,k1)<=0_goto n -> shiftable;
  coherence
  proof
   set k2=n;
   set ii= (a,k1)<=0_goto k2,
       J= Load ii;
     now let n,i such that
A1:    inspos n in dom J and
A2:    i=J.inspos n;
A3:    J=inspos 0 .--> ii by Def1;
       then dom J = { inspos 0 } by CQC_LANG:5;
then inspos n = inspos 0 by A1,TARSKI:def 1;
then A4:    ii =i by A2,A3,CQC_LANG:6;
       hence InsCode i <> 1 & InsCode i <> 3 by SCMPDS_2:26;
A5:    n+k2 >=0 by NAT_1:18;
     InsCode i <> 0 & InsCode i <> 4 & InsCode i <> 6 by A4,SCMPDS_2:26;
       hence i valid_at n by A4,A5,Def11;
    end;
   hence thesis by Def12;
   end;
end;

theorem
    for I being shiftable Program-block,k1,k2 be Integer,a be Int_position st
  card I + k2 >= 0 holds I ';' (a,k1)>=0_goto k2 is shiftable
proof
  let I be shiftable Program-block,k1,k2 be Integer,a be Int_position;
  assume A1: card I + k2 >= 0;
   set ii= (a,k1)>=0_goto k2,
       J= Load ii;
   set Ig=I ';' ii;
A2:  Ig=I ';' J by Def5;
then A3:  Ig=I +* Shift(J,card I) by Def3;
     now let n,i such that
A4:    inspos n in dom Ig and
A5:    i=Ig.(inspos n);
       set D = {inspos(l+card I): inspos l in dom J };
         dom Shift(J,card I) = D by SCMPDS_3:def 7;
then A6:    dom Ig = dom I \/ D by A3,FUNCT_4:def 1;
      per cases by A4,A6,XBOOLE_0:def 2;
       suppose A7:inspos n in dom I;
           then I.inspos n=i by A2,A5,Th37;
         hence InsCode i <> 1 & InsCode i <> 3 & i valid_at n by A7,Def12;
       suppose inspos n in D;
        then consider l such that
A8:      inspos n = inspos(l+card I) and
A9:      inspos l in dom J;
A10:    J=inspos 0 .--> ii by Def1;
       then dom J = { inspos 0 } by CQC_LANG:5;
then A11:    inspos l = inspos 0 by A9,TARSKI:def 1;
then A12:    ii =J.inspos l by A10,CQC_LANG:6
       .=Ig.(inspos l+card I) by A2,A9,Th38
       .=i by A5,A8,SCMPDS_3:def 3;
       hence InsCode i <> 1 & InsCode i <> 3 by SCMPDS_2:27;
         inspos n= inspos(0+card I) by A8,A11,SCMPDS_3:31;
then A13:    n+k2 >=0 by A1,SCMPDS_3:31;
     InsCode i <> 0 & InsCode i <> 4 & InsCode i <> 5 by A12,SCMPDS_2:27;
       hence i valid_at n by A12,A13,Def11;
    end;
   hence thesis by Def12;
end;

definition
  let k1 be Integer,a be Int_position,n be Nat;
  cluster Load (a,k1)>=0_goto n -> shiftable;
  coherence
  proof
   set k2=n;
   set ii= (a,k1)>=0_goto k2,
       J= Load ii;
     now let n,i such that
A1:    inspos n in dom J and
A2:    i=J.inspos n;
A3:    J=inspos 0 .--> ii by Def1;
       then dom J = { inspos 0 } by CQC_LANG:5;
then inspos n = inspos 0 by A1,TARSKI:def 1;
then A4:    ii =i by A2,A3,CQC_LANG:6;
       hence InsCode i <> 1 & InsCode i <> 3 by SCMPDS_2:27;
A5:    n+k2 >=0 by NAT_1:18;
     InsCode i <> 0 & InsCode i <> 4 & InsCode i <> 5 by A4,SCMPDS_2:27;
       hence i valid_at n by A4,A5,Def11;
    end;
   hence thesis by Def12;
   end;
end;

theorem Th82:
 for s1,s2 being State of SCMPDS, n,m being Nat,k1 be Integer st
     IC s1=inspos m & m+k1>=0 & IC s1 + n = IC s2
holds ICplusConst(s1,k1) +n = ICplusConst(s2,k1)
proof
   let s1,s2 be State of SCMPDS, n,m be Nat,k1 be Integer;
   assume that
A1: IC s1=inspos m and
A2: m+k1>=0 and
A3: IC s1 + n = IC s2;
    consider n1 be Nat such that
A4: n1 = IC s1 & ICplusConst(s1,k1) = abs(n1-2+2*k1)+2 by SCMPDS_2:def 20;
    consider n2 be Nat such that
A5: n2 = IC s2 & ICplusConst(s2,k1) = abs(n2-2+2*k1)+2 by SCMPDS_2:def 20;
    reconsider mk=m+k1 as Nat by A2,INT_1:16;
A6: 2*mk >= 0 by NAT_1:18;
A7: 2*mk + 2*n >= 0 by NAT_1:18;
A8: n2=inspos ( m + n) by A1,A3,A5,SCMPDS_3:def 3
    .=il.(m+n) by SCMPDS_3:def 2
    .=2*(m+n)+2 by AMI_3:def 20;
    consider nk be Nat such that
A9: inspos nk=ICplusConst(s1,k1) by SCMPDS_3:32;
A10: n1=il.m by A1,A4,SCMPDS_3:def 2
    .=2*m+2 by AMI_3:def 20;
      2*nk+2=il.nk by AMI_3:def 20
    .=abs(n1-2+2*k1)+2 by A4,A9,SCMPDS_3:def 2;
then A11: 2*nk=abs(2*m+2-2+2*k1) by A10,XCMPLX_1:2
    .=abs(2*m+2*k1) by XCMPLX_1:26
    .=abs(2*mk) by XCMPLX_1:8
    .=2*mk by A6,ABSVALUE:def 1;
    thus ICplusConst(s1,k1) +n=inspos(nk +n) by A9,SCMPDS_3:def 3
    .=il.(nk+n) by SCMPDS_3:def 2
    .=2*(nk+n)+2 by AMI_3:def 20
    .=2*mk+2*n+2 by A11,XCMPLX_1:8
    .=abs(2*mk+2*n)+2 by A7,ABSVALUE:def 1
    .=abs(2*m+2*k1+2*n)+2 by XCMPLX_1:8
    .=abs(2*m+2*n+2*k1)+2 by XCMPLX_1:1
    .=abs(2*(m+n)+2*k1)+2 by XCMPLX_1:8
    .=ICplusConst(s2,k1) by A5,A8,XCMPLX_1:26;
end;

theorem Th83:  ::S6A_41
 for s1,s2 being State of SCMPDS, n,m being Nat,
     i being Instruction of SCMPDS holds
     IC s1=inspos m & i valid_at m & InsCode i <> 1 & InsCode i <> 3 &
     IC s1 + n = IC s2 &
     s1 | SCM-Data-Loc = s2 | SCM-Data-Loc
 implies
     IC Exec(i,s1) + n = IC Exec(i,s2) &
     Exec(i,s1) | SCM-Data-Loc = Exec(i,s2) | SCM-Data-Loc
proof
   let s1,s2 be State of SCMPDS, n ,m be Nat;
   let i be Instruction of SCMPDS; assume that
A1: IC s1=inspos m and
A2: i valid_at m and
A3: InsCode i <> 1 and
A4: InsCode i <> 3 and
A5: IC s1 + n = IC s2 and
A6:s1 | SCM-Data-Loc = s2 | SCM-Data-Loc;
   set D = SCM-Data-Loc;
   consider k1 being Nat such that
A7: IC s1 = inspos k1 by SCMPDS_3:32;
A8: Next IC s1 + n = Next IC s2
    proof
      thus Next IC s1 + n = inspos (k1 + 1) + n by A7,Th70
      .= inspos (k1 + 1 + n) by SCMPDS_3:def 3
      .= inspos (k1 + n + 1) by XCMPLX_1:1
      .= Next inspos (k1 + n) by Th70
      .= Next (IC s2) by A5,A7,SCMPDS_3:def 3;
    end;
    set Ci=InsCode i;
A9:now assume
         Ci <> 0 & Ci<>1 & Ci<>4 & Ci<>5 & Ci<> 6;
      then A10: not Ci in {0,1,4,5,6} by ENUMSET1:23;
        IC Exec(i,s1) = Exec(i,s1).IC SCMPDS by AMI_1:def 15
      .= Next IC s1 by A10,Th6;
      hence IC Exec(i,s1) + n = Exec(i,s2).IC SCMPDS by A8,A10,Th6
      .= IC Exec(i,s2) by AMI_1:def 15;
    end;
A11: now let a,k1;
        thus s1.DataLoc(s1.a,k1) =s1.DataLoc(s2.a,k1) by A6,Th23
        .=s2.DataLoc(s2.a,k1) by A6,Th23;
    end;
A12: Ci <= 13 by SCMPDS_2:15;
   per cases by A3,A4,A12,SCMPDS_3:1;
   suppose Ci = 0;
    then consider k1 such that
A13:  i = goto k1 & m+k1 >= 0 by A2,Def11;
A14: now let a;
        thus Exec(i, s1).a = s1.a by A13,SCMPDS_2:66
        .=s2.a by A6,Th23
        .=Exec(i, s2).a by A13,SCMPDS_2:66;
     end;
       IC Exec(i,s1) = (Exec(i,s1).IC SCMPDS) by AMI_1:def 15
        .= ICplusConst(s1,k1) by A13,SCMPDS_2:66;
     hence IC Exec(i,s1) + n = ICplusConst(s2,k1) by A1,A5,A13,Th82
        .= Exec(i,s2).IC SCMPDS by A13,SCMPDS_2:66
        .= IC Exec(i,s2) by AMI_1:def 15;
     thus Exec(i,s1) | D = Exec(i,s2) | D by A14,Th23;

   suppose A15: Ci = 2;
    then consider a,k1 such that
A16:   i = a := k1 by SCMPDS_2:37;
A17:  now let b;
         per cases;
         suppose A18:a=b;
          hence Exec(i, s1).b= k1 by A16,SCMPDS_2:57
          .=Exec(i,s2).b by A16,A18,SCMPDS_2:57;
         suppose A19:a<>b;
          hence Exec(i,s1).b = s1.b by A16,SCMPDS_2:57
          .=s2.b by A6,Th23
          .=Exec(i,s2).b by A16,A19,SCMPDS_2:57;
     end;
     thus IC Exec(i,s1) + n = IC Exec(i,s2) by A9,A15;
     thus Exec(i,s1) | D = Exec(i,s2) | D by A17,Th23;

   suppose Ci = 4;
    then consider a,k1,k2 such that
A20:  i = (a,k1)<>0_goto k2 & m+k2 >= 0 by A2,Def11;
A21: now let a;
        thus Exec(i, s1).a = s1.a by A20,SCMPDS_2:67
        .=s2.a by A6,Th23
        .=Exec(i, s2).a by A20,SCMPDS_2:67;
     end;
     hereby
       per cases;
       suppose A22:s1.DataLoc(s1.a,k1) <> 0;
         then A23:s2.DataLoc(s2.a,k1) <> 0 by A11;
          IC Exec(i,s1) = (Exec(i,s1).IC SCMPDS) by AMI_1:def 15
        .= ICplusConst(s1,k2) by A20,A22,SCMPDS_2:67;
        hence IC Exec(i,s1) + n = ICplusConst(s2,k2) by A1,A5,A20,Th82
        .= Exec(i,s2).IC SCMPDS by A20,A23,SCMPDS_2:67
        .= IC Exec(i,s2) by AMI_1:def 15;
       suppose A24:s1.DataLoc(s1.a,k1) = 0;
         then A25:s2.DataLoc(s2.a,k1) = 0 by A11;
          IC Exec(i,s1) = (Exec(i,s1).IC SCMPDS) by AMI_1:def 15
        .= Next IC s1 by A20,A24,SCMPDS_2:67;
        hence IC Exec(i,s1) + n = Exec(i,s2).IC SCMPDS by A8,A20,A25,SCMPDS_2:
67
         .= IC Exec(i,s2) by AMI_1:def 15;
     end;
     thus Exec(i,s1) | D = Exec(i,s2) | D by A21,Th23;

   suppose Ci = 5;
    then consider a,k1,k2 such that
A26:  i = (a,k1)<=0_goto k2 & m+k2 >= 0 by A2,Def11;
A27: now let a;
        thus Exec(i, s1).a = s1.a by A26,SCMPDS_2:68
        .=s2.a by A6,Th23
        .=Exec(i, s2).a by A26,SCMPDS_2:68;
     end;
     hereby
       per cases;
       suppose A28:s1.DataLoc(s1.a,k1) <= 0;
         then A29:s2.DataLoc(s2.a,k1) <= 0 by A11;
          IC Exec(i,s1) = (Exec(i,s1).IC SCMPDS) by AMI_1:def 15
        .= ICplusConst(s1,k2) by A26,A28,SCMPDS_2:68;
        hence IC Exec(i,s1) + n = ICplusConst(s2,k2) by A1,A5,A26,Th82
        .= Exec(i,s2).IC SCMPDS by A26,A29,SCMPDS_2:68
        .= IC Exec(i,s2) by AMI_1:def 15;
       suppose A30:s1.DataLoc(s1.a,k1) > 0;
         then A31:s2.DataLoc(s2.a,k1) > 0 by A11;
          IC Exec(i,s1) = (Exec(i,s1).IC SCMPDS) by AMI_1:def 15
        .= Next IC s1 by A26,A30,SCMPDS_2:68;
        hence IC Exec(i,s1) + n = Exec(i,s2).IC SCMPDS by A8,A26,A31,SCMPDS_2:
68
         .= IC Exec(i,s2) by AMI_1:def 15;
     end;
     thus Exec(i,s1) | D = Exec(i,s2) | D by A27,Th23;

   suppose Ci = 6;
    then consider a,k1,k2 such that
A32:  i = (a,k1)>=0_goto k2 & m+k2 >= 0 by A2,Def11;
A33: now let a;
        thus Exec(i, s1).a = s1.a by A32,SCMPDS_2:69
        .=s2.a by A6,Th23
        .=Exec(i, s2).a by A32,SCMPDS_2:69;
     end;
     hereby
       per cases;
       suppose A34:s1.DataLoc(s1.a,k1) >= 0;
         then A35:s2.DataLoc(s2.a,k1) >= 0 by A11;
          IC Exec(i,s1) = (Exec(i,s1).IC SCMPDS) by AMI_1:def 15
        .= ICplusConst(s1,k2) by A32,A34,SCMPDS_2:69;
        hence IC Exec(i,s1) + n = ICplusConst(s2,k2) by A1,A5,A32,Th82
        .= Exec(i,s2).IC SCMPDS by A32,A35,SCMPDS_2:69
        .= IC Exec(i,s2) by AMI_1:def 15;
       suppose A36:s1.DataLoc(s1.a,k1) < 0;
         then A37:s2.DataLoc(s2.a,k1) < 0 by A11;
          IC Exec(i,s1) = (Exec(i,s1).IC SCMPDS) by AMI_1:def 15
        .= Next IC s1 by A32,A36,SCMPDS_2:69;
        hence IC Exec(i,s1) + n = Exec(i,s2).IC SCMPDS by A8,A32,A37,SCMPDS_2:
69
         .= IC Exec(i,s2) by AMI_1:def 15;
     end;
     thus Exec(i,s1) | D = Exec(i,s2) | D by A33,Th23;

    suppose A38: Ci = 7;
    then consider a,k1,k2 such that
A39:   i = (a,k1) := k2 by SCMPDS_2:42;
A40:  now let b;
         per cases;
         suppose A41:DataLoc(s1.a,k1)=b;
         then A42: DataLoc(s2.a,k1)=b by A6,Th23;
          thus Exec(i, s1).b= k2 by A39,A41,SCMPDS_2:58
          .=Exec(i,s2).b by A39,A42,SCMPDS_2:58;
         suppose A43:DataLoc(s1.a,k1)<>b;
         then A44: DataLoc(s2.a,k1)<>b by A6,Th23;
          thus Exec(i,s1).b = s1.b by A39,A43,SCMPDS_2:58
          .=s2.b by A6,Th23
          .=Exec(i,s2).b by A39,A44,SCMPDS_2:58;
     end;
     thus IC Exec(i,s1) + n = IC Exec(i,s2) by A9,A38;
     thus Exec(i,s1) | D = Exec(i,s2) | D by A40,Th23;

    suppose A45: Ci = 8;
    then consider a,k1,k2 such that
A46:   i = AddTo(a,k1,k2) by SCMPDS_2:43;
A47:  now let b;
         per cases;
         suppose A48:DataLoc(s1.a,k1)=b;
         then A49: DataLoc(s2.a,k1)=b by A6,Th23;
          thus Exec(i, s1).b= s1.DataLoc(s1.a,k1)+k2 by A46,A48,SCMPDS_2:60
          .= s2.DataLoc(s2.a,k1)+k2 by A11
          .=Exec(i,s2).b by A46,A49,SCMPDS_2:60;
         suppose A50:DataLoc(s1.a,k1)<>b;
         then A51: DataLoc(s2.a,k1)<>b by A6,Th23;
          thus Exec(i,s1).b = s1.b by A46,A50,SCMPDS_2:60
          .=s2.b by A6,Th23
          .=Exec(i,s2).b by A46,A51,SCMPDS_2:60;
     end;
     thus IC Exec(i,s1) + n = IC Exec(i,s2) by A9,A45;
     thus Exec(i,s1) | D = Exec(i,s2) | D by A47,Th23;

    suppose A52: Ci = 9;
    then consider a,b,k1,k2 such that
A53:   i = AddTo(a,k1,b,k2) by SCMPDS_2:44;
A54:  now let c;
         per cases;
         suppose A55:DataLoc(s1.a,k1)=c;
         then A56: DataLoc(s2.a,k1)=c by A6,Th23;
          thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)+s1.DataLoc(s1.b,k2)
             by A53,A55,SCMPDS_2:61
          .= s2.DataLoc(s2.a,k1)+s1.DataLoc(s1.b,k2) by A11
          .= s2.DataLoc(s2.a,k1)+s2.DataLoc(s2.b,k2) by A11
          .=Exec(i,s2).c by A53,A56,SCMPDS_2:61;
         suppose A57:DataLoc(s1.a,k1)<>c;
         then A58: DataLoc(s2.a,k1)<>c by A6,Th23;
          thus Exec(i,s1).c = s1.c by A53,A57,SCMPDS_2:61
          .=s2.c by A6,Th23
          .=Exec(i,s2).c by A53,A58,SCMPDS_2:61;
     end;
     thus IC Exec(i,s1) + n = IC Exec(i,s2) by A9,A52;
     thus Exec(i,s1) | D = Exec(i,s2) | D by A54,Th23;

    suppose A59: Ci = 10;
    then consider a,b,k1,k2 such that
A60:   i = SubFrom(a,k1,b,k2) by SCMPDS_2:45;
A61:  now let c;
         per cases;
         suppose A62:DataLoc(s1.a,k1)=c;
         then A63: DataLoc(s2.a,k1)=c by A6,Th23;
          thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)-s1.DataLoc(s1.b,k2)
             by A60,A62,SCMPDS_2:62
          .= s2.DataLoc(s2.a,k1)-s1.DataLoc(s1.b,k2) by A11
          .= s2.DataLoc(s2.a,k1)-s2.DataLoc(s2.b,k2) by A11
          .=Exec(i,s2).c by A60,A63,SCMPDS_2:62;
         suppose A64:DataLoc(s1.a,k1)<>c;
         then A65: DataLoc(s2.a,k1)<>c by A6,Th23;
          thus Exec(i,s1).c = s1.c by A60,A64,SCMPDS_2:62
          .=s2.c by A6,Th23
          .=Exec(i,s2).c by A60,A65,SCMPDS_2:62;
     end;
     thus IC Exec(i,s1) + n = IC Exec(i,s2) by A9,A59;
     thus Exec(i,s1) | D = Exec(i,s2) | D by A61,Th23;

    suppose A66: Ci = 11;
    then consider a,b,k1,k2 such that
A67:   i = MultBy(a,k1,b,k2) by SCMPDS_2:46;
A68:  now let c;
         per cases;
         suppose A69:DataLoc(s1.a,k1)=c;
         then A70: DataLoc(s2.a,k1)=c by A6,Th23;
          thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)*s1.DataLoc(s1.b,k2)
             by A67,A69,SCMPDS_2:63
          .= s2.DataLoc(s2.a,k1)*s1.DataLoc(s1.b,k2) by A11
          .= s2.DataLoc(s2.a,k1)*s2.DataLoc(s2.b,k2) by A11
          .=Exec(i,s2).c by A67,A70,SCMPDS_2:63;
         suppose A71:DataLoc(s1.a,k1)<>c;
         then A72: DataLoc(s2.a,k1)<>c by A6,Th23;
          thus Exec(i,s1).c = s1.c by A67,A71,SCMPDS_2:63
          .=s2.c by A6,Th23
          .=Exec(i,s2).c by A67,A72,SCMPDS_2:63;
     end;
     thus IC Exec(i,s1) + n = IC Exec(i,s2) by A9,A66;
     thus Exec(i,s1) | D = Exec(i,s2) | D by A68,Th23;

    suppose A73: Ci = 12;
    then consider a,b,k1,k2 such that
A74:   i = Divide(a,k1,b,k2) by SCMPDS_2:47;
A75:  now let c;
         per cases;
         suppose A76:DataLoc(s1.b,k2)=c;
         then A77: DataLoc(s2.b,k2)=c by A6,Th23;
          thus Exec(i, s1).c = s1.DataLoc(s1.a,k1) mod s1.DataLoc(s1.b,k2)
             by A74,A76,SCMPDS_2:64
          .= s2.DataLoc(s2.a,k1) mod s1.DataLoc(s1.b,k2) by A11
          .= s2.DataLoc(s2.a,k1) mod s2.DataLoc(s2.b,k2) by A11
          .= Exec(i,s2).c by A74,A77,SCMPDS_2:64;
         suppose A78:DataLoc(s1.b,k2)<>c;
         then A79: DataLoc(s2.b,k2)<>c by A6,Th23;
           hereby
             per cases;
             suppose A80:DataLoc(s1.a,k1)<>c;
             then A81: DataLoc(s2.a,k1)<>c by A6,Th23;
            thus Exec(i, s1).c = s1.c by A74,A78,A80,SCMPDS_2:64
                .=s2.c by A6,Th23
                .=Exec(i,s2).c by A74,A79,A81,SCMPDS_2:64;
             suppose A82:DataLoc(s1.a,k1)=c;
              then A83: DataLoc(s2.a,k1)=c by A6,Th23;
             thus Exec(i, s1).c = s1.DataLoc(s1.a,k1) div s1.DataLoc(s1.b,k2)
               by A74,A78,A82,SCMPDS_2:64
             .= s2.DataLoc(s2.a,k1) div s1.DataLoc(s1.b,k2) by A11
             .= s2.DataLoc(s2.a,k1) div s2.DataLoc(s2.b,k2) by A11
             .= Exec(i,s2).c by A74,A79,A83,SCMPDS_2:64;
           end;
     end;
     thus IC Exec(i,s1) + n = IC Exec(i,s2) by A9,A73;
     thus Exec(i,s1) | D = Exec(i,s2) | D by A75,Th23;

    suppose A84: Ci = 13;
    then consider a,b,k1,k2 such that
A85:   i = (a,k1):=(b,k2) by SCMPDS_2:48;
A86:  now let c;
         per cases;
         suppose A87:DataLoc(s1.a,k1)=c;
         then A88: DataLoc(s2.a,k1)=c by A6,Th23;
          thus Exec(i, s1).c = s1.DataLoc(s1.b,k2) by A85,A87,SCMPDS_2:59
          .= s2.DataLoc(s2.b,k2) by A11
          .=Exec(i,s2).c by A85,A88,SCMPDS_2:59;
         suppose A89:DataLoc(s1.a,k1)<>c;
         then A90: DataLoc(s2.a,k1)<>c by A6,Th23;
          thus Exec(i,s1).c = s1.c by A85,A89,SCMPDS_2:59
          .=s2.c by A6,Th23
          .=Exec(i,s2).c by A85,A90,SCMPDS_2:59;
     end;
     thus IC Exec(i,s1) + n = IC Exec(i,s2) by A9,A84;
     thus Exec(i,s1) | D = Exec(i,s2) | D by A86,Th23;
end;

theorem  ::Th27 T0
   for J being parahalting shiftable Program-block st Initialized stop J c= s1
 for n being Nat st Shift(stop J,n) c= s2 &
   IC s2 = inspos n &
   s1 | SCM-Data-Loc = s2 | SCM-Data-Loc
   for i being Nat holds
     IC (Computation s1).i + n = IC (Computation s2).i &
     CurInstr ((Computation s1).i) = CurInstr ((Computation s2).i) &
     (Computation s1).i | SCM-Data-Loc = (Computation s2).i | SCM-Data-Loc
proof
   let I be parahalting shiftable Program-block;
   set SI=stop I,
       II = Initialized SI;
    assume
A1: II c= s1;
   let n be Nat; assume that
A2: Shift(SI,n) c= s2 and
A3: IC s2 = inspos n and
A4: s1 | SCM-Data-Loc = s2 | SCM-Data-Loc;
   set C1 = Computation s1;
   set C2 = Computation s2;
   let i be Nat;
   defpred P[Nat] means
       IC C1.$1 + n = IC C2.$1 &
       CurInstr (C1.$1) = CurInstr (C2.$1) &
       C1.$1 | SCM-Data-Loc = C2.$1 | SCM-Data-Loc;
A5: II= SI +* Start-At inspos 0 by Def2;
       dom SI misses dom Start-At inspos 0 by Th54;
then A6:  SI c= II by A5,FUNCT_4:33;
then A7: dom SI c= dom II by GRFUNC_1:8;
A8: inspos 0 in dom SI by Th75;
A9: P[0]
    proof
A10:  IC SCMPDS in dom II by Th7;
       inspos 0 + n in dom Shift(SI,n) by A8,Th76;
then A11:  inspos (0 + n) in dom Shift(SI,n) by SCMPDS_3:def 3;
       IC C1.0 = IC s1 by AMI_1:def 19
    .= s1.IC SCMPDS by AMI_1:def 15
    .= II.IC SCMPDS by A1,A10,GRFUNC_1:8
    .= inspos 0 by Th29;
   hence IC C1.0 + n = inspos (0 + n) by SCMPDS_3:def 3
      .= IC C2.0 by A3,AMI_1:def 19;
A12: s1.IC s1 = s1.(s1.IC SCMPDS) by AMI_1:def 15
      .= s1.((II).IC SCMPDS) by A1,A10,GRFUNC_1:8
      .= s1.inspos 0 by Th29
      .= II.inspos 0 by A1,A7,A8,GRFUNC_1:8
      .= SI.inspos 0 by A6,A8,GRFUNC_1:8;
    thus CurInstr (C1.0)
       = CurInstr s1 by AMI_1:def 19
      .= s1.IC s1 by AMI_1:def 17
      .= Shift(SI,n).(inspos 0 + n) by A8,A12,SCMPDS_3:37
      .= Shift(SI,n).inspos (0 + n) by SCMPDS_3:def 3
      .= s2.IC s2 by A2,A3,A11,GRFUNC_1:8
      .= CurInstr s2 by AMI_1:def 17
      .= CurInstr (C2.0) by AMI_1:def 19;
  thus C1.0 | SCM-Data-Loc
       = s2 | SCM-Data-Loc by A4,AMI_1:def 19
      .= C2.0 | SCM-Data-Loc by AMI_1:def 19;
     end;
A13: for k being Nat st P[k] holds P[k + 1]
     proof
       let k be Nat;
       assume A14: P[k];
      set i = CurInstr C1.k;
  A15: C1.(k + 1) = Following C1.k by AMI_1:def 19
      .= Exec(CurInstr C1.k,C1.k) by AMI_1:def 18;
  A16: C2.(k + 1) = Following C2.k by AMI_1:def 19
      .= Exec(CurInstr C2.k,C2.k) by AMI_1:def 18;

   A17: IC C1.k in dom SI by A1,Def9;
   A18: i = C1.k.(IC C1.k) by AMI_1:def 17
      .= s1.IC C1.k by AMI_1:54
      .= II.IC C1.k by A1,A7,A17,GRFUNC_1:8
      .= SI.IC C1.k by A6,A17,GRFUNC_1:8;
       consider m such that
   A19: IC C1.k =inspos m by SCMPDS_3:32;
   A20: InsCode i <> 1 & InsCode i <> 3 & i valid_at m by A17,A18,A19,Def12;
  hence A21: IC C1.(k + 1) + n
       = IC C2.(k + 1) by A14,A15,A16,A19,Th83;
      set l = IC C1.(k + 1);
   A22: IC C1.(k + 1) in dom SI by A1,Def9;
   A23: CurInstr C1.(k + 1) = C1.(k + 1).l by AMI_1:def 17
      .= s1.l by AMI_1:54
      .= II.l by A1,A7,A22,GRFUNC_1:8
      .= SI.l by A6,A22,GRFUNC_1:8;
   A24: IC C2.(k + 1) in dom Shift(SI,n) by A21,A22,Th76;
      thus CurInstr C1.(k + 1)
       = Shift(SI,n).(IC C2.(k + 1)) by A21,A22,A23,SCMPDS_3:37
      .= s2.IC C2.(k + 1) by A2,A24,GRFUNC_1:8
      .= C2.(k + 1).IC C2.(k + 1) by AMI_1:54
      .= CurInstr C2.(k + 1) by AMI_1:def 17;
      thus C1.(k + 1) | SCM-Data-Loc
       = C2.(k + 1) | SCM-Data-Loc by A14,A15,A16,A19,A20,Th83;
     end;
     for k being Nat holds P[k] from Ind(A9,A13);
   hence thesis;
end;


Back to top