:: AMI_7 semantic presentation

theorem E1: :: AMI_7:1
for b1, b2, b3 being set holds
( ( ) implies ( not b1 <> b2 or not b1 <> b3 or {b1,b2,b3} \ {b1} = {b2,b3} ) )
proof
let c1, c2, c3 be set ;
assume E2: ( c1 <> c2 & c1 <> c3 ) ;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10
let c4 be set ;
assume c4 in {c1,c2,c3} \ {c1} ;
then ( c4 in {c1,c2,c3} & not c4 in {c1} ) by XBOOLE_0:def 4;
then ( not ( not c4 = c1 & not c4 = c2 & not c4 = c3 ) & c4 <> c1 ) by ENUMSET1:def 1, TARSKI:def 1;
hence c4 in {c2,c3} by TARSKI:def 2;
end;
let c4 be set ; :: according to TARSKI:def 3
assume c4 in {c2,c3} ;
then ( c4 = c2 or c4 = c3 ) by TARSKI:def 2;
then ( c4 in {c1,c2,c3} & not c4 in {c1} ) by E2, ENUMSET1:def 1, TARSKI:def 1;
hence c4 in {c1,c2,c3} \ {c1} by XBOOLE_0:def 4;
end;

theorem E2: :: AMI_7:2
for b1 being with_non-empty_elements set
for b2 being non empty non void AMI-Struct of b1
for b3 being State of b2
for b4 being Object of b2 holds b3 . b4 in ObjectKind b4
proof
let c1 be with_non-empty_elements set ;
let c2 be non empty non void AMI-Struct of c1;
let c3 be State of c2;
let c4 be Object of c2;
dom the Object-Kind of c2 = the carrier of c2 by FUNCT_2:def 1;
hence c3 . c4 in ObjectKind c4 by CARD_3:18;
end;

theorem :: AMI_7:3
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite realistic AMI-Struct of b1
for b3 being State of b2
for b4 being Instruction-Location of b2
for b5 being Element of ObjectKind (IC b2) holds (b3 +* (IC b2),b5) . b4 = b3 . b4
proof
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite realistic AMI-Struct of c1;
let c3 be State of c2;
let c4 be Instruction-Location of c2;
let c5 be Element of ObjectKind (IC c2);
c4 <> IC c2 by AMI_1:48;
hence (c3 +* (IC c2),c5) . c4 = c3 . c4 by FUNCT_7:34;
end;

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite AMI-Struct of c1;
let c3 be State of c2;
let c4 be Object of c2;
let c5 be Element of ObjectKind c4;
redefine func +* as c3 +* c4,c5 -> State of a2;
coherence
c3 +* c4,c5 is State of c2
proof
dom c3 = the carrier of c2 by AMI_3:36;
then c3 +* c4,c5 = c3 +* (c4 .--> c5) by FUNCT_7:def 3;
hence c3 +* c4,c5 is State of c2 ;
end;
end;

theorem E3: :: AMI_7:4
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of b1
for b3 being State of b2
for b4 being Object of b2
for b5 being Instruction-Location of b2
for b6 being Instruction of b2
for b7 being Element of ObjectKind b4 holds
( b5 <> b4 implies (Exec b6,b3) . b5 = (Exec b6,(b3 +* b4,b7)) . b5 )
proof
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated steady-programmed definite AMI-Struct of c1;
let c3 be State of c2;
let c4 be Object of c2;
let c5 be Instruction-Location of c2;
let c6 be Instruction of c2;
let c7 be Element of ObjectKind c4;
assume E4: c5 <> c4 ;
thus (Exec c6,c3) . c5 = c3 . c5 by AMI_1:def 13
.= (c3 +* c4,c7) . c5 by E4, FUNCT_7:34
.= (Exec c6,(c3 +* c4,c7)) . c5 by AMI_1:def 13 ;
end;

theorem E4: :: AMI_7:5
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being State of b2
for b4 being Object of b2
for b5 being Element of ObjectKind b4 holds
( b4 <> IC b2 implies IC b3 = IC (b3 +* b4,b5) ) by FUNCT_7:34;

theorem E5: :: AMI_7:6
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being Instruction of b2
for b4 being State of b2
for b5 being Object of b2
for b6 being Element of ObjectKind b5 holds
( ( b3 is sequential ) implies ( not b5 <> IC b2 or IC (Exec b3,b4) = IC (Exec b3,(b4 +* b5,b6)) ) )
proof
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite standard AMI-Struct of c1;
let c3 be Instruction of c2;
let c4 be State of c2;
let c5 be Object of c2;
let c6 be Element of ObjectKind c5;
assume that
E6: for b1 being State of c2 holds (Exec c3,b1) . (IC c2) = NextLoc (IC b1) and
E7: c5 <> IC c2 ; :: according to AMISTD_1:def 16
thus IC (Exec c3,c4) = (Exec c3,c4) . (IC c2)
.= NextLoc (IC c4) by E6
.= NextLoc (IC (c4 +* c5,c6)) by E7, E4
.= (Exec c3,(c4 +* c5,c6)) . (IC c2) by E6
.= IC (Exec c3,(c4 +* c5,c6)) ;
end;

theorem E6: :: AMI_7:7
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being Instruction of b2
for b4 being State of b2
for b5 being Object of b2
for b6 being Element of ObjectKind b5 holds
( ( b3 is sequential ) implies ( not b5 <> IC b2 or IC (Exec b3,(b4 +* b5,b6)) = IC ((Exec b3,b4) +* b5,b6) ) )
proof
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite standard AMI-Struct of c1;
let c3 be Instruction of c2;
let c4 be State of c2;
let c5 be Object of c2;
let c6 be Element of ObjectKind c5;
assume that
E7: c3 is sequential and
E8: c5 <> IC c2 ;
thus IC (Exec c3,(c4 +* c5,c6)) = IC (Exec c3,c4) by E7, E8, E5
.= (Exec c3,c4) . (IC c2)
.= ((Exec c3,c4) +* c5,c6) . (IC c2) by E8, FUNCT_7:34
.= IC ((Exec c3,c4) +* c5,c6) ;
end;

theorem E7: :: AMI_7:8
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated steady-programmed definite standard AMI-Struct of b1
for b3 being Instruction of b2
for b4 being State of b2
for b5 being Object of b2
for b6 being Element of ObjectKind b5
for b7 being Instruction-Location of b2 holds (Exec b3,(b4 +* b5,b6)) . b7 = ((Exec b3,b4) +* b5,b6) . b7
proof
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated steady-programmed definite standard AMI-Struct of c1;
let c3 be Instruction of c2;
let c4 be State of c2;
let c5 be Object of c2;
let c6 be Element of ObjectKind c5;
let c7 be Instruction-Location of c2;
E8: (Exec c3,(c4 +* c5,c6)) . c7 = (c4 +* c5,c6) . c7 by AMI_1:def 13;
E9: dom c4 = the carrier of c2 by AMI_3:36;
E10: dom (Exec c3,c4) = the carrier of c2 by AMI_3:36;
per cases not ( not c7 = c5 & not c7 <> c5 ) ;
suppose E11: c7 = c5 ;
hence (Exec c3,(c4 +* c5,c6)) . c7 = c6 by E8, E9, FUNCT_7:33
.= ((Exec c3,c4) +* c5,c6) . c7 by E10, E11, FUNCT_7:33 ;

end;
suppose E11: c7 <> c5 ;
hence (Exec c3,(c4 +* c5,c6)) . c7 = c4 . c7 by E8, FUNCT_7:34
.= (Exec c3,c4) . c7 by AMI_1:def 13
.= ((Exec c3,c4) +* c5,c6) . c7 by E11, FUNCT_7:34 ;

end;
end;
end;

definition
let c1 be set ;
let c2 be AMI-Struct of c1;
attr a2 is with_non_trivial_Instructions means :E8: :: AMI_7:def 1
not the Instructions of a2 is trivial;
end;

:: deftheorem E8 defines with_non_trivial_Instructions AMI_7:def 1 :
for b1 being set
for b2 being AMI-Struct of b1 holds
( b2 is with_non_trivial_Instructions iff not the Instructions of b2 is trivial );

definition
let c1 be set ;
let c2 be non empty AMI-Struct of c1;
attr a2 is with_non_trivial_ObjectKinds means :E9: :: AMI_7:def 2
for b1 being Object of a2 holds
not ObjectKind b1 is trivial;
end;

:: deftheorem E9 defines with_non_trivial_ObjectKinds AMI_7:def 2 :
for b1 being set
for b2 being non empty AMI-Struct of b1 holds
( b2 is with_non_trivial_ObjectKinds iff for b3 being Object of b2 holds
not ObjectKind b3 is trivial );

registration
let c1 be with_non-empty_elements set ;
cluster STC a1 -> with_non_trivial_ObjectKinds ;
coherence
STC c1 is with_non_trivial_ObjectKinds
proof
let c2 be Object of (STC c1); :: according to AMI_7:def 2
E10: the carrier of (STC c1) = NAT \/ {NAT } by AMISTD_1:def 11;
E11: the Object-Kind of (STC c1) = (NAT --> {[1,0],[0,0]}) +* (NAT .--> NAT ) by AMISTD_1:def 11;
E12: dom (NAT .--> NAT ) = {NAT } by FUNCOP_1:19;
per cases ( c2 in NAT or c2 in {NAT } ) by E10, XBOOLE_0:def 2;
suppose E13: c2 in NAT ;
then c2 <> NAT ;
then not c2 in dom (NAT .--> NAT ) by E12, TARSKI:def 1;
then E14: ObjectKind c2 = (NAT --> {[1,0],[0,0]}) . c2 by E11, FUNCT_4:12
.= {[1,0],[0,0]} by E13, FUNCOP_1:13 ;
E15: [1,0] <> [0,0] by ZFMISC_1:33;
( [1,0] in {[1,0],[0,0]} & [0,0] in {[1,0],[0,0]} ) by TARSKI:def 2;
hence not ObjectKind c2 is trivial by E14, E15, YELLOW_8:def 1;
end;
suppose E13: c2 in {NAT } ;
then ObjectKind c2 = (NAT .--> NAT ) . c2 by E11, E12, FUNCT_4:14
.= NAT by E13, FUNCOP_1:13 ;
hence not ObjectKind c2 is trivial ;
end;
end;
end;
end;

registration
let c1 be with_non-empty_elements set ;
cluster non empty non void halting IC-Ins-separated steady-programmed definite realistic programmable standard with_explicit_jumps without_implicit_jumps regular IC-good Exec-preserving with_non_trivial_Instructions with_non_trivial_ObjectKinds AMI-Struct of a1;
existence
ex b1 being non empty non void IC-Ins-separated definite standard regular AMI-Struct of c1 st
( b1 is halting & b1 is realistic & b1 is steady-programmed & b1 is programmable & b1 is with_explicit_jumps & b1 is without_implicit_jumps & b1 is IC-good & b1 is Exec-preserving & b1 is with_non_trivial_ObjectKinds & b1 is with_non_trivial_Instructions )
proof
take STC c1 ;
STC c1 is with_non_trivial_Instructions
proof
E10: the Instructions of (STC c1) = {[0,0],[1,0]} by AMISTD_1:def 11;
E11: [1,0] <> [0,0] by ZFMISC_1:33;
( [1,0] in {[1,0],[0,0]} & [0,0] in {[1,0],[0,0]} ) by TARSKI:def 2;
hence not the Instructions of (STC c1) is trivial by E10, E11, YELLOW_8:def 1; :: according to AMI_7:def 1
end;
hence ( STC c1 is halting & STC c1 is realistic & STC c1 is steady-programmed & STC c1 is programmable & STC c1 is with_explicit_jumps & STC c1 is without_implicit_jumps & STC c1 is IC-good & STC c1 is Exec-preserving & STC c1 is with_non_trivial_ObjectKinds & STC c1 is with_non_trivial_Instructions ) ;
end;
end;

registration
let c1 be with_non-empty_elements set ;
cluster non empty non void definite with_non_trivial_ObjectKinds -> non empty non void definite with_non_trivial_Instructions AMI-Struct of a1;
coherence
for b1 being non empty non void definite AMI-Struct of c1 holds
( b1 is with_non_trivial_ObjectKinds implies b1 is with_non_trivial_Instructions )
proof
let c2 be non empty non void definite AMI-Struct of c1;
assume E10: for b1 being Object of c2 holds
not ObjectKind b1 is trivial ; :: according to AMI_7:def 2
consider c3 being Instruction-Location of c2;
ObjectKind c3 = the Instructions of c2 by AMI_1:def 14;
hence not the Instructions of c2 is trivial by E10; :: according to AMI_7:def 1
end;
end;

registration
let c1 be with_non-empty_elements set ;
cluster non empty IC-Ins-separated with_non_trivial_ObjectKinds -> non empty IC-Ins-separated with-non-trivial-Instruction-Locations AMI-Struct of a1;
coherence
for b1 being non empty IC-Ins-separated AMI-Struct of c1 holds
( b1 is with_non_trivial_ObjectKinds implies b1 is with-non-trivial-Instruction-Locations )
proof
let c2 be non empty IC-Ins-separated AMI-Struct of c1;
assume E10: for b1 being Object of c2 holds
not ObjectKind b1 is trivial ; :: according to AMI_7:def 2
ObjectKind (IC c2) = the Instruction-Locations of c2 by AMI_1:def 11;
hence not the Instruction-Locations of c2 is trivial by E10; :: according to AMISTD_2:def 10
end;
end;

registration
let c1 be with_non-empty_elements set ;
let c2 be non empty with_non_trivial_ObjectKinds AMI-Struct of c1;
let c3 be Object of c2;
cluster ObjectKind a3 -> non trivial ;
coherence
not ObjectKind c3 is trivial by E9;
end;

registration
let c1 be with_non-empty_elements set ;
let c2 be with_non_trivial_Instructions AMI-Struct of c1;
cluster the Instructions of a2 -> non trivial ;
coherence
not the Instructions of c2 is trivial by E8;
end;

registration
let c1 be with_non-empty_elements set ;
let c2 be non empty IC-Ins-separated with-non-trivial-Instruction-Locations AMI-Struct of c1;
cluster ObjectKind (IC a2) -> non trivial ;
coherence
not ObjectKind (IC c2) is trivial by AMI_1:def 11;
end;

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void AMI-Struct of c1;
let c3 be Instruction of c2;
func Output c3 -> Subset of a2 means :E10: :: AMI_7:def 3
for b1 being Object of a2 holds
( b1 in a4 iff not for b2 being State of a2 holds not b2 . b1 <> (Exec a3,b2) . b1 );
existence
ex b1 being Subset of c2 st
for b2 being Object of c2 holds
( b2 in b1 iff not for b3 being State of c2 holds not b3 . b2 <> (Exec c3,b3) . b2 )
proof
defpred S1[ set ] means not for b1 being State of c2 holds not b1 . a1 <> (Exec c3,b1) . a1;
consider c4 being Subset of c2 such that
E10: for b1 being set holds
( b1 in c4 iff ( b1 in the carrier of c2 & S1[b1] ) ) from SUBSET_1:sch 1();
 take c4 ;
thus for b1 being Object of c2 holds
( b1 in c4 iff not for b2 being State of c2 holds not b2 . b1 <> (Exec c3,b2) . b1 ) by E10;
end;
uniqueness
for b1, b2 being Subset of c2 holds
( ( ( for b3 being Object of c2 holds
( b3 in b1 iff not for b4 being State of c2 holds not b4 . b3 <> (Exec c3,b4) . b3 ) ) & ( for b3 being Object of c2 holds
( b3 in b2 iff not for b4 being State of c2 holds not b4 . b3 <> (Exec c3,b4) . b3 ) ) ) implies ( b1 = b2 ) )
proof
defpred S1[ set ] means not for b1 being State of c2 holds not b1 . a1 <> (Exec c3,b1) . a1;
thus for b1, b2 being Subset of c2 holds
( ( ( for b3 being Object of c2 holds
( b3 in b1 iff S1[b3] ) ) & ( for b3 being Object of c2 holds
( b3 in b2 iff S1[b3] ) ) ) implies ( b1 = b2 ) ) from SUBSET_1:sch 2();
end;
end;

:: deftheorem E10 defines Output AMI_7:def 3 :
for b1 being with_non-empty_elements set
for b2 being non empty non void AMI-Struct of b1
for b3 being Instruction of b2
for b4 being Subset of b2 holds
( b4 = Output b3 iff for b5 being Object of b2 holds
( b5 in b4 iff not for b6 being State of b2 holds not b6 . b5 <> (Exec b3,b6) . b5 ) );

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite AMI-Struct of c1;
let c3 be Instruction of c2;
func Out_\_Inp c3 -> Subset of a2 means :E11: :: AMI_7:def 4
for b1 being Object of a2 holds
( b1 in a4 iff for b2 being State of a2
for b3 being Element of ObjectKind b1 holds Exec a3,b2 = Exec a3,(b2 +* b1,b3) );
existence
ex b1 being Subset of c2 st
for b2 being Object of c2 holds
( b2 in b1 iff for b3 being State of c2
for b4 being Element of ObjectKind b2 holds Exec c3,b3 = Exec c3,(b3 +* b2,b4) )
proof
defpred S1[ set ] means ex b1 being Object of c2 st
( b1 = a1 & ( for b2 being State of c2
for b3 being Element of ObjectKind b1 holds Exec c3,b2 = Exec c3,(b2 +* b1,b3) ) );
consider c4 being Subset of c2 such that
E11: for b1 being set holds
( b1 in c4 iff ( b1 in the carrier of c2 & S1[b1] ) ) from SUBSET_1:sch 1();
 take c4 ;
let c5 be Object of c2;
hereby
assume c5 in c4 ;
then S1[c5] by E11;
hence for b1 being State of c2
for b2 being Element of ObjectKind c5 holds Exec c3,b1 = Exec c3,(b1 +* c5,b2) ;
end;
thus ( ( for b1 being State of c2
for b2 being Element of ObjectKind c5 holds Exec c3,b1 = Exec c3,(b1 +* c5,b2) ) implies c5 in c4 ) by E11;
end;
uniqueness
for b1, b2 being Subset of c2 holds
( ( ( for b3 being Object of c2 holds
( b3 in b1 iff for b4 being State of c2
for b5 being Element of ObjectKind b3 holds Exec c3,b4 = Exec c3,(b4 +* b3,b5) ) ) & ( for b3 being Object of c2 holds
( b3 in b2 iff for b4 being State of c2
for b5 being Element of ObjectKind b3 holds Exec c3,b4 = Exec c3,(b4 +* b3,b5) ) ) ) implies ( b1 = b2 ) )
proof
defpred S1[ Object of c2] means for b1 being State of c2
for b2 being Element of ObjectKind a1 holds Exec c3,b1 = Exec c3,(b1 +* a1,b2);
thus for b1, b2 being Subset of c2 holds
( ( ( for b3 being Object of c2 holds
( b3 in b1 iff S1[b3] ) ) & ( for b3 being Object of c2 holds
( b3 in b2 iff S1[b3] ) ) ) implies ( b1 = b2 ) ) from SUBSET_1:sch 2();
end;
func Out_U_Inp c3 -> Subset of a2 means :E12: :: AMI_7:def 5
for b1 being Object of a2 holds
( b1 in a4 iff not for b2 being State of a2
for b3 being Element of ObjectKind b1 holds not Exec a3,(b2 +* b1,b3) <> (Exec a3,b2) +* b1,b3 );
existence
ex b1 being Subset of c2 st
for b2 being Object of c2 holds
( b2 in b1 iff not for b3 being State of c2
for b4 being Element of ObjectKind b2 holds not Exec c3,(b3 +* b2,b4) <> (Exec c3,b3) +* b2,b4 )
proof
defpred S1[ set ] means ex b1 being Object of c2 st
( b1 = a1 & not for b2 being State of c2
for b3 being Element of ObjectKind b1 holds not Exec c3,(b2 +* b1,b3) <> (Exec c3,b2) +* b1,b3 );
consider c4 being Subset of c2 such that
E11: for b1 being set holds
( b1 in c4 iff ( b1 in the carrier of c2 & S1[b1] ) ) from SUBSET_1:sch 1();
 take c4 ;
let c5 be Object of c2;
hereby
assume c5 in c4 ;
then S1[c5] by E11;
hence not for b1 being State of c2
for b2 being Element of ObjectKind c5 holds not Exec c3,(b1 +* c5,b2) <> (Exec c3,b1) +* c5,b2 ;
end;
thus ( not for b1 being State of c2
for b2 being Element of ObjectKind c5 holds not Exec c3,(b1 +* c5,b2) <> (Exec c3,b1) +* c5,b2 implies c5 in c4 ) by E11;
end;
uniqueness
for b1, b2 being Subset of c2 holds
( ( ( for b3 being Object of c2 holds
( b3 in b1 iff not for b4 being State of c2
for b5 being Element of ObjectKind b3 holds not Exec c3,(b4 +* b3,b5) <> (Exec c3,b4) +* b3,b5 ) ) & ( for b3 being Object of c2 holds
( b3 in b2 iff not for b4 being State of c2
for b5 being Element of ObjectKind b3 holds not Exec c3,(b4 +* b3,b5) <> (Exec c3,b4) +* b3,b5 ) ) ) implies ( b1 = b2 ) )
proof
defpred S1[ Object of c2] means not for b1 being State of c2
for b2 being Element of ObjectKind a1 holds not Exec c3,(b1 +* a1,b2) <> (Exec c3,b1) +* a1,b2;
thus for b1, b2 being Subset of c2 holds
( ( ( for b3 being Object of c2 holds
( b3 in b1 iff S1[b3] ) ) & ( for b3 being Object of c2 holds
( b3 in b2 iff S1[b3] ) ) ) implies ( b1 = b2 ) ) from SUBSET_1:sch 2();
end;
end;

:: deftheorem E11 defines Out_\_Inp AMI_7:def 4 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being Instruction of b2
for b4 being Subset of b2 holds
( b4 = Out_\_Inp b3 iff for b5 being Object of b2 holds
( b5 in b4 iff for b6 being State of b2
for b7 being Element of ObjectKind b5 holds Exec b3,b6 = Exec b3,(b6 +* b5,b7) ) );

:: deftheorem E12 defines Out_U_Inp AMI_7:def 5 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being Instruction of b2
for b4 being Subset of b2 holds
( b4 = Out_U_Inp b3 iff for b5 being Object of b2 holds
( b5 in b4 iff not for b6 being State of b2
for b7 being Element of ObjectKind b5 holds not Exec b3,(b6 +* b5,b7) <> (Exec b3,b6) +* b5,b7 ) );

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite AMI-Struct of c1;
let c3 be Instruction of c2;
func Input c3 -> Subset of a2 equals :: AMI_7:def 6
(Out_U_Inp a3) \ (Out_\_Inp a3);
coherence
(Out_U_Inp c3) \ (Out_\_Inp c3) is Subset of c2 ;
end;

:: deftheorem defines Input AMI_7:def 6 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being Instruction of b2 holds Input b3 = (Out_U_Inp b3) \ (Out_\_Inp b3);

theorem E13: :: AMI_7:9
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being Instruction of b2 holds Out_\_Inp b3 misses Input b3 by XBOOLE_1:85;

theorem E14: :: AMI_7:10
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of b1
for b3 being Instruction of b2 holds Out_\_Inp b3 c= Output b3
proof
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of c1;
let c3 be Instruction of c2;
for b1 being Object of c2 holds
( b1 in Out_\_Inp c3 implies b1 in Output c3 )
proof
let c4 be Object of c2;
assume E15: ( c4 in Out_\_Inp c3 & not c4 in Output c3 ) ;
consider c5 being State of c2, c6 being Element of ObjectKind c4;
consider c7 being set such that
E16: ( c7 in ObjectKind c4 & c7 <> c6 ) by YELLOW15:4;
reconsider c8 = c7 as Element of ObjectKind c4 by E16;
set c9 = c5 +* c4,c8;
E17: dom c5 = the carrier of c2 by AMI_3:36;
E18: dom (c5 +* c4,c8) = the carrier of c2 by AMI_3:36;
E19: (Exec c3,(c5 +* c4,c8)) . c4 = (c5 +* c4,c8) . c4 by E15, E10
.= c8 by E17, FUNCT_7:33 ;
(Exec c3,((c5 +* c4,c8) +* c4,c6)) . c4 = ((c5 +* c4,c8) +* c4,c6) . c4 by E15, E10
.= c6 by E18, FUNCT_7:33 ;
hence not verum by E15, E16, E19, E11;
end;
hence Out_\_Inp c3 c= Output c3 by SUBSET_1:7;
end;

theorem E15: :: AMI_7:11
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being Instruction of b2 holds Output b3 c= Out_U_Inp b3
proof
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite AMI-Struct of c1;
let c3 be Instruction of c2;
for b1 being Object of c2 holds
( b1 in Output c3 implies b1 in Out_U_Inp c3 )
proof
let c4 be Object of c2;
assume E16: ( c4 in Output c3 & not c4 in Out_U_Inp c3 ) ;
for b1 being State of c2 holds b1 . c4 = (Exec c3,b1) . c4
proof
let c5 be State of c2;
reconsider c6 = c5 . c4 as Element of ObjectKind c4 by E2;
E17: Exec c3,(c5 +* c4,c6) = (Exec c3,c5) +* c4,c6 by E16, E12;
dom (Exec c3,c5) = the carrier of c2 by AMI_3:36;
hence c5 . c4 = ((Exec c3,c5) +* c4,c6) . c4 by FUNCT_7:33
.= (Exec c3,c5) . c4 by E17, FUNCT_7:37 ;

end;
hence not verum by E16, E10;
end;
hence Output c3 c= Out_U_Inp c3 by SUBSET_1:7;
end;

theorem E16: :: AMI_7:12
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being Instruction of b2 holds Input b3 c= Out_U_Inp b3 by XBOOLE_1:36;

theorem :: AMI_7:13
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of b1
for b3 being Instruction of b2 holds Out_\_Inp b3 = (Output b3) \ (Input b3)
proof
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of c1;
let c3 be Instruction of c2;
for b1 being Object of c2 holds
( b1 in Out_\_Inp c3 iff b1 in (Output c3) \ (Input c3) )
proof
let c4 be Object of c2;
hereby
assume E17: c4 in Out_\_Inp c3 ;
E18: Out_\_Inp c3 c= Output c3 by E14;
Out_\_Inp c3 misses Input c3 by E13;
then not c4 in Input c3 by E17, XBOOLE_0:3;
hence c4 in (Output c3) \ (Input c3) by E17, E18, XBOOLE_0:def 4;
end;
assume E17: c4 in (Output c3) \ (Input c3) ;
then not c4 in Input c3 by XBOOLE_0:def 4;
then E18: not c4 in (Out_U_Inp c3) \ (Out_\_Inp c3) ;
per cases not ( c4 in Out_U_Inp c3 & not c4 in Out_\_Inp c3 ) by E18, XBOOLE_0:def 4;
suppose E19: not c4 in Out_U_Inp c3 ;
Output c3 c= Out_U_Inp c3 by E15;
then not c4 in Output c3 by E19;
hence c4 in Out_\_Inp c3 by E17, XBOOLE_0:def 4;
end;
suppose c4 in Out_\_Inp c3 ;
hence c4 in Out_\_Inp c3 ;
end;
end;
end;
hence Out_\_Inp c3 = (Output c3) \ (Input c3) by SUBSET_1:8;
end;

theorem :: AMI_7:14
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of b1
for b3 being Instruction of b2 holds Out_U_Inp b3 = (Output b3) \/ (Input b3)
proof
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of c1;
let c3 be Instruction of c2;
for b1 being Object of c2 holds
( b1 in Out_U_Inp c3 implies b1 in (Output c3) \/ (Input c3) )
proof
let c4 be Object of c2;
assume E17: c4 in Out_U_Inp c3 ;
( c4 in Input c3 or c4 in Output c3 )
proof
assume E18: not c4 in Input c3 ;
per cases not ( c4 in Out_U_Inp c3 & not c4 in Out_\_Inp c3 ) by E18, XBOOLE_0:def 4;
suppose not c4 in Out_U_Inp c3 ;
hence c4 in Output c3 by E17;
end;
suppose E19: c4 in Out_\_Inp c3 ;
Out_\_Inp c3 c= Output c3 by E14;
hence c4 in Output c3 by E19;
end;
end;
end;
hence c4 in (Output c3) \/ (Input c3) by XBOOLE_0:def 2;
end;
hence Out_U_Inp c3 c= (Output c3) \/ (Input c3) by SUBSET_1:7; :: according to XBOOLE_0:def 10
( Output c3 c= Out_U_Inp c3 & Input c3 c= Out_U_Inp c3 ) by E15, E16;
hence (Output c3) \/ (Input c3) c= Out_U_Inp c3 by XBOOLE_1:8;
end;

theorem E17: :: AMI_7:15
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being Instruction of b2
for b4 being Object of b2 holds
not ( ObjectKind b4 is trivial & b4 in Out_U_Inp b3 )
proof
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite AMI-Struct of c1;
let c3 be Instruction of c2;
let c4 be Object of c2;
assume E18: ObjectKind c4 is trivial ;
assume c4 in Out_U_Inp c3 ;
then consider c5 being State of c2, c6 being Element of ObjectKind c4 such that
E19: Exec c3,(c5 +* c4,c6) <> (Exec c3,c5) +* c4,c6 by E12;
c5 . c4 is Element of ObjectKind c4 by E2;
then c5 . c4 = c6 by E18, YELLOW_8:def 1;
then E20: Exec c3,(c5 +* c4,c6) = Exec c3,c5 by FUNCT_7:37;
E21: dom ((Exec c3,c5) +* c4,c6) = the carrier of c2 by AMI_3:36;
E22: dom (Exec c3,c5) = the carrier of c2 by AMI_3:36;
for b1 being set holds
( b1 in the carrier of c2 implies ((Exec c3,c5) +* c4,c6) . b1 = (Exec c3,c5) . b1 )
proof
let c7 be set ;
assume c7 in the carrier of c2 ;
per cases not ( not c7 = c4 & not c7 <> c4 ) ;
suppose E23: c7 = c4 ;
E24: (Exec c3,c5) . c4 is Element of ObjectKind c4 by E2;
thus ((Exec c3,c5) +* c4,c6) . c7 = c6 by E22, E23, FUNCT_7:33
.= (Exec c3,c5) . c7 by E18, E23, E24, YELLOW_8:def 1 ;
end;
suppose c7 <> c4 ;
hence ((Exec c3,c5) +* c4,c6) . c7 = (Exec c3,c5) . c7 by FUNCT_7:34;
end;
end;
end;
hence not verum by E19, E20, E21, E22, FUNCT_1:9;
end;

theorem :: AMI_7:16
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being Instruction of b2
for b4 being Object of b2 holds
not ( ObjectKind b4 is trivial & b4 in Input b3 )
proof
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite AMI-Struct of c1;
let c3 be Instruction of c2;
let c4 be Object of c2;
assume E18: ObjectKind c4 is trivial ;
Input c3 c= Out_U_Inp c3 by E16;
hence not c4 in Input c3 by E18, E17;
end;

theorem :: AMI_7:17
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being Instruction of b2
for b4 being Object of b2 holds
not ( ObjectKind b4 is trivial & b4 in Output b3 )
proof
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite AMI-Struct of c1;
let c3 be Instruction of c2;
let c4 be Object of c2;
assume E18: ObjectKind c4 is trivial ;
Output c3 c= Out_U_Inp c3 by E15;
hence not c4 in Output c3 by E18, E17;
end;

theorem E18: :: AMI_7:18
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being Instruction of b2 holds
( b3 is halting iff Output b3 is empty )
proof
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite AMI-Struct of c1;
let c3 be Instruction of c2;
thus ( c3 is halting implies Output c3 is empty )
proof
assume E19: for b1 being State of c2 holds Exec c3,b1 = b1 ; :: according to AMI_1:def 8
assume not Output c3 is empty ;
then consider c4 being Object of c2 such that
E20: c4 in Output c3 by SUBSET_1:10;
not for b1 being State of c2 holds not b1 . c4 <> (Exec c3,b1) . c4 by E20, E10;
hence not verum by E19;
end;
assume E19: Output c3 is empty ;
let c4 be State of c2; :: according to AMI_1:def 8
E20: dom c4 = the carrier of c2 by AMI_3:36;
E21: dom (Exec c3,c4) = the carrier of c2 by AMI_3:36;
assume Exec c3,c4 <> c4 ;
then ex b1 being set st
( b1 in the carrier of c2 & (Exec c3,c4) . b1 <> c4 . b1 ) by E20, E21, FUNCT_1:9;
hence not verum by E19, E10;
end;

theorem E19: :: AMI_7:19
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of b1
for b3 being Instruction of b2 holds
( b3 is halting implies Out_\_Inp b3 is empty )
proof
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of c1;
let c3 be Instruction of c2;
assume E20: c3 is halting ;
Out_\_Inp c3 c= Output c3 by E14;
then Out_\_Inp c3 c= {} by E20, E18;
hence Out_\_Inp c3 is empty by XBOOLE_1:3;
end;

theorem E20: :: AMI_7:20
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1
for b3 being I