ami_5.miz



    begin

    reserve x,y for set;

    theorem :: AMI_5:1

    

     Th1: for dl be Data-Location holds ex i be Nat st dl = ( dl. i)

    proof

      let dl be Data-Location;

      dl in ( Data-Locations SCM ) by AMI_2:def 16, AMI_3: 27;

      then

      consider x,y be object such that

       A1: x in {1} and

       A2: y in NAT and

       A3: dl = [x, y] by AMI_3: 27, ZFMISC_1: 84;

      reconsider k = y as Nat by A2;

      take k;

      thus thesis by A1, A3, TARSKI:def 1;

    end;

    theorem :: AMI_5:2

    

     Th2: for dl be Data-Location holds dl <> ( IC SCM ) by Th1, AMI_3: 13;

    theorem :: AMI_5:3

    for il be Nat, dl be Data-Location holds il <> dl

    proof

      let il be Nat, dl be Data-Location;

      ex j be Nat st dl = ( dl. j) by Th1;

      hence thesis;

    end;

    reserve i,j,k for Nat;

    theorem :: AMI_5:4

    for s be State of SCM , d be Data-Location holds d in ( dom s)

    proof

      let s be State of SCM , d be Data-Location;

      

       A1: ( dom s) = the carrier of SCM by PARTFUN1:def 2;

      thus d in ( dom s) by A1;

    end;

    registration

      cluster ( Data-Locations SCM ) -> infinite;

      coherence by AMI_3: 27;

    end

    reserve I,J,K for Element of ( Segm 9),

a,a1 for Nat,

b,b1,c for Element of ( Data-Locations SCM );

    

     Lm1: b is Data-Location

    proof

      b in ( Data-Locations SCM );

      then

      reconsider b as Object of SCM ;

      b is Data-Location by AMI_2:def 16, AMI_3: 27;

      hence thesis;

    end;

    theorem :: AMI_5:5

    for l be Instruction of SCM holds ( InsCode l) <= 8

    proof

      let l be Instruction of SCM ;

      l in (( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) \/ { [K, <*a1*>, <*b1*>] : K in {7, 8} }) or l in { [I, {} , <*b, c*>] : I in {1, 2, 3, 4, 5} } by AMI_3: 27, XBOOLE_0:def 3;

      then

       A1: l in ( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) or l in { [K, <*a1*>, <*b1*>] : K in {7, 8} } or l in { [I, {} , <*b, c*>] : I in {1, 2, 3, 4, 5} } by XBOOLE_0:def 3;

      per cases by A1, XBOOLE_0:def 3;

        suppose l in { [ SCM-Halt , {} , {} ]};

        then l = [ SCM-Halt , {} , {} ] by TARSKI:def 1;

        then (l `1_3 ) = 0 ;

        hence thesis;

      end;

        suppose l in { [J, <*a*>, {} ] : J = 6 };

        then ex J, a st l = [J, <*a*>, {} ] & J = 6;

        then (l `1_3 ) = 6;

        hence thesis;

      end;

        suppose l in { [K, <*a1*>, <*b1*>] : K in {7, 8} };

        then ex K, a1, b1 st l = [K, <*a1*>, <*b1*>] & K in {7, 8};

        then (l `1_3 ) in {7, 8};

        then (l `1_3 ) = 7 or (l `1_3 ) = 8 by TARSKI:def 2;

        hence thesis;

      end;

        suppose l in { [I, {} , <*b, c*>] : I in {1, 2, 3, 4, 5} };

        then ex I, b, c st l = [I, {} , <*b, c*>] & I in {1, 2, 3, 4, 5};

        then (l `1_3 ) in {1, 2, 3, 4, 5};

        then (l `1_3 ) = 1 or (l `1_3 ) = 2 or (l `1_3 ) = 3 or (l `1_3 ) = 4 or (l `1_3 ) = 5 by ENUMSET1:def 3;

        hence thesis;

      end;

    end;

    reserve a,b for Data-Location,

loc for Nat;

    reserve I,J,K for Element of ( Segm 9),

a,a1 for Nat,

b,b1,c for Element of ( Data-Locations SCM ),

da,db for Data-Location;

    ::$Canceled

    theorem :: AMI_5:7

    for ins be Instruction of SCM st ( InsCode ins) = 0 holds ins = ( halt SCM )

    proof

      let ins be Instruction of SCM such that

       A1: ( InsCode ins) = 0 ;

       A2:

      now

        assume ins in { [J, <*a*>, {} ] : J = 6 };

        then ex J, a st ins = [J, <*a*>, {} ] & J = 6;

        then ( InsCode ins) = 6;

        hence contradiction by A1;

      end;

      now

        assume ins in { [I, {} , <*b, c*>] : I in {1, 2, 3, 4, 5} };

        then ex I, b, c st ins = [I, {} , <*b, c*>] & I in {1, 2, 3, 4, 5};

        then ( InsCode ins) in {1, 2, 3, 4, 5};

        hence contradiction by A1, ENUMSET1:def 3;

      end;

      then

       A3: ins in (( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) \/ { [K, <*a1*>, <*b1*>] : K in {7, 8} }) by AMI_3: 27, XBOOLE_0:def 3;

      now

        assume ins in { [K, <*a1*>, <*b1*>] : K in {7, 8} };

        then ex K, a1, b1 st ins = [K, <*a1*>, <*b1*>] & K in {7, 8};

        then ( InsCode ins) in {7, 8};

        hence contradiction by A1, TARSKI:def 2;

      end;

      then ins in ( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) by A3, XBOOLE_0:def 3;

      then ins in { [ SCM-Halt , {} , {} ]} by A2, XBOOLE_0:def 3;

      then ins = [ SCM-Halt , {} , {} ] by TARSKI:def 1;

      hence thesis by AMI_3: 26;

    end;

    theorem :: AMI_5:8

    for ins be Instruction of SCM st ( InsCode ins) = 1 holds ex da, db st ins = (da := db)

    proof

      let ins be Instruction of SCM such that

       A1: ( InsCode ins) = 1;

       A2:

      now

        assume ins in { [J, <*a*>, {} ] : J = 6 };

        then ex J, a st ins = [J, <*a*>, {} ] & J = 6;

        hence contradiction by A1;

      end;

       A3:

      now

        assume ins in { [K, <*a1*>, <*b1*>] : K in {7, 8} };

        then

        consider K, a1, b1 such that

         A4: ins = [K, <*a1*>, <*b1*>] and

         A5: K in {7, 8};

        ( InsCode ins) = K by A4;

        hence contradiction by A1, A5, TARSKI:def 2;

      end;

      ( InsCode ( halt SCM )) = 0 by COMPOS_1: 70;

      then not ins in { [ SCM-Halt , {} , {} ]} by A1, AMI_3: 26, TARSKI:def 1;

      then not ins in ( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) by A2, XBOOLE_0:def 3;

      then not ins in (( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) \/ { [K, <*a1*>, <*b1*>] : K in {7, 8} }) by A3, XBOOLE_0:def 3;

      then ins in { [I, {} , <*b, c*>] : I in {1, 2, 3, 4, 5} } by AMI_3: 27, XBOOLE_0:def 3;

      then

      consider I, b, c such that

       A6: ins = [I, {} , <*b, c*>] and I in {1, 2, 3, 4, 5};

      reconsider da = b, db = c as Data-Location by Lm1;

      take da, db;

      thus thesis by A1, A6;

    end;

    theorem :: AMI_5:9

    for ins be Instruction of SCM st ( InsCode ins) = 2 holds ex da, db st ins = ( AddTo (da,db))

    proof

      let ins be Instruction of SCM such that

       A1: ( InsCode ins) = 2;

       A2:

      now

        assume ins in { [J, <*a*>, {} ] : J = 6 };

        then ex J, a st ins = [J, <*a*>, {} ] & J = 6;

        hence contradiction by A1;

      end;

       A3:

      now

        assume ins in { [K, <*a1*>, <*b1*>] : K in {7, 8} };

        then

        consider K, a1, b1 such that

         A4: ins = [K, <*a1*>, <*b1*>] and

         A5: K in {7, 8};

        ( InsCode ins) = K by A4;

        hence contradiction by A1, A5, TARSKI:def 2;

      end;

      ( InsCode ( halt SCM )) = 0 by COMPOS_1: 70;

      then not ins in { [ SCM-Halt , {} , {} ]} by A1, AMI_3: 26, TARSKI:def 1;

      then not ins in ( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) by A2, XBOOLE_0:def 3;

      then not ins in (( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) \/ { [K, <*a1*>, <*b1*>] : K in {7, 8} }) by A3, XBOOLE_0:def 3;

      then ins in { [I, {} , <*b, c*>] : I in {1, 2, 3, 4, 5} } by AMI_3: 27, XBOOLE_0:def 3;

      then

      consider I, b, c such that

       A6: ins = [I, {} , <*b, c*>] and I in {1, 2, 3, 4, 5};

      reconsider da = b, db = c as Data-Location by Lm1;

      take da, db;

      thus thesis by A1, A6;

    end;

    theorem :: AMI_5:10

    for ins be Instruction of SCM st ( InsCode ins) = 3 holds ex da, db st ins = ( SubFrom (da,db))

    proof

      let ins be Instruction of SCM such that

       A1: ( InsCode ins) = 3;

       A2:

      now

        assume ins in { [J, <*a*>, {} ] : J = 6 };

        then ex J, a st ins = [J, <*a*>, {} ] & J = 6;

        hence contradiction by A1;

      end;

       A3:

      now

        assume ins in { [K, <*a1*>, <*b1*>] : K in {7, 8} };

        then

        consider K, a1, b1 such that

         A4: ins = [K, <*a1*>, <*b1*>] and

         A5: K in {7, 8};

        ( InsCode ins) = K by A4;

        hence contradiction by A1, A5, TARSKI:def 2;

      end;

      ( InsCode ( halt SCM )) = 0 by COMPOS_1: 70;

      then not ins in { [ SCM-Halt , {} , {} ]} by A1, AMI_3: 26, TARSKI:def 1;

      then not ins in ( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) by A2, XBOOLE_0:def 3;

      then not ins in (( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) \/ { [K, <*a1*>, <*b1*>] : K in {7, 8} }) by A3, XBOOLE_0:def 3;

      then ins in { [I, {} , <*b, c*>] : I in {1, 2, 3, 4, 5} } by AMI_3: 27, XBOOLE_0:def 3;

      then

      consider I, b, c such that

       A6: ins = [I, {} , <*b, c*>] and I in {1, 2, 3, 4, 5};

      reconsider da = b, db = c as Data-Location by Lm1;

      take da, db;

      thus thesis by A1, A6;

    end;

    theorem :: AMI_5:11

    for ins be Instruction of SCM st ( InsCode ins) = 4 holds ex da, db st ins = ( MultBy (da,db))

    proof

      let ins be Instruction of SCM such that

       A1: ( InsCode ins) = 4;

       A2:

      now

        assume ins in { [J, <*a*>, {} ] : J = 6 };

        then ex J, a st ins = [J, <*a*>, {} ] & J = 6;

        hence contradiction by A1;

      end;

       A3:

      now

        assume ins in { [K, <*a1*>, <*b1*>] : K in {7, 8} };

        then

        consider K, a1, b1 such that

         A4: ins = [K, <*a1*>, <*b1*>] and

         A5: K in {7, 8};

        ( InsCode ins) = K by A4;

        hence contradiction by A1, A5, TARSKI:def 2;

      end;

      ( InsCode ( halt SCM )) = 0 by COMPOS_1: 70;

      then not ins in { [ SCM-Halt , {} , {} ]} by A1, AMI_3: 26, TARSKI:def 1;

      then not ins in ( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) by A2, XBOOLE_0:def 3;

      then not ins in (( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) \/ { [K, <*a1*>, <*b1*>] : K in {7, 8} }) by A3, XBOOLE_0:def 3;

      then ins in { [I, {} , <*b, c*>] : I in {1, 2, 3, 4, 5} } by AMI_3: 27, XBOOLE_0:def 3;

      then

      consider I, b, c such that

       A6: ins = [I, {} , <*b, c*>] and I in {1, 2, 3, 4, 5};

      reconsider da = b, db = c as Data-Location by Lm1;

      take da, db;

      thus thesis by A1, A6;

    end;

    theorem :: AMI_5:12

    for ins be Instruction of SCM st ( InsCode ins) = 5 holds ex da, db st ins = ( Divide (da,db))

    proof

      let ins be Instruction of SCM such that

       A1: ( InsCode ins) = 5;

       A2:

      now

        assume ins in { [J, <*a*>, {} ] : J = 6 };

        then ex J, a st ins = [J, <*a*>, {} ] & J = 6;

        hence contradiction by A1;

      end;

       A3:

      now

        assume ins in { [K, <*a1*>, <*b1*>] : K in {7, 8} };

        then

        consider K, a1, b1 such that

         A4: ins = [K, <*a1*>, <*b1*>] and

         A5: K in {7, 8};

        ( InsCode ins) = K by A4;

        hence contradiction by A1, A5, TARSKI:def 2;

      end;

      ( InsCode ( halt SCM )) = 0 by COMPOS_1: 70;

      then not ins in { [ SCM-Halt , {} , {} ]} by A1, AMI_3: 26, TARSKI:def 1;

      then not ins in ( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) by A2, XBOOLE_0:def 3;

      then not ins in (( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) \/ { [K, <*a1*>, <*b1*>] : K in {7, 8} }) by A3, XBOOLE_0:def 3;

      then ins in { [I, {} , <*b, c*>] : I in {1, 2, 3, 4, 5} } by AMI_3: 27, XBOOLE_0:def 3;

      then

      consider I, b, c such that

       A6: ins = [I, {} , <*b, c*>] and I in {1, 2, 3, 4, 5};

      reconsider da = b, db = c as Data-Location by Lm1;

      take da, db;

      thus thesis by A1, A6;

    end;

    theorem :: AMI_5:13

    for ins be Instruction of SCM st ( InsCode ins) = 6 holds ex loc st ins = ( SCM-goto loc)

    proof

      let ins be Instruction of SCM such that

       A1: ( InsCode ins) = 6;

      now

        assume ins in { [I, {} , <*b, c*>] : I in {1, 2, 3, 4, 5} };

        then

        consider I, b, c such that

         A2: ins = [I, {} , <*b, c*>] and

         A3: I in {1, 2, 3, 4, 5};

        ( InsCode ins) = I by A2;

        hence contradiction by A1, A3, ENUMSET1:def 3;

      end;

      then

       A4: ins in (( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) \/ { [K, <*a1*>, <*b1*>] : K in {7, 8} }) by AMI_3: 27, XBOOLE_0:def 3;

      now

        assume ins in { [K, <*a1*>, <*b1*>] : K in {7, 8} };

        then

        consider K, a1, b1 such that

         A5: ins = [K, <*a1*>, <*b1*>] and

         A6: K in {7, 8};

        ( InsCode ins) = K by A5;

        hence contradiction by A1, A6, TARSKI:def 2;

      end;

      then

       A7: ins in ( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) by A4, XBOOLE_0:def 3;

      ( InsCode ( halt SCM )) = 0 by COMPOS_1: 70;

      then not ins in { [ SCM-Halt , {} , {} ]} by A1, AMI_3: 26, TARSKI:def 1;

      then ins in { [J, <*a*>, {} ] : J = 6 } by A7, XBOOLE_0:def 3;

      then

      consider J, a such that

       A8: ins = [J, <*a*>, {} ] & J = 6;

      reconsider loc = a as Nat;

      take loc;

      thus thesis by A8;

    end;

    theorem :: AMI_5:14

    for ins be Instruction of SCM st ( InsCode ins) = 7 holds ex loc, da st ins = (da =0_goto loc)

    proof

      let ins be Instruction of SCM such that

       A1: ( InsCode ins) = 7;

       A2:

      now

        assume ins in { [J, <*a*>, {} ] : J = 6 };

        then ex J, a st ins = [J, <*a*>, {} ] & J = 6;

        hence contradiction by A1;

      end;

      now

        assume ins in { [I, {} , <*b, c*>] : I in {1, 2, 3, 4, 5} };

        then

        consider I, b, c such that

         A3: ins = [I, {} , <*b, c*>] and

         A4: I in {1, 2, 3, 4, 5};

        ( InsCode ins) = I by A3;

        hence contradiction by A1, A4, ENUMSET1:def 3;

      end;

      then

       A5: ins in (( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) \/ { [K, <*a1*>, <*b1*>] : K in {7, 8} }) by AMI_3: 27, XBOOLE_0:def 3;

      ( InsCode ( halt SCM )) = 0 by COMPOS_1: 70;

      then not ins in { [ SCM-Halt , {} , {} ]} by A1, AMI_3: 26, TARSKI:def 1;

      then not ins in ( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) by A2, XBOOLE_0:def 3;

      then ins in { [K, <*a1*>, <*b1*>] : K in {7, 8} } by A5, XBOOLE_0:def 3;

      then

      consider K, a1, b1 such that

       A6: ins = [K, <*a1*>, <*b1*>] and K in {7, 8};

      reconsider da = b1 as Data-Location by Lm1;

      reconsider loc = a1 as Nat;

      take loc, da;

      thus thesis by A1, A6;

    end;

    theorem :: AMI_5:15

    for ins be Instruction of SCM st ( InsCode ins) = 8 holds ex loc, da st ins = (da >0_goto loc)

    proof

      let ins be Instruction of SCM such that

       A1: ( InsCode ins) = 8;

       A2:

      now

        assume ins in { [J, <*a*>, {} ] : J = 6 };

        then ex J, a st ins = [J, <*a*>, {} ] & J = 6;

        hence contradiction by A1;

      end;

      now

        assume ins in { [I, {} , <*b, c*>] : I in {1, 2, 3, 4, 5} };

        then

        consider I, b, c such that

         A3: ins = [I, {} , <*b, c*>] and

         A4: I in {1, 2, 3, 4, 5};

        ( InsCode ins) = I by A3;

        hence contradiction by A1, A4, ENUMSET1:def 3;

      end;

      then

       A5: ins in (( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) \/ { [K, <*a1*>, <*b1*>] : K in {7, 8} }) by AMI_3: 27, XBOOLE_0:def 3;

      ( InsCode ( halt SCM )) = 0 by COMPOS_1: 70;

      then not ins in { [ SCM-Halt , {} , {} ]} by A1, AMI_3: 26, TARSKI:def 1;

      then not ins in ( { [ SCM-Halt , {} , {} ]} \/ { [J, <*a*>, {} ] : J = 6 }) by A2, XBOOLE_0:def 3;

      then ins in { [K, <*a1*>, <*b1*>] : K in {7, 8} } by A5, XBOOLE_0:def 3;

      then

      consider K, a1, b1 such that

       A6: ins = [K, <*a1*>, <*b1*>] and K in {7, 8};

      reconsider da = b1 as Data-Location by Lm1;

      reconsider loc = a1 as Nat;

      take loc, da;

      thus thesis by A1, A6;

    end;

    begin

    theorem :: AMI_5:16

    for s be State of SCM , iloc be Nat, a be Data-Location holds (s . a) = ((s +* ( Start-At (iloc, SCM ))) . a)

    proof

      let s be State of SCM , iloc be Nat, a be Data-Location;

      a in the carrier of SCM ;

      then a in ( dom s) by PARTFUN1:def 2;

      then

       A1: ( dom ( Start-At (iloc, SCM ))) = {( IC SCM )} & a in (( dom s) \/ ( dom ( Start-At (iloc, SCM )))) by XBOOLE_0:def 3;

      a <> ( IC SCM ) by Th2;

      then not a in {( IC SCM )} by TARSKI:def 1;

      hence thesis by A1, FUNCT_4:def 1;

    end;

    begin

    registration

      cluster SCM -> IC-recognized;

      coherence

      proof

        for q be non halt-free finitethe InstructionsF of SCM -valued NAT -defined Function holds for p be q -autonomic FinPartState of SCM st ( DataPart p) <> {} holds ( IC SCM ) in ( dom p)

        proof

          let q be non halt-free finitethe InstructionsF of SCM -valued NAT -defined Function;

          let p be q -autonomic FinPartState of SCM ;

          assume ( DataPart p) <> {} ;

          then

           A1: ( dom ( DataPart p)) <> {} ;

          assume

           A2: not ( IC SCM ) in ( dom p);

          then ( dom p) misses {( IC SCM )} by ZFMISC_1: 50;

          then

           A3: (( dom p) /\ {( IC SCM )}) = {} by XBOOLE_0:def 7;

           not p is q -autonomic

          proof

            set il = the Element of ( NAT \ ( dom q));

            set d2 = the Element of (( Data-Locations SCM ) \ ( dom p));

            set d1 = the Element of ( dom ( DataPart p));

            

             A4: d1 in ( dom ( DataPart p)) by A1;

            ( DataPart p) c= p by MEMSTR_0: 12;

            then

             A5: ( dom ( DataPart p)) c= ( dom p) by RELAT_1: 11;

            ( dom ( DataPart p)) c= the carrier of SCM by RELAT_1:def 18;

            then

            reconsider d1 as Element of SCM by A4;

             not ( Data-Locations SCM ) c= ( dom p);

            then

             A6: (( Data-Locations SCM ) \ ( dom p)) <> {} by XBOOLE_1: 37;

            then d2 in ( Data-Locations SCM ) by XBOOLE_0:def 5;

            then

            reconsider d2 as Data-Location by AMI_2:def 16, AMI_3: 27;

            

             A7: not d2 in ( dom p) by A6, XBOOLE_0:def 5;

            then

             A8: ( dom p) misses {d2} by ZFMISC_1: 50;

             not NAT c= ( dom q);

            then

             A9: ( NAT \ ( dom q)) <> {} by XBOOLE_1: 37;

            then

            reconsider il as Element of NAT by XBOOLE_0:def 5;

            

             A10: not il in ( dom q) by A9, XBOOLE_0:def 5;

            ( dom ( DataPart p)) c= ( Data-Locations SCM ) by RELAT_1: 58;

            then

            reconsider d1 as Data-Location by A4, AMI_2:def 16, AMI_3: 27;

            set p2 = (p +* ((d2 .--> 1) +* ( Start-At (il, SCM ))));

            set p1 = (p +* ((d2 .--> 0 ) +* ( Start-At (il, SCM ))));

            set q2 = (q +* (il .--> (d1 := d2)));

            set q1 = (q +* (il .--> (d1 := d2)));

            consider s1 be State of SCM such that

             A11: p1 c= s1 by PBOOLE: 141;

            consider S1 be Instruction-Sequence of SCM such that

             A12: q1 c= S1 by PBOOLE: 145;

            

             A13: ( dom p) misses {d2} by A7, ZFMISC_1: 50;

            

             A14: ( dom ((d2 .--> 1) +* ( Start-At (il, SCM )))) = (( dom (d2 .--> 1)) \/ ( dom ( Start-At (il, SCM )))) by FUNCT_4:def 1;

            consider s2 be State of SCM such that

             A15: p2 c= s2 by PBOOLE: 141;

            consider S2 be Instruction-Sequence of SCM such that

             A16: q2 c= S2 by PBOOLE: 145;

            

             A17: ( dom p) c= the carrier of SCM by RELAT_1:def 18;

            ( dom ( Comput (S2,s2,1))) = the carrier of SCM by PARTFUN1:def 2;

            then

             A18: ( dom (( Comput (S2,s2,1)) | ( dom p))) = ( dom p) by A17, RELAT_1: 62;

            

             A19: ( dom ( Comput (S1,s1,1))) = the carrier of SCM by PARTFUN1:def 2;

            

             A20: ( dom (( Comput (S1,s1,1)) | ( dom p))) = ( dom p) by A17, A19, RELAT_1: 62;

            

             A21: ( dom p2) = (( dom p) \/ ( dom ((d2 .--> 1) +* ( Start-At (il, SCM ))))) by FUNCT_4:def 1;

            

             A22: ( dom q2) = (( dom q) \/ ( dom (il .--> (d1 := d2)))) by FUNCT_4:def 1;

            

             A24: ( IC SCM ) in ( dom ( Start-At (il, SCM ))) by TARSKI:def 1;

            then

             A25: ( IC SCM ) in ( dom ((d2 .--> 1) +* ( Start-At (il, SCM )))) by A14, XBOOLE_0:def 3;

            then ( IC SCM ) in ( dom p2) by A21, XBOOLE_0:def 3;

            

            then

             A26: ( IC s2) = (p2 . ( IC SCM )) by A15, GRFUNC_1: 2

            .= (((d2 .--> 1) +* ( Start-At (il, SCM ))) . ( IC SCM )) by A25, FUNCT_4: 13

            .= (( Start-At (il, SCM )) . ( IC SCM )) by A24, FUNCT_4: 13

            .= il by FUNCOP_1: 72;

            d2 <> ( IC SCM ) by Th2;

            then

             A27: not d2 in ( dom ( Start-At (il, SCM ))) by TARSKI:def 1;

            d2 in ( dom (d2 .--> 1)) by TARSKI:def 1;

            then

             A28: d2 in ( dom ((d2 .--> 1) +* ( Start-At (il, SCM )))) by A14, XBOOLE_0:def 3;

            then d2 in ( dom p2) by A21, XBOOLE_0:def 3;

            

            then

             A29: (s2 . d2) = (p2 . d2) by A15, GRFUNC_1: 2

            .= (((d2 .--> 1) +* ( Start-At (il, SCM ))) . d2) by A28, FUNCT_4: 13

            .= ((d2 .--> 1) . d2) by A27, FUNCT_4: 11

            .= 1 by FUNCOP_1: 72;

            

             A31: il in ( dom (il .--> (d1 := d2))) by TARSKI:def 1;

            then il in ( dom q2) by A22, XBOOLE_0:def 3;

            

            then

             A32: (S2 . il) = (q2 . il) by A16, GRFUNC_1: 2

            .= ((il .--> (d1 := d2)) . il) by A31, FUNCT_4: 13

            .= (d1 := d2) by FUNCOP_1: 72;

            

             A33: (S2 /. ( IC s2)) = (S2 . ( IC s2)) by PBOOLE: 143;

            

             A34: (( Comput (S2,s2,( 0 + 1))) . d1) = (( Following (S2,( Comput (S2,s2, 0 )))) . d1) by EXTPRO_1: 3

            .= (( Following (S2,s2)) . d1)

            .= 1 by A26, A32, A29, A33, AMI_3: 2;

            ( dom p) misses {( IC SCM )} by A2, ZFMISC_1: 50;

            then

             A35: (( dom p) /\ {( IC SCM )}) = {} by XBOOLE_0:def 7;

            take P = S1, Q = S2;

            ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM )))) = (( dom (d2 .--> 0 )) \/ ( dom ( Start-At (il, SCM )))) by FUNCT_4:def 1

            .= (( dom (d2 .--> 0 )) \/ {( IC SCM )})

            .= ( {d2} \/ {( IC SCM )});

            

            then (( dom p) /\ ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM ))))) = ((( dom p) /\ {d2}) \/ {} ) by A35, XBOOLE_1: 23

            .= {} by A8, XBOOLE_0:def 7;

            then ( dom p) misses ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM )))) by XBOOLE_0:def 7;

            then p c= p1 by FUNCT_4: 32;

            then

             A36: p c= s1 by A11, XBOOLE_1: 1;

            ( dom q) misses ( dom (il .--> (d1 := d2))) by A10, ZFMISC_1: 50;

            then q c= q1 by FUNCT_4: 32;

            hence q c= P by A12, XBOOLE_1: 1;

            

             A37: ( dom p1) = (( dom p) \/ ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM ))))) by FUNCT_4:def 1;

            ( dom ((d2 .--> 1) +* ( Start-At (il, SCM )))) = (( dom (d2 .--> 1)) \/ ( dom ( Start-At (il, SCM )))) by FUNCT_4:def 1

            .= (( dom (d2 .--> 1)) \/ {( IC SCM )})

            .= ( {d2} \/ {( IC SCM )});

            

            then (( dom p) /\ ( dom ((d2 .--> 1) +* ( Start-At (il, SCM ))))) = ((( dom p) /\ {d2}) \/ {} ) by A3, XBOOLE_1: 23

            .= {} by A13, XBOOLE_0:def 7;

            then ( dom p) misses ( dom ((d2 .--> 1) +* ( Start-At (il, SCM )))) by XBOOLE_0:def 7;

            then p c= p2 by FUNCT_4: 32;

            then

             A38: p c= s2 by A15, XBOOLE_1: 1;

            ( dom q) misses ( dom (il .--> (d1 := d2))) by A10, ZFMISC_1: 50;

            then q c= q2 by FUNCT_4: 32;

            hence q c= Q by A16, XBOOLE_1: 1;

            take s1, s2;

            thus p c= s1 by A36;

            thus p c= s2 by A38;

            take 1;

            

             A39: ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM )))) = (( dom (d2 .--> 0 )) \/ ( dom ( Start-At (il, SCM )))) by FUNCT_4:def 1;

            

             A41: ( IC SCM ) in ( dom ( Start-At (il, SCM ))) by TARSKI:def 1;

            then

             A42: ( IC SCM ) in ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM )))) by A39, XBOOLE_0:def 3;

            then ( IC SCM ) in ( dom p1) by A37, XBOOLE_0:def 3;

            

            then

             A43: ( IC s1) = (p1 . ( IC SCM )) by A11, GRFUNC_1: 2

            .= (((d2 .--> 0 ) +* ( Start-At (il, SCM ))) . ( IC SCM )) by A42, FUNCT_4: 13

            .= (( Start-At (il, SCM )) . ( IC SCM )) by A41, FUNCT_4: 13

            .= il by FUNCOP_1: 72;

            d2 <> ( IC SCM ) by Th2;

            then

             A44: not d2 in ( dom ( Start-At (il, SCM ))) by TARSKI:def 1;

            d2 in ( dom (d2 .--> 0 )) by TARSKI:def 1;

            then

             A45: d2 in ( dom ((d2 .--> 0 ) +* ( Start-At (il, SCM )))) by A39, XBOOLE_0:def 3;

            then d2 in ( dom p1) by A37, XBOOLE_0:def 3;

            

            then

             A46: (s1 . d2) = (p1 . d2) by A11, GRFUNC_1: 2

            .= (((d2 .--> 0 ) +* ( Start-At (il, SCM ))) . d2) by A45, FUNCT_4: 13

            .= ((d2 .--> 0 ) . d2) by A44, FUNCT_4: 11

            .= 0 by FUNCOP_1: 72;

            

             A47: il in ( dom (il .--> (d1 := d2))) by TARSKI:def 1;

            ( dom q1) = (( dom q) \/ ( dom (il .--> (d1 := d2)))) by FUNCT_4:def 1;

            then il in ( dom q1) by A47, XBOOLE_0:def 3;

            

            then

             A48: (S1 . il) = (q1 . il) by A12, GRFUNC_1: 2

            .= ((il .--> (d1 := d2)) . il) by A47, FUNCT_4: 13

            .= (d1 := d2) by FUNCOP_1: 72;

            

             A49: (S1 /. ( IC s1)) = (S1 . ( IC s1)) by PBOOLE: 143;

            (( Comput (S1,s1,( 0 + 1))) . d1) = (( Following (S1,( Comput (S1,s1, 0 )))) . d1) by EXTPRO_1: 3

            .= 0 by A43, A48, A46, A49, AMI_3: 2;

            then ((( Comput (P,s1,1)) | ( dom p)) . d1) = 0 by A4, A5, A20, FUNCT_1: 47;

            hence (( Comput (P,s1,1)) | ( dom p)) <> (( Comput (Q,s2,1)) | ( dom p)) by A18, A34, A4, A5, FUNCT_1: 47;

          end;

          hence contradiction;

        end;

        hence thesis by AMISTD_5: 3;

      end;

    end

    registration

      cluster SCM -> CurIns-recognized;

      coherence

      proof

        let q be non halt-free finitethe InstructionsF of SCM -valued NAT -defined Function;

        let p be q -autonomic non empty FinPartState of SCM , s be State of SCM such that

         A1: p c= s;

        let P be Instruction-Sequence of SCM such that

         A2: q c= P;

        let i be Nat;

        set Csi = ( Comput (P,s,i));

        set loc = ( IC Csi);

        assume

         A3: not ( IC ( Comput (P,s,i))) in ( dom q);

        set I = (( dl. 0 ) := ( dl. 0 ));

        set q1 = (q +* (loc .--> I));

        set q2 = (q +* (loc .--> ( halt SCM )));

        reconsider P1 = (P +* (loc .--> I)) as Instruction-Sequence of SCM ;

        reconsider P2 = (P +* (loc .--> ( halt SCM ))) as Instruction-Sequence of SCM ;

        

         A5: loc in ( dom (loc .--> ( halt SCM ))) by TARSKI:def 1;

        

         A7: loc in ( dom (loc .--> I)) by TARSKI:def 1;

        

         A8: ( dom q) misses ( dom (loc .--> ( halt SCM ))) by A3, ZFMISC_1: 50;

        

         A9: ( dom q) misses ( dom (loc .--> I)) by A3, ZFMISC_1: 50;

        

         A10: q1 c= P1 by A2, FUNCT_4: 123;

        

         A11: q2 c= P2 by A2, FUNCT_4: 123;

        set Cs2i = ( Comput (P2,s,i)), Cs1i = ( Comput (P1,s,i));

         not p is q -autonomic

        proof

          ((loc .--> ( halt SCM )) . loc) = ( halt SCM ) by FUNCOP_1: 72;

          then

           A12: (P2 . loc) = ( halt SCM ) by A5, FUNCT_4: 13;

          

           A13: ((loc .--> I) . loc) = I by FUNCOP_1: 72;

          take P1, P2;

          q c= q1 by A9, FUNCT_4: 32;

          hence

           A14: q c= P1 by A10, XBOOLE_1: 1;

          q c= q2 by A8, FUNCT_4: 32;

          hence

           A15: q c= P2 by A11, XBOOLE_1: 1;

          take s, s;

          thus p c= s by A1;

          

           A16: (Cs1i | ( dom p)) = (Csi | ( dom p)) by A14, A2, A1, EXTPRO_1:def 10;

          thus p c= s by A1;

          

           A17: (Cs1i | ( dom p)) = (Cs2i | ( dom p)) by A14, A15, A1, EXTPRO_1:def 10;

          take k = (i + 1);

          set Cs1k = ( Comput (P1,s,k));

          

           A18: ( IC SCM ) in ( dom p) by AMISTD_5: 6;

          ( IC Csi) = ( IC (Csi | ( dom p))) by A18, FUNCT_1: 49;

          then ( IC Cs1i) = loc by A16, A18, FUNCT_1: 49;

          

          then

           A19: ( CurInstr (P1,Cs1i)) = (P1 . loc) by PBOOLE: 143

          .= I by A13, A7, FUNCT_4: 13;

          

           A20: Cs1k = ( Following (P1,Cs1i)) by EXTPRO_1: 3

          .= ( Exec (I,Cs1i)) by A19;

          

           A21: ( IC ( Exec (I,Cs1i))) = (( IC Cs1i) + 1) by AMI_3: 2;

          

           A22: ( IC SCM ) in ( dom p) by AMISTD_5: 6;

          

           A23: ( IC Csi) = ( IC (Csi | ( dom p))) by A22, FUNCT_1: 49;

          then

           A24: ( IC Cs1k) = (loc + 1) by A20, A21, A16, A22, FUNCT_1: 49;

          set Cs2k = ( Comput (P2,s,k));

          

           A25: Cs2k = ( Following (P2,Cs2i)) by EXTPRO_1: 3

          .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

          

           A26: (P2 /. ( IC Cs2i)) = (P2 . ( IC Cs2i)) by PBOOLE: 143;

          ( IC Cs2i) = loc by A16, A23, A17, A22, FUNCT_1: 49;

          then

           A27: ( IC Cs2k) = loc by A25, A12, A26, EXTPRO_1:def 3;

          ( IC (Cs1k | ( dom p))) = ( IC Cs1k) & ( IC (Cs2k | ( dom p))) = ( IC Cs2k) by A22, FUNCT_1: 49;

          hence thesis by A24, A27;

        end;

        hence contradiction;

      end;

    end

    theorem :: AMI_5:17

    for q be non halt-free finitethe InstructionsF of SCM -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM , s1,s2 be State of SCM st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM st q c= P1 & q c= P2 holds for i be Nat, da,db be Data-Location, I be Instruction of SCM st I = ( CurInstr (P1,( Comput (P1,s1,i)))) holds I = (da := db) & da in ( dom p) implies (( Comput (P1,s1,i)) . db) = (( Comput (P2,s2,i)) . db)

    proof

      let q be non halt-free finitethe InstructionsF of SCM -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM , s1,s2 be State of SCM such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da,db be Data-Location, I be Instruction of SCM such that

       A3: I = ( CurInstr (P1,( Comput (P1,s1,i))));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      set Cs2i = ( Comput (P2,s2,i));

      

       A4: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      assume that

       A5: I = (da := db) and

       A6: da in ( dom p) & (( Comput (P1,s1,i)) . db) <> (( Comput (P2,s2,i)) . db);

      I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A3, A2, A1, AMISTD_5: 7;

      then

       A7: (Cs2i1 . da) = (Cs2i . db) by A4, A5, AMI_3: 2;

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs1i = ( Comput (P1,s1,i));

      

       A8: da in ( dom p) implies ((Cs1i1 | ( dom p)) . da) = (Cs1i1 . da) & ((Cs2i1 | ( dom p)) . da) = (Cs2i1 . da) by FUNCT_1: 49;

      Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      then (Cs1i1 . da) = (Cs1i . db) by A3, A5, AMI_3: 2;

      hence contradiction by A8, A6, A7, A2, A1, EXTPRO_1:def 10;

    end;

    theorem :: AMI_5:18

    for q be non halt-free finitethe InstructionsF of SCM -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM , s1,s2 be State of SCM st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM st q c= P1 & q c= P2 holds for i be Nat, da,db be Data-Location, I be Instruction of SCM st I = ( CurInstr (P1,( Comput (P1,s1,i)))) holds I = ( AddTo (da,db)) & da in ( dom p) implies ((( Comput (P1,s1,i)) . da) + (( Comput (P1,s1,i)) . db)) = ((( Comput (P2,s2,i)) . da) + (( Comput (P2,s2,i)) . db))

    proof

      let q be non halt-free finitethe InstructionsF of SCM -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM , s1,s2 be State of SCM such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da,db be Data-Location, I be Instruction of SCM such that

       A3: I = ( CurInstr (P1,( Comput (P1,s1,i))));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      set Cs2i = ( Comput (P2,s2,i));

      

       A4: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      assume that

       A5: I = ( AddTo (da,db)) and

       A6: da in ( dom p) & ((( Comput (P1,s1,i)) . da) + (( Comput (P1,s1,i)) . db)) <> ((( Comput (P2,s2,i)) . da) + (( Comput (P2,s2,i)) . db));

      I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A3, A2, A1, AMISTD_5: 7;

      then

       A7: (Cs2i1 . da) = ((Cs2i . da) + (Cs2i . db)) by A4, A5, AMI_3: 3;

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs1i = ( Comput (P1,s1,i));

      

       A8: da in ( dom p) implies ((Cs1i1 | ( dom p)) . da) = (Cs1i1 . da) & ((Cs2i1 | ( dom p)) . da) = (Cs2i1 . da) by FUNCT_1: 49;

      Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      then (Cs1i1 . da) = ((Cs1i . da) + (Cs1i . db)) by A3, A5, AMI_3: 3;

      hence contradiction by A8, A6, A7, A2, A1, EXTPRO_1:def 10;

    end;

    theorem :: AMI_5:19

    for q be non halt-free finitethe InstructionsF of SCM -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM , s1,s2 be State of SCM st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM st q c= P1 & q c= P2 holds for i be Nat, da,db be Data-Location, I be Instruction of SCM st I = ( CurInstr (P1,( Comput (P1,s1,i)))) holds I = ( SubFrom (da,db)) & da in ( dom p) implies ((( Comput (P1,s1,i)) . da) - (( Comput (P1,s1,i)) . db)) = ((( Comput (P2,s2,i)) . da) - (( Comput (P2,s2,i)) . db))

    proof

      let q be non halt-free finitethe InstructionsF of SCM -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM , s1,s2 be State of SCM such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da,db be Data-Location, I be Instruction of SCM such that

       A3: I = ( CurInstr (P1,( Comput (P1,s1,i))));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      set Cs2i = ( Comput (P2,s2,i));

      

       A4: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      assume that

       A5: I = ( SubFrom (da,db)) and

       A6: da in ( dom p) & ((( Comput (P1,s1,i)) . da) - (( Comput (P1,s1,i)) . db)) <> ((( Comput (P2,s2,i)) . da) - (( Comput (P2,s2,i)) . db));

      I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A3, A2, A1, AMISTD_5: 7;

      then

       A7: (Cs2i1 . da) = ((Cs2i . da) - (Cs2i . db)) by A4, A5, AMI_3: 4;

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs1i = ( Comput (P1,s1,i));

      

       A8: da in ( dom p) implies ((Cs1i1 | ( dom p)) . da) = (Cs1i1 . da) & ((Cs2i1 | ( dom p)) . da) = (Cs2i1 . da) by FUNCT_1: 49;

      Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      then (Cs1i1 . da) = ((Cs1i . da) - (Cs1i . db)) by A3, A5, AMI_3: 4;

      hence contradiction by A8, A6, A7, A2, A1, EXTPRO_1:def 10;

    end;

    theorem :: AMI_5:20

    for q be non halt-free finitethe InstructionsF of SCM -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM , s1,s2 be State of SCM st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM st q c= P1 & q c= P2 holds for i be Nat, da,db be Data-Location, I be Instruction of SCM st I = ( CurInstr (P1,( Comput (P1,s1,i)))) holds I = ( MultBy (da,db)) & da in ( dom p) implies ((( Comput (P1,s1,i)) . da) * (( Comput (P1,s1,i)) . db)) = ((( Comput (P2,s2,i)) . da) * (( Comput (P2,s2,i)) . db))

    proof

      let q be non halt-free finitethe InstructionsF of SCM -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM , s1,s2 be State of SCM such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da,db be Data-Location, I be Instruction of SCM such that

       A3: I = ( CurInstr (P1,( Comput (P1,s1,i))));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      set Cs2i = ( Comput (P2,s2,i));

      

       A4: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      assume that

       A5: I = ( MultBy (da,db)) and

       A6: da in ( dom p) & ((( Comput (P1,s1,i)) . da) * (( Comput (P1,s1,i)) . db)) <> ((( Comput (P2,s2,i)) . da) * (( Comput (P2,s2,i)) . db));

      I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A3, A2, A1, AMISTD_5: 7;

      then

       A7: (Cs2i1 . da) = ((Cs2i . da) * (Cs2i . db)) by A4, A5, AMI_3: 5;

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs1i = ( Comput (P1,s1,i));

      

       A8: da in ( dom p) implies ((Cs1i1 | ( dom p)) . da) = (Cs1i1 . da) & ((Cs2i1 | ( dom p)) . da) = (Cs2i1 . da) by FUNCT_1: 49;

      Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      then (Cs1i1 . da) = ((Cs1i . da) * (Cs1i . db)) by A3, A5, AMI_3: 5;

      hence contradiction by A8, A6, A7, A2, A1, EXTPRO_1:def 10;

    end;

    theorem :: AMI_5:21

    for q be non halt-free finitethe InstructionsF of SCM -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM , s1,s2 be State of SCM st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM st q c= P1 & q c= P2 holds for i be Nat, da,db be Data-Location, I be Instruction of SCM st I = ( CurInstr (P1,( Comput (P1,s1,i)))) holds I = ( Divide (da,db)) & da in ( dom p) & da <> db implies ((( Comput (P1,s1,i)) . da) div (( Comput (P1,s1,i)) . db)) = ((( Comput (P2,s2,i)) . da) div (( Comput (P2,s2,i)) . db))

    proof

      let q be non halt-free finitethe InstructionsF of SCM -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM , s1,s2 be State of SCM such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da,db be Data-Location, I be Instruction of SCM such that

       A3: I = ( CurInstr (P1,( Comput (P1,s1,i))));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      set Cs2i = ( Comput (P2,s2,i));

      

       A4: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      assume that

       A5: I = ( Divide (da,db)) and

       A6: da in ( dom p) and

       A7: da <> db and

       A8: ((( Comput (P1,s1,i)) . da) div (( Comput (P1,s1,i)) . db)) <> ((( Comput (P2,s2,i)) . da) div (( Comput (P2,s2,i)) . db));

      I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A3, A2, A1, AMISTD_5: 7;

      then

       A9: (Cs2i1 . da) = ((Cs2i . da) div (Cs2i . db)) by A4, A5, A7, AMI_3: 6;

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs1i = ( Comput (P1,s1,i));

      

       A10: da in ( dom p) implies ((Cs1i1 | ( dom p)) . da) = (Cs1i1 . da) & ((Cs2i1 | ( dom p)) . da) = (Cs2i1 . da) by FUNCT_1: 49;

      Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      then (Cs1i1 . da) = ((Cs1i . da) div (Cs1i . db)) by A3, A5, A7, AMI_3: 6;

      hence contradiction by A10, A8, A9, A2, A6, A1, EXTPRO_1:def 10;

    end;

    theorem :: AMI_5:22

    for q be non halt-free finitethe InstructionsF of SCM -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM , s1,s2 be State of SCM st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM st q c= P1 & q c= P2 holds for i be Nat, da,db be Data-Location, I be Instruction of SCM st I = ( CurInstr (P1,( Comput (P1,s1,i)))) holds I = ( Divide (da,db)) & db in ( dom p) implies ((( Comput (P1,s1,i)) . da) mod (( Comput (P1,s1,i)) . db)) = ((( Comput (P2,s2,i)) . da) mod (( Comput (P2,s2,i)) . db))

    proof

      let q be non halt-free finitethe InstructionsF of SCM -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM , s1,s2 be State of SCM such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da,db be Data-Location, I be Instruction of SCM such that

       A3: I = ( CurInstr (P1,( Comput (P1,s1,i))));

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs1i = ( Comput (P1,s1,i));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      set Cs2i = ( Comput (P2,s2,i));

      

       A4: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      assume that

       A5: I = ( Divide (da,db)) and

       A6: db in ( dom p) and

       A7: ((( Comput (P1,s1,i)) . da) mod (( Comput (P1,s1,i)) . db)) <> ((( Comput (P2,s2,i)) . da) mod (( Comput (P2,s2,i)) . db));

      

       A8: ((Cs1i1 | ( dom p)) . db) = (Cs1i1 . db) & ((Cs2i1 | ( dom p)) . db) = (Cs2i1 . db) by A6, FUNCT_1: 49;

      I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A3, A2, A1, AMISTD_5: 7;

      then

       A9: (Cs2i1 . db) = ((Cs2i . da) mod (Cs2i . db)) by A4, A5, AMI_3: 6;

      Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      then (Cs1i1 . db) = ((Cs1i . da) mod (Cs1i . db)) by A3, A5, AMI_3: 6;

      hence contradiction by A7, A8, A9, A2, A1, EXTPRO_1:def 10;

    end;

    theorem :: AMI_5:23

    for q be non halt-free finitethe InstructionsF of SCM -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM , s1,s2 be State of SCM st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM st q c= P1 & q c= P2 holds for i be Nat, da be Data-Location, loc be Nat, I be Instruction of SCM st I = ( CurInstr (P1,( Comput (P1,s1,i)))) holds I = (da =0_goto loc) & loc <> (( IC ( Comput (P1,s1,i))) + 1) implies ((( Comput (P1,s1,i)) . da) = 0 iff (( Comput (P2,s2,i)) . da) = 0 )

    proof

      let q be non halt-free finitethe InstructionsF of SCM -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM , s1,s2 be State of SCM such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da be Data-Location, loc be Nat, I be Instruction of SCM such that

       A3: I = ( CurInstr (P1,( Comput (P1,s1,i))));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      set Cs2i = ( Comput (P2,s2,i));

      set Cs1i = ( Comput (P1,s1,i));

      

       A4: Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      

       A5: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      ( IC SCM ) in ( dom p) by AMISTD_5: 6;

      then

       A6: ((Cs1i1 | ( dom p)) . ( IC SCM )) = ( IC Cs1i1) & ((Cs2i1 | ( dom p)) . ( IC SCM )) = ( IC Cs2i1) by FUNCT_1: 49;

      assume that

       A7: I = (da =0_goto loc) and

       A8: loc <> (( IC ( Comput (P1,s1,i))) + 1);

      

       A9: I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A3, A2, A1, AMISTD_5: 7;

       A10:

      now

        assume (( Comput (P2,s2,i)) . da) = 0 & (( Comput (P1,s1,i)) . da) <> 0 ;

        then (Cs2i1 . ( IC SCM )) = loc & (Cs1i1 . ( IC SCM )) = (( IC Cs1i) + 1) by A3, A9, A4, A5, A7, AMI_3: 8;

        hence contradiction by A6, A8, A2, A1, EXTPRO_1:def 10;

      end;

      

       A11: (Cs1i1 | ( dom p)) = (Cs2i1 | ( dom p)) by A2, A1, EXTPRO_1:def 10;

      now

        assume (( Comput (P1,s1,i)) . da) = 0 & (( Comput (P2,s2,i)) . da) <> 0 ;

        then (Cs1i1 . ( IC SCM )) = loc & (Cs2i1 . ( IC SCM )) = (( IC Cs2i) + 1) by A3, A9, A4, A5, A7, AMI_3: 8;

        hence contradiction by A6, A11, A8, A2, A1, AMISTD_5: 7;

      end;

      hence thesis by A10;

    end;

    theorem :: AMI_5:24

    for q be non halt-free finitethe InstructionsF of SCM -valued NAT -defined Function holds for p be q -autonomic non empty FinPartState of SCM , s1,s2 be State of SCM st p c= s1 & p c= s2 holds for P1,P2 be Instruction-Sequence of SCM st q c= P1 & q c= P2 holds for i be Nat, da be Data-Location, loc be Nat, I be Instruction of SCM st I = ( CurInstr (P1,( Comput (P1,s1,i)))) holds I = (da >0_goto loc) & loc <> (( IC ( Comput (P1,s1,i))) + 1) implies ((( Comput (P1,s1,i)) . da) > 0 iff (( Comput (P2,s2,i)) . da) > 0 )

    proof

      let q be non halt-free finitethe InstructionsF of SCM -valued NAT -defined Function;

      let p be q -autonomic non empty FinPartState of SCM , s1,s2 be State of SCM such that

       A1: p c= s1 & p c= s2;

      let P1,P2 be Instruction-Sequence of SCM such that

       A2: q c= P1 & q c= P2;

      let i be Nat, da be Data-Location, loc be Nat, I be Instruction of SCM such that

       A3: I = ( CurInstr (P1,( Comput (P1,s1,i))));

      set Cs2i1 = ( Comput (P2,s2,(i + 1)));

      set Cs1i1 = ( Comput (P1,s1,(i + 1)));

      

       A4: (Cs1i1 | ( dom p)) = (Cs2i1 | ( dom p)) by A2, A1, EXTPRO_1:def 10;

      set Cs2i = ( Comput (P2,s2,i));

      set Cs1i = ( Comput (P1,s1,i));

      

       A5: Cs1i1 = ( Following (P1,Cs1i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P1,Cs1i)),Cs1i));

      ( IC SCM ) in ( dom p) by AMISTD_5: 6;

      then

       A6: ((Cs1i1 | ( dom p)) . ( IC SCM )) = ( IC Cs1i1) & ((Cs2i1 | ( dom p)) . ( IC SCM )) = ( IC Cs2i1) by FUNCT_1: 49;

      

       A7: Cs2i1 = ( Following (P2,Cs2i)) by EXTPRO_1: 3

      .= ( Exec (( CurInstr (P2,Cs2i)),Cs2i));

      assume that

       A8: I = (da >0_goto loc) and

       A9: loc <> (( IC ( Comput (P1,s1,i))) + 1);

      

       A10: I = ( CurInstr (P2,( Comput (P2,s2,i)))) by A3, A2, A1, AMISTD_5: 7;

       A11:

      now

        assume that

         A12: (( Comput (P2,s2,i)) . da) > 0 and

         A13: (( Comput (P1,s1,i)) . da) <= 0 ;

        (Cs2i1 . ( IC SCM )) = loc by A10, A7, A8, A12, AMI_3: 9;

        hence contradiction by A3, A5, A6, A4, A8, A9, A13, AMI_3: 9;

      end;

      

       A14: ( IC Cs1i) = ( IC Cs2i) by A2, A1, AMISTD_5: 7;

      now

        assume that

         A15: (( Comput (P1,s1,i)) . da) > 0 and

         A16: (( Comput (P2,s2,i)) . da) <= 0 ;

        (Cs1i1 . ( IC SCM )) = loc by A3, A5, A8, A15, AMI_3: 9;

        hence contradiction by A14, A10, A7, A6, A4, A8, A9, A16, AMI_3: 9;

      end;

      hence thesis by A11;

    end;

    theorem :: AMI_5:25

    for s1,s2 be State of SCM st ( IC s1) = ( IC s2) & (for a be Data-Location holds (s1 . a) = (s2 . a)) holds s1 = s2

    proof

      let s1,s2 be State of SCM such that

       A1: ( IC s1) = ( IC s2);

      ( IC SCM ) in ( dom s1) & ( IC SCM ) in ( dom s2) by MEMSTR_0: 2;

      then

       A2: s1 = (( DataPart s1) +* ( Start-At (( IC s1), SCM ))) & s2 = (( DataPart s2) +* ( Start-At (( IC s2), SCM ))) by MEMSTR_0: 26;

      assume

       A3: for a be Data-Location holds (s1 . a) = (s2 . a);

      ( DataPart s1) = ( DataPart s2)

      proof

        

         A4: ( dom ( DataPart s1)) = ( Data-Locations SCM ) by MEMSTR_0: 9;

        hence ( dom ( DataPart s1)) = ( dom ( DataPart s2)) by MEMSTR_0: 9;

        let x be object;

        assume

         A5: x in ( dom ( DataPart s1));

        then

         A6: x is Data-Location by A4, AMI_2:def 16, AMI_3: 27;

        

        thus (( DataPart s1) . x) = (s1 . x) by A5, A4, FUNCT_1: 49

        .= (s2 . x) by A6, A3

        .= (( DataPart s2) . x) by A5, A4, FUNCT_1: 49;

      end;

      hence thesis by A1, A2;

    end;