:: AMI_1 semantic presentation

theorem :: AMI_1:1
canceled;

theorem E1: :: AMI_1:2
for b1, b2 being set holds
1 <> [b1,b2]
proof
let c1, c2 be set ;
E2: ( 1 = {{} } & [c1,c2] = {{c1,c2},{c1}} ) by CARD_5:1;
assume 1 = [c1,c2] ;
hence not verum by E2, ZFMISC_1:8;
end;

theorem :: AMI_1:3
for b1, b2 being set holds
2 <> [b1,b2]
proof
let c1, c2 be set ;
E2: ( 2 = {{} ,{{} }} & [c1,c2] = {{c1,c2},{c1}} ) by CARD_5:1;
assume 2 = [c1,c2] ;
hence not verum by E2, ZFMISC_1:10;
end;

theorem :: AMI_1:4
canceled;

theorem E2: :: AMI_1:5
for b1, b2, b3, b4 being set holds
( b1 <> b2 implies product (b1,b2 --> {b3},{b4}) = {(b1,b2 --> b3,b4)} )
proof
let c1, c2, c3, c4 be set ;
assume E3: c1 <> c2 ;
set c5 = {(c1,c2 --> c3,c4)};
set c6 = c1,c2 --> {c3},{c4};
E4: dom (c1,c2 --> {c3},{c4}) = {c1,c2} by FUNCT_4:65;
now
let c7 be set ;
thus not ( c7 in {(c1,c2 --> c3,c4)} & for b1 being Function holds
not ( c7 = b1 & dom b1 = dom (c1,c2 --> {c3},{c4}) & for b2 being set holds
( b2 in dom (c1,c2 --> {c3},{c4}) implies b1 . b2 in (c1,c2 --> {c3},{c4}) . b2 ) ) )
proof
assume E5: c7 in {(c1,c2 --> c3,c4)} ;
take c8 = c1,c2 --> c3,c4;
thus c7 = c8 by E5, TARSKI:def 1;
thus dom c8 = dom (c1,c2 --> {c3},{c4}) by E4, FUNCT_4:65;
let c9 be set ;
assume c9 in dom (c1,c2 --> {c3},{c4}) ;
then E6: ( c9 = c1 or c9 = c2 ) by E4, TARSKI:def 2;
( c8 . c1 = c3 & (c1,c2 --> {c3},{c4}) . c1 = {c3} & c8 . c2 = c4 & (c1,c2 --> {c3},{c4}) . c2 = {c4} ) by E3, FUNCT_4:66;
hence c8 . c9 in (c1,c2 --> {c3},{c4}) . c9 by E6, TARSKI:def 1;
end;
given c8 being Function such that E5: c7 = c8
and E6: dom c8 = dom (c1,c2 --> {c3},{c4})
and E7: for b1 being set holds
( b1 in dom (c1,c2 --> {c3},{c4}) implies c8 . b1 in (c1,c2 --> {c3},{c4}) . b1 ) ;
( c1 in dom (c1,c2 --> {c3},{c4}) & c2 in dom (c1,c2 --> {c3},{c4}) ) by E4, TARSKI:def 2;
then ( c8 . c1 in (c1,c2 --> {c3},{c4}) . c1 & c8 . c2 in (c1,c2 --> {c3},{c4}) . c2 & (c1,c2 --> {c3},{c4}) . c1 = {c3} & (c1,c2 --> {c3},{c4}) . c2 = {c4} ) by E3, E7, FUNCT_4:66;
then ( c8 . c1 = c3 & c8 . c2 = c4 ) by TARSKI:def 1;
then c8 = c1,c2 --> c3,c4 by E4, E6, FUNCT_4:69;
hence c7 in {(c1,c2 --> c3,c4)} by E5, TARSKI:def 1;
end;
hence product (c1,c2 --> {c3},{c4}) = {(c1,c2 --> c3,c4)} by CARD_3:def 5;
end;

definition
let c1 be set ;
attr a2 is strict;
struct AMI-Struct of a1 -> 1-sorted ;
aggr AMI-Struct(# carrier, Instruction-Counter, Instruction-Locations, Instruction-Codes, Instructions, Object-Kind, Execution #) -> AMI-Struct of a1;
sel Instruction-Counter a2 -> Element of the carrier of a2;
sel Instruction-Locations a2 -> Subset of the carrier of a2;
sel Instruction-Codes a2 -> non empty set ;
sel Instructions a2 -> non empty Subset of [:the Instruction-Codes of a2,(((union a1) \/ the carrier of a2) * ):];
sel Object-Kind a2 -> Function of the carrier of a2,a1 \/ {the Instructions of a2,the Instruction-Locations of a2};
sel Execution a2 -> Function of the Instructions of a2, Funcs (product the Object-Kind of a2),(product the Object-Kind of a2);
end;

definition
let c1 be set ;
canceled;
func Trivial-AMI a1 -> strict AMI-Struct of a1 means :E3: :: AMI_1:def 2
( the carrier of a2 = {0,1} & the Instruction-Counter of a2 = 0 & the Instruction-Locations of a2 = {1} & the Instruction-Codes of a2 = {0} & the Instructions of a2 = {[0,{} ]} & the Object-Kind of a2 = 0,1 --> {1},{[0,{} ]} & the Execution of a2 = {[0,{} ]} --> (id (product (0,1 --> {1},{[0,{} ]}))) );
existence
ex b1 being strict AMI-Struct of c1 st
( the carrier of b1 = {0,1} & the Instruction-Counter of b1 = 0 & the Instruction-Locations of b1 = {1} & the Instruction-Codes of b1 = {0} & the Instructions of b1 = {[0,{} ]} & the Object-Kind of b1 = 0,1 --> {1},{[0,{} ]} & the Execution of b1 = {[0,{} ]} --> (id (product (0,1 --> {1},{[0,{} ]}))) )
proof
reconsider c2 = 0 as Element of {0,1} by TARSKI:def 2;
( 0 in {0} & {} in ((union c1) \/ {0,1}) * ) by FINSEQ_1:66, TARSKI:def 1;
then [0,{} ] in [:{0},(((union c1) \/ {0,1}) * ):] by ZFMISC_1:106;
then reconsider c3 = {[0,{} ]} as non empty Subset of [:{0},(((union c1) \/ {0,1}) * ):] by ZFMISC_1:37;
reconsider c4 = {1} as non empty Subset of {0,1} by ZFMISC_1:12;
set c5 = 0,1 --> c4,c3;
( rng (0,1 --> c4,c3) c= {c3,c4} & {c3,c4} c= c1 \/ {c3,c4} ) by FUNCT_4:65, XBOOLE_1:7;
then ( dom (0,1 --> c4,c3) = {0,1} & rng (0,1 --> c4,c3) c= c1 \/ {c3,c4} ) by FUNCT_4:65, XBOOLE_1:1;
then reconsider c6 = 0,1 --> c4,c3 as Function of {0,1},c1 \/ {c3,c4} by FUNCT_2:def 1, RELSET_1:11;
id (product c6) in Funcs (product c6),(product c6) by FUNCT_2:12;
then reconsider c7 = c3 --> (id (product c6)) as Function of c3, Funcs (product c6),(product c6) by FUNCOP_1:57;
take AMI-Struct {0,1},c2,c4,{0},c3,c6,c7 ;
thus ( the carrier of (AMI-Struct {0,1},c2,c4,{0},c3,c6,c7) = {0,1} & the Instruction-Counter of (AMI-Struct {0,1},c2,c4,{0},c3,c6,c7) = 0 & the Instruction-Locations of (AMI-Struct {0,1},c2,c4,{0},c3,c6,c7) = {1} & the Instruction-Codes of (AMI-Struct {0,1},c2,c4,{0},c3,c6,c7) = {0} & the Instructions of (AMI-Struct {0,1},c2,c4,{0},c3,c6,c7) = {[0,{} ]} & the Object-Kind of (AMI-Struct {0,1},c2,c4,{0},c3,c6,c7) = 0,1 --> {1},{[0,{} ]} & the Execution of (AMI-Struct {0,1},c2,c4,{0},c3,c6,c7) = {[0,{} ]} --> (id (product (0,1 --> {1},{[0,{} ]}))) ) ;
end;
uniqueness
for b1, b2 being strict AMI-Struct of c1 holds
( ( the carrier of b1 = {0,1} & the Instruction-Counter of b1 = 0 & the Instruction-Locations of b1 = {1} & the Instruction-Codes of b1 = {0} & the Instructions of b1 = {[0,{} ]} & the Object-Kind of b1 = 0,1 --> {1},{[0,{} ]} & the Execution of b1 = {[0,{} ]} --> (id (product (0,1 --> {1},{[0,{} ]}))) & the carrier of b2 = {0,1} & the Instruction-Counter of b2 = 0 & the Instruction-Locations of b2 = {1} & the Instruction-Codes of b2 = {0} & the Instructions of b2 = {[0,{} ]} & the Object-Kind of b2 = 0,1 --> {1},{[0,{} ]} & the Execution of b2 = {[0,{} ]} --> (id (product (0,1 --> {1},{[0,{} ]}))) ) implies ( b1 = b2 ) ) ;
end;

:: deftheorem AMI_1:def 1 :
canceled;

:: deftheorem E3 defines Trivial-AMI AMI_1:def 2 :
for b1 being set
for b2 being strict AMI-Struct of b1 holds
( b2 = Trivial-AMI b1 iff ( the carrier of b2 = {0,1} & the Instruction-Counter of b2 = 0 & the Instruction-Locations of b2 = {1} & the Instruction-Codes of b2 = {0} & the Instructions of b2 = {[0,{} ]} & the Object-Kind of b2 = 0,1 --> {1},{[0,{} ]} & the Execution of b2 = {[0,{} ]} --> (id (product (0,1 --> {1},{[0,{} ]}))) ) );

definition
let c1 be set ;
let c2 be AMI-Struct of c1;
attr a2 is void means :E4: :: AMI_1:def 3
the Instruction-Locations of a2 is empty;
end;

:: deftheorem E4 defines void AMI_1:def 3 :
for b1 being set
for b2 being AMI-Struct of b1 holds
( b2 is void iff the Instruction-Locations of b2 is empty );

registration
let c1 be set ;
cluster Trivial-AMI a1 -> non empty strict non void ;
coherence
( not Trivial-AMI c1 is empty & not Trivial-AMI c1 is void )
proof
thus not the carrier of (Trivial-AMI c1) is empty by E3; :: uses STRUCT_0:def 1
thus not the Instruction-Locations of (Trivial-AMI c1) is empty by E3; :: uses AMI_1:def 3
end;
end;

registration
let c1 be set ;
cluster non empty non void AMI-Struct of a1;
existence
ex b1 being AMI-Struct of c1 st
( not b1 is empty & not b1 is void )
proof
take Trivial-AMI c1 ;
thus ( not Trivial-AMI c1 is empty & not Trivial-AMI c1 is void ) ;
end;
end;

registration
let c1 be set ;
let c2 be non void AMI-Struct of c1;
cluster the Instruction-Locations of a2 -> non empty ;
coherence
not the Instruction-Locations of c2 is empty by E4;
end;

definition
let c1 be set ;
let c2 be non empty AMI-Struct of c1;
mode Object is Element of a2;
end;

definition
let c1 be set ;
let c2 be non empty non void AMI-Struct of c1;
mode Instruction-Location is Element of the Instruction-Locations of a2;
end;

definition
let c1 be set ;
let c2 be AMI-Struct of c1;
mode Instruction is Element of the Instructions of a2;
end;

definition
let c1 be set ;
let c2 be non empty AMI-Struct of c1;
canceled;
func IC a2 -> Object of a2 equals :: AMI_1:def 5
the Instruction-Counter of a2;
correctness
coherence
the Instruction-Counter of c2 is Object of c2;
;
end;

:: deftheorem AMI_1:def 4 :
canceled;

:: deftheorem defines IC AMI_1:def 5 :
for b1 being set
for b2 being non empty AMI-Struct of b1 holds IC b2 = the Instruction-Counter of b2;

definition
let c1 be set ;
let c2 be non empty AMI-Struct of c1;
let c3 be Object of c2;
func ObjectKind a3 -> Element of a1 \/ {the Instructions of a2,the Instruction-Locations of a2} equals :: AMI_1:def 6
the Object-Kind of a2 . a3;
correctness
coherence
the Object-Kind of c2 . c3 is Element of c1 \/ {the Instructions of c2,the Instruction-Locations of c2};
;
end;

:: deftheorem defines ObjectKind AMI_1:def 6 :
for b1 being set
for b2 being non empty AMI-Struct of b1
for b3 being Object of b2 holds ObjectKind b3 = the Object-Kind of b2 . b3;

registration
let c1 be Function;
cluster product a1 -> functional ;
coherence
product c1 is functional
proof
set c2 = product c1;
let c3 be set ; :: uses FRAENKEL:def 1
assume c3 in product c1 ;
then ex b1 being Function st
( c3 = b1 & dom b1 = dom c1 & for b2 being set holds
( b2 in dom c1 implies b1 . b2 in c1 . b2 ) ) by CARD_3:def 5;
hence c3 is Function ;
end;
end;

registration
let c1 be set ;
let c2 be with_non-empty_elements set ;
let c3 be Function of c1,c2;
cluster product a3 -> non empty functional ;
coherence
not product c3 is empty
proof
rng c3 c= c2 by RELSET_1:12;
then not {} in rng c3 by SETFAM_1:def 9;
hence not product c3 is empty by CARD_3:37;
end;
end;

definition
let c1 be set ;
let c2 be AMI-Struct of c1;
mode State is Element of product the Object-Kind of a2;
end;

definition
let c1 be with_non-empty_elements set ;
let c2 be non void AMI-Struct of c1;
let c3 be Instruction of c2;
let c4 be State of c2;
func Exec a3,a4 -> State of a2 equals :: AMI_1:def 7
(the Execution of a2 . a3) . a4;
coherence
(the Execution of c2 . c3) . c4 is State of c2
proof
consider c5 being Function such that
E5: ( the Execution of c2 . c3 = c5 & dom c5 = product the Object-Kind of c2 & rng c5 c= product the Object-Kind of c2 ) by FUNCT_2:def 2;
(the Execution of c2 . c3) . c4 in rng c5 by E5, FUNCT_1:def 5;
hence (the Execution of c2 . c3) . c4 is State of c2 by E5;
end;
end;

:: deftheorem defines Exec AMI_1:def 7 :
for b1 being with_non-empty_elements set
for b2 being non void AMI-Struct of b1
for b3 being Instruction of b2
for b4 being State of b2 holds Exec b3,b4 = (the Execution of b2 . b3) . b4;

definition
let c1 be with_non-empty_elements set ;
let c2 be non void AMI-Struct of c1;
let c3 be Instruction of c2;
attr a3 is halting means :E5: :: AMI_1:def 8
for b1 being State of a2 holds Exec a3,b1 = b1;
end;

:: deftheorem E5 defines halting AMI_1:def 8 :
for b1 being with_non-empty_elements set
for b2 being non void AMI-Struct of b1
for b3 being Instruction of b2 holds
( b3 is halting iff for b4 being State of b2 holds Exec b3,b4 = b4 );

definition
let c1 be with_non-empty_elements set ;
let c2 be non void AMI-Struct of c1;
attr a2 is halting means :E6: :: AMI_1:def 9
ex b1 being Instruction of a2 st
( b1 is halting & for b2 being Instruction of a2 holds
( b2 is halting implies b1 = b2 ) );
end;

:: deftheorem E6 defines halting AMI_1:def 9 :
for b1 being with_non-empty_elements set
for b2 being non void AMI-Struct of b1 holds
( b2 is halting iff ex b3 being Instruction of b2 st
( b3 is halting & for b4 being Instruction of b2 holds
( b4 is halting implies b3 = b4 ) ) );

theorem E7: :: AMI_1:6
for b1 being with_non-empty_elements set holds Trivial-AMI b1 is halting
proof
let c1 be with_non-empty_elements set ;
set c2 = Trivial-AMI c1;
E8: {[0,{} ]} = the Instructions of (Trivial-AMI c1) by E3;
then reconsider c3 = [0,{} ] as Instruction of (Trivial-AMI c1) by TARSKI:def 1;
take c3 ; :: uses AMI_1:def 9
thus c3 is halting
proof
let c4 be State of (Trivial-AMI c1); :: uses AMI_1:def 8
E9: product the Object-Kind of (Trivial-AMI c1) = product (0,1 --> {1},{[0,{} ]}) by E3
.= {(0,1 --> 1,[0,{} ])} by E2 ;
hence Exec c3,c4 = 0,1 --> 1,[0,{} ] by TARSKI:def 1
.= c4 by E9, TARSKI:def 1 ;

end;
let c4 be Instruction of (Trivial-AMI c1);
assume c4 is halting ;
thus c3 = c4 by E8, TARSKI:def 1;
end;

registration
let c1 be with_non-empty_elements set ;
cluster Trivial-AMI a1 -> non empty strict non void halting ;
coherence
Trivial-AMI c1 is halting by E7;
end;

registration
let c1 be with_non-empty_elements set ;
cluster non void halting AMI-Struct of a1;
existence
ex b1 being non void AMI-Struct of c1 st b1 is halting
proof
take Trivial-AMI c1 ;
thus Trivial-AMI c1 is halting ;
end;
end;

registration
let c1 be with_non-empty_elements set ;
let c2 be non void halting AMI-Struct of c1;
cluster halting Element of the Instructions of a2;
existence
ex b1 being Instruction of c2 st b1 is halting
proof
ex b1 being Instruction of c2 st
( b1 is halting & for b2 being Instruction of c2 holds
( b2 is halting implies b1 = b2 ) ) by E6;
hence ex b1 being Instruction of c2 st b1 is halting ;
end;
end;

definition
let c1 be with_non-empty_elements set ;
let c2 be non void halting AMI-Struct of c1;
func halt a2 -> Instruction of a2 means :E8: :: AMI_1:def 10
a3 is halting Instruction of a2;
existence
ex b1 being Instruction of c2 st
b1 is halting Instruction of c2
proof
consider c3 being Instruction of c2 such that
E8: c3 is halting
and for b1 being Instruction of c2 holds
( b1 is halting implies c3 = b1 ) by E6;
take c3 ;
thus c3 is halting Instruction of c2 by E8;
end;
uniqueness
for b1, b2 being Instruction of c2 holds
( ( b1 is halting Instruction of c2 & b2 is halting Instruction of c2 ) implies ( b1 = b2 ) )
proof
let c3, c4 be Instruction of c2;
assume that E8: c3 is halting Instruction of c2
and E9: c4 is halting Instruction of c2 ;
consider c5 being Instruction of c2 such that
E10: ( c5 is halting & for b1 being Instruction of c2 holds
( b1 is halting implies c5 = b1 ) ) by E6;
c5 = c3 by E8, E10;
hence c3 = c4 by E9, E10;
end;
end;

:: deftheorem E8 defines halt AMI_1:def 10 :
for b1 being with_non-empty_elements set
for b2 being non void halting AMI-Struct of b1
for b3 being Instruction of b2 holds
( b3 = halt b2 iff b3 is halting Instruction of b2 );

registration
let c1 be with_non-empty_elements set ;
let c2 be non void halting AMI-Struct of c1;
cluster halt a2 -> halting ;
coherence
halt c2 is halting by E8;
end;

definition
let c1 be set ;
let c2 be non empty AMI-Struct of c1;
attr a2 is IC-Ins-separated means :E9: :: AMI_1:def 11
 ObjectKind (IC a2) = the Instruction-Locations of a2;
end;

:: deftheorem E9 defines IC-Ins-separated AMI_1:def 11 :
for b1 being set
for b2 being non empty AMI-Struct of b1 holds
( b2 is IC-Ins-separated iff ObjectKind (IC b2) = the Instruction-Locations of b2 );

definition
let c1 be set ;
let c2 be AMI-Struct of c1;
attr a2 is data-oriented means :: AMI_1:def 12
the Object-Kind of a2 " {the Instructions of a2} c= the Instruction-Locations of a2;
end;

:: deftheorem defines data-oriented AMI_1:def 12 :
for b1 being set
for b2 being AMI-Struct of b1 holds
( b2 is data-oriented iff the Object-Kind of b2 " {the Instructions of b2} c= the Instruction-Locations of b2 );

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void AMI-Struct of c1;
attr a2 is steady-programmed means :E10: :: AMI_1:def 13
for b1 being State of a2
for b2 being Instruction of a2
for b3 being Instruction-Location of a2 holds (Exec b2,b1) . b3 = b1 . b3;
end;

:: deftheorem E10 defines steady-programmed AMI_1:def 13 :
for b1 being with_non-empty_elements set
for b2 being non empty non void AMI-Struct of b1 holds
( b2 is steady-programmed iff for b3 being State of b2
for b4 being Instruction of b2
for b5 being Instruction-Location of b2 holds (Exec b4,b3) . b5 = b3 . b5 );

definition
let c1 be set ;
let c2 be non empty non void AMI-Struct of c1;
attr a2 is definite means :E11: :: AMI_1:def 14
for b1 being Instruction-Location of a2 holds ObjectKind b1 = the Instructions of a2;
end;

:: deftheorem E11 defines definite AMI_1:def 14 :
for b1 being set
for b2 being non empty non void AMI-Struct of b1 holds
( b2 is definite iff for b3 being Instruction-Location of b2 holds ObjectKind b3 = the Instructions of b2 );

theorem E12: :: AMI_1:7
for b1 being set holds Trivial-AMI b1 is IC-Ins-separated
proof
let c1 be set ;
E13: IC (Trivial-AMI c1) = the Instruction-Counter of (Trivial-AMI c1)
.= 0 by E3 ;
thus ObjectKind (IC (Trivial-AMI c1)) = the Object-Kind of (Trivial-AMI c1) . (IC (Trivial-AMI c1))
.= (0,1 --> {1},{[0,{} ]}) . 0 by E13, E3
.= {1} by FUNCT_4:66
.= the Instruction-Locations of (Trivial-AMI c1) by E3 ; :: uses AMI_1:def 11
end;

theorem E13: :: AMI_1:8
for b1 being set holds Trivial-AMI b1 is data-oriented
proof
let c1 be set ;
let c2 be set ; :: uses TARSKI:def 3,AMI_1:def 12
E14: 1 <> [0,{} ] by E1;
assume E15: c2 in the Object-Kind of (Trivial-AMI c1) " {the Instructions of (Trivial-AMI c1)} ;
then ( c2 in the carrier of (Trivial-AMI c1) & the Object-Kind of (Trivial-AMI c1) . c2 in {the Instructions of (Trivial-AMI c1)} ) by FUNCT_2:46;
then E16: the Object-Kind of (Trivial-AMI c1) . c2 = the Instructions of (Trivial-AMI c1) by TARSKI:def 1
.= {[0,{} ]} by E3 ;
E17: the Object-Kind of (Trivial-AMI c1) . 0 = (0,1 --> {1},{[0,{} ]}) . 0 by E3
.= {1} by FUNCT_4:66 ;
the carrier of (Trivial-AMI c1) = {0,1} by E3;
then ( c2 = 0 or c2 = 1 ) by E15, TARSKI:def 2;
then c2 in {1} by E14, E16, E17, TARSKI:def 1, ZFMISC_1:6;
hence c2 in the Instruction-Locations of (Trivial-AMI c1) by E3;
end;

theorem E14: :: AMI_1:9
for b1 being set
for b2, b3 being State of (Trivial-AMI b1) holds b2 = b3
proof
let c1 be set ;
let c2, c3 be State of (Trivial-AMI c1);
E15: product the Object-Kind of (Trivial-AMI c1) = product (0,1 --> {1},{[0,{} ]}) by E3
.= {(0,1 --> 1,[0,{} ])} by E2 ;
hence c2 = 0,1 --> 1,[0,{} ] by TARSKI:def 1
.= c3 by E15, TARSKI:def 1 ;

end;

theorem E15: :: AMI_1:10
for b1 being with_non-empty_elements set holds Trivial-AMI b1 is steady-programmed
proof
let c1 be with_non-empty_elements set ;
let c2 be State of (Trivial-AMI c1); :: uses AMI_1:def 13
let c3 be Instruction of (Trivial-AMI c1);
let c4 be Instruction-Location of (Trivial-AMI c1);
thus (Exec c3,c2) . c4 = c2 . c4 by E14;
end;

theorem E16: :: AMI_1:11
for b1 being set holds Trivial-AMI b1 is definite
proof
let c1 be set ;
let c2 be Instruction-Location of (Trivial-AMI c1); :: uses AMI_1:def 14
c2 in the Instruction-Locations of (Trivial-AMI c1) ;
then c2 in {1} by E3;
then E17: c2 = 1 by TARSKI:def 1;
thus ObjectKind c2 = the Object-Kind of (Trivial-AMI c1) . c2
.= (0,1 --> {1},{[0,{} ]}) . 1 by E17, E3
.= {[0,{} ]} by FUNCT_4:66
.= the Instructions of (Trivial-AMI c1) by E3 ;
end;

registration
let c1 be set ;
cluster Trivial-AMI a1 -> non empty strict non void data-oriented ;
coherence
Trivial-AMI c1 is data-oriented by E13;
end;

registration
let c1 be set ;
cluster Trivial-AMI a1 -> non empty strict non void IC-Ins-separated data-oriented definite ;
coherence
( Trivial-AMI c1 is IC-Ins-separated & Trivial-AMI c1 is definite ) by E12, E16;
end;

registration
let c1 be with_non-empty_elements set ;
cluster Trivial-AMI a1 -> non empty strict non void halting IC-Ins-separated data-oriented steady-programmed definite ;
coherence
Trivial-AMI c1 is steady-programmed by E15;
end;

registration
let c1 be set ;
cluster strict data-oriented AMI-Struct of a1;
existence
ex b1 being AMI-Struct of c1 st
( b1 is data-oriented & b1 is strict )
proof
take Trivial-AMI c1 ;
thus ( Trivial-AMI c1 is data-oriented & Trivial-AMI c1 is strict ) ;
end;
end;

registration
let c1 be set ;
cluster non empty strict non void IC-Ins-separated data-oriented definite AMI-Struct of a1;
existence
ex b1 being non empty non void AMI-Struct of c1 st
( b1 is IC-Ins-separated & b1 is data-oriented & b1 is definite & b1 is strict )
proof
take Trivial-AMI c1 ;
thus ( Trivial-AMI c1 is IC-Ins-separated & Trivial-AMI c1 is data-oriented & Trivial-AMI c1 is definite & Trivial-AMI c1 is strict ) ;
end;
end;

registration
let c1 be with_non-empty_elements set ;
cluster non empty strict non void halting IC-Ins-separated data-oriented steady-programmed definite AMI-Struct of a1;
existence
ex b1 being non empty non void AMI-Struct of c1 st
( b1 is IC-Ins-separated & b1 is data-oriented & b1 is halting & b1 is steady-programmed & b1 is definite & b1 is strict )
proof
take Trivial-AMI c1 ;
thus ( Trivial-AMI c1 is IC-Ins-separated & Trivial-AMI c1 is data-oriented & Trivial-AMI c1 is halting & Trivial-AMI c1 is steady-programmed & Trivial-AMI c1 is definite & Trivial-AMI c1 is strict ) ;
end;
end;

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated AMI-Struct of c1;
let c3 be State of c2;
func IC a3 -> Instruction-Location of a2 equals :: AMI_1:def 15
a3 . (IC a2);
coherence
c3 . (IC c2) is Instruction-Location of c2
proof
dom the Object-Kind of c2 = the carrier of c2 by FUNCT_2:def 1;
then pi (product the Object-Kind of c2),(IC c2) = the Object-Kind of c2 . (IC c2) by CARD_3:22
.= ObjectKind (IC c2)
.= the Instruction-Locations of c2 by E9 ;
hence c3 . (IC c2) is Instruction-Location of c2 by CARD_3:def 6;
end;
end;

:: deftheorem defines IC AMI_1:def 15 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated AMI-Struct of b1
for b3 being State of b2 holds IC b3 = b3 . (IC b2);

theorem :: AMI_1:12
canceled;

theorem :: AMI_1:13
canceled;

theorem E17: :: AMI_1:14
for b1, b2, b3 being set
for b4, b5 being Function holds
( ( b4 tolerates b5 & [b1,b2] in b4 & [b1,b3] in b5 ) implies ( b2 = b3 ) )
proof
let c1, c2, c3 be set ;
let c4, c5 be Function;
assume c4 tolerates c5 ;
then consider c6 being Function such that
E18: c6 = c4 \/ c5 by PARTFUN1:130;
assume ( [c1,c2] in c4 & [c1,c3] in c5 ) ;
then ( [c1,c2] in c6 & [c1,c3] in c6 ) by E18, XBOOLE_0:def 2;
hence c2 = c3 by FUNCT_1:def 1;
end;

theorem E18: :: AMI_1:15
for b1 being set holds
( ( for b2 being set holds
( b2 in b1 implies b2 is Function ) & for b2, b3 being Function holds
( ( b2 in b1 & b3 in b1 ) implies ( b2 tolerates b3 ) ) ) implies ( union b1 is Function ) )
proof
let c1 be set ;
assume that E19: for b1 being set holds
( b1 in c1 implies b1 is Function )
and E20: for b1, b2 being Function holds
( ( b1 in c1 & b2 in c1 ) implies ( b1 tolerates b2 ) ) ;
E21: now
let c2 be set ;
assume c2 in union c1 ;
then consider c3 being set such that
E22: ( c2 in c3 & c3 in c1 ) by TARSKI:def 4;
reconsider c4 = c3 as Function by E19, E22;
c4 = c4 ;
hence ex b1, b2 being set st [b1,b2] = c2 by E22, RELAT_1:def 1;
end;
now
let c2, c3, c4 be set ;
assume E22: ( [c2,c3] in union c1 & [c2,c4] in union c1 ) ;
then consider c5 being set such that
E23: ( [c2,c3] in c5 & c5 in c1 ) by TARSKI:def 4;
consider c6 being set such that
E24: ( [c2,c4] in c6 & c6 in c1 ) by E22, TARSKI:def 4;
reconsider c7 = c5, c8 = c6 as Function by E19, E23, E24;
c7 tolerates c8 by E20, E23, E24;
hence c3 = c4 by E23, E24, E17;
end;
hence union c1 is Function by E21, FUNCT_1:def 1, RELAT_1:def 1;
end;

theorem :: AMI_1:16
canceled;

theorem :: AMI_1:17
canceled;

theorem E19: :: AMI_1:18
for b1, b2, b3, b4 being set holds b1,b2 --> b3<