:: AMISTD_4 semantic presentation

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 funcs +* (o,a) ->  State of A;
coherence
 s +* (o,a) is State of A
proof
 dom s = the carrier of A by PARTFUN1:def_2;
then  s +* (o,a) = s +* (o .--> a) by FUNCT_7:def_3;
hence  s +* (o,a) is State of A ; ::_thesis: verum
end;
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))))
proof
let N be with_zero set ; ::_thesis: 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))))
let A be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; ::_thesis: 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))))
let I be Instruction of A; ::_thesis: 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))))
let s be State of A; ::_thesis: 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))))
let o be Object of A; ::_thesis: for w being Element of Values o st I is sequential & o <> IC holds
IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w))))
let w be Element of Values o; ::_thesis: ( I is sequential & o <> IC implies IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w)))) )
assume that
A1: for s being State of A holds (Exec (I,s)) . (IC ) = succ (IC s) and
A2: o <> IC ; :: according to AMISTD_1:def_8 ::_thesis: IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w))))
thus  IC (Exec (I,s)) = succ (IC s) by A1
.= succ (IC (s +* (o,w))) by A2, FUNCT_7:32
.= IC (Exec (I,(s +* (o,w)))) by A1 ; ::_thesis: verum
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))
proof
let N be with_zero set ; ::_thesis: 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))
let A be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; ::_thesis: 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))
let I be Instruction of A; ::_thesis: 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))
let s be State of A; ::_thesis: 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))
let o be Object of A; ::_thesis: 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))
let w be Element of Values o; ::_thesis: ( I is sequential & o <> IC implies IC (Exec (I,(s +* (o,w)))) = IC ((Exec (I,s)) +* (o,w)) )
assume that
A1: I is sequential and
A2: o <> IC ; ::_thesis: IC (Exec (I,(s +* (o,w)))) = IC ((Exec (I,s)) +* (o,w))
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 ; ::_thesis: verum
end;

begin

definition
let A be COM-Struct ;
attrA is with_non_trivial_Instructions  means :Def1: :: AMISTD_4:def 1
 not the InstructionsF of A is trivial ;
end;

:: 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 );

definition
let N be with_zero set ;
let A be non empty with_non-empty_values AMI-Struct over N;
attrA is with_non_trivial_ObjectKinds  means :Def2: :: AMISTD_4:def 2
 for o being Object of A holds not Values o is trivial ;
end;

:: 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 );

registration
let N be with_zero set ;
cluster STC N ->  with_non_trivial_ObjectKinds ;
coherence
 STC N is with_non_trivial_ObjectKinds
proof
let o be Object of (STC N); :: according to AMISTD_4:def_2 ::_thesis: not Values o is trivial
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;
percases o in {0} by A1;
supposeA3: o in {0} ; ::_thesis: not Values o is trivial
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  not Values o is trivial ; ::_thesis: verum
end;
end;
end;
end;

registration
let N be with_zero set ;
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 b1 being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N st
( b1 is with_explicit_jumps & b1 is IC-relocable & b1 is with_non_trivial_ObjectKinds & b1 is with_non_trivial_Instructions )
proof
take  STC N ; ::_thesis: ( STC N is with_explicit_jumps & STC N is IC-relocable & STC N is with_non_trivial_ObjectKinds & STC N is with_non_trivial_Instructions )
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  not the InstructionsF of (STC N) is trivial by A1, ZFMISC_1:def_10;
hence  ( STC N is with_explicit_jumps & STC N is IC-relocable & STC N is with_non_trivial_ObjectKinds & STC N is with_non_trivial_Instructions ) by Def1; ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
cluster STC N ->  with_non_trivial_Instructions ;
coherence
 STC N is with_non_trivial_Instructions
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  not the InstructionsF of (STC N) is trivial by A1, ZFMISC_1:def_10; :: according to AMISTD_4:def_1 ::_thesis: verum
end;
end;

registration
let N be with_zero set ;
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 b1 being non empty with_non-empty_values AMI-Struct over N st
( b1 is with_non_trivial_ObjectKinds & b1 is with_non_trivial_Instructions & b1 is IC-Ins-separated )
proof
take  STC N ; ::_thesis: ( STC N is with_non_trivial_ObjectKinds & STC N is with_non_trivial_Instructions & STC N is IC-Ins-separated )
thus  ( STC N is with_non_trivial_ObjectKinds & STC N is with_non_trivial_Instructions & STC N is IC-Ins-separated ) ; ::_thesis: verum
end;
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;
cluster Values o ->  non trivial ;
coherence
 not Values o is trivial by Def2;
end;

registration
let N be with_zero set ;
let A be with_non-empty_values with_non_trivial_Instructions AMI-Struct over N;
cluster the InstructionsF of A ->  non trivial ;
coherence
 not the InstructionsF of A is trivial by Def1;
end;

registration
let N be with_zero set ;
let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
cluster Values (IC ) ->  non trivial ;
coherence
 not Values (IC ) is trivial by MEMSTR_0:def_6;
end;

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;
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
 ex b1 being Subset of A st
for o being Object of A holds
( o in b1 iff ex s being State of A st s . o <> (Exec (I,s)) . o )
proof
defpred S1[ set ] means  ex s being State of A st s . $1 <> (Exec (I,s)) . $1;
consider X being Subset of A such that
A1: for x being set holds
( x in X iff ( x in the carrier of A & S1[x] ) ) from SUBSET_1:sch_1();
take  X ; ::_thesis: for o being Object of A holds
( o in X iff ex s being State of A st s . o <> (Exec (I,s)) . o )
thus  for o being Object of A holds
( o in X iff ex s being State of A st s . o <> (Exec (I,s)) . o ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of A st ( for o being Object of A holds
( o in b1 iff ex s being State of A st s . o <> (Exec (I,s)) . o ) ) & ( for o being Object of A holds
( o in b2 iff ex s being State of A st s . o <> (Exec (I,s)) . o ) ) holds
b1 = b2
proof
defpred S1[ set ] means  ex s being State of A st s . $1 <> (Exec (I,s)) . $1;
let a, b be Subset of A; ::_thesis: ( ( for o being Object of A holds
( o in a iff ex s being State of A st s . o <> (Exec (I,s)) . o ) ) & ( for o being Object of A holds
( o in b iff ex s being State of A st s . o <> (Exec (I,s)) . o ) ) implies a = b )
assume that
A2: for o being Object of A holds
( o in a iff S1[o] ) and
A3: for o being Object of A holds
( o in b iff S1[o] ) ; ::_thesis: a = b
thus  a = b from SUBSET_1:sch_2(A2, A3); ::_thesis: verum
end;
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 b4 being Subset of A holds
( b4 = Output I iff for o being Object of A holds
( o in b4 iff ex s being State of A st s . o <> (Exec (I,s)) . o ) );

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;
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
 ex b1 being Subset of A st
for o being Object of A holds
( o in b1 iff for s being State of A
for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) )
proof
defpred S1[ set ] means  ex l being Object of A st
( l = $1 & ( for s being State of A
for a being Element of Values l holds Exec (I,s) = Exec (I,(s +* (l,a))) ) );
consider X being Subset of A such that
A1: for x being set holds
( x in X iff ( x in the carrier of A & S1[x] ) ) from SUBSET_1:sch_1();
take  X ; ::_thesis: for o being Object of A holds
( o in X iff for s being State of A
for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) )
let l be Object of A; ::_thesis: ( l in X iff for s being State of A
for a being Element of Values l holds Exec (I,s) = Exec (I,(s +* (l,a))) )
hereby  ::_thesis: ( ( for s being State of A
for a being Element of Values l holds Exec (I,s) = Exec (I,(s +* (l,a))) ) implies l in X )
assume  l in X ; ::_thesis: for s being State of A
for a being Element of Values l holds Exec (I,s) = Exec (I,(s +* (l,a)))
then  S1[l] by A1;
hence  for s being State of A
for a being Element of Values l holds Exec (I,s) = Exec (I,(s +* (l,a))) ; ::_thesis: verum
end;
thus  ( ( for s being State of A
for a being Element of Values l holds Exec (I,s) = Exec (I,(s +* (l,a))) ) implies l in X ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of A st ( for o being Object of A holds
( o in b1 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 b2 iff for s being State of A
for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) ) holds
b1 = b2
proof
defpred S1[ Object of A] means  for s being State of A
for a being Element of Values $1 holds Exec (I,s) = Exec (I,(s +* ($1,a)));
let a, b be Subset of A; ::_thesis: ( ( for o being Object of A holds
( o in a 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 iff for s being State of A
for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) ) implies a = b )
assume that
A2: for o being Object of A holds
( o in a iff S1[o] ) and
A3: for o being Object of A holds
( o in b iff S1[o] ) ; ::_thesis: a = b
thus  a = b from SUBSET_1:sch_2(A2, A3); ::_thesis: verum
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
 ex b1 being Subset of A st
for o being Object of A holds
( o in b1 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) )
proof
defpred S1[ set ] means  ex l being Object of A st
( l = $1 & ex s being State of A ex a being Element of Values l st Exec (I,(s +* (l,a))) <> (Exec (I,s)) +* (l,a) );
consider X being Subset of A such that
A4: for x being set holds
( x in X iff ( x in the carrier of A & S1[x] ) ) from SUBSET_1:sch_1();
take  X ; ::_thesis: for o being Object of A holds
( o in X 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) )
let l be Object of A; ::_thesis: ( l in X iff ex s being State of A ex a being Element of Values l st Exec (I,(s +* (l,a))) <> (Exec (I,s)) +* (l,a) )
hereby  ::_thesis: ( ex s being State of A ex a being Element of Values l st Exec (I,(s +* (l,a))) <> (Exec (I,s)) +* (l,a) implies l in X )
assume  l in X ; ::_thesis: ex s being State of A ex a being Element of Values l st Exec (I,(s +* (l,a))) <> (Exec (I,s)) +* (l,a)
then  S1[l] by A4;
hence  ex s being State of A ex a being Element of Values l st Exec (I,(s +* (l,a))) <> (Exec (I,s)) +* (l,a) ; ::_thesis: verum
end;
thus  ( ex s being State of A ex a being Element of Values l st Exec (I,(s +* (l,a))) <> (Exec (I,s)) +* (l,a) implies l in X ) by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of A st ( for o being Object of A holds
( o in b1 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 b2 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
b1 = b2
proof
defpred S1[ Object of A] means  ex s being State of A ex a being Element of Values $1 st Exec (I,(s +* ($1,a))) <> (Exec (I,s)) +* ($1,a);
let a, b be Subset of A; ::_thesis: ( ( for o being Object of A holds
( o in a 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 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) ) ) implies a = b )
assume that
A5: for o being Object of A holds
( o in a iff S1[o] ) and
A6: for o being Object of A holds
( o in b iff S1[o] ) ; ::_thesis: a = b
thus  a = b from SUBSET_1:sch_2(A5, A6); ::_thesis: verum
end;
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 b4 being Subset of A holds
( b4 = Out_\_Inp I iff for o being Object of A holds
( o in b4 iff for s being State of A
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 b4 being Subset of A holds
( b4 = Out_U_Inp I iff for o being Object of A holds
( o in b4 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) ) );

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;
func Input I ->  Subset of A equals :: AMISTD_4:def 6
(Out_U_Inp I) \ (Out_\_Inp I);
coherence
 (Out_U_Inp I) \ (Out_\_Inp I) is Subset of A ;
end;

:: 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);

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
proof
let N be with_zero set ; ::_thesis: 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
let A be non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N; ::_thesis: for I being Instruction of A holds Out_\_Inp I c= Output I
let I be Instruction of A; ::_thesis: Out_\_Inp I c= Output I
 for o being Object of A st o in Out_\_Inp I holds
o in Output I
proof
let o be Object of A; ::_thesis: ( o in Out_\_Inp I implies o in Output I )
set s = the State of A;
set a = the Element of Values o;
consider w being set  such that
A1: w in Values o and
A2: w <> the Element of Values o by SUBSET_1:48;
reconsider w = w as Element of Values o by A1;
set t = the State of A +* (o,w);
A3: dom ( the State of A +* (o,w)) = the carrier of A by PARTFUN1:def_2;
A4: dom the State of A = the carrier of A by PARTFUN1:def_2;
assume A5: ( o in Out_\_Inp I & not o in Output I ) ; ::_thesis: contradiction
then A6: (Exec (I,(( the State of A +* (o,w)) +* (o, the Element of Values o)))) . o = (( the State of A +* (o,w)) +* (o, the Element of Values o)) . o by Def3
.= the Element of Values o by A3, FUNCT_7:31 ;
(Exec (I,( the State of A +* (o,w)))) . o = ( the State of A +* (o,w)) . o by A5, Def3
.= w by A4, FUNCT_7:31 ;
hence  contradiction by A5, A2, A6, Def4; ::_thesis: verum
end;
hence  Out_\_Inp I c= Output I by SUBSET_1:2; ::_thesis: verum
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
proof
let N be with_zero set ; ::_thesis: 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
let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for I being Instruction of A holds Output I c= Out_U_Inp I
let I be Instruction of A; ::_thesis: Output I c= Out_U_Inp I
 for o being Object of A st o in Output I holds
o in Out_U_Inp I
proof
let o be Object of A; ::_thesis: ( o in Output I implies o in Out_U_Inp I )
assume A1: ( o in Output I & not o in Out_U_Inp I ) ; ::_thesis: contradiction
 for s being State of A holds s . o = (Exec (I,s)) . o
proof
let s be State of A; ::_thesis: s . o = (Exec (I,s)) . o
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 ;
::_thesis: verum
end;
hence  contradiction by A1, Def3; ::_thesis: verum
end;
hence  Output I c= Out_U_Inp I by SUBSET_1:2; ::_thesis: verum
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)
proof
let N be with_zero set ; ::_thesis: 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)
let A be non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N; ::_thesis: for I being Instruction of A holds Out_\_Inp I = (Output I) \ (Input I)
let I be Instruction of A; ::_thesis: Out_\_Inp I = (Output I) \ (Input I)
 for o being Object of A holds
( o in Out_\_Inp I iff o in (Output I) \ (Input I) )
proof
let o be Object of A; ::_thesis: ( o in Out_\_Inp I iff o in (Output I) \ (Input I) )
hereby  ::_thesis: ( o in (Output I) \ (Input I) implies o in Out_\_Inp I )
A1: Out_\_Inp I c= Output I by Th3;
assume A2: o in Out_\_Inp I ; ::_thesis: o in (Output I) \ (Input 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; ::_thesis: verum
end;
assume A3: o in (Output I) \ (Input I) ; ::_thesis: o in Out_\_Inp I
then A4: not o in Input I by XBOOLE_0:def_5;
percases ( not o in Out_U_Inp I or o in Out_\_Inp I ) by A4, XBOOLE_0:def_5;
supposeA5: not o in Out_U_Inp I ; ::_thesis: o in Out_\_Inp I
 Output I c= Out_U_Inp I by Th4;
then  not o in Output I by A5;
hence  o in Out_\_Inp I by A3, XBOOLE_0:def_5; ::_thesis: verum
end;
suppose o in Out_\_Inp I ; ::_thesis: o in Out_\_Inp I
hence  o in Out_\_Inp I ; ::_thesis: verum
end;
end;
end;
hence  Out_\_Inp I = (Output I) \ (Input I) by SUBSET_1:3; ::_thesis: verum
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)
proof
let N be with_zero set ; ::_thesis: 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)
let A be non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N; ::_thesis: for I being Instruction of A holds Out_U_Inp I = (Output I) \/ (Input I)
let I be Instruction of A; ::_thesis: Out_U_Inp I = (Output I) \/ (Input I)
 for o being Object of A st o in Out_U_Inp I holds
o in (Output I) \/ (Input I)
proof
let o be Object of A; ::_thesis: ( o in Out_U_Inp I implies o in (Output I) \/ (Input I) )
assume A1: o in Out_U_Inp I ; ::_thesis: o in (Output I) \/ (Input I)
 ( o in Input I or o in Output I )
proof
assume A2: not o in Input I ; ::_thesis: o in Output I
percases ( not o in Out_U_Inp I or o in Out_\_Inp I ) by A2, XBOOLE_0:def_5;
suppose not o in Out_U_Inp I ; ::_thesis: o in Output I
hence  o in Output I by A1; ::_thesis: verum
end;
supposeA3: o in Out_\_Inp I ; ::_thesis: o in Output I
 Out_\_Inp I c= Output I by Th3;
hence  o in Output I by A3; ::_thesis: verum
end;
end;
end;
hence  o in (Output I) \/ (Input I) by XBOOLE_0:def_3; ::_thesis: verum
end;
hence  Out_U_Inp I c= (Output I) \/ (Input I) by SUBSET_1:2; :: according to XBOOLE_0:def_10 ::_thesis: (Output I) \/ (Input I) c= Out_U_Inp I
 ( Output I c= Out_U_Inp I & Input I c= Out_U_Inp I ) by Th4, XBOOLE_1:36;
hence  (Output I) \/ (Input I) c= Out_U_Inp I by XBOOLE_1:8; ::_thesis: verum
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
proof
let N be with_zero set ; ::_thesis: 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
let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: 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
let I be Instruction of A; ::_thesis: for o being Object of A st Values o is trivial holds
not o in Out_U_Inp I
let o be Object of A; ::_thesis: ( Values o is trivial implies not o in Out_U_Inp I )
assume A1: Values o is trivial ; ::_thesis: not o in Out_U_Inp I
assume  o in Out_U_Inp I ; ::_thesis: contradiction
then consider s being State of A, a being 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 being set st x in the carrier of A holds
((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x
proof
let x be set ; ::_thesis: ( x in the carrier of A implies ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x )
assume  x in the carrier of A ; ::_thesis: ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x
percases ( x = o or x <> o ) ;
supposeA6: x = o ; ::_thesis: ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x
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 ; ::_thesis: verum
end;
suppose x <> o ; ::_thesis: ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x
hence  ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x by FUNCT_7:32; ::_thesis: verum
end;
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; ::_thesis: verum
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
proof
let N be with_zero set ; ::_thesis: 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
let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for I being Instruction of A
for o being Object of A st Values o is trivial holds
not o in Input I
let I be Instruction of A; ::_thesis: for o being Object of A st Values o is trivial holds
not o in Input I
let o be Object of A; ::_thesis: ( Values o is trivial implies not o in Input I )
A1: Input I c= Out_U_Inp I by XBOOLE_1:36;
assume  Values o is trivial ; ::_thesis: not o in Input I
hence  not o in Input I by A1, Th7; ::_thesis: verum
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
proof
let N be with_zero set ; ::_thesis: 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
let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for I being Instruction of A
for o being Object of A st Values o is trivial holds
not o in Output I
let I be Instruction of A; ::_thesis: for o being Object of A st Values o is trivial holds
not o in Output I
let o be Object of A; ::_thesis: ( Values o is trivial implies not o in Output I )
assume A1: Values o is trivial ; ::_thesis: not o in Output I
 Output I c= Out_U_Inp I by Th4;
hence  not o in Output I by A1, Th7; ::_thesis: verum
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 )
proof
let N be with_zero set ; ::_thesis: 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 )
let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for I being Instruction of A holds
( I is halting iff Output I is empty )
let I be Instruction of A; ::_thesis: ( I is halting iff Output I is empty )
thus  ( I is halting implies Output I is empty ) ::_thesis: ( Output I is empty implies I is halting )
proof
assume A1: for s being State of A holds Exec (I,s) = s ; :: according to EXTPRO_1:def_3 ::_thesis: Output I is empty
assume  not Output I is empty ; ::_thesis: contradiction
then consider o being Object of A such that
A2: o in Output I by SUBSET_1:4;
 ex s being State of A st s . o <> (Exec (I,s)) . o by A2, Def3;
hence  contradiction by A1; ::_thesis: verum
end;
assume A3: Output I is empty ; ::_thesis: I is halting
let s be State of A; :: according to EXTPRO_1:def_3 ::_thesis: Exec (I,s) = s
assume A4: Exec (I,s) <> s ; ::_thesis: contradiction
 ( dom s = the carrier of A & dom (Exec (I,s)) = the carrier of A ) by PARTFUN1:def_2;
then  ex x being set st
( x in the carrier of A & (Exec (I,s)) . x <> s . x ) by A4, FUNCT_1:2;
hence  contradiction by A3, Def3; ::_thesis: verum
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
proof
let N be with_zero set ; ::_thesis: 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
let A be non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N; ::_thesis: for I being Instruction of A st I is halting holds
Out_\_Inp I is empty
let I be Instruction of A; ::_thesis: ( I is halting implies Out_\_Inp I is empty )
assume A1: I is halting ; ::_thesis: Out_\_Inp I is empty
 Out_\_Inp I c= Output I by Th3;
then  Out_\_Inp I c= {} by A1, Th10;
hence  Out_\_Inp I is empty by XBOOLE_1:3; ::_thesis: verum
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
proof
let N be with_zero set ; ::_thesis: 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
let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for I being Instruction of A st I is halting holds
Out_U_Inp I is empty
let I be Instruction of A; ::_thesis: ( I is halting implies Out_U_Inp I is empty )
assume A1: for s being State of A holds Exec (I,s) = s ; :: according to EXTPRO_1:def_3 ::_thesis: Out_U_Inp I is empty
assume  not Out_U_Inp I is empty ; ::_thesis: contradiction
then consider o being Object of A such that
A2: o in Out_U_Inp I by SUBSET_1:4;
consider s being State of A, a being 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  contradiction by A3; ::_thesis: verum
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
proof
let N be with_zero set ; ::_thesis: 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
let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for I being Instruction of A st I is halting holds
Input I is empty
let I be Instruction of A; ::_thesis: ( I is halting implies Input I is empty )
assume  I is halting ; ::_thesis: Input I is empty
then  Input I = {} \ (Out_\_Inp I) by Th12
.= {} ;
hence  Input I is empty ; ::_thesis: verum
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;
cluster Input I ->  empty ;
coherence
 Input I is empty by Th13;
cluster Output I ->  empty ;
coherence
 Output I is empty by Th10;
cluster Out_U_Inp I ->  empty ;
coherence
 Out_U_Inp I is empty by Th12;
end;

registration
let N be with_zero set ;
cluster non empty with_non-empty_values IC-Ins-separated halting with_non_trivial_ObjectKinds for AMI-Struct over N;
existence
 ex b1 being non empty with_non-empty_values AMI-Struct over N st
( b1 is halting & b1 is with_non_trivial_ObjectKinds & b1 is IC-Ins-separated )
proof
take  STC N ; ::_thesis: ( STC N is halting & STC N is with_non_trivial_ObjectKinds & STC N is IC-Ins-separated )
thus  ( STC N is halting & STC N is with_non_trivial_ObjectKinds & STC N is IC-Ins-separated ) ; ::_thesis: verum
end;
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;
cluster Out_\_Inp I ->  empty ;
coherence
 Out_\_Inp I is empty by Th11;
end;

registration
let N be with_zero set ;
cluster non empty with_non-empty_values IC-Ins-separated with_non_trivial_Instructions for AMI-Struct over N;
existence
 ex b1 being non empty with_non-empty_values AMI-Struct over N st
( b1 is with_non_trivial_Instructions & b1 is IC-Ins-separated )
proof
take  STC N ; ::_thesis: ( STC N is with_non_trivial_Instructions & STC N is IC-Ins-separated )
thus  ( STC N is with_non_trivial_Instructions & STC N is IC-Ins-separated ) ; ::_thesis: verum
end;
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
proof
let N be with_zero set ; ::_thesis: 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
let A be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; ::_thesis: for I being Instruction of A st I is sequential holds
not IC in Out_\_Inp I
let I be Instruction of A; ::_thesis: ( I is sequential implies not IC in Out_\_Inp I )
set t = the State of A;
set l = IC ;
reconsider sICt = succ (IC the State of A) as Element of NAT by ORDINAL1:def_12;
reconsider w = sICt as Element of Values (IC ) by MEMSTR_0:def_6;
set s = the State of A +* ((IC ),w);
assume  for s being State of A holds (Exec (I,s)) . (IC ) = succ (IC s) ; :: according to AMISTD_1:def_8 ::_thesis: not IC in Out_\_Inp I
then A1: ( (Exec (I, the State of A)) . (IC ) = succ (IC the State of A) & (Exec (I,( the State of A +* ((IC ),w)))) . (IC ) = succ (IC ( the State of A +* ((IC ),w))) ) ;
 dom the State of A = the carrier of A by PARTFUN1:def_2;
then  Exec (I, the State of A) <> Exec (I,( the State of A +* ((IC ),w))) by A1, FUNCT_7:31, ORDINAL1:9;
hence  not IC in Out_\_Inp I by Def4; ::_thesis: verum
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;

registration
let N be with_zero set ;
cluster non empty with_non-empty_values IC-Ins-separated standard for AMI-Struct over N;
existence
 ex b1 being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st b1 is standard
proof
take  STC N ; ::_thesis: STC N is standard
thus  STC N is standard ; ::_thesis: verum
end;
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
proof
let N be with_zero set ; ::_thesis: 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
let A be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; ::_thesis: for I being Instruction of A st I is sequential holds
IC in Output I
let I be Instruction of A; ::_thesis: ( I is sequential implies IC in Output I )
assume A1: for s being State of A holds (Exec (I,s)) . (IC ) = succ (IC s) ; :: according to AMISTD_1:def_8 ::_thesis: IC in Output I
set s = the State of A;
 (Exec (I, the State of A)) . (IC ) = succ (IC the State of A) by A1;
then  (Exec (I, the State of A)) . (IC ) <> IC the State of A by ORDINAL1:9;
hence  IC in Output I by Def3; ::_thesis: verum
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
proof
let N be with_zero set ; ::_thesis: 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
let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: 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
let I be Instruction of A; ::_thesis: ( ex s being State of A st (Exec (I,s)) . (IC ) <> IC s implies IC in Out_U_Inp I )
assume  ex s being State of A st (Exec (I,s)) . (IC ) <> IC s ; ::_thesis: IC in Out_U_Inp I
then A1: IC in Output I by Def3;
 Output I c= Out_U_Inp I by Th4;
hence  IC in Out_U_Inp I by A1; ::_thesis: verum
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
proof
let N be with_zero set ; ::_thesis: 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
let A be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; ::_thesis: for I being Instruction of A st I is sequential holds
IC in Out_U_Inp I
let I be Instruction of A; ::_thesis: ( I is sequential implies IC in Out_U_Inp I )
set s = the State of A;
assume  for s being State of A holds (Exec (I,s)) . (IC ) = succ (IC s) ; :: according to AMISTD_1:def_8 ::_thesis: IC in Out_U_Inp I
then  (Exec (I, the State of A)) . (IC ) = succ (IC the State of A) ;
then  (Exec (I, the State of A)) . (IC ) <> IC the State of A by ORDINAL1:9;
hence  IC in Out_U_Inp I by Th17; ::_thesis: verum
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
proof
let N be with_zero set ; ::_thesis: 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
let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; ::_thesis: for I being Instruction of A
for o being Object of A st I is jump-only & o in Output I holds
o = IC
let I be Instruction of A; ::_thesis: for o being Object of A st I is jump-only & o in Output I holds
o = IC
let o be Object of A; ::_thesis: ( I is jump-only & o in Output I implies o = IC )
assume A1: for s being State of A
for o being Object of A
for J being Instruction of A st InsCode I = InsCode J & o in Data-Locations holds
(Exec (J,s)) . o = s . o ; :: according to AMISTD_1:def_1,AMISTD_1:def_2 ::_thesis: ( not o in Output I or o = IC )
assume  o in Output I ; ::_thesis: o = IC
then  ex s being State of A st s . o <> (Exec (I,s)) . o by Def3;
then A2: not o in Data-Locations by A1;
 o in the carrier of A ;
then  o in {(IC )} \/ (Data-Locations ) by STRUCT_0:4;
then  o in {(IC )} by A2, XBOOLE_0:def_3;
hence  o = IC by TARSKI:def_1; ::_thesis: verum
end;