amistd_4.miz



    begin

    reserve N for with_zero set;

    definition

      let N be with_zero set, A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, s be State of A, o be Object of A, a be Element of ( Values o);

      :: original: +*

      redefine

      func s +* (o,a) -> State of A ;

      coherence

      proof

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

        then (s +* (o,a)) = (s +* (o .--> a)) by FUNCT_7:def 3;

        hence thesis;

      end;

    end

    theorem :: AMISTD_4:1

    

     Th1: for A be standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A, s be State of A, o be Object of A, w be Element of ( Values o) st I is sequential & o <> ( IC A) holds ( IC ( Exec (I,s))) = ( IC ( Exec (I,(s +* (o,w)))))

    proof

      let A be standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A, s be State of A, o be Object of A, w be Element of ( Values o) such that

       A1: for s be State of A holds (( Exec (I,s)) . ( IC A)) = (( IC s) + 1) and

       A2: o <> ( IC A);

      

      thus ( IC ( Exec (I,s))) = (( IC s) + 1) by A1

      .= (( IC (s +* (o,w))) + 1) by A2, FUNCT_7: 32

      .= ( IC ( Exec (I,(s +* (o,w))))) by A1;

    end;

    theorem :: AMISTD_4:2

    for A be standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A, s be State of A, o be Object of A, w be Element of ( Values o) st I is sequential & o <> ( IC A) holds ( IC ( Exec (I,(s +* (o,w))))) = ( IC (( Exec (I,s)) +* (o,w)))

    proof

      let A be standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A, s be State of A, o be Object of A, w be Element of ( Values o) such that

       A1: I is sequential and

       A2: o <> ( IC A);

      

      thus ( IC ( Exec (I,(s +* (o,w))))) = ( IC ( Exec (I,s))) by A1, A2, Th1

      .= ( IC (( Exec (I,s)) +* (o,w))) by A2, FUNCT_7: 32;

    end;

    begin

    definition

      let A be COM-Struct;

      :: AMISTD_4:def1

      attr A is with_non_trivial_Instructions means

      : Def1: the InstructionsF of A is non trivial;

    end

    definition

      let N be with_zero set, A be non empty with_non-empty_values AMI-Struct over N;

      :: AMISTD_4:def2

      attr A is with_non_trivial_ObjectKinds means

      : Def2: for o be Object of A holds ( Values o) is non trivial;

    end

    registration

      let N be with_zero set;

      cluster ( STC N) -> with_non_trivial_ObjectKinds;

      coherence

      proof

        let o be Object of ( STC N);

        

         A1: the carrier of ( STC N) = { 0 } by AMISTD_1:def 7;

        

         A2: the Object-Kind of ( STC N) = ( 0 .--> 0 ) by AMISTD_1:def 7;

        per cases by A1;

          suppose

           A3: o in { 0 };

          

           A4: the ValuesF of ( STC N) = (N --> NAT ) by AMISTD_1:def 7;

           0 in N by MEASURE6:def 2;

          then ( the_Values_of ( STC N)) = ( 0 .--> NAT ) by A2, A4, FUNCOP_1: 89;

          

          then ( Values o) = (( 0 .--> NAT ) . o)

          .= NAT by A3, FUNCOP_1: 7;

          hence thesis;

        end;

      end;

    end

    registration

      let N be with_zero set;

      cluster with_explicit_jumps IC-relocable with_non_trivial_ObjectKinds with_non_trivial_Instructions for standard halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

      existence

      proof

        take ( STC N);

        

         A1: [1, 0 , 0 ] in { [1, 0 , 0 ], [ 0 , 0 , 0 ]} & [ 0 , 0 , 0 ] in { [1, 0 , 0 ], [ 0 , 0 , 0 ]} by TARSKI:def 2;

        the InstructionsF of ( STC N) = { [ 0 , 0 , 0 ], [1, 0 , 0 ]} & [1, 0 , 0 ] <> [ 0 , 0 , 0 ] by AMISTD_1:def 7, XTUPLE_0: 3;

        then the InstructionsF of ( STC N) is non trivial by A1, ZFMISC_1:def 10;

        hence thesis;

      end;

    end

    registration

      let N be with_zero set;

      cluster ( STC N) -> with_non_trivial_Instructions;

      coherence

      proof

        

         A1: [ 0 , 0 , 0 ] <> [1, 0 , 0 ] by XTUPLE_0: 3;

        the InstructionsF of ( STC N) = { [ 0 , 0 , 0 ], [1, 0 , 0 ]} by AMISTD_1:def 7;

        then [ 0 , 0 , 0 ] in the InstructionsF of ( STC N) & [1, 0 , 0 ] in the InstructionsF of ( STC N) by TARSKI:def 2;

        hence the InstructionsF of ( STC N) is non trivial by A1, ZFMISC_1:def 10;

      end;

    end

    registration

      let N be with_zero set;

      cluster with_non_trivial_ObjectKinds with_non_trivial_Instructions IC-Ins-separated for non empty with_non-empty_values AMI-Struct over N;

      existence

      proof

        take ( STC N);

        thus thesis;

      end;

    end

    registration

      let N be with_zero set, A be with_non_trivial_ObjectKinds non empty with_non-empty_values AMI-Struct over N, o be Object of A;

      cluster ( Values o) -> non trivial;

      coherence by Def2;

    end

    registration

      let N be with_zero set, A be with_non_trivial_Instructions with_non-empty_values AMI-Struct over N;

      cluster the InstructionsF of A -> non trivial;

      coherence by Def1;

    end

    registration

      let N be with_zero set, A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

      cluster ( Values ( IC A)) -> non trivial;

      coherence by MEMSTR_0:def 6;

    end

    definition

      let N be with_zero set, A be non empty with_non-empty_values AMI-Struct over N, I be Instruction of A;

      :: AMISTD_4:def3

      func Output I -> Subset of A means

      : Def3: for o be Object of A holds o in it iff ex s be State of A st (s . o) <> (( Exec (I,s)) . o);

      existence

      proof

        defpred P[ set] means ex s be State of A st (s . $1) <> (( Exec (I,s)) . $1);

        consider X be Subset of A such that

         A1: for x be set holds x in X iff x in the carrier of A & P[x] from SUBSET_1:sch 1;

        take X;

        thus thesis by A1;

      end;

      uniqueness

      proof

        defpred P[ set] means ex s be State of A st (s . $1) <> (( Exec (I,s)) . $1);

        let a,b be Subset of A such that

         A2: for o be Object of A holds o in a iff P[o] and

         A3: for o be Object of A holds o in b iff P[o];

        thus a = b from SUBSET_1:sch 2( A2, A3);

      end;

    end

    definition

      let N be with_zero set, A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A;

      :: AMISTD_4:def4

      func Out_\_Inp I -> Subset of A means

      : Def4: for o be Object of A holds o in it iff for s be State of A, a be Element of ( Values o) holds ( Exec (I,s)) = ( Exec (I,(s +* (o,a))));

      existence

      proof

        defpred P[ set] means ex l be Object of A st l = $1 & for s be State of A, a be Element of ( Values l) holds ( Exec (I,s)) = ( Exec (I,(s +* (l,a))));

        consider X be Subset of A such that

         A1: for x be set holds x in X iff x in the carrier of A & P[x] from SUBSET_1:sch 1;

        take X;

        let l be Object of A;

        hereby

          assume l in X;

          then P[l] by A1;

          hence for s be State of A, a be Element of ( Values l) holds ( Exec (I,s)) = ( Exec (I,(s +* (l,a))));

        end;

        thus thesis by A1;

      end;

      uniqueness

      proof

        defpred P[ Object of A] means for s be State of A, a be Element of ( Values $1) holds ( Exec (I,s)) = ( Exec (I,(s +* ($1,a))));

        let a,b be Subset of A such that

         A2: for o be Object of A holds o in a iff P[o] and

         A3: for o be Object of A holds o in b iff P[o];

        thus a = b from SUBSET_1:sch 2( A2, A3);

      end;

      :: AMISTD_4:def5

      func Out_U_Inp I -> Subset of A means

      : Def5: for o be Object of A holds o in it iff ex s be State of A, a be Element of ( Values o) st ( Exec (I,(s +* (o,a)))) <> (( Exec (I,s)) +* (o,a));

      existence

      proof

        defpred P[ set] means ex l be Object of A st l = $1 & ex s be State of A, a be Element of ( Values l) st ( Exec (I,(s +* (l,a)))) <> (( Exec (I,s)) +* (l,a));

        consider X be Subset of A such that

         A4: for x be set holds x in X iff x in the carrier of A & P[x] from SUBSET_1:sch 1;

        take X;

        let l be Object of A;

        hereby

          assume l in X;

          then P[l] by A4;

          hence ex s be State of A, a be Element of ( Values l) st ( Exec (I,(s +* (l,a)))) <> (( Exec (I,s)) +* (l,a));

        end;

        thus thesis by A4;

      end;

      uniqueness

      proof

        defpred P[ Object of A] means ex s be State of A, a be Element of ( Values $1) st ( Exec (I,(s +* ($1,a)))) <> (( Exec (I,s)) +* ($1,a));

        let a,b be Subset of A such that

         A5: for o be Object of A holds o in a iff P[o] and

         A6: for o be Object of A holds o in b iff P[o];

        thus a = b from SUBSET_1:sch 2( A5, A6);

      end;

    end

    definition

      let N be with_zero set, A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A;

      :: AMISTD_4:def6

      func Input I -> Subset of A equals (( Out_U_Inp I) \ ( Out_\_Inp I));

      coherence ;

    end

    theorem :: AMISTD_4:3

    

     Th3: for A be with_non_trivial_ObjectKinds IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A holds ( Out_\_Inp I) c= ( Output I)

    proof

      let A be with_non_trivial_ObjectKinds IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A;

      for o be Object of A holds o in ( Out_\_Inp I) implies o in ( Output I)

      proof

        let o be Object of A;

        set s = the State of A, a = the Element of ( Values o);

        consider w be object such that

         A1: w in ( Values o) and

         A2: w <> a by SUBSET_1: 48;

        reconsider w as Element of ( Values o) by A1;

        set t = (s +* (o,w));

        

         A3: ( dom t) = the carrier of A by PARTFUN1:def 2;

        

         A4: ( dom s) = the carrier of A by PARTFUN1:def 2;

        assume

         A5: not thesis;

        

        then

         A6: (( Exec (I,(t +* (o,a)))) . o) = ((t +* (o,a)) . o) by Def3

        .= a by A3, FUNCT_7: 31;

        (( Exec (I,t)) . o) = (t . o) by A5, Def3

        .= w by A4, FUNCT_7: 31;

        hence contradiction by A5, A2, A6, Def4;

      end;

      hence thesis by SUBSET_1: 2;

    end;

    theorem :: AMISTD_4:4

    

     Th4: for A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A holds ( Output I) c= ( Out_U_Inp I)

    proof

      let A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A;

      for o be Object of A holds o in ( Output I) implies o in ( Out_U_Inp I)

      proof

        let o be Object of A;

        assume

         A1: not thesis;

        for s be State of A holds (s . o) = (( Exec (I,s)) . o)

        proof

          let s be State of A;

          reconsider so = (s . o) as Element of ( Values o) by MEMSTR_0: 77;

          

           A2: ( Exec (I,(s +* (o,so)))) = (( Exec (I,s)) +* (o,so)) by A1, Def5;

          ( dom ( Exec (I,s))) = the carrier of A by PARTFUN1:def 2;

          

          hence (s . o) = ((( Exec (I,s)) +* (o,so)) . o) by FUNCT_7: 31

          .= (( Exec (I,s)) . o) by A2, FUNCT_7: 35;

        end;

        hence contradiction by A1, Def3;

      end;

      hence thesis by SUBSET_1: 2;

    end;

    theorem :: AMISTD_4:5

    for A be with_non_trivial_ObjectKinds IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A holds ( Out_\_Inp I) = (( Output I) \ ( Input I))

    proof

      let A be with_non_trivial_ObjectKinds IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A;

      for o be Object of A holds o in ( Out_\_Inp I) iff o in (( Output I) \ ( Input I))

      proof

        let o be Object of A;

        hereby

          

           A1: ( Out_\_Inp I) c= ( Output I) by Th3;

          assume

           A2: o in ( Out_\_Inp I);

          ( Out_\_Inp I) misses ( Input I) by XBOOLE_1: 85;

          then not o in ( Input I) by A2, XBOOLE_0: 3;

          hence o in (( Output I) \ ( Input I)) by A2, A1, XBOOLE_0:def 5;

        end;

        assume

         A3: o in (( Output I) \ ( Input I));

        then

         A4: not o in ( Input I) by XBOOLE_0:def 5;

        per cases by A4, XBOOLE_0:def 5;

          suppose

           A5: not o in ( Out_U_Inp I);

          ( Output I) c= ( Out_U_Inp I) by Th4;

          then not o in ( Output I) by A5;

          hence thesis by A3, XBOOLE_0:def 5;

        end;

          suppose o in ( Out_\_Inp I);

          hence thesis;

        end;

      end;

      hence thesis by SUBSET_1: 3;

    end;

    theorem :: AMISTD_4:6

    for A be with_non_trivial_ObjectKinds IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A holds ( Out_U_Inp I) = (( Output I) \/ ( Input I))

    proof

      let A be with_non_trivial_ObjectKinds IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A;

      for o be Object of A st o in ( Out_U_Inp I) holds o in (( Output I) \/ ( Input I))

      proof

        let o be Object of A such that

         A1: o in ( Out_U_Inp I);

        o in ( Input I) or o in ( Output I)

        proof

          assume

           A2: not o in ( Input I);

          per cases by A2, XBOOLE_0:def 5;

            suppose not o in ( Out_U_Inp I);

            hence thesis by A1;

          end;

            suppose

             A3: o in ( Out_\_Inp I);

            ( Out_\_Inp I) c= ( Output I) by Th3;

            hence thesis by A3;

          end;

        end;

        hence thesis by XBOOLE_0:def 3;

      end;

      hence ( Out_U_Inp I) c= (( Output I) \/ ( Input I)) by SUBSET_1: 2;

      ( Output I) c= ( Out_U_Inp I) & ( Input I) c= ( Out_U_Inp I) by Th4, XBOOLE_1: 36;

      hence thesis by XBOOLE_1: 8;

    end;

    theorem :: AMISTD_4:7

    

     Th7: for A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A, o be Object of A st ( Values o) is trivial holds not o in ( Out_U_Inp I)

    proof

      let A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A, o be Object of A such that

       A1: ( Values o) is trivial;

      assume o in ( Out_U_Inp I);

      then

      consider s be State of A, a be Element of ( Values o) such that

       A2: ( Exec (I,(s +* (o,a)))) <> (( Exec (I,s)) +* (o,a)) by Def5;

      (s . o) is Element of ( Values o) by MEMSTR_0: 77;

      then (s . o) = a by A1, ZFMISC_1:def 10;

      then

       A3: ( Exec (I,(s +* (o,a)))) = ( Exec (I,s)) by FUNCT_7: 35;

      

       A4: ( dom ( Exec (I,s))) = the carrier of A by PARTFUN1:def 2;

      

       A5: for x be object st x in the carrier of A holds ((( Exec (I,s)) +* (o,a)) . x) = (( Exec (I,s)) . x)

      proof

        let x be object such that x in the carrier of A;

        per cases ;

          suppose

           A6: x = o;

          

           A7: (( Exec (I,s)) . o) is Element of ( Values o) by MEMSTR_0: 77;

          

          thus ((( Exec (I,s)) +* (o,a)) . x) = a by A4, A6, FUNCT_7: 31

          .= (( Exec (I,s)) . x) by A1, A6, A7, ZFMISC_1:def 10;

        end;

          suppose x <> o;

          hence thesis by FUNCT_7: 32;

        end;

      end;

      ( dom (( Exec (I,s)) +* (o,a))) = the carrier of A by PARTFUN1:def 2;

      hence contradiction by A2, A3, A4, A5, FUNCT_1: 2;

    end;

    theorem :: AMISTD_4:8

    for A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A, o be Object of A st ( Values o) is trivial holds not o in ( Input I)

    proof

      let A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A, o be Object of A;

      

       A1: ( Input I) c= ( Out_U_Inp I) by XBOOLE_1: 36;

      assume ( Values o) is trivial;

      hence thesis by A1, Th7;

    end;

    theorem :: AMISTD_4:9

    for A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A, o be Object of A st ( Values o) is trivial holds not o in ( Output I)

    proof

      let A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A, o be Object of A;

      assume

       A1: ( Values o) is trivial;

      ( Output I) c= ( Out_U_Inp I) by Th4;

      hence thesis by A1, Th7;

    end;

    theorem :: AMISTD_4:10

    

     Th10: for A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A holds I is halting iff ( Output I) is empty

    proof

      let A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A;

      thus I is halting implies ( Output I) is empty

      proof

        assume

         A1: for s be State of A holds ( Exec (I,s)) = s;

        assume not thesis;

        then

        consider o be Object of A such that

         A2: o in ( Output I);

        ex s be State of A st (s . o) <> (( Exec (I,s)) . o) by A2, Def3;

        hence thesis by A1;

      end;

      assume

       A3: ( Output I) is empty;

      let s be State of A;

      assume

       A4: ( Exec (I,s)) <> s;

      ( dom s) = the carrier of A & ( dom ( Exec (I,s))) = the carrier of A by PARTFUN1:def 2;

      then ex x be object st x in the carrier of A & (( Exec (I,s)) . x) <> (s . x) by A4, FUNCT_1: 2;

      hence contradiction by A3, Def3;

    end;

    theorem :: AMISTD_4:11

    

     Th11: for A be with_non_trivial_ObjectKinds IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A st I is halting holds ( Out_\_Inp I) is empty

    proof

      let A be with_non_trivial_ObjectKinds IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A such that

       A1: I is halting;

      ( Out_\_Inp I) c= ( Output I) by Th3;

      then ( Out_\_Inp I) c= {} by A1, Th10;

      hence thesis;

    end;

    theorem :: AMISTD_4:12

    

     Th12: for A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A st I is halting holds ( Out_U_Inp I) is empty

    proof

      let A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A such that

       A1: for s be State of A holds ( Exec (I,s)) = s;

      assume not thesis;

      then

      consider o be Object of A such that

       A2: o in ( Out_U_Inp I);

      consider s be State of A, a be Element of ( Values o) such that

       A3: ( Exec (I,(s +* (o,a)))) <> (( Exec (I,s)) +* (o,a)) by A2, Def5;

      ( Exec (I,(s +* (o,a)))) = (s +* (o,a)) by A1

      .= (( Exec (I,s)) +* (o,a)) by A1;

      hence thesis by A3;

    end;

    theorem :: AMISTD_4:13

    

     Th13: for A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A st I is halting holds ( Input I) is empty

    proof

      let A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A;

      assume I is halting;

      

      then ( Input I) = ( {} \ ( Out_\_Inp I)) by Th12

      .= {} ;

      hence thesis;

    end;

    registration

      let N be with_zero set, A be halting IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be halting Instruction of A;

      cluster ( Input I) -> empty;

      coherence by Th13;

      cluster ( Output I) -> empty;

      coherence by Th10;

      cluster ( Out_U_Inp I) -> empty;

      coherence by Th12;

    end

    registration

      let N be with_zero set;

      cluster halting with_non_trivial_ObjectKinds IC-Ins-separated for non empty with_non-empty_values AMI-Struct over N;

      existence

      proof

        take ( STC N);

        thus thesis;

      end;

    end

    registration

      let N be with_zero set, A be halting with_non_trivial_ObjectKinds IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be halting Instruction of A;

      cluster ( Out_\_Inp I) -> empty;

      coherence by Th11;

    end

    registration

      let N;

      cluster with_non_trivial_Instructions IC-Ins-separated for non empty with_non-empty_values AMI-Struct over N;

      existence

      proof

        take ( STC N);

        thus thesis;

      end;

    end

    theorem :: AMISTD_4:14

    for A be standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A st I is sequential holds not ( IC A) in ( Out_\_Inp I)

    proof

      let A be standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A;

      set t = the State of A;

      set l = ( IC A);

      reconsider sICt = (( IC t) + 1) as Element of NAT ;

      reconsider w = sICt as Element of ( Values l) by MEMSTR_0:def 6;

      set s = (t +* (l,w));

      assume for s be State of A holds (( Exec (I,s)) . ( IC A)) = (( IC s) + 1);

      then

       A1: (( Exec (I,t)) . l) = (( IC t) + 1) & (( Exec (I,s)) . l) = (( IC s) + 1);

      ( dom t) = the carrier of A by PARTFUN1:def 2;

      then (s . l) = w by FUNCT_7: 31;

      then ( Exec (I,t)) <> ( Exec (I,s)) by A1, NAT_1: 16;

      hence thesis by Def4;

    end;

    theorem :: AMISTD_4:15

    for A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A st ex s be State of A st (( Exec (I,s)) . ( IC A)) <> ( IC s) holds ( IC A) in ( Output I) by Def3;

    registration

      let N;

      cluster standard for IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;

      existence

      proof

        take ( STC N);

        thus thesis;

      end;

    end

    theorem :: AMISTD_4:16

    for A be standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A st I is sequential holds ( IC A) in ( Output I)

    proof

      let A be standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A such that

       A1: for s be State of A holds (( Exec (I,s)) . ( IC A)) = (( IC s) + 1);

      set s = the State of A;

      (( Exec (I,s)) . ( IC A)) = (( IC s) + 1) by A1;

      then (( Exec (I,s)) . ( IC A)) <> ( IC s) by NAT_1: 16;

      hence thesis by Def3;

    end;

    theorem :: AMISTD_4:17

    

     Th17: for A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A st ex s be State of A st (( Exec (I,s)) . ( IC A)) <> ( IC s) holds ( IC A) in ( Out_U_Inp I)

    proof

      let A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A;

      assume ex s be State of A st (( Exec (I,s)) . ( IC A)) <> ( IC s);

      then

       A1: ( IC A) in ( Output I) by Def3;

      ( Output I) c= ( Out_U_Inp I) by Th4;

      hence thesis by A1;

    end;

    theorem :: AMISTD_4:18

    for A be standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A st I is sequential holds ( IC A) in ( Out_U_Inp I)

    proof

      let A be standard IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A;

      set s = the State of A;

      assume for s be State of A holds (( Exec (I,s)) . ( IC A)) = (( IC s) + 1);

      then (( Exec (I,s)) . ( IC A)) = (( IC s) + 1);

      then (( Exec (I,s)) . ( IC A)) <> ( IC s) by NAT_1: 16;

      hence thesis by Th17;

    end;

    theorem :: AMISTD_4:19

    for A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A, o be Object of A st I is jump-only holds o in ( Output I) implies o = ( IC A)

    proof

      let A be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N, I be Instruction of A, o be Object of A;

      assume

       A1: for s be State of A, o be Object of A, J be Instruction of A st ( InsCode I) = ( InsCode J) & o in ( Data-Locations A) holds (( Exec (J,s)) . o) = (s . o);

      assume o in ( Output I);

      then ex s be State of A st (s . o) <> (( Exec (I,s)) . o) by Def3;

      then

       A2: not o in ( Data-Locations A) by A1;

      o in the carrier of A;

      then o in ( {( IC A)} \/ ( Data-Locations A)) by STRUCT_0: 4;

      then o in {( IC A)} by A2, XBOOLE_0:def 3;

      hence thesis by TARSKI:def 1;

    end;