:: by Artur Korni{\l}owicz

::

:: Received May 8, 2001

:: Copyright (c) 2001-2012 Association of Mizar Users

begin

definition

let N be with_zero set ;

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

let s be State of A;

let o be Object of A;

let a be Element of Values o;

:: original: +*

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

coherence

s +* (o,a) is State of A

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

let s be State of A;

let o be Object of A;

let a be Element of Values o;

:: original: +*

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

coherence

s +* (o,a) is State of A

proof end;

theorem Th1: :: AMISTD_4:1

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N

for I being Instruction of A

for s being State of A

for o being Object of A

for w being Element of Values o st I is sequential & o <> IC holds

IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w))))

for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N

for I being Instruction of A

for s being State of A

for o being Object of A

for w being Element of Values o st I is sequential & o <> IC holds

IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w))))

proof end;

theorem :: AMISTD_4:2

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N

for I being Instruction of A

for s being State of A

for o being Object of A

for w being Element of Values o st I is sequential & o <> IC holds

IC (Exec (I,(s +* (o,w)))) = IC ((Exec (I,s)) +* (o,w))

for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N

for I being Instruction of A

for s being State of A

for o being Object of A

for w being Element of Values o st I is sequential & o <> IC holds

IC (Exec (I,(s +* (o,w)))) = IC ((Exec (I,s)) +* (o,w))

proof end;

begin

definition

let A be COM-Struct ;

end;
attr A is with_non_trivial_Instructions means :Def1: :: AMISTD_4:def 1

not the InstructionsF of A is trivial ;

not the InstructionsF of A is trivial ;

:: deftheorem Def1 defines with_non_trivial_Instructions AMISTD_4:def 1 :

for A being COM-Struct holds

( A is with_non_trivial_Instructions iff not the InstructionsF of A is trivial );

for A being COM-Struct holds

( A is with_non_trivial_Instructions iff not the InstructionsF of A is trivial );

definition

let N be with_zero set ;

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

end;
let A be non empty with_non-empty_values AMI-Struct over N;

attr A is with_non_trivial_ObjectKinds means :Def2: :: AMISTD_4:def 2

for o being Object of A holds not Values o is trivial ;

for o being Object of A holds not Values o is trivial ;

:: deftheorem Def2 defines with_non_trivial_ObjectKinds AMISTD_4:def 2 :

for N being with_zero set

for A being non empty with_non-empty_values AMI-Struct over N holds

( A is with_non_trivial_ObjectKinds iff for o being Object of A holds not Values o is trivial );

for N being with_zero set

for A being non empty with_non-empty_values AMI-Struct over N holds

( A is with_non_trivial_ObjectKinds iff for o being Object of A holds not Values o is trivial );

registration
end;

registration

let N be with_zero set ;

ex b_{1} being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N st

( b_{1} is with_explicit_jumps & b_{1} is IC-relocable & b_{1} is with_non_trivial_ObjectKinds & b_{1} is with_non_trivial_Instructions )

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

existence ex b

( b

proof end;

registration
end;

registration

let N be with_zero set ;

ex b_{1} being non empty with_non-empty_values AMI-Struct over N st

( b_{1} is with_non_trivial_ObjectKinds & b_{1} is with_non_trivial_Instructions & b_{1} is IC-Ins-separated )

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

existence ex b

( b

proof end;

registration

let N be with_zero set ;

let A be non empty with_non-empty_values with_non_trivial_ObjectKinds AMI-Struct over N;

let o be Object of A;

coherence

not Values o is trivial by Def2;

end;
let A be non empty with_non-empty_values with_non_trivial_ObjectKinds AMI-Struct over N;

let o be Object of A;

coherence

not Values o is trivial by Def2;

registration

let N be with_zero set ;

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

coherence

not the InstructionsF of A is trivial by Def1;

end;
let A be with_non-empty_values with_non_trivial_Instructions AMI-Struct over N;

coherence

not the InstructionsF of A is trivial by Def1;

registration

let N be with_zero set ;

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

coherence

not Values (IC ) is trivial by MEMSTR_0:def 6;

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

coherence

not Values (IC ) is trivial by MEMSTR_0:def 6;

definition

let N be with_zero set ;

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

let I be Instruction of A;

ex b_{1} being Subset of A st

for o being Object of A holds

( o in b_{1} iff ex s being State of A st s . o <> (Exec (I,s)) . o )

for b_{1}, b_{2} being Subset of A st ( for o being Object of A holds

( o in b_{1} iff ex s being State of A st s . o <> (Exec (I,s)) . o ) ) & ( for o being Object of A holds

( o in b_{2} iff ex s being State of A st s . o <> (Exec (I,s)) . o ) ) holds

b_{1} = b_{2}

end;
let A be non empty with_non-empty_values AMI-Struct over N;

let I be Instruction of A;

func Output I -> Subset of A means :Def3: :: AMISTD_4:def 3

for o being Object of A holds

( o in it iff ex s being State of A st s . o <> (Exec (I,s)) . o );

existence for o being Object of A holds

( o in it iff ex s being State of A st s . o <> (Exec (I,s)) . o );

ex b

for o being Object of A holds

( o in b

proof end;

uniqueness for b

( o in b

( o in b

b

proof end;

:: deftheorem Def3 defines Output AMISTD_4:def 3 :

for N being with_zero set

for A being non empty with_non-empty_values AMI-Struct over N

for I being Instruction of A

for b_{4} being Subset of A holds

( b_{4} = Output I iff for o being Object of A holds

( o in b_{4} iff ex s being State of A st s . o <> (Exec (I,s)) . o ) );

for N being with_zero set

for A being non empty with_non-empty_values AMI-Struct over N

for I being Instruction of A

for b

( b

( o in b

definition

let N be with_zero set ;

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

let I be Instruction of A;

ex b_{1} being Subset of A st

for o being Object of A holds

( o in b_{1} iff for s being State of A

for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) )

for b_{1}, b_{2} being Subset of A st ( for o being Object of A holds

( o in b_{1} iff for s being State of A

for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) ) & ( for o being Object of A holds

( o in b_{2} iff for s being State of A

for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) ) holds

b_{1} = b_{2}

ex b_{1} being Subset of A st

for o being Object of A holds

( o in b_{1} iff ex s being State of A ex a being Element of Values o st Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) )

for b_{1}, b_{2} being Subset of A st ( for o being Object of A holds

( o in b_{1} iff ex s being State of A ex a being Element of Values o st Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) ) ) & ( for o being Object of A holds

( o in b_{2} iff ex s being State of A ex a being Element of Values o st Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) ) ) holds

b_{1} = b_{2}

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

let I be Instruction of A;

func Out_\_Inp I -> Subset of A means :Def4: :: AMISTD_4:def 4

for o being Object of A holds

( o in it iff for s being State of A

for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) );

existence for o being Object of A holds

( o in it iff for s being State of A

for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) );

ex b

for o being Object of A holds

( o in b

for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) )

proof end;

uniqueness for b

( o in b

for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) ) & ( for o being Object of A holds

( o in b

for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) ) holds

b

proof end;

func Out_U_Inp I -> Subset of A means :Def5: :: AMISTD_4:def 5

for o being Object of A holds

( o in it iff ex s being State of A ex a being Element of Values o st Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) );

existence for o being Object of A holds

( o in it iff ex s being State of A ex a being Element of Values o st Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) );

ex b

for o being Object of A holds

( o in b

proof end;

uniqueness for b

( o in b

( o in b

b

proof end;

:: deftheorem Def4 defines Out_\_Inp AMISTD_4:def 4 :

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A

for b_{4} being Subset of A holds

( b_{4} = Out_\_Inp I iff for o being Object of A holds

( o in b_{4} iff for s being State of A

for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) );

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A

for b

( b

( o in b

for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) );

:: deftheorem Def5 defines Out_U_Inp AMISTD_4:def 5 :

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A

for b_{4} being Subset of A holds

( b_{4} = Out_U_Inp I iff for o being Object of A holds

( o in b_{4} iff ex s being State of A ex a being Element of Values o st Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) ) );

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A

for b

( b

( o in b

definition

let N be with_zero set ;

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

let I be Instruction of A;

coherence

(Out_U_Inp I) \ (Out_\_Inp I) is Subset of A ;

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

let I be Instruction of A;

coherence

(Out_U_Inp I) \ (Out_\_Inp I) is Subset of A ;

:: deftheorem defines Input AMISTD_4:def 6 :

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A holds Input I = (Out_U_Inp I) \ (Out_\_Inp I);

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A holds Input I = (Out_U_Inp I) \ (Out_\_Inp I);

theorem Th3: :: AMISTD_4:3

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N

for I being Instruction of A holds Out_\_Inp I c= Output I

for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N

for I being Instruction of A holds Out_\_Inp I c= Output I

proof end;

theorem Th4: :: AMISTD_4:4

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A holds Output I c= Out_U_Inp I

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A holds Output I c= Out_U_Inp I

proof end;

theorem :: AMISTD_4:5

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N

for I being Instruction of A holds Out_\_Inp I = (Output I) \ (Input I)

for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N

for I being Instruction of A holds Out_\_Inp I = (Output I) \ (Input I)

proof end;

theorem :: AMISTD_4:6

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N

for I being Instruction of A holds Out_U_Inp I = (Output I) \/ (Input I)

for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N

for I being Instruction of A holds Out_U_Inp I = (Output I) \/ (Input I)

proof end;

theorem Th7: :: AMISTD_4:7

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A

for o being Object of A st Values o is trivial holds

not o in Out_U_Inp I

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A

for o being Object of A st Values o is trivial holds

not o in Out_U_Inp I

proof end;

theorem :: AMISTD_4:8

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A

for o being Object of A st Values o is trivial holds

not o in Input I

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A

for o being Object of A st Values o is trivial holds

not o in Input I

proof end;

theorem :: AMISTD_4:9

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A

for o being Object of A st Values o is trivial holds

not o in Output I

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A

for o being Object of A st Values o is trivial holds

not o in Output I

proof end;

theorem Th10: :: AMISTD_4:10

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A holds

( I is halting iff Output I is empty )

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A holds

( I is halting iff Output I is empty )

proof end;

theorem Th11: :: AMISTD_4:11

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N

for I being Instruction of A st I is halting holds

Out_\_Inp I is empty

for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N

for I being Instruction of A st I is halting holds

Out_\_Inp I is empty

proof end;

theorem Th12: :: AMISTD_4:12

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A st I is halting holds

Out_U_Inp I is empty

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A st I is halting holds

Out_U_Inp I is empty

proof end;

theorem Th13: :: AMISTD_4:13

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A st I is halting holds

Input I is empty

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A st I is halting holds

Input I is empty

proof end;

registration

let N be with_zero set ;

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

let I be halting Instruction of A;

coherence

Input I is empty by Th13;

coherence

Output I is empty by Th10;

coherence

Out_U_Inp I is empty by Th12;

end;
let A be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

let I be halting Instruction of A;

coherence

Input I is empty by Th13;

coherence

Output I is empty by Th10;

coherence

Out_U_Inp I is empty by Th12;

registration

let N be with_zero set ;

ex b_{1} being non empty with_non-empty_values AMI-Struct over N st

( b_{1} is halting & b_{1} is with_non_trivial_ObjectKinds & b_{1} is IC-Ins-separated )

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

existence ex b

( b

proof end;

registration

let N be with_zero set ;

let A be non empty with_non-empty_values IC-Ins-separated halting with_non_trivial_ObjectKinds AMI-Struct over N;

let I be halting Instruction of A;

coherence

Out_\_Inp I is empty by Th11;

end;
let A be non empty with_non-empty_values IC-Ins-separated halting with_non_trivial_ObjectKinds AMI-Struct over N;

let I be halting Instruction of A;

coherence

Out_\_Inp I is empty by Th11;

registration

let N be with_zero set ;

ex b_{1} being non empty with_non-empty_values AMI-Struct over N st

( b_{1} is with_non_trivial_Instructions & b_{1} is IC-Ins-separated )

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

existence ex b

( b

proof end;

theorem :: AMISTD_4:14

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N

for I being Instruction of A st I is sequential holds

not IC in Out_\_Inp I

for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N

for I being Instruction of A st I is sequential holds

not IC in Out_\_Inp I

proof end;

theorem :: AMISTD_4:15

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A st ex s being State of A st (Exec (I,s)) . (IC ) <> IC s holds

IC in Output I by Def3;

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A st ex s being State of A st (Exec (I,s)) . (IC ) <> IC s holds

IC in Output I by Def3;

registration

let N be with_zero set ;

existence

ex b_{1} being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st b_{1} is standard

end;
existence

ex b

proof end;

theorem :: AMISTD_4:16

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N

for I being Instruction of A st I is sequential holds

IC in Output I

for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N

for I being Instruction of A st I is sequential holds

IC in Output I

proof end;

theorem Th17: :: AMISTD_4:17

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A st ex s being State of A st (Exec (I,s)) . (IC ) <> IC s holds

IC in Out_U_Inp I

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A st ex s being State of A st (Exec (I,s)) . (IC ) <> IC s holds

IC in Out_U_Inp I

proof end;

theorem :: AMISTD_4:18

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N

for I being Instruction of A st I is sequential holds

IC in Out_U_Inp I

for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N

for I being Instruction of A st I is sequential holds

IC in Out_U_Inp I

proof end;

theorem :: AMISTD_4:19

for N being with_zero set

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A

for o being Object of A st I is jump-only & o in Output I holds

o = IC

for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for I being Instruction of A

for o being Object of A st I is jump-only & o in Output I holds

o = IC

proof end;