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

registration
cluster non trivial set ;
existence
not for b1 being FinSequence holds b1 is trivial
proof
take <*0,0*> ;
thus not <*0,0*> is trivial ;
end;
end;

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;
rng c2 c= c1 by FINSEQ_1:def 4;
hence 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 ; :: uses 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 K338(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, c2 be set ;
cluster a1 .--> a2 -> trivial with_non-empty_elements ;
coherence
c1 .--> c2 is trivial
proof
c1 .--> c2 = {[c1,c2]} by AMI_1:19;
hence c1 .--> c2 is trivial ;
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 E3: :: AMISTD_1:5
for b1 being non empty set
for b2 being non empty FinSequence of b1
for b3 being FinSequence of b1 holds (b2 ^' b3) /. 1 = b2 /. 1
proof
let c1 be non empty set ;
let c2 be non empty FinSequence of c1;
let c3 be FinSequence of c1;
E4: 1 in dom c2 by FINSEQ_5:6;
E5: 1 in dom (c2 ^ (2,(len c3) -cut c3)) by FINSEQ_5:6;
thus (c2 ^' c3) /. 1 = (c2 ^ (2,(len c3) -cut c3)) /. 1 by GRAPH_2:def 2
.= (c2 ^ (2,(len c3) -cut c3)) . 1 by E5, FINSEQ_4:def 4
.= c2 . 1 by E4, FINSEQ_1:def 7
.= c2 /. 1 by E4, FINSEQ_4:def 4 ;
end;

theorem E4: :: AMISTD_1:6
for b1 being non empty set
for b2 being FinSequence of b1
for b3 being non trivial FinSequence of b1 holds (b2 ^' b3) /. (len (b2 ^' b3)) = b3 /. (len b3)
proof
let c1 be non empty set ;
let c2 be FinSequence of c1;
let c3 be non trivial FinSequence of c1;
2 <= len c3 by REALSET1:13;
then E5: 1 < len c3 by XREAL_1:2;
0 <= len c2 by NAT_1:18;
then E6: 1 + 0 < (len c2) + (len c3) by E5, XREAL_1:10;
(len (c2 ^' c3)) + 1 = (len c2) + (len c3) by GRAPH_2:13;
then 1 <= len (c2 ^' c3) by E6, NAT_1:38;
hence (c2 ^' c3) /. (len (c2 ^' c3)) = (c2 ^' c3) . (len (c2 ^' c3)) by FINSEQ_4:24
.= c3 . (len c3) by E5, GRAPH_2:16
.= c3 /. (len c3) by E5, FINSEQ_4:24 ;

end;

theorem E5: :: AMISTD_1:7
for b1 being FinSequence holds b1 ^' {} = b1
proof
let c1 be FinSequence;
len {} = 0 by FINSEQ_1:25;
then E6: 2 > (len {} ) + 1 ;
thus c1 ^' {} = c1 ^ (2,(len {} ) -cut {} ) by GRAPH_2:def 2
.= c1 ^ {} by E6, GRAPH_2:def 1
.= c1 by FINSEQ_1:47 ;
end;

theorem E6: :: AMISTD_1:8
for b1 being set
for b2 being FinSequence holds b2 ^' <*b1*> = b2
proof
let c1 be set ;
let c2 be FinSequence;
len <*c1*> = 1 by FINSEQ_1:56;
then 0 + (1 + 1) = (len (2,(len <*c1*>) -cut <*c1*>)) + 2 by GRAPH_2:def 1;
then 0 = len (2,(len <*c1*>) -cut <*c1*>) ;
then 2,(len <*c1*>) -cut <*c1*> = {} by FINSEQ_1:25;
hence c2 ^' <*c1*> = c2 ^ {} by GRAPH_2:def 2
.= c2 by FINSEQ_1:47 ;

end;

theorem E7: :: AMISTD_1:9
for b1 being non empty set
for b2 being Nat
for b3, b4 being FinSequence of b1 holds
( ( 1 <= b2 & b2 <= len b3 ) implies ( (b3 ^' b4) /. b2 = b3 /. b2 ) )
proof
let c1 be non empty set ;
let c2 be Nat;
let c3, c4 be FinSequence of c1;
assume that E8: 1 <= c2
and E9: c2 <= len c3 ;
per cases not ( not c4 = {} & not c4 <> {} ) ;
suppose c4 = {} ;
hence (c3 ^' c4) /. c2 = c3 /. c2 by E5;
end;
suppose E10: c4 <> {} ;
then E11: (len (c3 ^' c4)) + 1 = (len c3) + (len c4) by GRAPH_2:13;
len c4 <> 0 by E10, FINSEQ_1:25;
then 0 < len c4 by NAT_1:19;
then (len c3) + 0 < (len c3) + (len c4) by XREAL_1:8;
then c2 < (len (c3 ^' c4)) + 1 by E9, E11, XREAL_1:2;
then c2 <= len (c3 ^' c4) by NAT_1:38;
hence (c3 ^' c4) /. c2 = (c3 ^' c4) . c2 by E8, FINSEQ_4:24
.= c3 . c2 by E8, E9, GRAPH_2:14
.= c3 /. c2 by E8, E9, FINSEQ_4:24 ;

end;
end;
end;

theorem E8: :: AMISTD_1:10
for b1 being non empty set
for b2 being Nat
for b3, b4 being FinSequence of b1 holds
( ( 1 <= b2 ) implies ( not b2 < len b4 or (b3 ^' b4) /. ((len b3) + b2) = b4 /. (b2 + 1) ) )
proof
let c1 be non empty set ;
let c2 be Nat;
let c3, c4 be FinSequence of c1;
assume that E9: 1 <= c2
and E10: c2 < len c4 ;
0 <= len c3 by NAT_1:18;
then E11: 0 + 1 <= (len c3) + c2 by E9, XREAL_1:9;
E12: now
per cases not ( not c4 <> {} & not c4 = {} ) ;
suppose c4 <> {} ;
then E13: (len (c3 ^' c4)) + 1 = (len c3) + (len c4) by GRAPH_2:13;
(len c3) + c2 < (len c3) + (len c4) by E10, XREAL_1:8;
hence (len c3) + c2 <= len (c3 ^' c4) by E13, NAT_1:38;
end;
suppose c4 = {} ;
then len c4 = 0 by FINSEQ_1:25;
hence (len c3) + c2 <= len (c3 ^' c4) by E10, NAT_1:18;
end;
end;
end;
0 <= c2 by NAT_1:18;
then E13: 0 + 1 <= c2 + 1 by XREAL_1:8;
E14: c2 + 1 <= len c4 by E10, NAT_1:38;
thus (c3 ^' c4) /. ((len c3) + c2) = (c3 ^' c4) . ((len c3) + c2) by E11, E12, FINSEQ_4:24
.= c4 . (c2 + 1) by E9, E10, GRAPH_2:15
.= c4 /. (c2 + 1) by E13, E14, FINSEQ_4:24 ;
end;

theorem E9: :: 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;
E10: dom (the Instruction-Locations of c2 --> c3) = the Instruction-Locations of c2 by FUNCOP_1:19;
E11: dom c4 = the carrier of c2 by AMI_3:36;
then E12: 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 E13: c7 in dom (the Instruction-Locations of c2 --> c3) ;
then E14: (the Instruction-Locations of c2 --> c3) . c7 = c3 by E10, FUNCOP_1:13;
reconsider c8 = c7 as Instruction-Location of c2 by E13, 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 E14;
end;
then the Instruction-Locations of c2 --> c3 in sproduct the Object-Kind of c2 by E10, E11, E12, 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 ; :: uses 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 ) ; :: uses 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;

E10: 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 E11: c5 = c3 .--> c4 ;
let c6, c7 be State of c2; :: uses AMI_1:def 25
assume that E12: c5 c= c6
and E13: c5 c= c7 ;
let c8 be Nat;
E14: dom c5 = {c3} by E11, CQC_LANG:5;
E15: for b1 being Function holds
( c5 c= b1 implies b1 . c3 = c4 )
proof
let c9 be Function;
assume E16: c5 c= c9 ;
c3 in {c3} by TARSKI:def 1;
hence c9 . c3 = c5 . c3 by E14, E16, GRFUNC_1:8
.= c4 by E11, CQC_LANG:6 ;

end;
set c9 = ((Computation c6) . c8) | (dom c5);
set c10 = ((Computation c7) . c8) | (dom c5);
E16: {c3} c= the carrier of c2 ;
then {c3} c= dom ((Computation c6) . c8) by AMI_3:36;
then E17: dom (((Computation c6) . c8) | (dom c5)) = {c3} by E14, RELAT_1:91;
{c3} c= dom ((Computation c7) . c8) by E16, AMI_3:36;
then E18: dom (((Computation c7) . c8) | (dom c5)) = {c3} by E14, 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 E19: c11 in {c3} ;
then E20: c11 = c3 by TARSKI:def 1;
E21: c5 c= (Computation c6) . c8 by E11, E12, AMI_3:38;
E22: c5 c= (Computation c7) . c8 by E11, E13, AMI_3:38;
thus (((Computation c6) . c8) | (dom c5)) . c11 = ((Computation c6) . c8) . c11 by E14, E19, FUNCT_1:72
.= c4 by E15, E20, E21
.= ((Computation c7) . c8) . c11 by E15, E20, E22
.= (((Computation c7) . c8) | (dom c5)) . c11 by E14, E19, FUNCT_1:72 ;
end;
hence ((Computation c6) . c8) | (dom c5) = ((Computation c7) . c8) | (dom c5) by E17, E18, 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 E10;
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 E10;

theorem E11: :: 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 ; :: uses AMI_1:def 27
thus ( not c3 .--> c4 is empty & c3 .--> c4 is autonomic ) by E10;
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 E11;
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 a4,a3 -> 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 ; :: uses 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 ) } ;

E12: 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 E13: c6 = (IC c2),c4 --> c4,c3 ;
set c7 = c5 +* c6;
E14: IC c2 <> c4 by AMI_1:48;
E15: dom c6 = {(IC c2),c4} by E13, FUNCT_4:65;
then E16: IC c2 in dom c6 by TARSKI:def 2;
E17: IC (c5 +* c6) = (c5 +* c6) . (IC c2)
.= c6 . (IC c2) by E16, FUNCT_4:14
.= c4 by E13, E14, FUNCT_4:66 ;
c4 in dom c6 by E15, TARSKI:def 2;
then (c5 +* c6) . c4 = c6 . c4 by FUNCT_4:14
.= c3 by E13, E14, FUNCT_4:66 ;
hence IC (Following (c5 +* c6)) in NIC c3,c4 by E17;
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 E12;
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 a3 -> 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 ; :: uses 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 a3 -> 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 ; :: uses 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 E13: :: 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 E14: c4 <> c5 ; :: uses YELLOW_8:def 1
assume E15: 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
E16: 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 E15;
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 E16, SETFAM_1:def 1;
then ( c7 = c4 & c7 = c5 ) by TARSKI:def 1;
hence not verum by E14;
end;

theorem E14: :: 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 E15: for b1 being State of c2 holds Exec c4,b1 = b1 ; :: uses AMI_1:def 8
hereby :: uses 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
E16: ( c5 = IC (Following c6) & IC c6 = c3 & c6 . c3 = c4 ) ;
c5 = IC (Exec (CurInstr c6),c6) by E16
.= IC (Exec (c6 . (IC c6)),c6)
.= c3 by E15, E16 ;
hence c5 in {c3} by TARSKI:def 1;
end; let c5 be set ; :: uses TARSKI:def 3
assume E16: 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;
E17: dom c7 = {(IC c2),c3} by FUNCT_4:65;
then E18: IC c2 in dom c7 by TARSKI:def 2;
E19: c3 in dom c7 by E17, TARSKI:def 2;
E20: IC c2 <> c3 by AMI_1:48;
E21: (c6 +* c7) . (IC c2) = c7 . (IC c2) by E18, FUNCT_4:14
.= c3 by E20, FUNCT_4:66 ;
E22: (c6 +* c7) . (IC (c6 +* c7)) = (c6 +* c7) . ((c6 +* c7) . (IC c2))
.= c7 . c3 by E19, E21, FUNCT_4:14
.= c4 by E20, 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 E15, E22
.= c5 by E16, E21, TARSKI:def 1 ;
hence c5 in NIC c4,c3 by E12;
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 a3 <= a4 means :E15: :: 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 E15 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 E16: c6 /. 1 = c3
and E17: c6 /. (len c6) = c4
and E18: for b1 being Nat holds
( ( 1 <= b1 ) implies ( not b1 < len c6 or c6 /. (b1 + 1) in SUCC (c6 /. b1) ) ) ; :: uses AMISTD_1:def 8
given c7 being non empty FinSequence of the Instruction-Locations of c2 such that E19: c7 /. 1 = c4
and E20: c7 /. (len c7) = c5
and E21: for b1 being Nat holds
( ( 1 <= b1 ) implies ( not b1 < len c7 or c7 /. (b1 + 1) in SUCC (c7 /. b1) ) ) ; :: uses AMISTD_1:def 8
take c6 ^' c7 ; :: uses AMISTD_1:def 8
thus (c6 ^' c7) /. 1 = c3 by E16, E3;
now
per cases not ( not c7 is trivial & c7 is trivial ) ;
suppose c7 is trivial ;
<