:: AMISTD_1 semantic presentation

theorem E1: :: AMISTD_1:1
for b1 being real number holds max {b1} = b1
proof
let c1 be real number ;
( c1 in {c1} & ( for b1 being real number holds
( b1 in {c1} implies b1 <= c1 ) ) ) by TARSKI:def 1;
hence max {c1} = c1 by PRE_CIRC:def 1;
end;

theorem :: AMISTD_1:2
for b1 being Nat holds max {b1} = b1 by E1;

theorem E2: :: AMISTD_1:3
for b1 being non empty set
for b2 being trivial FinSequence of b1 holds
not ( not b2 is empty & ( for b3 being Element of b1 holds
not b2 = <*b3*> ) )
proof
let c1 be non empty set ;
let c2 be trivial FinSequence of c1;
assume not c2 is empty ;
then consider c3 being set such that
E3: c2 = {c3} by REALSET1:def 4;
E4: c3 in {c3} by TARSKI:def 1;
then consider c4, c5 being set such that
E5: c3 = [c4,c5] by E3, RELAT_1:def 1;
take c5 ;
E6: c5 in rng c2 by E3, E4, E5, RELAT_1:def 5;
thus c5 is Element of c1 by E6;
E7: 1 in dom c2 by E3, FINSEQ_5:6;
dom c2 = {c4} by E3, E5, RELAT_1:23;
then 1 = c4 by E7, TARSKI:def 1;
hence c2 = <*c5*> by E3, E5, FINSEQ_1:def 5;
end;

registration
cluster -> with_non-empty_elements set ;
coherence
for b1 being Relation holds b1 is with_non-empty_elements
proof
let c1 be Relation;
assume {} in c1 ; :: according to SETFAM_1:def 9
then ex b1, b2 being set st {} = [b1,b2] by RELAT_1:def 1;
hence not verum ;
end;
end;

registration
let c1 be finite set ;
let c2 be set ;
cluster K344(a1,a2) -> finite ;
coherence
c1 --> c2 is finite
proof
dom (c1 --> c2) = c1 by FUNCOP_1:19;
hence c1 --> c2 is finite by FINSET_1:29;
end;
end;

registration
let c1 be non empty FinSequence;
let c2 be FinSequence;
cluster a1 ^' a2 -> non empty with_non-empty_elements ;
coherence
not c1 ^' c2 is empty
proof
c1 ^' c2 = c1 ^ (2,(len c2) -cut c2) by GRAPH_2:def 2;
hence not c1 ^' c2 is empty ;
end;
end;

theorem :: AMISTD_1:4
canceled;

theorem :: AMISTD_1:5
canceled;

theorem :: AMISTD_1:6
canceled;

theorem :: AMISTD_1:7
canceled;

theorem :: AMISTD_1:8
canceled;

theorem :: AMISTD_1:9
canceled;

theorem :: AMISTD_1:10
canceled;

theorem E3: :: AMISTD_1:11
for b1 being with_non-empty_elements set
for b2 being non empty non void definite AMI-Struct of b1
for b3 being Element of the Instructions of b2
for b4 being State of b2 holds
b4 +* (the Instruction-Locations of b2 --> b3) is State of b2
proof
let c1 be with_non-empty_elements set ;
let c2 be non empty non void definite AMI-Struct of c1;
let c3 be Element of the Instructions of c2;
let c4 be State of c2;
set c5 = the Instruction-Locations of c2 --> c3;
set c6 = the Object-Kind of c2;
E4: dom (the Instruction-Locations of c2 --> c3) = the Instruction-Locations of c2 by FUNCOP_1:19;
E5: dom c4 = the carrier of c2 by AMI_3:36;
then E6: dom the Object-Kind of c2 = dom c4 by FUNCT_2:def 1;
for b1 being set holds
( b1 in dom (the Instruction-Locations of c2 --> c3) implies (the Instruction-Locations of c2 --> c3) . b1 in the Object-Kind of c2 . b1 )
proof
let c7 be set ;
assume E7: c7 in dom (the Instruction-Locations of c2 --> c3) ;
then E8: (the Instruction-Locations of c2 --> c3) . c7 = c3 by E4, FUNCOP_1:13;
reconsider c8 = c7 as Instruction-Location of c2 by E7, FUNCOP_1:19;
the Object-Kind of c2 . c8 = ObjectKind c8
.= the Instructions of c2 by AMI_1:def 14 ;
hence (the Instruction-Locations of c2 --> c3) . c7 in the Object-Kind of c2 . c7 by E8;
end;
then the Instruction-Locations of c2 --> c3 in sproduct the Object-Kind of c2 by E4, E5, E6, AMI_1:def 16;
hence c4 +* (the Instruction-Locations of c2 --> c3) is State of c2 by AMI_1:29;
end;

registration
let c1 be set ;
let c2 be AMI-Struct of c1;
cluster empty -> with_non-empty_elements programmed FinPartState of a2;
coherence
for b1 being FinPartState of c2 holds
( b1 is empty implies b1 is programmed )
proof
let c3 be FinPartState of c2;
assume c3 is empty ;
then reconsider c4 = c3 as empty Function ;
dom c4 c= the Instruction-Locations of c2 by XBOOLE_1:2;
hence dom c3 c= the Instruction-Locations of c2 ; :: according to AMI_3:def 13
end;
end;

registration
let c1 be set ;
let c2 be AMI-Struct of c1;
cluster empty with_non-empty_elements programmed FinPartState of a2;
existence
ex b1 being FinPartState of c2 st b1 is empty
proof
reconsider c3 = {} as Element of sproduct the Object-Kind of c2 by AMI_1:26;
take c3 ;
thus ( c3 is finite & c3 is empty ) ; :: according to AMI_1:def 24
end;
end;

registration
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite AMI-Struct of c1;
cluster non empty trivial with_non-empty_elements programmed FinPartState of a2;
existence
ex b1 being FinPartState of c2 st
( not b1 is empty & b1 is trivial & b1 is programmed )
proof
consider c3 being Instruction-Location of c2, c4 being Instruction of c2;
take c3 .--> c4 ;
thus ( not c3 .--> c4 is empty & c3 .--> c4 is trivial & c3 .--> c4 is programmed ) ;
end;
end;

registration
let c1 be with_non-empty_elements set ;
let c2 be non void AMI-Struct of c1;
let c3 be Element of the Instructions of c2;
let c4 be State of c2;
cluster (the Execution of a2 . a3) . a4 -> Relation-like Function-like with_non-empty_elements ;
coherence
( (the Execution of c2 . c3) . c4 is Function-like & (the Execution of c2 . c3) . c4 is Relation-like )
proof
reconsider c5 = the Execution of c2 . c3 as Function of product the Object-Kind of c2, product the Object-Kind of c2 by FUNCT_2:121;
c5 . c4 in product the Object-Kind of c2 ;
hence ( (the Execution of c2 . c3) . c4 is Function-like & (the Execution of c2 . c3) . c4 is Relation-like ) ;
end;
end;

E4: 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 Instruction-Location of b2
for b4 being Element of the Instructions of b2
for b5 being FinPartState of b2 holds
( b5 = b3 .--> b4 implies b5 is autonomic )
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 Instruction-Location of c2;
let c4 be Element of the Instructions of c2;
let c5 be FinPartState of c2;
assume E5: c5 = c3 .--> c4 ;
let c6, c7 be State of c2; :: according to AMI_1:def 25
assume that
E6: c5 c= c6 and
E7: c5 c= c7 ;
let c8 be Nat;
E8: dom c5 = {c3} by E5, CQC_LANG:5;
E9: for b1 being Function holds
( c5 c= b1 implies b1 . c3 = c4 )
proof
let c9 be Function;
assume E10: c5 c= c9 ;
c3 in {c3} by TARSKI:def 1;
hence c9 . c3 = c5 . c3 by E8, E10, GRFUNC_1:8
.= c4 by E5, CQC_LANG:6 ;

end;
set c9 = ((Computation c6) . c8) | (dom c5);
set c10 = ((Computation c7) . c8) | (dom c5);
E10: {c3} c= the carrier of c2 ;
then {c3} c= dom ((Computation c6) . c8) by AMI_3:36;
then E11: dom (((Computation c6) . c8) | (dom c5)) = {c3} by E8, RELAT_1:91;
{c3} c= dom ((Computation c7) . c8) by E10, AMI_3:36;
then E12: dom (((Computation c7) . c8) | (dom c5)) = {c3} by E8, RELAT_1:91;
for b1 being set holds
( b1 in {c3} implies (((Computation c6) . c8) | (dom c5)) . b1 = (((Computation c7) . c8) | (dom c5)) . b1 )
proof
let c11 be set ;
assume E13: c11 in {c3} ;
then E14: c11 = c3 by TARSKI:def 1;
E15: c5 c= (Computation c6) . c8 by E5, E6, AMI_3:38;
E16: c5 c= (Computation c7) . c8 by E5, E7, AMI_3:38;
thus (((Computation c6) . c8) | (dom c5)) . c11 = ((Computation c6) . c8) . c11 by E8, E13, FUNCT_1:72
.= c4 by E9, E14, E15
.= ((Computation c7) . c8) . c11 by E9, E14, E16
.= (((Computation c7) . c8) | (dom c5)) . c11 by E8, E13, FUNCT_1:72 ;
end;
hence ((Computation c6) . c8) | (dom c5) = ((Computation c7) . c8) | (dom c5) by E11, E12, FUNCT_1:9;
end;

registration
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;
cluster non empty trivial with_non-empty_elements autonomic programmed FinPartState of a2;
existence
ex b1 being FinPartState of c2 st
( not b1 is empty & b1 is trivial & b1 is autonomic & b1 is programmed )
proof
consider c3 being Instruction-Location of c2;
consider c4 being Instruction of c2;
take c3 .--> c4 ;
thus ( not c3 .--> c4 is empty & c3 .--> c4 is trivial & c3 .--> c4 is autonomic & c3 .--> c4 is programmed ) by E4;
end;
end;

theorem :: AMISTD_1:12
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 Instruction-Location of b2
for b4 being Element of the Instructions of b2 holds b3 .--> b4 is autonomic by E4;

theorem E5: :: AMISTD_1:13
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 holds b2 is programmable
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;
consider c3 being Instruction-Location of c2;
consider c4 being Instruction of c2;
take c3 .--> c4 ; :: according to AMI_1:def 27
thus ( not c3 .--> c4 is empty & c3 .--> c4 is autonomic ) by E4;
end;

registration
let c1 be with_non-empty_elements set ;
cluster non empty non void IC-Ins-separated steady-programmed definite -> non empty non void IC-Ins-separated definite programmable AMI-Struct of a1;
coherence
for b1 being non empty non void IC-Ins-separated definite AMI-Struct of c1 holds
( b1 is steady-programmed implies b1 is programmable ) by E5;
end;

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void AMI-Struct of c1;
let c3 be InsType of c2;
canceled;
canceled;
attr a3 is jump-only means :: AMISTD_1:def 3
for b1 being State of a2
for b2 being Object of a2
for b3 being Instruction of a2 holds
( ( InsCode b3 = a3 ) implies ( not b2 <> IC a2 or (Exec b3,b1) . b2 = b1 . b2 ) );
end;

:: deftheorem AMISTD_1:def 1 :
canceled;

:: deftheorem AMISTD_1:def 2 :
canceled;

:: deftheorem defines jump-only AMISTD_1:def 3 :
for b1 being with_non-empty_elements set
for b2 being non empty non void AMI-Struct of b1
for b3 being InsType of b2 holds
( b3 is jump-only iff for b4 being State of b2
for b5 being Object of b2
for b6 being Instruction of b2 holds
( ( InsCode b6 = b3 ) implies ( not b5 <> IC b2 or (Exec b6,b4) . b5 = b4 . b5 ) ) );

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;
attr a3 is jump-only means :: AMISTD_1:def 4
 InsCode a3 is jump-only;
end;

:: deftheorem defines jump-only AMISTD_1:def 4 :
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 holds
( b3 is jump-only iff InsCode b3 is jump-only );

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-Location of c2;
let c4 be Element of the Instructions of c2;
func NIC c4,c3 -> Subset of the Instruction-Locations of a2 equals :: AMISTD_1:def 5
{ (IC (Following b1)) where B is State of a2 : ( IC b1 = a3 & b1 . a3 = a4 ) } ;
coherence
{ (IC (Following b1)) where B is State of c2 : ( IC b1 = c3 & b1 . c3 = c4 ) } is Subset of the Instruction-Locations of c2
proof
{ (IC (Following b1)) where B is State of c2 : ( IC b1 = c3 & b1 . c3 = c4 ) } c= the Instruction-Locations of c2
proof
let c5 be set ; :: according to TARSKI:def 3
assume c5 in { (IC (Following b1)) where B is State of c2 : ( IC b1 = c3 & b1 . c3 = c4 ) } ;
then ex b1 being State of c2 st
( c5 = IC (Following b1) & IC b1 = c3 & b1 . c3 = c4 ) ;
hence c5 in the Instruction-Locations of c2 ;
end;
hence { (IC (Following b1)) where B is State of c2 : ( IC b1 = c3 & b1 . c3 = c4 ) } is Subset of the Instruction-Locations of c2 ;
end;
end;

:: deftheorem defines NIC AMISTD_1: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-Location of b2
for b4 being Element of the Instructions of b2 holds NIC b4,b3 = { (IC (Following b5)) where B is State of b2 : ( IC b5 = b3 & b5 . b3 = b4 ) } ;

E6: now
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 Element of the Instructions of c2;
let c4 be Instruction-Location of c2;
let c5 be State of c2;
let c6 be FinPartState of c2;
assume E7: c6 = (IC c2),c4 --> c4,c3 ;
set c7 = c5 +* c6;
E8: IC c2 <> c4 by AMI_1:48;
E9: dom c6 = {(IC c2),c4} by E7, FUNCT_4:65;
then E10: IC c2 in dom c6 by TARSKI:def 2;
E11: IC (c5 +* c6) = (c5 +* c6) . (IC c2)
.= c6 . (IC c2) by E10, FUNCT_4:14
.= c4 by E7, E8, FUNCT_4:66 ;
c4 in dom c6 by E9, TARSKI:def 2;
then (c5 +* c6) . c4 = c6 . c4 by FUNCT_4:14
.= c3 by E7, E8, FUNCT_4:66 ;
hence IC (Following (c5 +* c6)) in NIC c3,c4 by E11;
end;

registration
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 Element of the Instructions of c2;
let c4 be Instruction-Location of c2;
cluster NIC a3,a4 -> non empty ;
coherence
not NIC c3,c4 is empty
proof
consider c5 being State of c2;
( ObjectKind (IC c2) = the Instruction-Locations of c2 & ObjectKind c4 = the Instructions of c2 ) by AMI_1:def 11, AMI_1:def 14;
then reconsider c6 = (IC c2),c4 --> c4,c3 as FinPartState of c2 by AMI_1:58;
IC (Following (c5 +* c6)) in NIC c3,c4 by E6;
hence not NIC c3,c4 is empty ;
end;
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 Element of the Instructions of c2;
func JUMP c3 -> Subset of the Instruction-Locations of a2 equals :: AMISTD_1:def 6
 meet { (NIC a3,b1) where B is Instruction-Location of a2 : verum } ;
coherence
meet { (NIC c3,b1) where B is Instruction-Location of c2 : verum } is Subset of the Instruction-Locations of c2
proof
set c4 = { (NIC c3,b1) where B is Instruction-Location of c2 : verum } ;
{ (NIC c3,b1) where B is Instruction-Location of c2 : verum } c= bool the Instruction-Locations of c2
proof
let c5 be set ; :: according to TARSKI:def 3
assume c5 in { (NIC c3,b1) where B is Instruction-Location of c2 : verum } ;
then ex b1 being Instruction-Location of c2 st c5 = NIC c3,b1 ;
hence c5 in bool the Instruction-Locations of c2 ;
end;
then reconsider c5 = { (NIC c3,b1) where B is Instruction-Location of c2 : verum } as Subset-Family of the Instruction-Locations of c2 ;
meet c5 c= the Instruction-Locations of c2 ;
hence meet { (NIC c3,b1) where B is Instruction-Location of c2 : verum } is Subset of the Instruction-Locations of c2 ;
end;
end;

:: deftheorem defines JUMP AMISTD_1: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 Element of the Instructions of b2 holds JUMP b3 = meet { (NIC b3,b4) where B is Instruction-Location of b2 : verum } ;

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-Location of c2;
func SUCC c3 -> Subset of the Instruction-Locations of a2 equals :: AMISTD_1:def 7
 union { ((NIC b1,a3) \ (JUMP b1)) where B is Element of the Instructions of a2 : verum } ;
coherence
union { ((NIC b1,c3) \ (JUMP b1)) where B is Element of the Instructions of c2 : verum } is Subset of the Instruction-Locations of c2
proof
set c4 = { ((NIC b1,c3) \ (JUMP b1)) where B is Element of the Instructions of c2 : verum } ;
{ ((NIC b1,c3) \ (JUMP b1)) where B is Element of the Instructions of c2 : verum } c= bool the Instruction-Locations of c2
proof
let c5 be set ; :: according to TARSKI:def 3
assume c5 in { ((NIC b1,c3) \ (JUMP b1)) where B is Element of the Instructions of c2 : verum } ;
then ex b1 being Element of the Instructions of c2 st c5 = (NIC b1,c3) \ (JUMP b1) ;
hence c5 in bool the Instruction-Locations of c2 ;
end;
then reconsider c5 = { ((NIC b1,c3) \ (JUMP b1)) where B is Element of the Instructions of c2 : verum } as Subset-Family of the Instruction-Locations of c2 ;
union c5 c= the Instruction-Locations of c2 ;
hence union { ((NIC b1,c3) \ (JUMP b1)) where B is Element of the Instructions of c2 : verum } is Subset of the Instruction-Locations of c2 ;
end;
end;

:: deftheorem defines SUCC AMISTD_1:def 7 :
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-Location of b2 holds SUCC b3 = union { ((NIC b4,b3) \ (JUMP b4)) where B is Element of the Instructions of b2 : verum } ;

theorem E7: :: AMISTD_1:14
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 Element of the Instructions of b2 holds
( ( ( for b4 being Instruction-Location of b2 holds NIC b3,b4 = {b4} ) ) implies ( the Instruction-Locations of b2 is trivial or JUMP 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 Element of the Instructions of c2;
given c4, c5 being Element of the Instruction-Locations of c2 such that E8: c4 <> c5 ; :: according to YELLOW_8:def 1
assume E9: for b1 being Instruction-Location of c2 holds NIC c3,b1 = {b1} ;
set c6 = { (NIC c3,b1) where B is Instruction-Location of c2 : verum } ;
assume not JUMP c3 is empty ;
then not meet { (NIC c3,b1) where B is Instruction-Location of c2 : verum } is empty ;
then consider c7 being set such that
E10: c7 in meet { (NIC c3,b1) where B is Instruction-Location of c2 : verum } by XBOOLE_0:def 1;
( NIC c3,c4 = {c4} & NIC c3,c5 = {c5} ) by E9;
then ( {c4} in { (NIC c3,b1) where B is Instruction-Location of c2 : verum } & {c5} in { (NIC c3,b1) where B is Instruction-Location of c2 : verum } ) ;
then ( c7 in {c4} & c7 in {c5} ) by E10, SETFAM_1:def 1;
then ( c7 = c4 & c7 = c5 ) by TARSKI:def 1;
hence not verum by E8;
end;

theorem E8: :: AMISTD_1:15
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 Instruction-Location of b2
for b4 being Instruction of b2 holds
( b4 is halting implies NIC b4,b3 = {b3} )
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 Instruction-Location of c2;
let c4 be Instruction of c2;
assume E9: for b1 being State of c2 holds Exec c4,b1 = b1 ; :: according to AMI_1:def 8
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10
let c5 be set ;
assume c5 in NIC c4,c3 ;
then consider c6 being State of c2 such that
E10: ( c5 = IC (Following c6) & IC c6 = c3 & c6 . c3 = c4 ) ;
c5 = IC (Exec (CurInstr c6),c6) by E10
.= IC (Exec (c6 . (IC c6)),c6)
.= c3 by E9, E10 ;
hence c5 in {c3} by TARSKI:def 1;
end;
let c5 be set ; :: according to TARSKI:def 3
assume E10: c5 in {c3} ;
consider c6 being State of c2;
( ObjectKind (IC c2) = the Instruction-Locations of c2 & ObjectKind c3 = the Instructions of c2 ) by AMI_1:def 11, AMI_1:def 14;
then reconsider c7 = (IC c2),c3 --> c3,c4 as FinPartState of c2 by AMI_1:58;
set c8 = c6 +* c7;
E11: dom c7 = {(IC c2),c3} by FUNCT_4:65;
then E12: IC c2 in dom c7 by TARSKI:def 2;
E13: c3 in dom c7 by E11, TARSKI:def 2;
E14: IC c2 <> c3 by AMI_1:48;
E15: (c6 +* c7) . (IC c2) = c7 . (IC c2) by E12, FUNCT_4:14
.= c3 by E14, FUNCT_4:66 ;
E16: (c6 +* c7) . (IC (c6 +* c7)) = (c6 +* c7) . ((c6 +* c7) . (IC c2))
.= c7 . c3 by E13, E15, FUNCT_4:14
.= c4 by E14, FUNCT_4:66 ;
IC (Following (c6 +* c7)) = IC (Exec (CurInstr (c6 +* c7)),(c6 +* c7))
.= IC (Exec ((c6 +* c7) . (IC (c6 +* c7))),(c6 +* c7))
.= (Exec ((c6 +* c7) . (IC (c6 +* c7))),(c6 +* c7)) . (IC c2)
.= (c6 +* c7) . (IC c2) by E9, E16
.= c5 by E10, E15, TARSKI:def 1 ;
hence c5 in NIC c4,c3 by E6;
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, c4 be Instruction-Location of c2;
pred c3 <= c4 means :E9: :: AMISTD_1:def 8
ex b1 being non empty FinSequence of the Instruction-Locations of a2 st
( b1 /. 1 = a3 & b1 /. (len b1) = a4 & ( for b2 being Nat holds
( ( 1 <= b2 ) implies ( not b2 < len b1 or b1 /. (b2 + 1) in SUCC (b1 /. b2) ) ) ) );
reflexivity
for b1 being Instruction-Location of c2 holds
ex b2 being non empty FinSequence of the Instruction-Locations of c2 st
( b2 /. 1 = b1 & b2 /. (len b2) = b1 & ( for b3 being Nat holds
( ( 1 <= b3 ) implies ( not b3 < len b2 or b2 /. (b3 + 1) in SUCC (b2 /. b3) ) ) ) )
proof
let c5 be Instruction-Location of c2;
take <*c5*> ;
thus <*c5*> /. 1 = c5 by FINSEQ_4:25;
hence ( <*c5*> /. (len <*c5*>) = c5 & ( for b1 being Nat holds
( ( 1 <= b1 ) implies ( not b1 < len <*c5*> or <*c5*> /. (b1 + 1) in SUCC (<*c5*> /. b1) ) ) ) ) by FINSEQ_1:56;
end;
end;

:: deftheorem E9 defines <= AMISTD_1:def 8 :
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, b4 being Instruction-Location of b2 holds
( b3 <= b4 iff ex b5 being non empty FinSequence of the Instruction-Locations of b2 st
( b5 /. 1 = b3 & b5 /. (len b5) = b4 & ( for b6 being Nat holds
( ( 1 <= b6 ) implies ( not b6 < len b5 or b5 /. (b6 + 1) in SUCC (b5 /. b6) ) ) ) ) );

theorem :: AMISTD_1: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, b4, b5 being Instruction-Location of b2 holds
( ( b3 <= b4 & b4 <= b5 ) implies ( b3 <= b5 ) )
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, c4, c5 be Instruction-Location of c2;
given c6 being non empty FinSequence of the Instruction-Locations of c2 such that E10: c6 /. 1 = c3 and
E11: c6 /. (len c6) = c4 and
E12: for b1 being Nat holds
( ( 1 <= b1 ) implies ( not b1 < len c6 or c6 /. (b1 + 1) in SUCC (c6 /. b1) ) ) ; :: according to AMISTD_1:def 8
given c7 being non empty FinSequence of the Instruction-Locations of c2 such that E13: c7 /. 1 = c4 and
E14: c7 /. (len c7) = c5 and
E15: for b1 being Nat holds
( ( 1 <= b1 ) implies ( not b1 < len c7 or c7 /. (b1 + 1) in SUCC (c7 /. b1) ) ) ; :: according to AMISTD_1:def 8
take c6 ^' c7 ; :: according to AMISTD_1:def 8
thus (c6 ^' c7) /. 1 = c3 by E10, GRAPH_2:57;
now
per cases not ( not c7 is trivial & c7 is trivial ) ;
suppose c7 is trivial ;
then consider c8 being Instruction-Location of c2 such that
E16: c7 = <*c8*> by E2;
c6 ^' c7 = c6 by E16, GRAPH_2:60;
hence (c6 ^' c7) /. (len (c6 ^' c7)) = c5 by E11, E13, E14, E16, FINSEQ_1:56;
end;
suppose not c7 is trivial ;
hence (c6 ^' c7) /. (len (c6 ^' c7)) = c5 by E14, GRAPH_2:58;
end;
end;
end;
hence (c6 ^' c7) /. (len (c6 ^' c7)) = c5 ;
let c8 be Nat;
assume that
E16: 1 <= c8 and
E17: c8 < len (c6 ^' c7) ;
E18: 1 <= c8 + 1 by NAT_1:29;
E19: (len (c6 ^' c7)) + 1 = (len c6) + (len c7) by GRAPH_2:13;
per cases not ( not c8 < len c6 & not c8 = len c6 & not c8 > len c6 ) by XXREAL_0:1;
suppose E20: c8 < len c6 ;
then c8 + 1 <= len c6 by NAT_1:38;
then E21: (c6 ^' c7) /. (c8 + 1) = c6 /. (c8 + 1) by E18, GRAPH_2:61;
(c6 ^' c7) /. c8 = c6 /. c8 by E16, E20, GRAPH_2:61;
hence (c6 ^' c7) /. (c8 + 1) in SUCC ((c6 ^' c7) /. c8) by E12, E16, E20, E21;
end;
suppose E20: c8 = len c6 ;
then E21: (c6 ^' c7) /. c8 = c7 /. 1 by E11, E13, E16, GRAPH_2:61;
c8 + 1 < (len (c6 ^' c7)) + 1 by E17, XREAL_1:8;
then E22: 1 < len c7 by E19, E20, XREAL_1:8;
then (c6 ^' c7) /. (c8 + 1) = c7 /. (1 + 1) by E20, GRAPH_2:62;
hence (c6 ^' c7) /. (c8 + 1) in SUCC ((c6 ^' c7) /. c8) by E15, E21, E22;
end;
suppose E20: c8 > len c6 ;
then consider c9 being Nat such that
E21: (len c6) + c9 = c8 by NAT_1:28;
(len c6) + c9 > (len c6) + 0 by E20, E21;
then E22: 1 <= c9 by NAT_1:39;
E23: 1 <= c9 + 1 by NAT_1:29;
((len c6) + c9) + 1 < (len c6) + (len c7) by E17, E19, E21, XREAL_1:8;
then (len c6) + (c9 + 1) < (len c6) + (len c7) ;
then E24: c9 + 1 < len c7 by XREAL_1:8;
c9 <= c9 + 1 by NAT_1:29;
then c9 < len c7 by E24, XXREAL_0:2;
then E25: (c6 ^' c7) /. c8 = c7 /. (c9 + 1) by E21, E22, GRAPH_2:62;
(c6 ^' c7) /. (c8 + 1) = (c6 ^' c7) /. ((len c6) + (c9 + 1)) by E21
.= c7 /. ((c9 + 1) + 1) by E23, E24, GRAPH_2:62 ;
hence (c6 ^' c7) /. (c8 + 1) in SUCC ((c6 ^' c7) /. c8) by E15, E23, E24, E25;
end;
end;
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;
attr a2 is InsLoc-antisymmetric means :: AMISTD_1:def 9
for b1, b2 being Instruction-Location of a2 holds
( ( b1 <= b2 & b2 <= b1 ) implies ( b1 = b2 ) );
end;

:: deftheorem defines InsLoc-antisymmetric AMISTD_1:def 9 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1 holds
( b2 is InsLoc-antisymmetric iff for b3, b4 being Instruction-Location of b2 holds
( ( b3 <= b4 & b4 <= b3 ) implies ( b3 = b4 ) ) );

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite AMI-Struct of c1;
attr a2 is standard means :E10: :: AMISTD_1:def 10
ex b1 being Function of NAT ,the Instruction-Locations of a2 st
( b1 is bijective & ( for b2, b3 being Nat holds
( b2 <= b3 iff b1 . b2 <= b1 . b3 ) ) );
end;

:: deftheorem E10 defines standard AMISTD_1:def 10 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite AMI-Struct of b1 holds
( b2 is standard iff ex b3 being Function of NAT ,the Instruction-Locations of b2 st
( b3 is bijective & ( for b4, b5 being Nat holds
( b4 <= b5 iff b3 . b4 <= b3 . b5 ) ) ) );

theorem E11: :: AMISTD_1: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, b4 being Function of NAT ,the Instruction-Locations of b2 holds
( ( b3 is bijective & ( for b5, b6 being Nat holds
( b5 <= b6 iff b3 . b5 <= b3 . b6 ) ) & b4 is bijective & ( for b5, b6 being Nat holds
( b5 <= b6 iff b4 . b5 <= b4 . b6 ) ) ) implies ( b3 = b4 ) )
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, c4 be Function of NAT ,the Instruction-Locations of c2;
assume that
E12: c3 is bijective and
E13: for b1, b2 being Nat holds
( b1 <= b2 iff c3 . b1 <= c3 . b2 ) and
E14: c4 is bijective and
E15: for b1, b2 being Nat holds
( b1 <= b2 iff c4 . b1 <= c4 . b2 ) ;
defpred S1[ Nat] means c3 . a1 <> c4 . a1;
assume c3 <> c4 ;
then E16: ex b1 being Nat st
S1[b1] by FUNCT_2:113;
consider c5 being Nat such that
E17: S1[c5] and
E18: for b1 being Nat holds
( S1[b1] implies c5 <= b1 ) from NAT_1:sch 5(E16);
 ( c3 is onto & c4 is onto ) by E12, E14, FUNCT_2:def 4;
then E19: ( rng c3 = the Instruction-Locations of c2 & rng c4 = the Instruction-Locations of c2 ) by FUNCT_2:def 3;
then consider c6 being set such that
E20: ( c6 in dom c4 & c3 . c5 = c4 . c6 ) by FUNCT_1:def 5;
reconsider c7 = c6 as Nat by E20;
consider c8 being set such that
E21: ( c8 in dom c3 & c4 . c5 = c3 . c8 ) by E19, FUNCT_1:def 5;
reconsider c9 = c8 as Nat by E21;
E22: ( c3 is one-to-one & c4 is one-to-one ) by E12, E14, FUNCT_2:def 4;
E23: ( dom c3 = NAT & dom c4 = NAT ) by FUNCT_2:def 1;
per cases not ( not ( c9 <= c5 & c7 <= c5 ) & not ( c5 <= c9 & c7 <= c5 ) & not ( c9 <= c5 & c5 <= c7 ) & not ( c5 <= c9 & c5 <= c7 ) ) ;
suppose E24: ( c9 <= c5 & c7 <= c5 ) ;
then c4 . c7 <= c4 . c5 by E15;
then c5 <= c9 by E13, E20, E21;
hence not verum by E17, E21, E24, XXREAL_0:1;
end;
suppose E24: ( c5 <= c9 & c7