:: AMI_6 semantic presentation

theorem E1: :: AMI_6:1
for b1 being Data-Location holds
not b1 in the Instruction-Locations of SCM
proof
let c1 be Data-Location ;
c1 in SCM-Data-Loc by AMI_3:def 2;
hence not c1 in the Instruction-Locations of SCM by AMI_3:def 1, AMI_5:33, XBOOLE_0:3;
end;

theorem E2: :: AMI_6:2
SCM-Data-Loc <> the Instruction-Locations of SCM
proof
assume E3: not SCM-Data-Loc <> the Instruction-Locations of SCM ;
consider c1 being Element of SCM-Instr-Loc ;
c1 in SCM-Instr-Loc ;
hence not verum by E3, AMI_2:12, AMI_3:def 1;
end;

theorem E3: :: AMI_6:3
for b1 being Object of SCM holds
not ( not b1 = IC SCM & not b1 in the Instruction-Locations of SCM & not b1 is Data-Location )
proof
let c1 be Object of SCM ;
( c1 in {(IC SCM )} \/ SCM-Data-Loc or c1 in SCM-Instr-Loc ) by AMI_5:23, XBOOLE_0:def 2;
then not ( not c1 in {(IC SCM )} & not c1 in SCM-Data-Loc & not c1 in SCM-Instr-Loc ) by XBOOLE_0:def 2;
hence not ( not c1 = IC SCM & not c1 in the Instruction-Locations of SCM & not c1 is Data-Location ) by AMI_3:def 1, AMI_3:def 2, TARSKI:def 1;
end;

theorem E4: :: AMI_6:4
for b1, b2 being Instruction-Location of SCM holds
not ( b1 <> b2 & not Next b1 <> Next b2 )
proof
let c1, c2 be Instruction-Location of SCM ;
assume E5: ( c1 <> c2 & Next c1 = Next c2 ) ;
consider c3 being Element of SCM-Instr-Loc such that
E6: ( c3 = c1 & Next c1 = Next c3 ) by AMI_3:def 11;
consider c4 being Element of SCM-Instr-Loc such that
E7: ( c4 = c2 & Next c2 = Next c4 ) by AMI_3:def 11;
( Next c3 = c3 + 2 & Next c4 = c4 + 2 ) by AMI_2:def 15;
hence not verum by E5, E6, E7, XCMPLX_1:2;
end;

theorem E5: :: AMI_6:5
for b1 being Data-Location
for b2, b3 being State of SCM holds
( b2,b3 equal_outside the Instruction-Locations of SCM implies b2 . b1 = b3 . b1 )
proof
let c1 be Data-Location ;
let c2, c3 be State of SCM ;
set c4 = the Instruction-Locations of SCM ;
assume E6: c2,c3 equal_outside the Instruction-Locations of SCM ;
E7: dom c2 = the carrier of SCM by AMI_3:36;
E8: dom c3 = the carrier of SCM by AMI_3:36;
E9: not c1 in the Instruction-Locations of SCM by E1;
then c1 in (dom c2) \ the Instruction-Locations of SCM by E7, XBOOLE_0:def 4;
then E10: c1 in (dom c2) /\ ((dom c2) \ the Instruction-Locations of SCM ) by E7, XBOOLE_0:def 3;
c1 in (dom c3) \ the Instruction-Locations of SCM by E8, E9, XBOOLE_0:def 4;
then E11: c1 in (dom c3) /\ ((dom c3) \ the Instruction-Locations of SCM ) by E8, XBOOLE_0:def 3;
thus c2 . c1 = (c2 | ((dom c2) \ the Instruction-Locations of SCM )) . c1 by E10, FUNCT_1:71
.= (c3 | ((dom c3) \ the Instruction-Locations of SCM )) . c1 by E6, FUNCT_7:def 2
.= c3 . c1 by E11, FUNCT_1:71 ;
end;

theorem E6: :: AMI_6:6
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, b4 being State of b2
for b5 being Instruction-Location of b2
for b6 being Element of ObjectKind (IC b2)
for b7 being Element of ObjectKind b5 holds
( ( b6 = b5 & b4 = b3 +* ((IC b2),b5 --> b6,b7) ) implies ( ( b4 . b5 = b7 & IC b4 = b5 & IC (Following b4) = (Exec (b4 . (IC b4)),b4) . (IC b2) ) ) )
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, c4 be State of c2;
let c5 be Instruction-Location of c2;
let c6 be Element of ObjectKind (IC c2);
let c7 be Element of ObjectKind c5;
assume that E7: c6 = c5
and E8: c4 = c3 +* ((IC c2),c5 --> c6,c7) ;
E9: dom ((IC c2),c5 --> c6,c7) = {(IC c2),c5} by FUNCT_4:65;
then E10: IC c2 in dom ((IC c2),c5 --> c6,c7) by TARSKI:def 2;
E11: IC c2 <> c5 by AMI_1:48;
c5 in dom ((IC c2),c5 --> c6,c7) by E9, TARSKI:def 2;
hence c4 . c5 = ((IC c2),c5 --> c6,c7) . c5 by E8, FUNCT_4:14
.= c7 by E11, FUNCT_4:66 ;

thus IC c4 = c4 . (IC c2) by AMI_1:def 15
.= ((IC c2),c5 --> c6,c7) . (IC c2) by E8, E10, FUNCT_4:14
.= c5 by E7, E11, FUNCT_4:66 ;
thus IC (Following c4) = IC (Exec (CurInstr c4),c4) by AMI_1:def 18
.= IC (Exec (c4 . (IC c4)),c4) by AMI_1:def 17
.= (Exec (c4 . (IC c4)),c4) . (IC c2) by AMI_1:def 15 ;
end;

E7: for b1, b2 being set holds
( b1 in dom <*b2*> implies b1 = 1 )
proof
let c1, c2 be set ;
assume c1 in dom <*c2*> ;
then c1 in Seg 1 by FINSEQ_1:def 8;
hence c1 = 1 by FINSEQ_1:4, TARSKI:def 1;
end;

E8: for b1, b2, b3 being set holds
not ( b1 in dom <*b2,b3*> & not b1 = 1 & not b1 = 2 )
proof
let c1, c2, c3 be set ;
assume c1 in dom <*c2,c3*> ;
then c1 in Seg 2 by FINSEQ_3:29;
hence not ( not c1 = 1 & not c1 = 2 ) by FINSEQ_1:4, TARSKI:def 2;
end;

E9: for b1 being InsType of SCM holds
not ( not b1 = 0 & not b1 = 1 & not b1 = 2 & not b1 = 3 & not b1 = 4 & not b1 = 5 & not b1 = 6 & not b1 = 7 & not b1 = 8 )
proof
let c1 be InsType of SCM ;
c1 in Segm 9 by AMI_3:def 1;
then reconsider c2 = c1 as Nat ;
not ( not c2 = 0 & not c2 < 8 + 1 ) by AMI_3:def 1, GR_CY_1:10;
then ( c2 = 0 or c2 <= 8 ) by NAT_1:38;
hence not ( not c1 = 0 & not c1 = 1 & not c1 = 2 & not c1 = 3 & not c1 = 4 & not c1 = 5 & not c1 = 6 & not c1 = 7 & not c1 = 8 ) by CQC_THE1:9;
end;

theorem E10: :: AMI_6:7
AddressPart (halt SCM ) = {}
proof
thus AddressPart (halt SCM ) = (halt SCM ) `2
.= {} by AMI_3:71, MCART_1:def 2 ;
end;

theorem E11: :: AMI_6:8
for b1, b2 being Data-Location holds AddressPart (b1 := b2) = <*b1,b2*>
proof
let c1, c2 be Data-Location ;
thus AddressPart (c1 := c2) = (c1 := c2) `2
.= [1,<*c1,c2*>] `2 by AMI_3:def 3
.= <*c1,c2*> by MCART_1:def 2 ;
end;

theorem E12: :: AMI_6:9
for b1, b2 being Data-Location holds AddressPart (AddTo b1,b2) = <*b1,b2*>
proof
let c1, c2 be Data-Location ;
thus AddressPart (AddTo c1,c2) = (AddTo c1,c2) `2
.= [2,<*c1,c2*>] `2 by AMI_3:def 4
.= <*c1,c2*> by MCART_1:def 2 ;
end;

theorem E13: :: AMI_6:10
for b1, b2 being Data-Location holds AddressPart (SubFrom b1,b2) = <*b1,b2*>
proof
let c1, c2 be Data-Location ;
thus AddressPart (SubFrom c1,c2) = (SubFrom c1,c2) `2
.= [3,<*c1,c2*>] `2 by AMI_3:def 5
.= <*c1,c2*> by MCART_1:def 2 ;
end;

theorem E14: :: AMI_6:11
for b1, b2 being Data-Location holds AddressPart (MultBy b1,b2) = <*b1,b2*>
proof
let c1, c2 be Data-Location ;
thus AddressPart (MultBy c1,c2) = (MultBy c1,c2) `2
.= [4,<*c1,c2*>] `2 by AMI_3:def 6
.= <*c1,c2*> by MCART_1:def 2 ;
end;

theorem E15: :: AMI_6:12
for b1, b2 being Data-Location holds AddressPart (Divide b1,b2) = <*b1,b2*>
proof
let c1, c2 be Data-Location ;
thus AddressPart (Divide c1,c2) = (Divide c1,c2) `2
.= [5,<*c1,c2*>] `2 by AMI_3:def 7
.= <*c1,c2*> by MCART_1:def 2 ;
end;

theorem E16: :: AMI_6:13
for b1 being Instruction-Location of SCM holds AddressPart (goto b1) = <*b1*>
proof
let c1 be Instruction-Location of SCM ;
thus AddressPart (goto c1) = (goto c1) `2
.= [6,<*c1*>] `2 by AMI_3:def 8
.= <*c1*> by MCART_1:def 2 ;
end;

theorem E17: :: AMI_6:14
for b1 being Data-Location
for b2 being Instruction-Location of SCM holds AddressPart (b1 =0_goto b2) = <*b2,b1*>
proof
let c1 be Data-Location ;
let c2 be Instruction-Location of SCM ;
thus AddressPart (c1 =0_goto c2) = (c1 =0_goto c2) `2
.= [7,<*c2,c1*>] `2 by AMI_3:def 9
.= <*c2,c1*> by MCART_1:def 2 ;
end;

theorem E18: :: AMI_6:15
for b1 being Data-Location
for b2 being Instruction-Location of SCM holds AddressPart (b1 >0_goto b2) = <*b2,b1*>
proof
let c1 be Data-Location ;
let c2 be Instruction-Location of SCM ;
thus AddressPart (c1 >0_goto c2) = (c1 >0_goto c2) `2
.= [8,<*c2,c1*>] `2 by AMI_3:def 10
.= <*c2,c1*> by MCART_1:def 2 ;
end;

theorem E19: :: AMI_6:16
for b1 being InsType of SCM holds
( b1 = 0 implies AddressParts b1 = {0} )
proof
let c1 be InsType of SCM ;
assume E20: c1 = 0 ;
hereby :: uses TARSKI:def 3,XBOOLE_0:def 10
let c2 be set ;
assume c2 in AddressParts c1 ;
then consider c3 being Instruction of SCM such that
E21: c2 = AddressPart c3
and E22: InsCode c3 = c1 ;
c3 = halt SCM by E20, E22, AMI_5:46;
hence c2 in {0} by E21, E10, TARSKI:def 1;
end; let c2 be set ; :: uses TARSKI:def 3
assume c2 in {0} ;
then c2 = 0 by TARSKI:def 1;
hence c2 in AddressParts c1 by E20, E10, AMI_5:37;
end;

registration
let c1 be InsType of SCM ;
cluster AddressParts a1 -> non empty ;
coherence
not AddressParts c1 is empty
proof
consider c2, c3 being Data-Location , c4 being Instruction-Location of SCM ;
E20: not ( not c1 = 0 & not c1 = 1 & not c1 = 2 & not c1 = 3 & not c1 = 4 & not c1 = 5 & not c1 = 6 & not c1 = 7 & not c1 = 8 ) by E9;
( InsCode (halt SCM ) = 0 & InsCode (c2 := c3) = 1 & InsCode (AddTo c2,c3) = 2 & InsCode (SubFrom c2,c3) = 3 & InsCode (MultBy c2,c3) = 4 & InsCode (Divide c2,c3) = 5 & InsCode (goto c4) = 6 & InsCode (c2 =0_goto c4) = 7 & InsCode (c2 >0_goto c4) = 8 ) by AMI_5:37, AMI_5:38, AMI_5:39, AMI_5:40, AMI_5:41, AMI_5:42, AMI_5:43, AMI_5:44, AMI_5:45;
then not ( not AddressPart (halt SCM ) in AddressParts c1 & not AddressPart (c2 := c3) in AddressParts c1 & not AddressPart (AddTo c2,c3) in AddressParts c1 & not AddressPart (SubFrom c2,c3) in AddressParts c1 & not AddressPart (MultBy c2,c3) in AddressParts c1 & not AddressPart (Divide c2,c3) in AddressParts c1 & not AddressPart (goto c4) in AddressParts c1 & not AddressPart (c2 =0_goto c4) in AddressParts c1 & not AddressPart (c2 >0_goto c4) in AddressParts c1 ) by E20;
hence not AddressParts c1 is empty ;
end;
end;

theorem E20: :: AMI_6:17
for b1 being InsType of SCM holds
( b1 = 1 implies dom (PA (AddressParts b1)) = {1,2} )
proof
let c1 be InsType of SCM ;
assume E21: c1 = 1 ;
consider c2, c3 being Data-Location ;
E22: AddressPart (c2 := c3) = <*c2,c3*> by E11;
hereby :: uses TARSKI:def 3,XBOOLE_0:def 10
let c4 be set ;
assume E23: c4 in dom (PA (AddressParts c1)) ;
InsCode (c2 := c3) = 1 by AMI_5:38;
then AddressPart (c2 := c3) in AddressParts c1 by E21;
then c4 in dom (AddressPart (c2 := c3)) by E23, AMISTD_2:def 1;
hence c4 in {1,2} by E22, FINSEQ_1:4, FINSEQ_3:29;
end; let c4 be set ; :: uses TARSKI:def 3
assume E23: c4 in {1,2} ;
for b1 being Function holds
( b1 in AddressParts c1 implies c4 in dom b1 )
proof
let c5 be Function;
assume c5 in AddressParts c1 ;
then consider c6 being Instruction of SCM such that
E24: c5 = AddressPart c6
and E25: InsCode c6 = c1 ;
consider c7, c8 being Data-Location such that
E26: c6 = c7 := c8 by E21, E25, AMI_5:47;
c5 = <*c7,c8*> by E24, E26, E11;
hence c4 in dom c5 by E23, FINSEQ_1:4, FINSEQ_3:29;
end;
hence c4 in dom (PA (AddressParts c1)) by AMISTD_2:def 1;
end;

theorem E21: :: AMI_6:18
for b1 being InsType of SCM holds
( b1 = 2 implies dom (PA (AddressParts b1)) = {1,2} )
proof
let c1 be InsType of SCM ;
assume E22: c1 = 2 ;
consider c2, c3 being Data-Location ;
E23: AddressPart (AddTo c2,c3) = <*c2,c3*> by E12;
hereby :: uses TARSKI:def 3,XBOOLE_0:def 10
let c4 be set ;
assume E24: c4 in dom (PA (AddressParts c1)) ;
InsCode (AddTo c2,c3) = 2 by AMI_5:39;
then AddressPart (AddTo c2,c3) in AddressParts c1 by E22;
then c4 in dom (AddressPart (AddTo c2,c3)) by E24, AMISTD_2:def 1;
hence c4 in {1,2} by E23, FINSEQ_1:4, FINSEQ_3:29;
end; let c4 be set ; :: uses TARSKI:def 3
assume E24: c4 in {1,2} ;
for b1 being Function holds
( b1 in AddressParts c1 implies c4 in dom b1 )
proof
let c5 be Function;
assume c5 in AddressParts c1 ;
then consider c6 being Instruction of SCM such that
E25: c5 = AddressPart c6
and E26: InsCode c6 = c1 ;
consider c7, c8 being Data-Location such that
E27: c6 = AddTo c7,c8 by E22, E26, AMI_5:48;
c5 = <*c7,c8*> by E25, E27, E12;
hence c4 in dom c5 by E24, FINSEQ_1:4, FINSEQ_3:29;
end;
hence c4 in dom (PA (AddressParts c1)) by AMISTD_2:def 1;
end;

theorem E22: :: AMI_6:19
for b1 being InsType of SCM holds
( b1 = 3 implies dom (PA (AddressParts b1)) = {1,2} )
proof
let c1 be InsType of SCM ;
assume E23: c1 = 3 ;
consider c2, c3 being Data-Location ;
E24: AddressPart (SubFrom c2,c3) = <*c2,c3*> by E13;
hereby :: uses TARSKI:def 3,XBOOLE_0:def 10
let c4 be set ;
assume E25: c4 in dom (PA (AddressParts c1)) ;
InsCode (SubFrom c2,c3) = 3 by AMI_5:40;
then AddressPart (SubFrom c2,c3) in AddressParts c1 by E23;
then c4 in dom (AddressPart (SubFrom c2,c3)) by E25, AMISTD_2:def 1;
hence c4 in {1,2} by E24, FINSEQ_1:4, FINSEQ_3:29;
end; let c4 be set ; :: uses TARSKI:def 3
assume E25: c4 in {1,2} ;
for b1 being Function holds
( b1 in AddressParts c1 implies c4 in dom b1 )
proof
let c5 be Function;
assume c5 in AddressParts c1 ;
then consider c6 being Instruction of SCM such that
E26: c5 = AddressPart c6
and E27: InsCode c6 = c1 ;
consider c7, c8 being Data-Location such that
E28: c6 = SubFrom c7,c8 by E23, E27, AMI_5:49;
c5 = <*c7,c8*> by E26, E28, E13;
hence c4 in dom c5 by E25, FINSEQ_1:4, FINSEQ_3:29;
end;
hence c4 in dom (PA (AddressParts c1)) by AMISTD_2:def 1;
end;

theorem E23: :: AMI_6:20
for b1 being InsType of SCM holds
( b1 = 4 implies dom (PA (AddressParts b1)) = {1,2} )
proof
let c1 be InsType of SCM ;
assume E24: c1 = 4 ;
consider c2, c3 being Data-Location ;
E25: AddressPart (MultBy c2,c3) = <*c2,c3*> by E14;
hereby :: uses TARSKI:def 3,XBOOLE_0:def 10
let c4 be set ;
assume E26: c4 in dom (PA (AddressParts c1)) ;
InsCode (MultBy c2,c3) = 4 by AMI_5:41;
then AddressPart (MultBy c2,c3) in AddressParts c1 by E24;
then c4 in dom (AddressPart (MultBy c2,c3)) by E26, AMISTD_2:def 1;
hence c4 in {1,2} by E25, FINSEQ_1:4, FINSEQ_3:29;
end; let c4 be set ; :: uses TARSKI:def 3
assume E26: c4 in {1,2} ;
for b1 being Function holds
( b1 in AddressParts c1 implies c4 in dom b1 )
proof
let c5 be Function;
assume c5 in AddressParts c1 ;
then consider c6 being Instruction of SCM such that
E27: c5 = AddressPart c6
and E28: InsCode c6 = c1 ;
consider c7, c8 being Data-Location such that
E29: c6 = MultBy c7,c8 by E24, E28, AMI_5:50;
c5 = <*c7,c8*> by E27, E29, E14;
hence c4 in dom c5 by E26, FINSEQ_1:4, FINSEQ_3:29;
end;
hence c4 in dom (PA (AddressParts c1)) by AMISTD_2:def 1;
end;

theorem E24: :: AMI_6:21
for b1 being InsType of SCM holds
( b1 = 5 implies dom (PA (AddressParts b1)) = {1,2} )
proof
let c1 be InsType of SCM ;
assume E25: c1 = 5 ;
consider c2, c3 being Data-Location ;
E26: AddressPart (Divide c2,c3) = <*c2,c3*> by E15;
hereby :: uses TARSKI:def 3,XBOOLE_0:def 10
let c4 be set ;
assume E27: c4 in dom (PA (AddressParts c1)) ;
InsCode (Divide c2,c3) = 5 by AMI_5:42;
then AddressPart (Divide c2,c3) in AddressParts c1 by E25;
then c4 in dom (AddressPart (Divide c2,c3)) by E27, AMISTD_2:def 1;
hence c4 in {1,2} by E26, FINSEQ_1:4, FINSEQ_3:29;
end; let c4 be set ; :: uses TARSKI:def 3
assume E27: c4 in {1,2} ;
for b1 being Function holds
( b1 in AddressParts c1 implies c4 in dom b1 )
proof
let c5 be Function;
assume c5 in AddressParts c1 ;
then consider c6 being Instruction of SCM such that
E28: c5 = AddressPart c6
and E29: InsCode c6 = c1 ;
consider c7, c8 being Data-Location such that
E30: c6 = Divide c7,c8 by E25, E29, AMI_5:51;
c5 = <*c7,c8*> by E28, E30, E15;
hence c4 in dom c5 by E27, FINSEQ_1:4, FINSEQ_3:29;
end;
hence c4 in dom (PA (AddressParts c1)) by AMISTD_2:def 1;
end;

theorem E25: :: AMI_6:22
for b1 being InsType of SCM holds
( b1 = 6 implies dom (PA (AddressParts b1)) = {1} )
proof
let c1 be InsType of SCM ;
assume E26: c1 = 6 ;
consider c2 being Instruction-Location of SCM ;
E27: AddressPart (goto c2) = <*c2*> by E16;
hereby :: uses TARSKI:def 3,XBOOLE_0:def 10
let c3 be set ;
assume E28: c3 in dom (PA (AddressParts c1)) ;
InsCode (goto c2) = 6 by AMI_5:43;
then AddressPart (goto c2) in AddressParts c1 by E26;
then c3 in dom (AddressPart (goto c2)) by E28, AMISTD_2:def 1;
hence c3 in {1} by E27, FINSEQ_1:4, FINSEQ_1:def 8;
end; let c3 be set ; :: uses TARSKI:def 3
assume E28: c3 in {1} ;
for b1 being Function holds
( b1 in AddressParts c1 implies c3 in dom b1 )
proof
let c4 be Function;
assume c4 in AddressParts c1 ;
then consider c5 being Instruction of SCM such that
E29: c4 = AddressPart c5
and E30: InsCode c5 = c1 ;
consider c6 being Instruction-Location of SCM such that
E31: c5 = goto c6 by E26, E30, AMI_5:52;
c4 = <*c6*> by E29, E31, E16;
hence c3 in dom c4 by E28, FINSEQ_1:4, FINSEQ_1:def 8;
end;
hence c3 in dom (PA (AddressParts c1)) by AMISTD_2:def 1;
end;

theorem E26: :: AMI_6:23
for b1 being InsType of SCM holds
( b1 = 7 implies dom (PA (AddressParts b1)) = {1,2} )
proof
let c1 be InsType of SCM ;
assume E27: c1 = 7 ;
consider c2 being Instruction-Location of SCM , c3 being Data-Location ;
E28: AddressPart (c3 =0_goto c2) = <*c2,c3*> by E17;
hereby :: uses TARSKI:def 3,XBOOLE_0:def 10
let c4 be set ;
assume E29: c4 in dom (PA (AddressParts c1)) ;
InsCode (c3 =0_goto c2) = 7 by AMI_5:44;
then AddressPart (c3 =0_goto c2) in AddressParts c1 by E27;
then c4 in dom (AddressPart (c3 =0_goto c2)) by E29, AMISTD_2:def 1;
hence c4 in {1,2} by E28, FINSEQ_1:4, FINSEQ_3:29;
end; let c4 be set ; :: uses TARSKI:def 3
assume E29: c4 in {1,2} ;
for b1 being Function holds
( b1 in AddressParts c1 implies c4 in dom b1 )
proof
let c5 be Function;
assume c5 in AddressParts c1 ;
then consider c6 being Instruction of SCM such that
E30: c5 = AddressPart c6
and E31: InsCode c6 = c1 ;
consider c7 being Instruction-Location of SCM , c8 being Data-Location such that
E32: c6 = c8 =0_goto c7 by E27, E31, AMI_5:53;
c5 = <*c7,c8*> by E30, E32, E17;
hence c4 in dom c5 by E29, FINSEQ_1:4, FINSEQ_3:29;
end;
hence c4 in dom (PA (AddressParts c1)) by AMISTD_2:def 1;
end;

theorem E27: :: AMI_6:24
for b1 being InsType of SCM holds
( b1 = 8 implies dom (PA (AddressParts b1)) = {1,2} )
proof
let c1 be InsType of SCM ;
assume E28: c1 = 8 ;
consider c2 being Instruction-Location of SCM , c3 being Data-Location ;
E29: AddressPart (c3 >0_goto c2) = <*c2,c3*> by E18;
hereby :: uses TARSKI:def 3,XBOOLE_0:def 10
let c4 be set ;
assume E30: c4 in dom (PA (AddressParts c1)) ;
InsCode (c3 >0_goto c2) = 8 by AMI_5:45;
then AddressPart (c3 >0_goto c2) in AddressParts c1 by E28;
then c4 in dom (AddressPart (c3 >0_goto c2)) by E30, AMISTD_2:def 1;
hence c4 in {1,2} by E29, FINSEQ_1:4, FINSEQ_3:29;
end; let c4 be set ; :: uses TARSKI:def 3
assume E30: c4 in {1,2} ;
for b1 being Function holds
( b1 in AddressParts c1 implies c4 in dom b1 )
proof
let c5 be Function;
assume c5 in AddressParts c1 ;
then consider c6 being Instruction of SCM such that
E31: c5 = AddressPart c6
and E32: InsCode c6 = c1 ;
consider c7 being Instruction-Location of SCM , c8 being Data-Location such that
E33: c6 = c8 >0_goto c7 by E28, E32, AMI_5:54;
c5 = <*c7,c8*> by E31, E33, E18;
hence c4 in dom c5 by E30, FINSEQ_1:4, FINSEQ_3:29;
end;
hence c4 in dom (PA (AddressParts c1)) by AMISTD_2:def 1;
end;

theorem E28: :: AMI_6:25
for b1, b2 being Data-Location holds (PA (AddressParts (InsCode (b1 := b2)))) . 1 = SCM-Data-Loc
proof
let c1, c2 be Data-Location ;
E29: InsCode (c1 := c2) = 1 by AMI_5:38;
then dom (PA (AddressParts (InsCode (c1 := c2)))) = {1,2} by E20;
then E30: 1 in dom (PA (AddressParts (InsCode (c1 := c2)))) by TARSKI:def 2;
hereby :: uses TARSKI:def 3,XBOOLE_0:def 10
let c3 be set ;
assume c3 in (PA (AddressParts (InsCode (c1 := c2)))) . 1 ;
then c3 in pi (AddressParts (InsCode (c1 := c2))),1 by E30, AMISTD_2:def 1;
then consider c4 being Function such that
E31: c4 in AddressParts (InsCode (c1 := c2))
and E32: c4 . 1 = c3 by CARD_3:def 6;
consider c5 being Instruction of SCM such that
E33: c4 = AddressPart c5
and E34: InsCode c5 = InsCode (c1 := c2) by E31;
InsCode c5 = 1 by E34, AMI_5:38;
then consider c6, c7 being Data-Location such that
E35: c5 = c6 := c7 by AMI_5:47;
c3 = <*c6,c7*> . 1 by E32, E33, E35, E11
.= c6 by FINSEQ_1:61 ;
hence c3 in SCM-Data-Loc by AMI_3:def 2;
end; let c3 be set ; :: uses TARSKI:def 3
assume c3 in SCM-Data-Loc ;
then reconsider c4 = c3 as Data-Location by AMI_5:16;
InsCode (c4 := c2) = 1 by AMI_5:38;
then AddressPart (c4 := c2) in AddressParts (InsCode (c1 := c2)) by E29;
then E31: (AddressPart (c4 := c2)) . 1 in pi (AddressParts (InsCode (c1 := c2))),1 by CARD_3:def 6;
(AddressPart (c4 := c2)) . 1 = <*c4,c2*> . 1 by E11
.= c4 by FINSEQ_1:61 ;
hence c3 in (PA (AddressParts (InsCode (c1 := c2)))) . 1 by E30, E31, AMISTD_2:def 1;
end;

theorem E29: :: AMI_6:26
for b1, b2 being Data-Location holds (PA (AddressParts (InsCode (b1 := b2)))) . 2 = SCM-Data-Loc
proof
let c1, c2 be Data-Location ;
E30: InsCode (c1 := c2) = 1 by AMI_5:38;
then dom (PA (AddressParts (InsCode (c1 := c2)))) = {1,2} by E20;
then E31: 2 in dom (PA (AddressParts (InsCode (c1 := c2)))) by TARSKI:def 2;
hereby :: uses TARSKI:def 3,XBOOLE_0:def 10
let c3 be set ;
assume c3 in (PA (AddressParts (InsCode (c1 := c2)))) . 2 ;
then c3 in pi (AddressParts (InsCode (c1 := c2))),2 by E31, AMISTD_2:def 1;
then consider c4 being Function such that
E32: c4 in AddressParts (InsCode (c1 := c2))
and E33: c4 . 2 = c3 by CARD_3:def 6;
consider c5 being Instruction of SCM such that
E34: c4 = AddressPart c5
and E35: InsCode c5 = InsCode (c1 := c2) by E32;
InsCode c5 = 1 by E35, AMI_5:38;
then consider c6, c7 being Data-Location such that
E36: c5 = c6 := c7 by AMI_5:47;
c3 = <*c6,c7*> . 2 by E33, E34, E36, E11
.= c7 by FINSEQ_1:61 ;
hence c3 in SCM-Data-Loc by AMI_3:def 2;
end; let c3 be set ; :: uses TARSKI:def 3
assume c3 in SCM-Data-Loc ;
then reconsider c4 = c3 as Data-Location by AMI_5:16;
InsCode (c1 := c4) = 1 by AMI_5:38;
then AddressPart (c1 := c4) in AddressParts (InsCode (c1 := c2)) by E30;
then E32: (AddressPart (c1 := c4)) . 2 in pi (AddressParts (InsCode (c1 := c2))),2 by CARD_3:def 6;
(AddressPart (c1 := c4)) . 2 = <*c1,c4*> . 2 by E11
.= c4 by FINSEQ_1:61 ;
hence c3 in (PA (AddressParts (InsCode (c1 := c2)))) . 2 by E31, E32, AMISTD_2:def 1;
end;

theorem E30: :: AMI_6:27
for b1, b2 being Data-Location holds (PA (AddressParts (InsCode (AddTo b1,b2)))) . 1 = SCM-Data-Loc
proof
let c1, c2 be Data-Location ;
E31: InsCode (AddTo c1,c2) = 2 by AMI_5:39;
then dom (PA (AddressParts (InsCode (AddTo c1,c2)))) = {1,2} by E21;
then E32: 1 in dom (PA (AddressParts (InsCode (AddTo c1,c2)))) by TARSKI:def 2;
hereby :: uses TARSKI:def 3,XBOOLE_0:def 10
let c3 be set ;
assume c3 in (PA (AddressParts (InsCode (AddTo c1,c2)))) . 1 ;
then c3 in pi (AddressParts (InsCode (AddTo c1,c2))),1 by E32, AMISTD_2:def 1;
then consider c4 being Function such that
E33: c4 in AddressParts (InsCode (AddTo c1,c2))
and E34: c4 . 1 = c3 by CARD_3:def 6;
consider c5 being Instruction of SCM such that
E35: c4 = AddressPart c5
and E36: InsCode c5 = InsCode (AddTo c1,c2) by E33;
InsCode c5 = 2 by E36, AMI_5:39;
then consider c6, c7 being Data-Location such that
E37: c5 = AddTo c6,c7 by AMI_5:48;
c3 = <*c6,c7*> . 1 by E34, E35, E37, E12
.= c6 by FINSEQ_1:61 ;
hence c3 in SCM-Data-Loc by AMI_3:def 2;
end; let c3 be set ; :: uses TARSKI:def 3
assume c3 in SCM-Data-Loc ;
then reconsider c4 = c3 as Data-Location by AMI_5:16;
InsCode (AddTo c4,c2) = 2 by AMI_5:39;
then AddressPart (AddTo c4,c2) in AddressParts (InsCode (AddTo c1,c2)) by E31;
then E33: (AddressPart (AddTo c4,c2)) . 1 in pi (AddressParts (InsCode (AddTo c1,c2))),1 by CARD_3:def 6;
(AddressPart (AddTo c4,c2)) . 1 = <*c4,c2*> . 1 by E12
.= c4 by FINSEQ_1:61 ;
hence c3 in (PA (AddressParts (InsCode (AddTo c1,c2)))) . 1 by E32, E33, AMISTD_2:def 1;
end;

theorem E31: :: AMI_6:28
for b1, b2 being Data-Location holds (PA (AddressParts (InsCode (AddTo b1,b2)))) . 2 = SCM-Data-Loc
proof
let c1, c2 be Data-Location ;
E32: InsCode (AddTo c1,c2) = 2 by AMI_5:39;
then dom (PA (AddressParts (InsCode (AddTo c1,c2)))) = {1,2} by E21;
then E33: 2 in dom (PA (AddressParts (InsCode (AddTo c1,c2)))) by TARSKI:def 2;
hereby :: uses TARSKI:def 3,XBOOLE_0:def 10
let c3 be set ;
assume c3 in (PA (AddressParts (InsCode (AddTo c1,c2)))) . 2 ;
then c3 in pi (AddressParts (InsCode (AddTo c1,c2))),2 by E33, AMISTD_2:def 1;
then consider c4 being Function such that
E34: c4 in AddressParts (InsCode (AddTo c1,c2))
and E35: c4 . 2 = c3 by CARD_3:def 6;
consider c5 being Instruction of SCM such that
E36: c4 = AddressPart c5
and E37: InsCode c5 = InsCode (AddTo c1,c2) by E34;
InsCode c5 = 2 by E37, AMI_5:39;
then consider c6, c7 being Data-Location such that
E38: c5 = AddTo c6,c7 by AMI_5:48;
c3 = <*c6,c7*> . 2 by E35, E36, E38, E12
.= c7 by FINSEQ_1:61 ;
hence c3 in SCM-Data-Loc by AMI_3:def 2;
end; let c3 be set ; :: uses TARSKI:def 3
assume c3 in SCM-Data-Loc ;
then reconsider c4 = c3 as Data-Location by AMI_5:16;
InsCode (