ami_3.miz



    begin

    reserve i,j,k for Nat;

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

a,a1,a2 for Nat,

b,b1,b2,c,c1 for Element of SCM-Data-Loc ;

    reserve T for InsType of SCM-Instr ,

I for Element of SCM-Instr ;

    registration

      let n be non zero Nat;

      cluster ( Segm n) -> with_zero;

      coherence ;

    end

    definition

      :: AMI_3:def1

      func SCM -> strict AMI-Struct over ( Segm 2) equals AMI-Struct (# SCM-Memory , ( In ( NAT , SCM-Memory )), SCM-Instr , SCM-OK , SCM-VAL , SCM-Exec #);

      coherence ;

    end

    registration

      cluster SCM -> non empty;

      coherence ;

    end

    

     Lm1: ( the_Values_of SCM ) = (the ValuesF of SCM * the Object-Kind of SCM )

    .= ( SCM-VAL * SCM-OK );

    registration

      cluster SCM -> with_non-empty_values;

      coherence ;

    end

    registration

      cluster SCM -> IC-Ins-separated;

      coherence by AMI_2: 22, SUBSET_1:def 8, AMI_2: 6;

    end

    registration

      cluster Int-like for Object of SCM ;

      existence

      proof

        reconsider x = the Element of SCM-Data-Loc as Object of SCM ;

        take x;

        thus thesis;

      end;

    end

    definition

      mode Data-Location is Int-like Object of SCM ;

    end

    registration

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

      cluster (s . d) -> integer;

      coherence

      proof

        reconsider D = d as Element of SCM-Data-Loc by AMI_2:def 16;

        reconsider S = s as SCM-State by CARD_3: 107;

        (S . D) = (s . d);

        hence thesis;

      end;

    end

    reserve a,b,c for Data-Location,

loc for Nat,

I for Instruction of SCM ;

    definition

      ::$Canceled

      let a, b;

      :: AMI_3:def3

      func a := b -> Instruction of SCM equals [1, {} , <*a, b*>];

      correctness

      proof

        reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;

        1 in {1, 2, 3, 4, 5} by ENUMSET1:def 3;

        then [1, {} , <*mk, ml*>] in SCM-Instr by SCM_INST: 4;

        hence thesis;

      end;

      :: AMI_3:def4

      func AddTo (a,b) -> Instruction of SCM equals [2, {} , <*a, b*>];

      correctness

      proof

        reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;

        2 in {1, 2, 3, 4, 5} by ENUMSET1:def 3;

        then [2, {} , <*mk, ml*>] in SCM-Instr by SCM_INST: 4;

        hence thesis;

      end;

      :: AMI_3:def5

      func SubFrom (a,b) -> Instruction of SCM equals [3, {} , <*a, b*>];

      correctness

      proof

        reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;

        3 in {1, 2, 3, 4, 5} by ENUMSET1:def 3;

        then [3, {} , <*mk, ml*>] in SCM-Instr by SCM_INST: 4;

        hence thesis;

      end;

      :: AMI_3:def6

      func MultBy (a,b) -> Instruction of SCM equals [4, {} , <*a, b*>];

      correctness

      proof

        reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;

        4 in {1, 2, 3, 4, 5} by ENUMSET1:def 3;

        then [4, {} , <*mk, ml*>] in SCM-Instr by SCM_INST: 4;

        hence thesis;

      end;

      :: AMI_3:def7

      func Divide (a,b) -> Instruction of SCM equals [5, {} , <*a, b*>];

      correctness

      proof

        reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;

        5 in {1, 2, 3, 4, 5} by ENUMSET1:def 3;

        then [5, {} , <*mk, ml*>] in SCM-Instr by SCM_INST: 4;

        hence thesis;

      end;

    end

    definition

      let loc;

      :: AMI_3:def8

      func SCM-goto loc -> Instruction of SCM equals [6, <*loc*>, {} ];

      correctness by SCM_INST: 2;

      let a;

      :: AMI_3:def9

      func a =0_goto loc -> Instruction of SCM equals [7, <*loc*>, <*a*>];

      correctness

      proof

        reconsider a as Element of SCM-Data-Loc by AMI_2:def 16;

        reconsider loc as Nat;

        7 in {7, 8} by TARSKI:def 2;

        then [7, <*loc*>, <*a*>] in SCM-Instr by SCM_INST: 3;

        hence thesis;

      end;

      :: AMI_3:def10

      func a >0_goto loc -> Instruction of SCM equals [8, <*loc*>, <*a*>];

      correctness

      proof

        reconsider a as Element of SCM-Data-Loc by AMI_2:def 16;

        reconsider loc as Nat;

        8 in {7, 8} by TARSKI:def 2;

        then [8, <*loc*>, <*a*>] in SCM-Instr by SCM_INST: 3;

        hence thesis;

      end;

    end

    reserve s for State of SCM ;

    theorem :: AMI_3:1

    

     Th1: ( IC SCM ) = NAT by AMI_2: 22, SUBSET_1:def 8;

    begin

    theorem :: AMI_3:2

    

     Th2: (( Exec ((a := b),s)) . ( IC SCM )) = (( IC s) + 1) & (( Exec ((a := b),s)) . a) = (s . b) & for c st c <> a holds (( Exec ((a := b),s)) . c) = (s . c)

    proof

      reconsider S = s as SCM-State by CARD_3: 107;

      reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;

      reconsider I = (a := b) as Element of SCM-Instr ;

      set S1 = ( SCM-Chg (S,(I address_1 ),(S . (I address_2 ))));

      reconsider i = 1 as Element of ( Segm 9) by NAT_1: 44;

      

       A1: I = [i, {} , <*mk, ml*>];

      then

       A2: (I address_1 ) = mk by SCM_INST: 5;

      

       A3: (I address_2 ) = ml by A1, SCM_INST: 5;

      

       A4: ( Exec ((a := b),s)) = ( SCM-Exec-Res (I,S)) by AMI_2:def 15

      .= ( SCM-Chg (S1,(( IC S) + 1))) by A1, AMI_2:def 14;

      hence (( Exec ((a := b),s)) . ( IC SCM )) = (( IC s) + 1) by Th1, AMI_2: 11;

      

      thus (( Exec ((a := b),s)) . a) = (S1 . mk) by A4, AMI_2: 12

      .= (s . b) by A2, A3, AMI_2: 15;

      let c;

      reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;

      assume

       A5: c <> a;

      

      thus (( Exec ((a := b),s)) . c) = (S1 . mn) by A4, AMI_2: 12

      .= (s . c) by A2, A5, AMI_2: 16;

    end;

    theorem :: AMI_3:3

    

     Th3: (( Exec (( AddTo (a,b)),s)) . ( IC SCM )) = (( IC s) + 1) & (( Exec (( AddTo (a,b)),s)) . a) = ((s . a) + (s . b)) & for c st c <> a holds (( Exec (( AddTo (a,b)),s)) . c) = (s . c)

    proof

      reconsider S = s as SCM-State by CARD_3: 107;

      reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;

      reconsider I = ( AddTo (a,b)) as Element of SCM-Instr ;

      set S1 = ( SCM-Chg (S,(I address_1 ),((S . (I address_1 )) + (S . (I address_2 )))));

      reconsider i = 2 as Element of ( Segm 9) by NAT_1: 44;

      

       A1: I = [i, {} , <*mk, ml*>];

      then

       A2: (I address_1 ) = mk by SCM_INST: 5;

      

       A3: (I address_2 ) = ml by A1, SCM_INST: 5;

      

       A4: ( Exec (( AddTo (a,b)),s)) = ( SCM-Exec-Res (I,S)) by AMI_2:def 15

      .= ( SCM-Chg (S1,(( IC S) + 1))) by A1, AMI_2:def 14;

      hence (( Exec (( AddTo (a,b)),s)) . ( IC SCM )) = (( IC s) + 1) by Th1, AMI_2: 11;

      

      thus (( Exec (( AddTo (a,b)),s)) . a) = (S1 . mk) by A4, AMI_2: 12

      .= ((s . a) + (s . b)) by A2, A3, AMI_2: 15;

      let c;

      reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;

      assume

       A5: c <> a;

      

      thus (( Exec (( AddTo (a,b)),s)) . c) = (S1 . mn) by A4, AMI_2: 12

      .= (s . c) by A2, A5, AMI_2: 16;

    end;

    theorem :: AMI_3:4

    

     Th4: (( Exec (( SubFrom (a,b)),s)) . ( IC SCM )) = (( IC s) + 1) & (( Exec (( SubFrom (a,b)),s)) . a) = ((s . a) - (s . b)) & for c st c <> a holds (( Exec (( SubFrom (a,b)),s)) . c) = (s . c)

    proof

      reconsider S = s as SCM-State by CARD_3: 107;

      reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;

      reconsider I = ( SubFrom (a,b)) as Element of SCM-Instr ;

      set S1 = ( SCM-Chg (S,(I address_1 ),((S . (I address_1 )) - (S . (I address_2 )))));

      reconsider i = 3 as Element of ( Segm 9) by NAT_1: 44;

      

       A1: I = [i, {} , <*mk, ml*>];

      then

       A2: (I address_1 ) = mk by SCM_INST: 5;

      

       A3: (I address_2 ) = ml by A1, SCM_INST: 5;

      

       A4: ( Exec (( SubFrom (a,b)),s)) = ( SCM-Exec-Res (I,S)) by AMI_2:def 15

      .= ( SCM-Chg (S1,(( IC S) + 1))) by A1, AMI_2:def 14;

      hence (( Exec (( SubFrom (a,b)),s)) . ( IC SCM )) = (( IC s) + 1) by Th1, AMI_2: 11;

      

      thus (( Exec (( SubFrom (a,b)),s)) . a) = (S1 . mk) by A4, AMI_2: 12

      .= ((s . a) - (s . b)) by A2, A3, AMI_2: 15;

      let c;

      reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;

      assume

       A5: c <> a;

      

      thus (( Exec (( SubFrom (a,b)),s)) . c) = (S1 . mn) by A4, AMI_2: 12

      .= (s . c) by A2, A5, AMI_2: 16;

    end;

    theorem :: AMI_3:5

    

     Th5: (( Exec (( MultBy (a,b)),s)) . ( IC SCM )) = (( IC s) + 1) & (( Exec (( MultBy (a,b)),s)) . a) = ((s . a) * (s . b)) & for c st c <> a holds (( Exec (( MultBy (a,b)),s)) . c) = (s . c)

    proof

      reconsider S = s as SCM-State by CARD_3: 107;

      reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;

      reconsider I = ( MultBy (a,b)) as Element of SCM-Instr ;

      set S1 = ( SCM-Chg (S,(I address_1 ),((S . (I address_1 )) * (S . (I address_2 )))));

      reconsider i = 4 as Element of ( Segm 9) by NAT_1: 44;

      

       A1: I = [i, {} , <*mk, ml*>];

      then

       A2: (I address_1 ) = mk by SCM_INST: 5;

      

       A3: (I address_2 ) = ml by A1, SCM_INST: 5;

      

       A4: ( Exec (( MultBy (a,b)),s)) = ( SCM-Exec-Res (I,S)) by AMI_2:def 15

      .= ( SCM-Chg (S1,(( IC S) + 1))) by A1, AMI_2:def 14;

      hence (( Exec (( MultBy (a,b)),s)) . ( IC SCM )) = (( IC s) + 1) by Th1, AMI_2: 11;

      

      thus (( Exec (( MultBy (a,b)),s)) . a) = (S1 . mk) by A4, AMI_2: 12

      .= ((s . a) * (s . b)) by A2, A3, AMI_2: 15;

      let c;

      reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;

      assume

       A5: c <> a;

      

      thus (( Exec (( MultBy (a,b)),s)) . c) = (S1 . mn) by A4, AMI_2: 12

      .= (s . c) by A2, A5, AMI_2: 16;

    end;

    theorem :: AMI_3:6

    

     Th6: (( Exec (( Divide (a,b)),s)) . ( IC SCM )) = (( IC s) + 1) & (a <> b implies (( Exec (( Divide (a,b)),s)) . a) = ((s . a) div (s . b))) & (( Exec (( Divide (a,b)),s)) . b) = ((s . a) mod (s . b)) & for c st c <> a & c <> b holds (( Exec (( Divide (a,b)),s)) . c) = (s . c)

    proof

      reconsider S = s as SCM-State by CARD_3: 107;

      reconsider mk = a, ml = b as Element of SCM-Data-Loc by AMI_2:def 16;

      reconsider I = ( Divide (a,b)) as Element of SCM-Instr ;

      set S1 = ( SCM-Chg (S,(I address_1 ),((S . (I address_1 )) div (S . (I address_2 )))));

      set S19 = ( SCM-Chg (S1,(I address_2 ),((S . (I address_1 )) mod (S . (I address_2 )))));

      reconsider i = 5 as Element of ( Segm 9) by NAT_1: 44;

      

       A1: I = [i, {} , <*mk, ml*>];

      then

       A2: (I address_1 ) = mk by SCM_INST: 5;

      

       A3: ( Exec (( Divide (a,b)),s)) = ( SCM-Exec-Res (I,S)) by AMI_2:def 15

      .= ( SCM-Chg (S19,(( IC S) + 1))) by A1, AMI_2:def 14;

      hence (( Exec (( Divide (a,b)),s)) . ( IC SCM )) = (( IC s) + 1) by Th1, AMI_2: 11;

      

       A4: (I address_2 ) = ml by A1, SCM_INST: 5;

      hereby

        assume

         A5: a <> b;

        

        thus (( Exec (( Divide (a,b)),s)) . a) = (S19 . mk) by A3, AMI_2: 12

        .= (S1 . mk) by A4, A5, AMI_2: 16

        .= ((s . a) div (s . b)) by A2, A4, AMI_2: 15;

      end;

      

      thus (( Exec (( Divide (a,b)),s)) . b) = (S19 . ml) by A3, AMI_2: 12

      .= ((s . a) mod (s . b)) by A2, A4, AMI_2: 15;

      let c;

      reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;

      assume that

       A6: c <> a and

       A7: c <> b;

      

      thus (( Exec (( Divide (a,b)),s)) . c) = (S19 . mn) by A3, AMI_2: 12

      .= (S1 . mn) by A4, A7, AMI_2: 16

      .= (s . c) by A2, A6, AMI_2: 16;

    end;

    theorem :: AMI_3:7

    (( Exec (( SCM-goto loc),s)) . ( IC SCM )) = loc & (( Exec (( SCM-goto loc),s)) . c) = (s . c)

    proof

      reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;

      reconsider mj = loc as Element of NAT by ORDINAL1:def 12;

      reconsider I = ( SCM-goto loc) as Element of SCM-Instr ;

      reconsider S = s as SCM-State by CARD_3: 107;

      reconsider i = 6 as Element of ( Segm 9) by NAT_1: 44;

      

       A1: I = [i, <*mj*>, {} ];

      

       A2: ( Exec (( SCM-goto loc),s)) = ( SCM-Exec-Res (I,S)) by AMI_2:def 15

      .= ( SCM-Chg (S,(I jump_address ))) by AMI_2:def 14;

      (I jump_address ) = mj by A1, SCM_INST: 6;

      hence (( Exec (( SCM-goto loc),s)) . ( IC SCM )) = loc by A2, Th1, AMI_2: 11;

      

      thus (( Exec (( SCM-goto loc),s)) . c) = (S . mn) by A2, AMI_2: 12

      .= (s . c);

    end;

    theorem :: AMI_3:8

    

     Th8: ((s . a) = 0 implies (( Exec ((a =0_goto loc),s)) . ( IC SCM )) = loc) & ((s . a) <> 0 implies (( Exec ((a =0_goto loc),s)) . ( IC SCM )) = (( IC s) + 1)) & (( Exec ((a =0_goto loc),s)) . c) = (s . c)

    proof

      reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;

      reconsider I = (a =0_goto loc) as Element of SCM-Instr ;

      reconsider S = s as SCM-State by CARD_3: 107;

      reconsider i = 7 as Element of ( Segm 9) by NAT_1: 44;

      reconsider a9 = a as Element of SCM-Data-Loc by AMI_2:def 16;

      reconsider mj = loc as Element of NAT by ORDINAL1:def 12;

      

       A1: I = [i, <*mj*>, <*a9*>];

      

       A2: ( Exec ((a =0_goto loc),s)) = ( SCM-Exec-Res (I,S)) by AMI_2:def 15

      .= ( SCM-Chg (S,( IFEQ ((S . (I cond_address )), 0 ,(I cjump_address ),(( IC S) + 1))))) by A1, AMI_2:def 14;

      thus (s . a) = 0 implies (( Exec ((a =0_goto loc),s)) . ( IC SCM )) = loc

      proof

        assume (s . a) = 0 ;

        then

         A3: (S . (I cond_address )) = 0 by A1, SCM_INST: 7;

        

        thus (( Exec ((a =0_goto loc),s)) . ( IC SCM )) = ( IFEQ ((S . (I cond_address )), 0 ,(I cjump_address ),(( IC S) + 1))) by A2, Th1, AMI_2: 11

        .= (I cjump_address ) by A3, FUNCOP_1:def 8

        .= loc by A1, SCM_INST: 7;

      end;

      thus (s . a) <> 0 implies (( Exec ((a =0_goto loc),s)) . ( IC SCM )) = (( IC s) + 1)

      proof

        assume (s . a) <> 0 ;

        then

         A4: (S . (I cond_address )) <> 0 by A1, SCM_INST: 7;

        

        thus (( Exec ((a =0_goto loc),s)) . ( IC SCM )) = ( IFEQ ((S . (I cond_address )), 0 ,(I cjump_address ),(( IC S) + 1))) by A2, Th1, AMI_2: 11

        .= (( IC s) + 1) by A4, Th1, FUNCOP_1:def 8;

      end;

      

      thus (( Exec ((a =0_goto loc),s)) . c) = (S . mn) by A2, AMI_2: 12

      .= (s . c);

    end;

    theorem :: AMI_3:9

    

     Th9: ((s . a) > 0 implies (( Exec ((a >0_goto loc),s)) . ( IC SCM )) = loc) & ((s . a) <= 0 implies (( Exec ((a >0_goto loc),s)) . ( IC SCM )) = (( IC s) + 1)) & (( Exec ((a >0_goto loc),s)) . c) = (s . c)

    proof

      reconsider mn = c as Element of SCM-Data-Loc by AMI_2:def 16;

      reconsider I = (a >0_goto loc) as Element of SCM-Instr ;

      reconsider S = s as SCM-State by CARD_3: 107;

      reconsider i = 8 as Element of ( Segm 9) by NAT_1: 44;

      reconsider a9 = a as Element of SCM-Data-Loc by AMI_2:def 16;

      reconsider mj = loc as Nat;

      

       A1: I = [i, <*mj*>, <*a9*>];

      

       A2: ( Exec ((a >0_goto loc),s)) = ( SCM-Exec-Res (I,S)) by AMI_2:def 15

      .= ( SCM-Chg (S,( IFGT ((S . (I cond_address )), 0 ,(I cjump_address ),(( IC S) + 1))))) by A1, AMI_2:def 14;

      thus (s . a) > 0 implies (( Exec ((a >0_goto loc),s)) . ( IC SCM )) = loc

      proof

        assume (s . a) > 0 ;

        then

         A3: (S . (I cond_address )) > 0 by A1, SCM_INST: 7;

        

        thus (( Exec ((a >0_goto loc),s)) . ( IC SCM )) = ( IFGT ((S . (I cond_address )), 0 ,(I cjump_address ),(( IC S) + 1))) by A2, Th1, AMI_2: 11

        .= (I cjump_address ) by A3, XXREAL_0:def 11

        .= loc by A1, SCM_INST: 7;

      end;

      thus (s . a) <= 0 implies (( Exec ((a >0_goto loc),s)) . ( IC SCM )) = (( IC s) + 1)

      proof

        assume (s . a) <= 0 ;

        then

         A4: (S . (I cond_address )) <= 0 by A1, SCM_INST: 7;

        

        thus (( Exec ((a >0_goto loc),s)) . ( IC SCM )) = ( IFGT ((S . (I cond_address )), 0 ,(I cjump_address ),(( IC S) + 1))) by A2, Th1, AMI_2: 11

        .= (( IC s) + 1) by A4, Th1, XXREAL_0:def 11;

      end;

      

      thus (( Exec ((a >0_goto loc),s)) . c) = (S . mn) by A2, AMI_2: 12

      .= (s . c);

    end;

    reserve Y,K,T for Element of ( Segm 9),

a1,a2,a3 for Nat,

b1,b2,c1,c2,c3 for Element of SCM-Data-Loc ;

    

     Lm2: for I be Instruction of SCM st ex s st (( Exec (I,s)) . ( IC SCM )) = (( IC s) + 1) holds I is non halting

    proof

      let I be Instruction of SCM ;

      given s such that

       A1: (( Exec (I,s)) . ( IC SCM )) = (( IC s) + 1);

      assume I is halting;

      then (( Exec (I,s)) . ( IC SCM )) = (s . NAT ) by Th1;

      hence contradiction by A1, Th1;

      ( IC s) = (s . NAT ) by AMI_2: 22, SUBSET_1:def 8;

      then

      reconsider w = (s . NAT ) as Nat;

    end;

    

     Lm3: for I be Instruction of SCM st I = [ 0 , {} , {} ] holds I is halting

    proof

      let I be Instruction of SCM ;

      assume

       A1: I = [ 0 , {} , {} ];

      then

       A2: (I `3_3 ) = {} ;

      then

       A3: ( not (ex mk,ml be Element of SCM-Data-Loc st I = [1, {} , <*mk, ml*>])) & not (ex mk,ml be Element of SCM-Data-Loc st I = [2, {} , <*mk, ml*>]);

      

       A4: ( not (ex mk be Nat, ml be Element of SCM-Data-Loc st I = [7, <*mk*>, <*ml*>])) & not (ex mk be Nat, ml be Element of SCM-Data-Loc st I = [8, <*mk*>, <*ml*>]) by A2;

      (I `2_3 ) = {} by A1;

      then

       A5: ( not (ex mk,ml be Element of SCM-Data-Loc st I = [5, {} , <*mk, ml*>])) & not (ex mk be Nat st I = [6, <*mk*>, {} ]) by A2;

      reconsider L = I as Element of SCM-Instr ;

      let s be State of SCM ;

      reconsider t = s as SCM-State by CARD_3: 107;

      

       A6: ( not (ex mk,ml be Element of SCM-Data-Loc st I = [3, {} , <*mk, ml*>])) & not (ex mk,ml be Element of SCM-Data-Loc st I = [4, {} , <*mk, ml*>]) by A2;

      

      thus ( Exec (I,s)) = ( SCM-Exec-Res (L,t)) by AMI_2:def 15

      .= s by A3, A6, A5, A4, AMI_2:def 14;

    end;

    

     Lm4: (a := b) is non halting

    proof

      set s = the State of SCM ;

      (( Exec ((a := b),s)) . ( IC SCM )) = (( IC s) + 1) by Th2;

      hence thesis by Lm2;

    end;

    

     Lm5: ( AddTo (a,b)) is non halting

    proof

      set s = the State of SCM ;

      (( Exec (( AddTo (a,b)),s)) . ( IC SCM )) = (( IC s) + 1) by Th3;

      hence thesis by Lm2;

    end;

    

     Lm6: ( SubFrom (a,b)) is non halting

    proof

      set s = the State of SCM ;

      (( Exec (( SubFrom (a,b)),s)) . ( IC SCM )) = (( IC s) + 1) by Th4;

      hence thesis by Lm2;

    end;

    

     Lm7: ( MultBy (a,b)) is non halting

    proof

      set s = the State of SCM ;

      (( Exec (( MultBy (a,b)),s)) . ( IC SCM )) = (( IC s) + 1) by Th5;

      hence thesis by Lm2;

    end;

    

     Lm8: ( Divide (a,b)) is non halting

    proof

      set s = the State of SCM ;

      (( Exec (( Divide (a,b)),s)) . ( IC SCM )) = (( IC s) + 1) by Th6;

      hence thesis by Lm2;

    end;

    

     Lm9: ( SCM-goto loc) is non halting

    proof

      set f = ( the_Values_of SCM );

      set s = the SCM-State;

      assume

       A1: ( SCM-goto loc) is halting;

      reconsider a3 = loc as Nat;

      reconsider V = ( SCM-goto loc) as Element of SCM-Instr ;

      set t = (s +* ( NAT .--> (a3 + 1)));

      

       A2: ( dom s) = the carrier of SCM by AMI_2: 28;

       NAT in ( dom ( NAT .--> (a3 + 1))) by TARSKI:def 1;

      

      then

       A4: (t . NAT ) = (( NAT .--> (a3 + 1)) . NAT ) by FUNCT_4: 13

      .= (a3 + 1) by FUNCOP_1: 72;

      

       A5: for x be object st x in ( dom f) holds (t . x) in (f . x)

      proof

        let x be object such that

         A6: x in ( dom f);

        per cases ;

          suppose

           A7: x = NAT ;

          then (f . x) = NAT by AMI_2: 6;

          hence thesis by A4, A7, ORDINAL1:def 12;

        end;

          suppose x <> NAT ;

          then not x in ( dom ( NAT .--> (a3 + 1))) by TARSKI:def 1;

          then (t . x) = (s . x) by FUNCT_4: 11;

          hence thesis by A6, CARD_3: 9;

        end;

      end;

      

       A8: { NAT } c= SCM-Memory by AMI_2: 22, ZFMISC_1: 31;

      

       A9: ( dom t) = (( dom s) \/ ( dom ( NAT .--> (a3 + 1)))) by FUNCT_4:def 1

      .= ( SCM-Memory \/ ( dom ( NAT .--> (a3 + 1)))) by A2

      .= ( SCM-Memory \/ { NAT })

      .= SCM-Memory by A8, XBOOLE_1: 12;

      ( dom f) = SCM-Memory by AMI_2: 27;

      then

      reconsider t as State of SCM by A9, A5, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;

      reconsider w = t as SCM-State by CARD_3: 107;

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

      

      then

       A10: ((w +* ( NAT .--> loc)) . NAT ) = (( NAT .--> loc) . NAT ) by FUNCT_4: 13

      .= loc by FUNCOP_1: 72;

      6 is Element of ( Segm 9) by NAT_1: 44;

      

      then (w +* ( NAT .--> loc)) = ( SCM-Chg (w,(V jump_address ))) by SCM_INST: 6

      .= ( SCM-Exec-Res (V,w)) by AMI_2:def 14

      .= ( Exec (( SCM-goto loc),t)) by AMI_2:def 15

      .= t by A1;

      hence contradiction by A4, A10;

    end;

    

     Lm10: (a =0_goto loc) is non halting

    proof

      set f = ( the_Values_of SCM );

      set s = the SCM-State;

      reconsider V = (a =0_goto loc) as Element of SCM-Instr ;

      reconsider a3 = loc as Nat;

      set t = (s +* ( NAT .--> (a3 + 1)));

      

       A1: { NAT } c= SCM-Memory by AMI_2: 22, ZFMISC_1: 31;

      

       A2: ( dom s) = the carrier of SCM by AMI_2: 28;

      

       A3: ( dom t) = (( dom s) \/ ( dom ( NAT .--> (a3 + 1)))) by FUNCT_4:def 1

      .= ( SCM-Memory \/ ( dom ( NAT .--> (a3 + 1)))) by A2

      .= ( SCM-Memory \/ { NAT })

      .= SCM-Memory by A1, XBOOLE_1: 12;

      

       A4: 7 is Element of ( Segm 9) by NAT_1: 44;

       NAT in ( dom ( NAT .--> (a3 + 1))) by TARSKI:def 1;

      

      then

       A6: (t . NAT ) = (( NAT .--> (a3 + 1)) . NAT ) by FUNCT_4: 13

      .= (a3 + 1) by FUNCOP_1: 72;

      

       A7: for x be object st x in ( dom f) holds (t . x) in (f . x)

      proof

        let x be object such that

         A8: x in ( dom f);

        per cases ;

          suppose

           A9: x = NAT ;

          then (f . x) = NAT by AMI_2: 6;

          hence thesis by A6, A9, ORDINAL1:def 12;

        end;

          suppose x <> NAT ;

          then not x in ( dom ( NAT .--> (a3 + 1))) by TARSKI:def 1;

          then (t . x) = (s . x) by FUNCT_4: 11;

          hence thesis by A8, CARD_3: 9;

        end;

      end;

      ( dom f) = SCM-Memory by AMI_2: 27;

      then

      reconsider t as State of SCM by A3, A7, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;

      reconsider w = t as SCM-State by CARD_3: 107;

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

      

      then

       A10: ((w +* ( NAT .--> loc)) . NAT ) = (( NAT .--> loc) . NAT ) by FUNCT_4: 13

      .= loc by FUNCOP_1: 72;

      assume

       A11: (a =0_goto loc) is halting;

      

       A12: a is Element of SCM-Data-Loc by AMI_2:def 16;

      per cases ;

        suppose

         A13: (w . (V cond_address )) <> 0 ;

        ( IC w) = (w . NAT );

        then

        reconsider e = (w . NAT ) as Nat;

        ( IC t) = ( IC w) & (t . a) <> 0 by A4, A12, A13, AMI_2: 22, SCM_INST: 7, SUBSET_1:def 8;

        then

         A14: (( Exec ((a =0_goto loc),t)) . ( IC SCM )) = (e + 1) by Th8;

        (( Exec ((a =0_goto loc),t)) . ( IC SCM )) = (w . NAT ) by A11, Th1;

        hence contradiction by A14;

      end;

        suppose (w . (V cond_address )) = 0 ;

        then ( IFEQ ((w . (V cond_address )), 0 ,(V cjump_address ),(( IC w) + 1))) = (V cjump_address ) by FUNCOP_1:def 8;

        

        then (w +* ( NAT .--> loc)) = ( SCM-Chg (w,( IFEQ ((w . (V cond_address )), 0 ,(V cjump_address ),(( IC w) + 1))))) by A4, A12, SCM_INST: 7

        .= ( SCM-Exec-Res (V,w)) by A12, AMI_2:def 14

        .= ( Exec ((a =0_goto loc),t)) by AMI_2:def 15

        .= t by A11;

        hence contradiction by A6, A10;

      end;

    end;

    

     Lm11: (a >0_goto loc) is non halting

    proof

      set f = ( the_Values_of SCM );

      set s = the SCM-State;

      reconsider V = (a >0_goto loc) as Element of SCM-Instr ;

      reconsider a3 = loc as Nat;

      set t = (s +* ( NAT .--> (a3 + 1)));

      

       A1: { NAT } c= SCM-Memory by AMI_2: 22, ZFMISC_1: 31;

      

       A2: ( dom s) = the carrier of SCM by AMI_2: 28;

      

       A3: ( dom t) = (( dom s) \/ ( dom ( NAT .--> (a3 + 1)))) by FUNCT_4:def 1

      .= ( SCM-Memory \/ ( dom ( NAT .--> (a3 + 1)))) by A2

      .= ( SCM-Memory \/ { NAT })

      .= SCM-Memory by A1, XBOOLE_1: 12;

      

       A4: 8 is Element of ( Segm 9) by NAT_1: 44;

       NAT in ( dom ( NAT .--> (a3 + 1))) by TARSKI:def 1;

      

      then

       A6: (t . NAT ) = (( NAT .--> (a3 + 1)) . NAT ) by FUNCT_4: 13

      .= (a3 + 1) by FUNCOP_1: 72;

      

       A7: for x be object st x in ( dom f) holds (t . x) in (f . x)

      proof

        let x be object such that

         A8: x in ( dom f);

        per cases ;

          suppose

           A9: x = NAT ;

          then (f . x) = NAT by AMI_2: 6;

          hence thesis by A6, A9, ORDINAL1:def 12;

        end;

          suppose x <> NAT ;

          then not x in ( dom ( NAT .--> (a3 + 1))) by TARSKI:def 1;

          then (t . x) = (s . x) by FUNCT_4: 11;

          hence thesis by A8, CARD_3: 9;

        end;

      end;

      ( dom f) = SCM-Memory by AMI_2: 27;

      then

      reconsider t as State of SCM by A3, A7, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;

      reconsider w = t as SCM-State by CARD_3: 107;

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

      

      then

       A10: ((w +* ( NAT .--> loc)) . NAT ) = (( NAT .--> loc) . NAT ) by FUNCT_4: 13

      .= loc by FUNCOP_1: 72;

      assume

       A11: (a >0_goto loc) is halting;

      

       A12: a is Element of SCM-Data-Loc by AMI_2:def 16;

      per cases ;

        suppose

         A13: (w . (V cond_address )) <= 0 ;

        ( IC w) = (w . NAT );

        then

        reconsider e = (w . NAT ) as Nat;

        ( IC t) = ( IC w) & (t . a) <= 0 by A4, A12, A13, AMI_2: 22, SCM_INST: 7, SUBSET_1:def 8;

        then

         A14: (( Exec ((a >0_goto loc),t)) . ( IC SCM )) = (e + 1) by Th9;

        (( Exec ((a >0_goto loc),t)) . ( IC SCM )) = (w . NAT ) by A11, Th1;

        hence contradiction by A14;

      end;

        suppose (w . (V cond_address )) > 0 ;

        then ( IFGT ((w . (V cond_address )), 0 ,(V cjump_address ),(( IC w) + 1))) = (V cjump_address ) by XXREAL_0:def 11;

        

        then (w +* ( NAT .--> loc)) = ( SCM-Chg (w,( IFGT ((w . (V cond_address )), 0 ,(V cjump_address ),(( IC w) + 1))))) by A4, A12, SCM_INST: 7

        .= ( SCM-Exec-Res (V,w)) by A12, AMI_2:def 14

        .= ( Exec ((a >0_goto loc),t)) by AMI_2:def 15

        .= t by A11;

        hence contradiction by A6, A10;

      end;

    end;

    

     Lm12: for I be set holds I is Instruction of SCM iff I = [ 0 , {} , {} ] or (ex a, b st I = (a := b)) or (ex a, b st I = ( AddTo (a,b))) or (ex a, b st I = ( SubFrom (a,b))) or (ex a, b st I = ( MultBy (a,b))) or (ex a, b st I = ( Divide (a,b))) or (ex loc st I = ( SCM-goto loc)) or (ex a, loc st I = (a =0_goto loc)) or ex a, loc st I = (a >0_goto loc)

    proof

      let I be set;

      thus I is Instruction of SCM implies I = [ 0 , {} , {} ] or (ex a, b st I = (a := b)) or (ex a, b st I = ( AddTo (a,b))) or (ex a, b st I = ( SubFrom (a,b))) or (ex a, b st I = ( MultBy (a,b))) or (ex a, b st I = ( Divide (a,b))) or (ex loc st I = ( SCM-goto loc)) or (ex a, loc st I = (a =0_goto loc)) or ex a, loc st I = (a >0_goto loc)

      proof

        assume I is Instruction of SCM ;

        then I in (( { [ SCM-Halt , {} , {} ]} \/ { [Y, <*a3*>, {} ] : Y = 6 }) \/ { [K, <*a1*>, <*b1*>] : K in {7, 8} }) or I in { [T, {} , <*c2, c3*>] : T in {1, 2, 3, 4, 5} } by XBOOLE_0:def 3;

        then

         A1: I in ( { [ SCM-Halt , {} , {} ]} \/ { [Y, <*a3*>, {} ] : Y = 6 }) or I in { [K, <*a1*>, <*b1*>] : K in {7, 8} } or I in { [T, {} , <*c2, c3*>] : T in {1, 2, 3, 4, 5} } by XBOOLE_0:def 3;

        per cases by A1, XBOOLE_0:def 3;

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

          hence thesis by TARSKI:def 1;

        end;

          suppose I in { [Y, <*a3*>, {} ] : Y = 6 };

          then

          consider Y, a3 such that

           A2: I = [Y, <*a3*>, {} ] & Y = 6;

          I = ( SCM-goto a3) by A2;

          hence thesis;

        end;

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

          then

          consider K, a1, b1 such that

           A3: I = [K, <*a1*>, <*b1*>] & K in {7, 8};

          reconsider a = b1 as Data-Location by AMI_2:def 16;

          reconsider loc = a1 as Nat;

          I = (a =0_goto a1) or I = (a >0_goto a1) by A3, TARSKI:def 2;

          hence thesis;

        end;

          suppose I in { [T, {} , <*c2, c3*>] : T in {1, 2, 3, 4, 5} };

          then

          consider T, c2, c3 such that

           A4: I = [T, {} , <*c2, c3*>] & T in {1, 2, 3, 4, 5};

          reconsider a = c2, b = c3 as Data-Location by AMI_2:def 16;

          I = (a := b) or I = ( AddTo (a,b)) or I = ( SubFrom (a,b)) or I = ( MultBy (a,b)) or I = ( Divide (a,b)) by A4, ENUMSET1:def 3;

          hence thesis;

        end;

      end;

      thus thesis by SCM_INST: 1;

    end;

    

     Lm13: for W be Instruction of SCM st W is halting holds W = [ 0 , {} , {} ]

    proof

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

      let W be Instruction of SCM such that

       A1: W is halting;

      assume

       A2: I <> W;

      per cases by Lm12;

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

        hence thesis by A2;

      end;

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

        hence thesis by A1, Lm4;

      end;

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

        hence thesis by A1, Lm5;

      end;

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

        hence thesis by A1, Lm6;

      end;

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

        hence thesis by A1, Lm7;

      end;

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

        hence thesis by A1, Lm8;

      end;

        suppose ex loc st W = ( SCM-goto loc);

        hence thesis by A1, Lm9;

      end;

        suppose ex a, loc st W = (a =0_goto loc);

        hence thesis by A1, Lm10;

      end;

        suppose ex a, loc st W = (a >0_goto loc);

        hence thesis by A1, Lm11;

      end;

    end;

    registration

      cluster SCM -> halting;

      coherence by Lm3;

    end

    begin

    definition

      let k be Nat;

      :: AMI_3:def11

      func dl. k -> Data-Location equals [1, k];

      coherence

      proof

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

        1 in {1} by TARSKI:def 1;

        then [1, k] in SCM-Data-Loc by ZFMISC_1: 87;

        hence thesis by AMI_2:def 16;

      end;

    end

    reserve i,j,k for Nat;

    theorem :: AMI_3:10

    i <> j implies ( dl. i) <> ( dl. j) by XTUPLE_0: 1;

    theorem :: AMI_3:11

    

     Th11: for l be Data-Location holds ( Values l) = INT by AMI_2:def 16, AMI_2: 7;

    definition

      let la be Data-Location;

      let a be Integer;

      :: original: .-->

      redefine

      func la .--> a -> PartState of SCM ;

      coherence

      proof

        

         A1: a is Element of INT & ( Values la) = INT by Th11, INT_1:def 2;

        then

        reconsider a as Element of (( the_Values_of SCM ) . la);

        (la .--> a) is PartState of SCM by A1;

        hence thesis;

      end;

    end

    definition

      let la,lb be Data-Location;

      let a,b be Integer;

      :: original: -->

      redefine

      func (la,lb) --> (a,b) -> PartState of SCM ;

      coherence

      proof

        

         A1: a is Element of INT & b is Element of INT by INT_1:def 2;

        

         A2: ( Values la) = INT & ( Values lb) = INT by Th11;

        then

        reconsider a as Element of ( Values la) by A1;

        reconsider b as Element of ( Values lb) by A1, A2;

        ((la,lb) --> (a,b)) is PartState of SCM ;

        hence thesis;

      end;

    end

    theorem :: AMI_3:12

    ( dl. i) <> j;

    theorem :: AMI_3:13

    ( IC SCM ) <> ( dl. i) & ( IC SCM ) <> i by Th1;

    begin

    theorem :: AMI_3:14

    for I be Instruction of SCM st ex s st (( Exec (I,s)) . ( IC SCM )) = (( IC s) + 1) holds I is non halting by Lm2;

    theorem :: AMI_3:15

    for I be Instruction of SCM st I = [ 0 , {} , {} ] holds I is halting by Lm3;

    theorem :: AMI_3:16

    (a := b) is non halting by Lm4;

    theorem :: AMI_3:17

    ( AddTo (a,b)) is non halting by Lm5;

    theorem :: AMI_3:18

    ( SubFrom (a,b)) is non halting by Lm6;

    theorem :: AMI_3:19

    ( MultBy (a,b)) is non halting by Lm7;

    theorem :: AMI_3:20

    ( Divide (a,b)) is non halting by Lm8;

    theorem :: AMI_3:21

    ( SCM-goto loc) is non halting by Lm9;

    theorem :: AMI_3:22

    (a =0_goto loc) is non halting by Lm10;

    theorem :: AMI_3:23

    (a >0_goto loc) is non halting by Lm11;

    theorem :: AMI_3:24

    for I be set holds I is Instruction of SCM iff I = [ 0 , {} , {} ] or (ex a, b st I = (a := b)) or (ex a, b st I = ( AddTo (a,b))) or (ex a, b st I = ( SubFrom (a,b))) or (ex a, b st I = ( MultBy (a,b))) or (ex a, b st I = ( Divide (a,b))) or (ex loc st I = ( SCM-goto loc)) or (ex a, loc st I = (a =0_goto loc)) or ex a, loc st I = (a >0_goto loc) by Lm12;

    theorem :: AMI_3:25

    for I be Instruction of SCM st I is halting holds I = ( halt SCM ) by Lm13;

    theorem :: AMI_3:26

    ( halt SCM ) = [ 0 , {} , {} ];

    theorem :: AMI_3:27

    

     Th27: ( Data-Locations SCM ) = SCM-Data-Loc

    proof

       SCM-Data-Loc misses { NAT } by AMI_2: 20, ZFMISC_1: 50;

      then

       A1: SCM-Data-Loc misses { NAT };

      

      thus ( Data-Locations SCM ) = (( { NAT } \/ SCM-Data-Loc ) \ { NAT }) by AMI_2: 22, SUBSET_1:def 8

      .= (( SCM-Data-Loc \/ { NAT }) \ { NAT })

      .= ( SCM-Data-Loc \ { NAT }) by XBOOLE_1: 40

      .= SCM-Data-Loc by A1, XBOOLE_1: 83;

    end;

    theorem :: AMI_3:28

    for d be Data-Location holds d in ( Data-Locations SCM ) by Th27, AMI_2:def 16;

    theorem :: AMI_3:29

    for s be SCM-State holds s is State of SCM by Lm1;

    theorem :: AMI_3:30

    for l be Element of SCM-Instr holds ( InsCode l) <= 8 by SCM_INST: 10;