ami_6.miz



    begin

    reserve a,b,d1,d2 for Data-Location,

il,i1,i2 for Nat,

I for Instruction of SCM ,

s,s1,s2 for State of SCM ,

T for InsType of the InstructionsF of SCM ,

k,k1 for Nat;

    theorem :: AMI_6:1

    T = 0 or ... or T = 8

    proof

      consider y be object such that

       A1: [T, y] in ( proj1 the InstructionsF of SCM ) by XTUPLE_0:def 12;

      consider x be object such that

       A2: [ [T, y], x] in the InstructionsF of SCM by A1, XTUPLE_0:def 12;

      reconsider I = [T, y, x] as Instruction of SCM by A2;

      T = ( InsCode I);

      hence thesis by AMI_5: 5;

    end;

    theorem :: AMI_6:2

    

     Th2: ( JumpPart ( halt SCM )) = {} ;

    theorem :: AMI_6:3

    T = 0 implies ( JumpParts T) = { 0 }

    proof

      assume

       A1: T = 0 ;

      hereby

        let a be object;

        assume a in ( JumpParts T);

        then

        consider I such that

         A2: a = ( JumpPart I) and

         A3: ( InsCode I) = T;

        I = ( halt SCM ) by A1, A3, AMI_5: 7;

        hence a in { 0 } by A2, TARSKI:def 1;

      end;

      let a be object;

      assume a in { 0 };

      then

       A4: a = 0 by TARSKI:def 1;

      ( InsCode ( halt SCM )) = 0 ;

      hence thesis by A1, Th2, A4;

    end;

    theorem :: AMI_6:4

    T = 1 implies ( JumpParts T) = { {} }

    proof

      assume

       A1: T = 1;

      hereby

        let x be object;

        assume x in ( JumpParts T);

        then

        consider I be Instruction of SCM such that

         A2: x = ( JumpPart I) and

         A3: ( InsCode I) = T;

        consider a, b such that

         A4: I = (a := b) by A1, A3, AMI_5: 8;

        x = {} by A2, A4;

        hence x in { {} } by TARSKI:def 1;

      end;

      set a = the Data-Location;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      then

       A5: x = ( JumpPart (a := a));

      ( InsCode (a := a)) = 1;

      hence thesis by A5, A1;

    end;

    theorem :: AMI_6:5

    T = 2 implies ( JumpParts T) = { {} }

    proof

      assume

       A1: T = 2;

      hereby

        let x be object;

        assume x in ( JumpParts T);

        then

        consider I be Instruction of SCM such that

         A2: x = ( JumpPart I) and

         A3: ( InsCode I) = T;

        consider a, b such that

         A4: I = ( AddTo (a,b)) by A1, A3, AMI_5: 9;

        x = {} by A2, A4;

        hence x in { {} } by TARSKI:def 1;

      end;

      set a = the Data-Location;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      then

       A5: x = ( JumpPart ( AddTo (a,a)));

      ( InsCode ( AddTo (a,a))) = 2;

      hence thesis by A5, A1;

    end;

    theorem :: AMI_6:6

    T = 3 implies ( JumpParts T) = { {} }

    proof

      assume

       A1: T = 3;

      hereby

        let x be object;

        assume x in ( JumpParts T);

        then

        consider I be Instruction of SCM such that

         A2: x = ( JumpPart I) and

         A3: ( InsCode I) = T;

        consider a, b such that

         A4: I = ( SubFrom (a,b)) by A1, A3, AMI_5: 10;

        x = {} by A2, A4;

        hence x in { {} } by TARSKI:def 1;

      end;

      set a = the Data-Location;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      then

       A5: x = ( JumpPart ( SubFrom (a,a)));

      ( InsCode ( SubFrom (a,a))) = 3;

      hence thesis by A5, A1;

    end;

    theorem :: AMI_6:7

    T = 4 implies ( JumpParts T) = { {} }

    proof

      assume

       A1: T = 4;

      hereby

        let x be object;

        assume x in ( JumpParts T);

        then

        consider I be Instruction of SCM such that

         A2: x = ( JumpPart I) and

         A3: ( InsCode I) = T;

        consider a, b such that

         A4: I = ( MultBy (a,b)) by A1, A3, AMI_5: 11;

        x = {} by A2, A4;

        hence x in { {} } by TARSKI:def 1;

      end;

      set a = the Data-Location;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      then

       A5: x = ( JumpPart ( MultBy (a,a)));

      ( InsCode ( MultBy (a,a))) = 4;

      hence thesis by A5, A1;

    end;

    theorem :: AMI_6:8

    T = 5 implies ( JumpParts T) = { {} }

    proof

      assume

       A1: T = 5;

      hereby

        let x be object;

        assume x in ( JumpParts T);

        then

        consider I be Instruction of SCM such that

         A2: x = ( JumpPart I) and

         A3: ( InsCode I) = T;

        consider a, b such that

         A4: I = ( Divide (a,b)) by A1, A3, AMI_5: 12;

        x = {} by A2, A4;

        hence x in { {} } by TARSKI:def 1;

      end;

      set a = the Data-Location;

      let x be object;

      assume x in { {} };

      then x = {} by TARSKI:def 1;

      then

       A5: x = ( JumpPart ( Divide (a,a)));

      ( InsCode ( Divide (a,a))) = 5;

      hence thesis by A5, A1;

    end;

    theorem :: AMI_6:9

    

     Th9: T = 6 implies ( dom ( product" ( JumpParts T))) = {1}

    proof

      set i1 = the Element of NAT ;

      assume

       A1: T = 6;

      hereby

        let x be object;

        ( InsCode ( SCM-goto i1)) = 6;

        then

         A2: ( JumpPart ( SCM-goto i1)) in ( JumpParts T) by A1;

        assume x in ( dom ( product" ( JumpParts T)));

        then x in ( DOM ( JumpParts T)) by CARD_3:def 12;

        then x in ( dom ( JumpPart ( SCM-goto i1))) by A2, CARD_3: 108;

        hence x in {1} by FINSEQ_1: 2, FINSEQ_1:def 8;

      end;

      let x be object;

      assume

       A3: x in {1};

      for f be Function st f in ( JumpParts T) holds x in ( dom f)

      proof

        let f be Function;

        assume f in ( JumpParts T);

        then

        consider I be Instruction of SCM such that

         A4: f = ( JumpPart I) and

         A5: ( InsCode I) = T;

        consider i1 such that

         A6: I = ( SCM-goto i1) by A1, A5, AMI_5: 13;

        f = <*i1*> by A4, A6;

        hence thesis by A3, FINSEQ_1: 2, FINSEQ_1:def 8;

      end;

      then x in ( DOM ( JumpParts T)) by CARD_3: 109;

      hence thesis by CARD_3:def 12;

    end;

    theorem :: AMI_6:10

    

     Th10: T = 7 implies ( dom ( product" ( JumpParts T))) = {1}

    proof

      set i1 = the Element of NAT , a = the Data-Location;

      assume

       A1: T = 7;

      hereby

        let x be object;

        ( InsCode (a =0_goto i1)) = 7;

        then

         A2: ( JumpPart (a =0_goto i1)) in ( JumpParts T) by A1;

        assume x in ( dom ( product" ( JumpParts T)));

        then x in ( DOM ( JumpParts T)) by CARD_3:def 12;

        then x in ( dom ( JumpPart (a =0_goto i1))) by A2, CARD_3: 108;

        hence x in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      end;

      let x be object;

      assume

       A3: x in {1};

      for f be Function st f in ( JumpParts T) holds x in ( dom f)

      proof

        let f be Function;

        assume f in ( JumpParts T);

        then

        consider I be Instruction of SCM such that

         A4: f = ( JumpPart I) and

         A5: ( InsCode I) = T;

        consider i1, a such that

         A6: I = (a =0_goto i1) by A1, A5, AMI_5: 14;

        f = <*i1*> by A4, A6;

        hence thesis by A3, FINSEQ_1: 2, FINSEQ_1: 38;

      end;

      then x in ( DOM ( JumpParts T)) by CARD_3: 109;

      hence thesis by CARD_3:def 12;

    end;

    theorem :: AMI_6:11

    

     Th11: T = 8 implies ( dom ( product" ( JumpParts T))) = {1}

    proof

      set i1 = the Element of NAT , a = the Data-Location;

      assume

       A1: T = 8;

      hereby

        let x be object;

        ( InsCode (a >0_goto i1)) = 8;

        then

         A2: ( JumpPart (a >0_goto i1)) in ( JumpParts T) by A1;

        assume x in ( dom ( product" ( JumpParts T)));

        then x in ( DOM ( JumpParts T)) by CARD_3:def 12;

        then x in ( dom ( JumpPart (a >0_goto i1))) by A2, CARD_3: 108;

        hence x in {1} by FINSEQ_1: 2, FINSEQ_1: 38;

      end;

      let x be object;

      assume

       A3: x in {1};

      for f be Function st f in ( JumpParts T) holds x in ( dom f)

      proof

        let f be Function;

        assume f in ( JumpParts T);

        then

        consider I be Instruction of SCM such that

         A4: f = ( JumpPart I) and

         A5: ( InsCode I) = T;

        consider i1, a such that

         A6: I = (a >0_goto i1) by A1, A5, AMI_5: 15;

        f = <*i1*> by A4, A6;

        hence thesis by A3, FINSEQ_1: 2, FINSEQ_1: 38;

      end;

      then x in ( DOM ( JumpParts T)) by CARD_3: 109;

      hence thesis by CARD_3:def 12;

    end;

    theorem :: AMI_6:12

    (( product" ( JumpParts ( InsCode ( SCM-goto k1)))) . 1) = NAT

    proof

      ( dom ( product" ( JumpParts ( InsCode ( SCM-goto k1))))) = {1} by Th9;

      then

       A1: 1 in ( dom ( product" ( JumpParts ( InsCode ( SCM-goto k1))))) by TARSKI:def 1;

      hereby

        let x be object;

        assume x in (( product" ( JumpParts ( InsCode ( SCM-goto k1)))) . 1);

        then x in ( pi (( JumpParts ( InsCode ( SCM-goto k1))),1)) by A1, CARD_3:def 12;

        then

        consider g be Function such that

         A2: g in ( JumpParts ( InsCode ( SCM-goto k1))) and

         A3: x = (g . 1) by CARD_3:def 6;

        consider I be Instruction of SCM such that

         A4: g = ( JumpPart I) and

         A5: ( InsCode I) = ( InsCode ( SCM-goto k1)) by A2;

        ( InsCode I) = 6 by A5;

        then

        consider i2 such that

         A6: I = ( SCM-goto i2) by AMI_5: 13;

        g = <*i2*> by A4, A6;

        then x = i2 by A3, FINSEQ_1:def 8;

        hence x in NAT by ORDINAL1:def 12;

      end;

      let x be object;

      assume x in NAT ;

      then

      reconsider x as Element of NAT ;

      ( JumpPart ( SCM-goto x)) = <*x*> & ( InsCode ( SCM-goto k1)) = ( InsCode ( SCM-goto x));

      then

       A7: <*x*> in ( JumpParts ( InsCode ( SCM-goto k1)));

      ( <*x*> . 1) = x by FINSEQ_1:def 8;

      then x in ( pi (( JumpParts ( InsCode ( SCM-goto k1))),1)) by A7, CARD_3:def 6;

      hence thesis by A1, CARD_3:def 12;

    end;

    theorem :: AMI_6:13

    (( product" ( JumpParts ( InsCode (a =0_goto k1)))) . 1) = NAT

    proof

      ( dom ( product" ( JumpParts ( InsCode (a =0_goto k1))))) = {1} by Th10;

      then

       A1: 1 in ( dom ( product" ( JumpParts ( InsCode (a =0_goto k1))))) by TARSKI:def 1;

      hereby

        let x be object;

        assume x in (( product" ( JumpParts ( InsCode (a =0_goto k1)))) . 1);

        then x in ( pi (( JumpParts ( InsCode (a =0_goto k1))),1)) by A1, CARD_3:def 12;

        then

        consider g be Function such that

         A2: g in ( JumpParts ( InsCode (a =0_goto k1))) and

         A3: x = (g . 1) by CARD_3:def 6;

        consider I be Instruction of SCM such that

         A4: g = ( JumpPart I) and

         A5: ( InsCode I) = ( InsCode (a =0_goto k1)) by A2;

        ( InsCode I) = 7 by A5;

        then

        consider i2, b such that

         A6: I = (b =0_goto i2) by AMI_5: 14;

        g = <*i2*> by A4, A6;

        then x = i2 by A3, FINSEQ_1: 40;

        hence x in NAT by ORDINAL1:def 12;

      end;

      let x be object;

      assume x in NAT ;

      then

      reconsider x as Element of NAT ;

      ( JumpPart (a =0_goto x)) = <*x*> & ( InsCode (a =0_goto k1)) = ( InsCode (a =0_goto x));

      then

       A7: <*x*> in ( JumpParts ( InsCode (a =0_goto k1)));

      ( <*x*> . 1) = x by FINSEQ_1: 40;

      then x in ( pi (( JumpParts ( InsCode (a =0_goto k1))),1)) by A7, CARD_3:def 6;

      hence thesis by A1, CARD_3:def 12;

    end;

    theorem :: AMI_6:14

    (( product" ( JumpParts ( InsCode (a >0_goto k1)))) . 1) = NAT

    proof

      ( dom ( product" ( JumpParts ( InsCode (a >0_goto k1))))) = {1} by Th11;

      then

       A1: 1 in ( dom ( product" ( JumpParts ( InsCode (a >0_goto k1))))) by TARSKI:def 1;

      hereby

        let x be object;

        assume x in (( product" ( JumpParts ( InsCode (a >0_goto k1)))) . 1);

        then x in ( pi (( JumpParts ( InsCode (a >0_goto k1))),1)) by A1, CARD_3:def 12;

        then

        consider g be Function such that

         A2: g in ( JumpParts ( InsCode (a >0_goto k1))) and

         A3: x = (g . 1) by CARD_3:def 6;

        consider I be Instruction of SCM such that

         A4: g = ( JumpPart I) and

         A5: ( InsCode I) = ( InsCode (a >0_goto k1)) by A2;

        ( InsCode I) = 8 by A5;

        then

        consider i2, b such that

         A6: I = (b >0_goto i2) by AMI_5: 15;

        g = <*i2*> by A4, A6;

        then x = i2 by A3, FINSEQ_1: 40;

        hence x in NAT by ORDINAL1:def 12;

      end;

      let x be object;

      assume x in NAT ;

      then

      reconsider x as Element of NAT ;

      ( JumpPart (a >0_goto x)) = <*x*> & ( InsCode (a >0_goto k1)) = ( InsCode (a >0_goto x));

      then

       A7: <*x*> in ( JumpParts ( InsCode (a >0_goto k1)));

      ( <*x*> . 1) = x by FINSEQ_1: 40;

      then x in ( pi (( JumpParts ( InsCode (a >0_goto k1))),1)) by A7, CARD_3:def 6;

      hence thesis by A1, CARD_3:def 12;

    end;

    

     Lm1: for i be Instruction of SCM holds (for l be Element of NAT holds ( NIC (i,l)) = {(l + 1)}) implies ( JUMP i) is empty

    proof

      set p = 1, q = 2;

      let i be Instruction of SCM ;

      assume

       A1: for l be Element of NAT holds ( NIC (i,l)) = {(l + 1)};

      set X = the set of all ( NIC (i,f)) where f be Nat;

      reconsider p, q as Element of NAT ;

      assume not thesis;

      then

      consider x be object such that

       A2: x in ( meet X);

      ( NIC (i,p)) = {(p + 1)} by A1;

      then {( succ p)} in X;

      then x in {( succ p)} by A2, SETFAM_1:def 1;

      then

       A3: x = ( succ p) by TARSKI:def 1;

      ( NIC (i,q)) = {(q + 1)} by A1;

      then {( succ q)} in X;

      then x in {( succ q)} by A2, SETFAM_1:def 1;

      hence contradiction by A3, TARSKI:def 1;

    end;

    registration

      cluster ( JUMP ( halt SCM )) -> empty;

      coherence ;

    end

    registration

      let a, b;

      cluster (a := b) -> sequential;

      coherence by AMI_3: 2;

      cluster ( AddTo (a,b)) -> sequential;

      coherence by AMI_3: 3;

      cluster ( SubFrom (a,b)) -> sequential;

      coherence by AMI_3: 4;

      cluster ( MultBy (a,b)) -> sequential;

      coherence by AMI_3: 5;

      cluster ( Divide (a,b)) -> sequential;

      coherence by AMI_3: 6;

    end

    registration

      let a, b;

      cluster ( JUMP (a := b)) -> empty;

      coherence

      proof

        for l be Element of NAT holds ( NIC ((a := b),l)) = {(l + 1)} by AMISTD_1: 12;

        hence thesis by Lm1;

      end;

    end

    registration

      let a, b;

      cluster ( JUMP ( AddTo (a,b))) -> empty;

      coherence

      proof

        for l be Element of NAT holds ( NIC (( AddTo (a,b)),l)) = {(l + 1)} by AMISTD_1: 12;

        hence thesis by Lm1;

      end;

    end

    registration

      let a, b;

      cluster ( JUMP ( SubFrom (a,b))) -> empty;

      coherence

      proof

        for l be Element of NAT holds ( NIC (( SubFrom (a,b)),l)) = {(l + 1)} by AMISTD_1: 12;

        hence thesis by Lm1;

      end;

    end

    registration

      let a, b;

      cluster ( JUMP ( MultBy (a,b))) -> empty;

      coherence

      proof

        for l be Element of NAT holds ( NIC (( MultBy (a,b)),l)) = {(l + 1)} by AMISTD_1: 12;

        hence thesis by Lm1;

      end;

    end

    registration

      let a, b;

      cluster ( JUMP ( Divide (a,b))) -> empty;

      coherence

      proof

        for l be Element of NAT holds ( NIC (( Divide (a,b)),l)) = {(l + 1)} by AMISTD_1: 12;

        hence thesis by Lm1;

      end;

    end

    theorem :: AMI_6:15

    

     Th15: ( NIC (( SCM-goto k),il)) = {k}

    proof

      now

        let x be object;

         A1:

        now

          il in NAT by ORDINAL1:def 12;

          then

          reconsider il1 = il as Element of ( Values ( IC SCM )) by MEMSTR_0:def 6;

          set I = ( SCM-goto k);

          set t = the State of SCM , Q = the Instruction-Sequence of SCM ;

          assume

           A2: x = k;

          reconsider n = il as Element of NAT by ORDINAL1:def 12;

          reconsider u = (t +* (( IC SCM ),il1)) as Element of ( product ( the_Values_of SCM )) by CARD_3: 107;

          reconsider P = (Q +* (il,I)) as Instruction-Sequence of SCM ;

          reconsider ill = il as Element of NAT by ORDINAL1:def 12;

          

           A3: (P /. ill) = (P . ill) by PBOOLE: 143;

          ( IC SCM ) in ( dom t) by MEMSTR_0: 2;

          then

           A4: ( IC u) = n by FUNCT_7: 31;

          il in NAT by ORDINAL1:def 12;

          then il in ( dom Q) by PARTFUN1:def 2;

          then

           A5: (P . n) = I by FUNCT_7: 31;

          then ( IC ( Following (P,u))) = k by A3, A4, AMI_3: 7;

          hence x in { ( IC ( Exec (( SCM-goto k),s))) where s be Element of ( product ( the_Values_of SCM )) : ( IC s) = il } by A2, A4, A3, A5;

        end;

        now

          assume x in { ( IC ( Exec (( SCM-goto k),s))) where s be Element of ( product ( the_Values_of SCM )) : ( IC s) = il };

          then ex s be Element of ( product ( the_Values_of SCM )) st x = ( IC ( Exec (( SCM-goto k),s))) & ( IC s) = il;

          hence x = k by AMI_3: 7;

        end;

        hence x in {k} iff x in { ( IC ( Exec (( SCM-goto k),s))) where s be Element of ( product ( the_Values_of SCM )) : ( IC s) = il } by A1, TARSKI:def 1;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: AMI_6:16

    

     Th16: ( JUMP ( SCM-goto k)) = {k}

    proof

      set X = the set of all ( NIC (( SCM-goto k),il));

      now

        let x be object;

        hereby

          set il1 = 1;

          

           A1: ( NIC (( SCM-goto k),il1)) in X;

          assume x in ( meet X);

          then x in ( NIC (( SCM-goto k),il1)) by A1, SETFAM_1:def 1;

          hence x in {k} by Th15;

        end;

        assume x in {k};

        then

         A2: x = k by TARSKI:def 1;

         A3:

        now

          let Y be set;

          assume Y in X;

          then

          consider il be Nat such that

           A4: Y = ( NIC (( SCM-goto k),il));

          ( NIC (( SCM-goto k),il)) = {k} by Th15;

          hence k in Y by A4, TARSKI:def 1;

        end;

        reconsider k as Element of NAT by ORDINAL1:def 12;

        ( NIC (( SCM-goto k),k)) in X;

        hence x in ( meet X) by A2, A3, SETFAM_1:def 1;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let i1;

      cluster ( JUMP ( SCM-goto i1)) -> 1 -element;

      coherence

      proof

        ( JUMP ( SCM-goto i1)) = {i1} by Th16;

        hence thesis;

      end;

    end

    theorem :: AMI_6:17

    

     Th17: ( NIC ((a =0_goto k),il)) = {k, (il + 1)}

    proof

      set t = the State of SCM , Q = the Instruction-Sequence of SCM ;

      hereby

        let x be object;

        assume x in ( NIC ((a =0_goto k),il));

        then

        consider s be Element of ( product ( the_Values_of SCM )) such that

         A1: x = ( IC ( Exec ((a =0_goto k),s))) & ( IC s) = il;

        per cases ;

          suppose (s . a) = 0 ;

          then x = k by A1, AMI_3: 8;

          hence x in {k, (il + 1)} by TARSKI:def 2;

        end;

          suppose (s . a) <> 0 ;

          then x = (il + 1) by A1, AMI_3: 8;

          hence x in {k, (il + 1)} by TARSKI:def 2;

        end;

      end;

      let x be object;

      set I = (a =0_goto k);

      

       A2: ( IC SCM ) <> a by AMI_5: 2;

      reconsider n = il as Element of NAT by ORDINAL1:def 12;

      reconsider il1 = n as Element of ( Values ( IC SCM )) by MEMSTR_0:def 6;

      reconsider u = (t +* (( IC SCM ),il1)) as Element of ( product ( the_Values_of SCM )) by CARD_3: 107;

      reconsider P = (Q +* (il,I)) as Instruction-Sequence of SCM ;

      assume

       A3: x in {k, (il + 1)};

      per cases by A3, TARSKI:def 2;

        suppose

         A4: x = k;

        reconsider v = (u +* (a .--> 0 )) as Element of ( product ( the_Values_of SCM )) by CARD_3: 107;

        

         A5: ( IC SCM ) in ( dom t) by MEMSTR_0: 2;

         not ( IC SCM ) in ( dom (a .--> 0 )) by A2, TARSKI:def 1;

        

        then

         A7: ( IC v) = ( IC u) by FUNCT_4: 11

        .= n by A5, FUNCT_7: 31;

        reconsider il as Element of NAT by ORDINAL1:def 12;

        

         A8: (P /. il) = (P . il) by PBOOLE: 143;

        il in NAT ;

        then il in ( dom Q) by PARTFUN1:def 2;

        then

         A9: (P . il) = I by FUNCT_7: 31;

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

        

        then (v . a) = ((a .--> 0 ) . a) by FUNCT_4: 13

        .= 0 by FUNCOP_1: 72;

        then ( IC ( Following (P,v))) = k by A7, A9, A8, AMI_3: 8;

        hence thesis by A4, A7, A9, A8;

      end;

        suppose

         A10: x = (il + 1);

        reconsider v = (u +* (a .--> 1)) as Element of ( product ( the_Values_of SCM )) by CARD_3: 107;

        

         A11: ( IC SCM ) in ( dom t) by MEMSTR_0: 2;

         not ( IC SCM ) in ( dom (a .--> 1)) by A2, TARSKI:def 1;

        

        then

         A13: ( IC v) = ( IC u) by FUNCT_4: 11

        .= n by A11, FUNCT_7: 31;

        reconsider il as Element of NAT by ORDINAL1:def 12;

        

         A14: (P /. il) = (P . il) by PBOOLE: 143;

        il in NAT ;

        then il in ( dom Q) by PARTFUN1:def 2;

        then

         A15: (P . il) = I by FUNCT_7: 31;

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

        

        then (v . a) = ((a .--> 1) . a) by FUNCT_4: 13

        .= 1 by FUNCOP_1: 72;

        then ( IC ( Following (P,v))) = (il + 1) by A13, A15, A14, AMI_3: 8;

        hence thesis by A10, A13, A15, A14;

      end;

    end;

    theorem :: AMI_6:18

    

     Th18: ( JUMP (a =0_goto k)) = {k}

    proof

      set X = the set of all ( NIC ((a =0_goto k),il));

      now

        let x be object;

         A1:

        now

          let Y be set;

          assume Y in X;

          then

          consider il be Nat such that

           A2: Y = ( NIC ((a =0_goto k),il));

          ( NIC ((a =0_goto k),il)) = {k, (il + 1)} by Th17;

          hence k in Y by A2, TARSKI:def 2;

        end;

        hereby

          set il1 = 1, il2 = 2;

          assume

           A3: x in ( meet X);

          

           A4: ( NIC ((a =0_goto k),il2)) = {k, (il2 + 1)} by Th17;

          ( NIC ((a =0_goto k),il2)) in X;

          then x in ( NIC ((a =0_goto k),il2)) by A3, SETFAM_1:def 1;

          then

           A5: x = k or x = (il2 + 1) by A4, TARSKI:def 2;

          

           A6: ( NIC ((a =0_goto k),il1)) = {k, (il1 + 1)} by Th17;

          ( NIC ((a =0_goto k),il1)) in X;

          then x in ( NIC ((a =0_goto k),il1)) by A3, SETFAM_1:def 1;

          then x = k or x = (il1 + 1) by A6, TARSKI:def 2;

          hence x in {k} by A5, TARSKI:def 1;

        end;

        assume x in {k};

        then

         A7: x = k by TARSKI:def 1;

        reconsider k as Element of NAT by ORDINAL1:def 12;

        ( NIC ((a =0_goto k),k)) in X;

        hence x in ( meet X) by A7, A1, SETFAM_1:def 1;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let a, i1;

      cluster ( JUMP (a =0_goto i1)) -> 1 -element;

      coherence

      proof

        ( JUMP (a =0_goto i1)) = {i1} by Th18;

        hence thesis;

      end;

    end

    theorem :: AMI_6:19

    

     Th19: ( NIC ((a >0_goto k),il)) = {k, (il + 1)}

    proof

      set t = the State of SCM , Q = the Instruction-Sequence of SCM ;

      hereby

        let x be object;

        assume x in ( NIC ((a >0_goto k),il));

        then

        consider s be Element of ( product ( the_Values_of SCM )) such that

         A1: x = ( IC ( Exec ((a >0_goto k),s))) & ( IC s) = il;

        per cases ;

          suppose (s . a) > 0 ;

          then x = k by A1, AMI_3: 9;

          hence x in {k, (il + 1)} by TARSKI:def 2;

        end;

          suppose (s . a) <= 0 ;

          then x = (il + 1) by A1, AMI_3: 9;

          hence x in {k, (il + 1)} by TARSKI:def 2;

        end;

      end;

      let x be object;

      set I = (a >0_goto k);

      

       A2: ( IC SCM ) <> a by AMI_5: 2;

      assume

       A3: x in {k, (il + 1)};

      reconsider n = il as Element of NAT by ORDINAL1:def 12;

      reconsider il1 = n as Element of ( Values ( IC SCM )) by MEMSTR_0:def 6;

      reconsider u = (t +* (( IC SCM ),il1)) as Element of ( product ( the_Values_of SCM )) by CARD_3: 107;

      reconsider P = (Q +* (il,I)) as Instruction-Sequence of SCM ;

      per cases by A3, TARSKI:def 2;

        suppose

         A4: x = k;

        reconsider v = (u +* (a .--> 1)) as Element of ( product ( the_Values_of SCM )) by CARD_3: 107;

        

         A5: ( IC SCM ) in ( dom t) by MEMSTR_0: 2;

         not ( IC SCM ) in ( dom (a .--> 1)) by A2, TARSKI:def 1;

        

        then

         A7: ( IC v) = ( IC u) by FUNCT_4: 11

        .= n by A5, FUNCT_7: 31;

        reconsider il as Element of NAT by ORDINAL1:def 12;

        

         A8: (P /. il) = (P . il) by PBOOLE: 143;

        il in NAT ;

        then il in ( dom Q) by PARTFUN1:def 2;

        then

         A9: (P . il) = I by FUNCT_7: 31;

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

        

        then (v . a) = ((a .--> 1) . a) by FUNCT_4: 13

        .= 1 by FUNCOP_1: 72;

        then ( IC ( Following (P,v))) = k by A7, A9, A8, AMI_3: 9;

        hence thesis by A4, A7, A9, A8;

      end;

        suppose

         A10: x = (il + 1);

        reconsider v = (u +* (a .--> 0 )) as Element of ( product ( the_Values_of SCM )) by CARD_3: 107;

        

         A11: ( IC SCM ) in ( dom t) by MEMSTR_0: 2;

         not ( IC SCM ) in ( dom (a .--> 0 )) by A2, TARSKI:def 1;

        

        then

         A13: ( IC v) = ( IC u) by FUNCT_4: 11

        .= n by A11, FUNCT_7: 31;

        reconsider il as Element of NAT by ORDINAL1:def 12;

        

         A14: (P /. il) = (P . il) by PBOOLE: 143;

        il in NAT ;

        then il in ( dom Q) by PARTFUN1:def 2;

        then

         A15: (P . il) = I by FUNCT_7: 31;

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

        

        then (v . a) = ((a .--> 0 ) . a) by FUNCT_4: 13

        .= 0 by FUNCOP_1: 72;

        then ( IC ( Following (P,v))) = (il + 1) by A13, A15, A14, AMI_3: 9;

        hence thesis by A10, A13, A15, A14;

      end;

    end;

    theorem :: AMI_6:20

    

     Th20: ( JUMP (a >0_goto k)) = {k}

    proof

      set X = the set of all ( NIC ((a >0_goto k),il));

      now

        let x be object;

         A1:

        now

          let Y be set;

          assume Y in X;

          then

          consider il be Nat such that

           A2: Y = ( NIC ((a >0_goto k),il));

          ( NIC ((a >0_goto k),il)) = {k, (il + 1)} by Th19;

          hence k in Y by A2, TARSKI:def 2;

        end;

        hereby

          set il1 = 1, il2 = 2;

          assume

           A3: x in ( meet X);

          

           A4: ( NIC ((a >0_goto k),il2)) = {k, (il2 + 1)} by Th19;

          ( NIC ((a >0_goto k),il2)) in X;

          then x in ( NIC ((a >0_goto k),il2)) by A3, SETFAM_1:def 1;

          then

           A5: x = k or x = (il2 + 1) by A4, TARSKI:def 2;

          

           A6: ( NIC ((a >0_goto k),il1)) = {k, (il1 + 1)} by Th19;

          ( NIC ((a >0_goto k),il1)) in X;

          then x in ( NIC ((a >0_goto k),il1)) by A3, SETFAM_1:def 1;

          then x = k or x = (il1 + 1) by A6, TARSKI:def 2;

          hence x in {k} by A5, TARSKI:def 1;

        end;

        assume x in {k};

        then

         A7: x = k by TARSKI:def 1;

        reconsider k as Element of NAT by ORDINAL1:def 12;

        ( NIC ((a >0_goto k),k)) in X;

        hence x in ( meet X) by A7, A1, SETFAM_1:def 1;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let a, i1;

      cluster ( JUMP (a >0_goto i1)) -> 1 -element;

      coherence

      proof

        ( JUMP (a >0_goto i1)) = {i1} by Th20;

        hence thesis;

      end;

    end

    theorem :: AMI_6:21

    

     Th21: ( SUCC (il, SCM )) = {il, (il + 1)}

    proof

      set X = the set of all (( NIC (I,il)) \ ( JUMP I)) where I be Element of the InstructionsF of SCM ;

      set N = {il, (il + 1)};

      now

        let x be object;

        hereby

          assume x in ( union X);

          then

          consider Y be set such that

           A1: x in Y and

           A2: Y in X by TARSKI:def 4;

          consider i be Element of the InstructionsF of SCM such that

           A3: Y = (( NIC (i,il)) \ ( JUMP i)) by A2;

          per cases by AMI_3: 24;

            suppose i = [ 0 , {} , {} ];

            then x in ( {il} \ ( JUMP ( halt SCM ))) by A1, A3, AMISTD_1: 2;

            then x = il by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

            suppose ex a, b st i = (a := b);

            then

            consider a, b such that

             A4: i = (a := b);

            x in ( {(il + 1)} \ ( JUMP (a := b))) by A1, A3, A4, AMISTD_1: 12;

            then x = (il + 1) by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

            suppose ex a, b st i = ( AddTo (a,b));

            then

            consider a, b such that

             A5: i = ( AddTo (a,b));

            x in ( {(il + 1)} \ ( JUMP ( AddTo (a,b)))) by A1, A3, A5, AMISTD_1: 12;

            then x = (il + 1) by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

            suppose ex a, b st i = ( SubFrom (a,b));

            then

            consider a, b such that

             A6: i = ( SubFrom (a,b));

            x in ( {(il + 1)} \ ( JUMP ( SubFrom (a,b)))) by A1, A3, A6, AMISTD_1: 12;

            then x = (il + 1) by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

            suppose ex a, b st i = ( MultBy (a,b));

            then

            consider a, b such that

             A7: i = ( MultBy (a,b));

            x in ( {(il + 1)} \ ( JUMP ( MultBy (a,b)))) by A1, A3, A7, AMISTD_1: 12;

            then x = (il + 1) by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

            suppose ex a, b st i = ( Divide (a,b));

            then

            consider a, b such that

             A8: i = ( Divide (a,b));

            x in ( {(il + 1)} \ ( JUMP ( Divide (a,b)))) by A1, A3, A8, AMISTD_1: 12;

            then x = (il + 1) by TARSKI:def 1;

            hence x in N by TARSKI:def 2;

          end;

            suppose ex k st i = ( SCM-goto k);

            then

            consider k such that

             A9: i = ( SCM-goto k);

            x in ( {k} \ ( JUMP i)) by A1, A3, A9, Th15;

            then x in ( {k} \ {k}) by A9, Th16;

            hence x in N by XBOOLE_1: 37;

          end;

            suppose ex a, k st i = (a =0_goto k);

            then

            consider a, k such that

             A10: i = (a =0_goto k);

            

             A11: ( NIC (i,il)) = {k, (il + 1)} by A10, Th17;

            x in ( NIC (i,il)) by A1, A3, XBOOLE_0:def 5;

            then

             A12: x = k or x = (il + 1) by A11, TARSKI:def 2;

            x in (( NIC (i,il)) \ {k}) by A1, A3, A10, Th18;

            then not x in {k} by XBOOLE_0:def 5;

            hence x in N by A12, TARSKI:def 1, TARSKI:def 2;

          end;

            suppose ex a, k st i = (a >0_goto k);

            then

            consider a, k such that

             A13: i = (a >0_goto k);

            

             A14: ( NIC (i,il)) = {k, (il + 1)} by A13, Th19;

            x in ( NIC (i,il)) by A1, A3, XBOOLE_0:def 5;

            then

             A15: x = k or x = (il + 1) by A14, TARSKI:def 2;

            x in (( NIC (i,il)) \ {k}) by A1, A3, A13, Th20;

            then not x in {k} by XBOOLE_0:def 5;

            hence x in N by A15, TARSKI:def 1, TARSKI:def 2;

          end;

        end;

        assume

         A16: x in {il, (il + 1)};

        per cases by A16, TARSKI:def 2;

          suppose

           A17: x = il;

          set i = ( halt SCM );

          (( NIC (i,il)) \ ( JUMP i)) = {il} by AMISTD_1: 2;

          then

           A18: {il} in X;

          x in {il} by A17, TARSKI:def 1;

          hence x in ( union X) by A18, TARSKI:def 4;

        end;

          suppose

           A19: x = (il + 1);

          set a = the Data-Location;

          set i = ( AddTo (a,a));

          (( NIC (i,il)) \ ( JUMP i)) = {(il + 1)} by AMISTD_1: 12;

          then

           A20: {(il + 1)} in X;

          x in {(il + 1)} by A19, TARSKI:def 1;

          hence x in ( union X) by A20, TARSKI:def 4;

        end;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: AMI_6:22

    

     Th22: for k be Nat holds (k + 1) in ( SUCC (k, SCM )) & for j be Nat st j in ( SUCC (k, SCM )) holds k <= j

    proof

      let k be Nat;

      reconsider fk = k as Element of NAT by ORDINAL1:def 12;

      

       A1: ( SUCC (k, SCM )) = {k, (fk + 1)} by Th21;

      hence (k + 1) in ( SUCC (k, SCM )) by TARSKI:def 2;

      let j be Nat;

      assume

       A2: j in ( SUCC (k, SCM ));

      reconsider fk = k as Element of NAT by ORDINAL1:def 12;

      per cases by A1, A2, TARSKI:def 2;

        suppose j = k;

        hence thesis;

      end;

        suppose j = (fk + 1);

        hence thesis by NAT_1: 11;

      end;

    end;

    registration

      cluster SCM -> standard;

      coherence by Th22, AMISTD_1: 3;

    end

    registration

      cluster ( InsCode ( halt SCM )) -> jump-only;

      coherence

      proof

        now

          let s be State of SCM , o be Object of SCM , I be Instruction of SCM ;

          assume that

           A1: ( InsCode I) = ( InsCode ( halt SCM )) and o in ( Data-Locations SCM );

          I = ( halt SCM ) by A1, AMI_5: 7;

          hence (( Exec (I,s)) . o) = (s . o) by EXTPRO_1:def 3;

        end;

        hence thesis;

      end;

    end

    registration

      cluster ( halt SCM ) -> jump-only;

      coherence ;

    end

    registration

      let i1;

      cluster ( InsCode ( SCM-goto i1)) -> jump-only;

      coherence

      proof

        let T be InsType of the InstructionsF of SCM such that

         A1: T = ( InsCode ( SCM-goto i1));

        let s be State of SCM , o be Object of SCM , I be Instruction of SCM ;

        assume that

         A2: ( InsCode I) = T and

         A3: o in ( Data-Locations SCM );

        ( InsCode I) = 6 by A2, A1;

        then

         A4: ex i2 st I = ( SCM-goto i2) by AMI_5: 13;

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

        hence (( Exec (I,s)) . o) = (s . o) by A4, AMI_3: 7;

      end;

    end

    registration

      let i1;

      cluster ( SCM-goto i1) -> jump-only non sequential non ins-loc-free;

      coherence

      proof

        thus ( InsCode ( SCM-goto i1)) is jump-only;

        ( JUMP ( SCM-goto i1)) <> {} ;

        hence ( SCM-goto i1) is non sequential by AMISTD_1: 13;

        thus not ( JumpPart ( SCM-goto i1)) is empty;

      end;

    end

    registration

      let a, i1;

      cluster ( InsCode (a =0_goto i1)) -> jump-only;

      coherence

      proof

        set S = SCM ;

        now

          let s be State of S, o be Object of S, I be Instruction of S;

          assume that

           A1: ( InsCode I) = ( InsCode (a =0_goto i1)) and

           A2: o in ( Data-Locations SCM );

          ( InsCode I) = 7 by A1;

          then

           A3: ex i2, b st I = (b =0_goto i2) by AMI_5: 14;

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

          hence (( Exec (I,s)) . o) = (s . o) by A3, AMI_3: 8;

        end;

        hence thesis;

      end;

      cluster ( InsCode (a >0_goto i1)) -> jump-only;

      coherence

      proof

        set S = SCM ;

        now

          let s be State of S, o be Object of S, I be Instruction of S;

          assume that

           A4: ( InsCode I) = ( InsCode (a >0_goto i1)) and

           A5: o in ( Data-Locations SCM );

          ( InsCode I) = 8 by A4;

          then

           A6: ex i2, b st I = (b >0_goto i2) by AMI_5: 15;

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

          hence (( Exec (I,s)) . o) = (s . o) by A6, AMI_3: 9;

        end;

        hence thesis;

      end;

    end

    registration

      let a, i1;

      cluster (a =0_goto i1) -> jump-only non sequential non ins-loc-free;

      coherence

      proof

        thus ( InsCode (a =0_goto i1)) is jump-only;

        ( JUMP (a =0_goto i1)) <> {} ;

        hence (a =0_goto i1) is non sequential by AMISTD_1: 13;

        thus not ( JumpPart (a =0_goto i1)) is empty;

      end;

      cluster (a >0_goto i1) -> jump-only non sequential non ins-loc-free;

      coherence

      proof

        thus ( InsCode (a >0_goto i1)) is jump-only;

        ( JUMP (a >0_goto i1)) <> {} ;

        hence (a >0_goto i1) is non sequential by AMISTD_1: 13;

        thus not ( JumpPart (a >0_goto i1)) is empty;

      end;

    end

    

     Lm2: ( dl. 0 ) <> ( dl. 1) by AMI_3: 10;

    registration

      let a, b;

      cluster ( InsCode (a := b)) -> non jump-only;

      coherence

      proof

        set w = the State of SCM ;

        set t = (w +* ((( dl. 0 ),( dl. 1)) --> ( 0 ,1)));

        

         A1: ( InsCode (a := b)) = 1

        .= ( InsCode (( dl. 0 ) := ( dl. 1)));

        

         A2: ( dl. 0 ) in ( Data-Locations SCM ) by AMI_3: 28;

        

         A3: ( dom ((( dl. 0 ),( dl. 1)) --> ( 0 ,1))) = {( dl. 0 ), ( dl. 1)} by FUNCT_4: 62;

        then

         A4: ( dl. 1) in ( dom ((( dl. 0 ),( dl. 1)) --> ( 0 ,1))) by TARSKI:def 2;

        ( dl. 0 ) in ( dom ((( dl. 0 ),( dl. 1)) --> ( 0 ,1))) by A3, TARSKI:def 2;

        

        then

         A5: (t . ( dl. 0 )) = (((( dl. 0 ),( dl. 1)) --> ( 0 ,1)) . ( dl. 0 )) by FUNCT_4: 13

        .= 0 by AMI_3: 10, FUNCT_4: 63;

        (( Exec ((( dl. 0 ) := ( dl. 1)),t)) . ( dl. 0 )) = (t . ( dl. 1)) by AMI_3: 2

        .= (((( dl. 0 ),( dl. 1)) --> ( 0 ,1)) . ( dl. 1)) by A4, FUNCT_4: 13

        .= 1 by FUNCT_4: 63;

        hence thesis by A1, A2, A5;

      end;

      cluster ( InsCode ( AddTo (a,b))) -> non jump-only;

      coherence

      proof

        set w = the State of SCM ;

        set t = (w +* ((( dl. 0 ),( dl. 1)) --> ( 0 ,1)));

        

         A6: ( InsCode ( AddTo (a,b))) = 2

        .= ( InsCode ( AddTo (( dl. 0 ),( dl. 1))));

        

         A7: ( dom ((( dl. 0 ),( dl. 1)) --> ( 0 ,1))) = {( dl. 0 ), ( dl. 1)} by FUNCT_4: 62;

        then ( dl. 0 ) in ( dom ((( dl. 0 ),( dl. 1)) --> ( 0 ,1))) by TARSKI:def 2;

        

        then

         A8: (t . ( dl. 0 )) = (((( dl. 0 ),( dl. 1)) --> ( 0 ,1)) . ( dl. 0 )) by FUNCT_4: 13

        .= 0 by AMI_3: 10, FUNCT_4: 63;

        

         A9: ( dl. 0 ) in ( Data-Locations SCM ) by AMI_3: 28;

        ( dl. 1) in ( dom ((( dl. 0 ),( dl. 1)) --> ( 0 ,1))) by A7, TARSKI:def 2;

        

        then (t . ( dl. 1)) = (((( dl. 0 ),( dl. 1)) --> ( 0 ,1)) . ( dl. 1)) by FUNCT_4: 13

        .= 1 by FUNCT_4: 63;

        then ( dl. 0 ) <> ( IC SCM ) & (( Exec (( AddTo (( dl. 0 ),( dl. 1))),t)) . ( dl. 0 )) = ( 0 qua Nat + 1) by A8, AMI_3: 3, AMI_3: 13;

        hence thesis by A6, A8, A9;

      end;

      cluster ( InsCode ( SubFrom (a,b))) -> non jump-only;

      coherence

      proof

        set w = the State of SCM ;

        set t = (w +* ((( dl. 0 ),( dl. 1)) --> ( 0 ,1)));

        

         A10: ( InsCode ( SubFrom (a,b))) = 3

        .= ( InsCode ( SubFrom (( dl. 0 ),( dl. 1))));

        

         A11: ( dom ((( dl. 0 ),( dl. 1)) --> ( 0 ,1))) = {( dl. 0 ), ( dl. 1)} by FUNCT_4: 62;

        then ( dl. 0 ) in ( dom ((( dl. 0 ),( dl. 1)) --> ( 0 ,1))) by TARSKI:def 2;

        

        then

         A12: (t . ( dl. 0 )) = (((( dl. 0 ),( dl. 1)) --> ( 0 ,1)) . ( dl. 0 )) by FUNCT_4: 13

        .= 0 by AMI_3: 10, FUNCT_4: 63;

        

         A13: ( dl. 0 ) in ( Data-Locations SCM ) by AMI_3: 28;

        ( dl. 1) in ( dom ((( dl. 0 ),( dl. 1)) --> ( 0 ,1))) by A11, TARSKI:def 2;

        

        then

         A14: (t . ( dl. 1)) = (((( dl. 0 ),( dl. 1)) --> ( 0 ,1)) . ( dl. 1)) by FUNCT_4: 13

        .= 1 by FUNCT_4: 63;

        (( Exec (( SubFrom (( dl. 0 ),( dl. 1))),t)) . ( dl. 0 )) = ((t . ( dl. 0 )) - (t . ( dl. 1))) by AMI_3: 4

        .= ( - 1) by A12, A14;

        hence thesis by A10, A12, A13;

      end;

      cluster ( InsCode ( MultBy (a,b))) -> non jump-only;

      coherence

      proof

        set w = the State of SCM ;

        set t = (w +* ((( dl. 0 ),( dl. 1)) --> (1, 0 )));

        

         A15: ( InsCode ( MultBy (a,b))) = 4

        .= ( InsCode ( MultBy (( dl. 0 ),( dl. 1))));

        

         A16: ( dom ((( dl. 0 ),( dl. 1)) --> (1, 0 ))) = {( dl. 0 ), ( dl. 1)} by FUNCT_4: 62;

        then ( dl. 0 ) in ( dom ((( dl. 0 ),( dl. 1)) --> (1, 0 ))) by TARSKI:def 2;

        

        then

         A17: (t . ( dl. 0 )) = (((( dl. 0 ),( dl. 1)) --> (1, 0 )) . ( dl. 0 )) by FUNCT_4: 13

        .= 1 by AMI_3: 10, FUNCT_4: 63;

        

         A18: ( dl. 0 ) in ( Data-Locations SCM ) by AMI_3: 28;

        ( dl. 1) in ( dom ((( dl. 0 ),( dl. 1)) --> (1, 0 ))) by A16, TARSKI:def 2;

        

        then

         A19: (t . ( dl. 1)) = (((( dl. 0 ),( dl. 1)) --> (1, 0 )) . ( dl. 1)) by FUNCT_4: 13

        .= 0 by FUNCT_4: 63;

        (( Exec (( MultBy (( dl. 0 ),( dl. 1))),t)) . ( dl. 0 )) = ((t . ( dl. 0 )) * (t . ( dl. 1))) by AMI_3: 5

        .= 0 by A19;

        hence thesis by A15, A17, A18;

      end;

      cluster ( InsCode ( Divide (a,b))) -> non jump-only;

      coherence

      proof

        set w = the State of SCM ;

        set t = (w +* ((( dl. 0 ),( dl. 1)) --> (7,3)));

        

         A20: ( InsCode ( Divide (a,b))) = 5

        .= ( InsCode ( Divide (( dl. 0 ),( dl. 1))));

        

         A21: ( dom ((( dl. 0 ),( dl. 1)) --> (7,3))) = {( dl. 0 ), ( dl. 1)} by FUNCT_4: 62;

        then ( dl. 0 ) in ( dom ((( dl. 0 ),( dl. 1)) --> (7,3))) by TARSKI:def 2;

        

        then

         A22: (t . ( dl. 0 )) = (((( dl. 0 ),( dl. 1)) --> (7,3)) . ( dl. 0 )) by FUNCT_4: 13

        .= 7 by AMI_3: 10, FUNCT_4: 63;

        

         A23: 7 = ((2 * 3) + 1);

        

         A24: ( dl. 0 ) in ( Data-Locations SCM ) by AMI_3: 28;

        ( dl. 1) in ( dom ((( dl. 0 ),( dl. 1)) --> (7,3))) by A21, TARSKI:def 2;

        

        then (t . ( dl. 1)) = (((( dl. 0 ),( dl. 1)) --> (7,3)) . ( dl. 1)) by FUNCT_4: 13

        .= 3 by FUNCT_4: 63;

        

        then (( Exec (( Divide (( dl. 0 ),( dl. 1))),t)) . ( dl. 0 )) = (7 div 3 qua Element of NAT ) by A22, Lm2, AMI_3: 6

        .= 2 by A23, NAT_D:def 1;

        hence thesis by A20, A22, A24;

      end;

    end

    registration

      let a, b;

      cluster (a := b) -> non jump-only;

      coherence ;

      cluster ( AddTo (a,b)) -> non jump-only;

      coherence ;

      cluster ( SubFrom (a,b)) -> non jump-only;

      coherence ;

      cluster ( MultBy (a,b)) -> non jump-only;

      coherence ;

      cluster ( Divide (a,b)) -> non jump-only;

      coherence ;

    end

    registration

      cluster SCM -> with_explicit_jumps;

      coherence

      proof

        let I be Instruction of SCM ;

        thus ( JUMP I) c= ( rng ( JumpPart I))

        proof

          let f be object such that

           A1: f in ( JUMP I);

          per cases by AMI_3: 24;

            suppose I = [ 0 , {} , {} ];

            hence thesis by A1, AMI_3: 26;

          end;

            suppose ex a, b st I = (a := b);

            hence thesis by A1;

          end;

            suppose ex a, b st I = ( AddTo (a,b));

            hence thesis by A1;

          end;

            suppose ex a, b st I = ( SubFrom (a,b));

            hence thesis by A1;

          end;

            suppose ex a, b st I = ( MultBy (a,b));

            hence thesis by A1;

          end;

            suppose ex a, b st I = ( Divide (a,b));

            hence thesis by A1;

          end;

            suppose

             A2: ex k st I = ( SCM-goto k);

            consider k1 such that

             A3: I = ( SCM-goto k1) by A2;

            

             A4: ( rng <*k1*>) = {k1} by FINSEQ_1: 39;

            ( JUMP ( SCM-goto k1)) = {k1} by Th16;

            hence thesis by A1, A3, A4;

          end;

            suppose

             A5: ex a, k1 st I = (a =0_goto k1);

            consider a, k1 such that

             A6: I = (a =0_goto k1) by A5;

            

             A7: ( rng <*k1*>) = {k1} by FINSEQ_1: 39;

            ( JUMP (a =0_goto k1)) = {k1} by Th18;

            hence thesis by A1, A6, A7;

          end;

            suppose

             A8: ex a, k1 st I = (a >0_goto k1);

            consider a, k1 such that

             A9: I = (a >0_goto k1) by A8;

            

             A10: ( rng <*k1*>) = {k1} by FINSEQ_1: 39;

            ( JUMP (a >0_goto k1)) = {k1} by Th20;

            hence thesis by A1, A9, A10;

          end;

        end;

        let f be object;

        assume f in ( rng ( JumpPart I));

        then

        consider k be object such that

         A11: k in ( dom ( JumpPart I)) and

         A12: f = (( JumpPart I) . k) by FUNCT_1:def 3;

        per cases by AMI_3: 24;

          suppose I = [ 0 , {} , {} ];

          then ( dom ( JumpPart I)) = ( dom {} );

          hence thesis by A11;

        end;

          suppose ex a, b st I = (a := b);

          then

          consider a, b such that

           A13: I = (a := b);

          k in ( dom {} ) by A11, A13;

          hence thesis;

        end;

          suppose ex a, b st I = ( AddTo (a,b));

          then

          consider a, b such that

           A14: I = ( AddTo (a,b));

          k in ( dom {} ) by A11, A14;

          hence thesis;

        end;

          suppose ex a, b st I = ( SubFrom (a,b));

          then

          consider a, b such that

           A15: I = ( SubFrom (a,b));

          k in ( dom {} ) by A11, A15;

          hence thesis;

        end;

          suppose ex a, b st I = ( MultBy (a,b));

          then

          consider a, b such that

           A16: I = ( MultBy (a,b));

          k in ( dom {} ) by A11, A16;

          hence thesis;

        end;

          suppose ex a, b st I = ( Divide (a,b));

          then

          consider a, b such that

           A17: I = ( Divide (a,b));

          k in ( dom {} ) by A11, A17;

          hence thesis;

        end;

          suppose ex k st I = ( SCM-goto k);

          then

          consider k1 such that

           A18: I = ( SCM-goto k1);

          

           A19: ( JumpPart I) = <*k1*> by A18;

          then k = 1 by A11, FINSEQ_1: 90;

          then

           A20: f = k1 by A19, A12, FINSEQ_1:def 8;

          ( JUMP I) = {k1} by A18, Th16;

          hence thesis by A20, TARSKI:def 1;

        end;

          suppose ex a, k st I = (a =0_goto k);

          then

          consider a, k1 such that

           A21: I = (a =0_goto k1);

          

           A22: ( JumpPart I) = <*k1*> by A21;

          then k = 1 by A11, FINSEQ_1: 90;

          then

           A23: f = k1 by A22, A12, FINSEQ_1: 40;

          ( JUMP I) = {k1} by A21, Th18;

          hence thesis by A23, TARSKI:def 1;

        end;

          suppose ex a, k1 st I = (a >0_goto k1);

          then

          consider a, k1 such that

           A24: I = (a >0_goto k1);

          

           A25: ( JumpPart I) = <*k1*> by A24;

          then k = 1 by A11, FINSEQ_1: 90;

          then

           A26: f = k1 by A25, A12, FINSEQ_1: 40;

          ( JUMP I) = {k1} by A24, Th20;

          hence thesis by A26, TARSKI:def 1;

        end;

      end;

    end

    theorem :: AMI_6:23

    

     Th23: ( IncAddr (( SCM-goto i1),k)) = ( SCM-goto (i1 + k))

    proof

      

       A1: ( JumpPart ( IncAddr (( SCM-goto i1),k))) = (k + ( JumpPart ( SCM-goto i1))) by COMPOS_0:def 9;

      then

       A2: ( dom ( JumpPart ( IncAddr (( SCM-goto i1),k)))) = ( dom ( JumpPart ( SCM-goto i1))) by VALUED_1:def 2;

      

       A3: ( dom ( JumpPart ( SCM-goto (i1 + k)))) = ( dom <*(i1 + k)*>)

      .= ( Seg 1) by FINSEQ_1:def 8

      .= ( dom <*i1*>) by FINSEQ_1:def 8

      .= ( dom ( JumpPart ( SCM-goto i1)));

      

       A4: for x be object st x in ( dom ( JumpPart ( SCM-goto i1))) holds (( JumpPart ( IncAddr (( SCM-goto i1),k))) . x) = (( JumpPart ( SCM-goto (i1 + k))) . x)

      proof

        let x be object;

        assume

         A5: x in ( dom ( JumpPart ( SCM-goto i1)));

        then x in ( dom <*i1*>);

        then

         A6: x = 1 by FINSEQ_1: 90;

        set f = (( JumpPart ( SCM-goto i1)) . x);

        

         A7: (( JumpPart ( IncAddr (( SCM-goto i1),k))) . x) = (k + f) by A5, A2, A1, VALUED_1:def 2;

        f = ( <*i1*> . x)

        .= i1 by A6, FINSEQ_1:def 8;

        

        hence (( JumpPart ( IncAddr (( SCM-goto i1),k))) . x) = ( <*(i1 + k)*> . x) by A6, A7, FINSEQ_1:def 8

        .= (( JumpPart ( SCM-goto (i1 + k))) . x);

      end;

      

       A8: ( AddressPart ( IncAddr (( SCM-goto i1),k))) = ( AddressPart ( SCM-goto i1)) by COMPOS_0:def 9

      .= {}

      .= ( AddressPart ( SCM-goto (i1 + k)));

      

       A9: ( InsCode ( IncAddr (( SCM-goto i1),k))) = ( InsCode ( SCM-goto i1)) by COMPOS_0:def 9

      .= 6

      .= ( InsCode ( SCM-goto (i1 + k)));

      ( JumpPart ( IncAddr (( SCM-goto i1),k))) = ( JumpPart ( SCM-goto (i1 + k))) by A2, A3, A4, FUNCT_1: 2;

      hence thesis by A8, A9, COMPOS_0: 1;

    end;

    theorem :: AMI_6:24

    

     Th24: ( IncAddr ((a =0_goto i1),k)) = (a =0_goto (i1 + k))

    proof

      

       A1: ( JumpPart ( IncAddr ((a =0_goto i1),k))) = (k + ( JumpPart (a =0_goto i1))) by COMPOS_0:def 9;

      then

       A2: ( dom ( JumpPart ( IncAddr ((a =0_goto i1),k)))) = ( dom ( JumpPart (a =0_goto i1))) by VALUED_1:def 2;

      

       A3: ( dom ( JumpPart (a =0_goto (i1 + k)))) = ( dom <*(i1 + k)*>)

      .= ( Seg 1) by FINSEQ_1: 38

      .= ( dom <*i1*>) by FINSEQ_1: 38

      .= ( dom ( JumpPart (a =0_goto i1)));

      

       A4: for x be object st x in ( dom ( JumpPart (a =0_goto i1))) holds (( JumpPart ( IncAddr ((a =0_goto i1),k))) . x) = (( JumpPart (a =0_goto (i1 + k))) . x)

      proof

        let x be object;

        assume

         A5: x in ( dom ( JumpPart (a =0_goto i1)));

        then x in ( dom <*i1*>);

        then

         A6: x = 1 by FINSEQ_1: 90;

        set f = (( JumpPart (a =0_goto i1)) . x);

        

         A7: (( JumpPart ( IncAddr ((a =0_goto i1),k))) . x) = (k + f) by A1, A2, A5, VALUED_1:def 2;

        f = ( <*i1*> . x)

        .= i1 by A6, FINSEQ_1: 40;

        

        hence (( JumpPart ( IncAddr ((a =0_goto i1),k))) . x) = ( <*(i1 + k)*> . x) by A6, A7, FINSEQ_1: 40

        .= (( JumpPart (a =0_goto (i1 + k))) . x);

      end;

      

       A8: ( AddressPart ( IncAddr ((a =0_goto i1),k))) = ( AddressPart (a =0_goto i1)) by COMPOS_0:def 9

      .= <*a*>

      .= ( AddressPart (a =0_goto (i1 + k)));

      

       A9: ( InsCode ( IncAddr ((a =0_goto i1),k))) = ( InsCode (a =0_goto i1)) by COMPOS_0:def 9

      .= 7

      .= ( InsCode (a =0_goto (i1 + k)));

      ( JumpPart ( IncAddr ((a =0_goto i1),k))) = ( JumpPart (a =0_goto (i1 + k))) by A2, A3, A4, FUNCT_1: 2;

      hence thesis by A8, A9, COMPOS_0: 1;

    end;

    theorem :: AMI_6:25

    

     Th25: ( IncAddr ((a >0_goto i1),k)) = (a >0_goto (i1 + k))

    proof

      

       A1: ( JumpPart ( IncAddr ((a >0_goto i1),k))) = (k + ( JumpPart (a >0_goto i1))) by COMPOS_0:def 9;

      then

       A2: ( dom ( JumpPart ( IncAddr ((a >0_goto i1),k)))) = ( dom ( JumpPart (a >0_goto i1))) by VALUED_1:def 2;

      

       A3: ( dom ( JumpPart (a >0_goto (i1 + k)))) = ( dom <*(i1 + k)*>)

      .= ( Seg 1) by FINSEQ_1: 38

      .= ( dom <*i1*>) by FINSEQ_1: 38

      .= ( dom ( JumpPart (a >0_goto i1)));

      

       A4: for x be object st x in ( dom ( JumpPart (a >0_goto i1))) holds (( JumpPart ( IncAddr ((a >0_goto i1),k))) . x) = (( JumpPart (a >0_goto (i1 + k))) . x)

      proof

        let x be object;

        assume

         A5: x in ( dom ( JumpPart (a >0_goto i1)));

        then x in ( dom <*i1*>);

        then

         A6: x = 1 by FINSEQ_1: 90;

        set f = (( JumpPart (a >0_goto i1)) . x);

        

         A7: (( JumpPart ( IncAddr ((a >0_goto i1),k))) . x) = (k + f) by A1, A2, A5, VALUED_1:def 2;

        f = ( <*i1*> . x)

        .= i1 by A6, FINSEQ_1: 40;

        

        hence (( JumpPart ( IncAddr ((a >0_goto i1),k))) . x) = ( <*(i1 + k)*> . x) by A6, A7, FINSEQ_1: 40

        .= (( JumpPart (a >0_goto (i1 + k))) . x);

      end;

      

       A8: ( AddressPart ( IncAddr ((a >0_goto i1),k))) = ( AddressPart (a >0_goto i1)) by COMPOS_0:def 9

      .= <*a*>

      .= ( AddressPart (a >0_goto (i1 + k)));

      

       A9: ( InsCode ( IncAddr ((a >0_goto i1),k))) = ( InsCode (a >0_goto i1)) by COMPOS_0:def 9

      .= 8

      .= ( InsCode (a >0_goto (i1 + k)));

      ( JumpPart ( IncAddr ((a >0_goto i1),k))) = ( JumpPart (a >0_goto (i1 + k))) by A2, A3, A4, FUNCT_1: 2;

      hence thesis by A8, A9, COMPOS_0: 1;

    end;

    registration

      cluster SCM -> IC-relocable;

      coherence

      proof

        thus SCM is IC-relocable

        proof

          let I be Instruction of SCM ;

          per cases by AMI_3: 24;

            suppose I = [ 0 , {} , {} ];

            hence thesis by AMI_3: 26;

          end;

            suppose ex a, b st I = (a := b);

            hence thesis;

          end;

            suppose ex a, b st I = ( AddTo (a,b));

            hence thesis;

          end;

            suppose ex a, b st I = ( SubFrom (a,b));

            hence thesis;

          end;

            suppose ex a, b st I = ( MultBy (a,b));

            hence thesis;

          end;

            suppose ex a, b st I = ( Divide (a,b));

            hence thesis;

          end;

            suppose

             A1: ex k st I = ( SCM-goto k);

            let j,k be Nat, s1 be State of SCM ;

            set s2 = ( IncIC (s1,k));

            consider k1 such that

             A2: I = ( SCM-goto k1) by A1;

            reconsider i1 = k1 as Element of NAT by ORDINAL1:def 12;

            

            thus (( IC ( Exec (( IncAddr (I,j)),s1))) + k) = (( IC ( Exec (( SCM-goto (j + k1)),s1))) + k) by A2, Th23

            .= ((j + k1) + k) by AMI_3: 7

            .= ( IC ( Exec (( SCM-goto ((j + i1) + k)),s2))) by AMI_3: 7

            .= ( IC ( Exec (( SCM-goto ((j + k) + i1)),s2)))

            .= ( IC ( Exec (( IncAddr (I,(j + k))),s2))) by A2, Th23;

          end;

            suppose ex a, k st I = (a =0_goto k);

            then

            consider a, k1 such that

             A3: I = (a =0_goto k1);

            reconsider i1 = k1 as Element of NAT by ORDINAL1:def 12;

            let j,k be Nat, s1 be State of SCM ;

            set s2 = ( IncIC (s1,k));

            a <> ( IC SCM ) & ( dom (( IC SCM ) .--> (( IC s1) + k))) = {( IC SCM )} by AMI_5: 2;

            then not a in ( dom (( IC SCM ) .--> (( IC s1) + k))) by TARSKI:def 1;

            then

             A4: (s1 . a) = (s2 . a) by FUNCT_4: 11;

            now

              per cases ;

                suppose

                 A5: (s1 . a) = 0 ;

                

                thus (( IC ( Exec (( IncAddr (I,j)),s1))) + k) = (( IC ( Exec ((a =0_goto (j + k1)),s1))) + k) by A3, Th24

                .= ((j + k1) + k) by A5, AMI_3: 8

                .= ( IC ( Exec ((a =0_goto ((j + i1) + k)),s2))) by A4, A5, AMI_3: 8

                .= ( IC ( Exec ((a =0_goto ((j + k) + i1)),s2)))

                .= ( IC ( Exec (( IncAddr (I,(j + k))),s2))) by A3, Th24;

              end;

                suppose

                 A6: (s1 . a) <> 0 ;

                

                 A7: ( IncAddr (I,j)) = (a =0_goto (i1 + j)) by A3, Th24;

                

                 A8: ( IncAddr (I,(j + k))) = (a =0_goto (i1 + (j + k))) by A3, Th24;

                ( IC SCM ) in ( dom (( IC SCM ) .--> (( IC s1) + k))) by TARSKI:def 1;

                

                then

                 A9: ( IC s2) = ((( IC SCM ) .--> (( IC s1) + k)) . ( IC SCM )) by FUNCT_4: 13

                .= (( IC s1) + k) by FUNCOP_1: 72;

                

                thus (( IC ( Exec (( IncAddr (I,j)),s1))) + k) = ((( IC s1) + 1) + k) by A7, A6, AMI_3: 8

                .= ((( IC s1) + 1) + k)

                .= (( IC s2) + 1) by A9

                .= ( IC ( Exec (( IncAddr (I,(j + k))),s2))) by A8, A6, A4, AMI_3: 8;

              end;

            end;

            hence thesis;

          end;

            suppose ex a, k st I = (a >0_goto k);

            then

            consider a, k1 such that

             A10: I = (a >0_goto k1);

            reconsider i1 = k1 as Element of NAT by ORDINAL1:def 12;

            let j,k be Nat, s1 be State of SCM ;

            set s2 = ( IncIC (s1,k));

            a <> ( IC SCM ) & ( dom (( IC SCM ) .--> (( IC s1) + k))) = {( IC SCM )} by AMI_5: 2;

            then not a in ( dom (( IC SCM ) .--> (( IC s1) + k))) by TARSKI:def 1;

            then

             A11: (s1 . a) = (s2 . a) by FUNCT_4: 11;

            per cases ;

              suppose

               A12: (s1 . a) > 0 ;

              

              thus (( IC ( Exec (( IncAddr (I,j)),s1))) + k) = (( IC ( Exec ((a >0_goto (j + k1)),s1))) + k) by A10, Th25

              .= ((j + k1) + k) by A12, AMI_3: 9

              .= ( IC ( Exec ((a >0_goto ((j + i1) + k)),s2))) by A11, A12, AMI_3: 9

              .= ( IC ( Exec ((a >0_goto ((j + k) + i1)),s2)))

              .= ( IC ( Exec (( IncAddr (I,(j + k))),s2))) by A10, Th25;

            end;

              suppose

               A13: (s1 . a) <= 0 ;

              

               A14: ( IncAddr (I,j)) = (a >0_goto (i1 + j)) by A10, Th25;

              

               A15: ( IncAddr (I,(j + k))) = (a >0_goto (i1 + (j + k))) by A10, Th25;

              ( IC SCM ) in ( dom (( IC SCM ) .--> (( IC s1) + k))) by TARSKI:def 1;

              

              then

               A16: ( IC s2) = ((( IC SCM ) .--> (( IC s1) + k)) . ( IC SCM )) by FUNCT_4: 13

              .= (( IC s1) + k) by FUNCOP_1: 72;

              

              thus (( IC ( Exec (( IncAddr (I,j)),s1))) + k) = ((( IC s1) + 1) + k) by A14, A13, AMI_3: 9

              .= ((( IC s1) + 1) + k)

              .= (( IC s2) + 1) by A16

              .= ( IC ( Exec (( IncAddr (I,(j + k))),s2))) by A15, A13, A11, AMI_3: 9;

            end;

          end;

        end;

      end;

    end