:: AMI_6 semantic presentation

theorem Th1: :: 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 Th2: :: 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 Th3: :: 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 Th4: :: 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;
end;

theorem Th5: :: 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 Th1;
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 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 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 Th6: :: 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;

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

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

Lemma9: 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 Th7: :: AMI_6:7
AddressPart (halt SCM ) = {} by AMI_3:71, MCART_1:def 2;

theorem Th8: :: AMI_6:8
for b1, b2 being Data-Location holds AddressPart (b1 := b2) = <*b1,b2*> by MCART_1:def 2;

theorem Th9: :: AMI_6:9
for b1, b2 being Data-Location holds AddressPart (AddTo b1,b2) = <*b1,b2*> by MCART_1:def 2;

theorem Th10: :: AMI_6:10
for b1, b2 being Data-Location holds AddressPart (SubFrom b1,b2) = <*b1,b2*> by MCART_1:def 2;

theorem Th11: :: AMI_6:11
for b1, b2 being Data-Location holds AddressPart (MultBy b1,b2) = <*b1,b2*> by MCART_1:def 2;

theorem Th12: :: AMI_6:12
for b1, b2 being Data-Location holds AddressPart (Divide b1,b2) = <*b1,b2*> by MCART_1:def 2;

theorem Th13: :: AMI_6:13
for b1 being Instruction-Location of SCM holds AddressPart (goto b1) = <*b1*> by MCART_1:def 2;

theorem Th14: :: AMI_6:14
for b1 being Data-Location
for b2 being Instruction-Location of SCM holds AddressPart (b1 =0_goto b2) = <*b2,b1*> by MCART_1:def 2;

theorem Th15: :: AMI_6:15
for b1 being Data-Location
for b2 being Instruction-Location of SCM holds AddressPart (b1 >0_goto b2) = <*b2,b1*> by MCART_1:def 2;

theorem Th16: :: 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 :: according to 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, Th7, TARSKI:def 1;
end;
let c2 be set ; :: according to TARSKI:def 3
assume c2 in {0} ;
then c2 = 0 by TARSKI:def 1;
hence c2 in AddressParts c1 by E20, Th7, 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 Lemma9;
( 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, MCART_1:7;
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 Th17: :: 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 Th8;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10
let c4 be set ;
assume E23: c4 in dom (PA (AddressParts c1)) ;
InsCode (c2 := c3) = 1 by MCART_1:7;
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 ; :: according to 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, Th8;
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 Th18: :: 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 Th9;
hereby :: according to 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 MCART_1:7;
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 ; :: according to 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, Th9;
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 Th19: :: 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 Th10;
hereby :: according to 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 MCART_1:7;
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 ; :: according to 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, Th10;
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 Th20: :: 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 Th11;
hereby :: according to 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 MCART_1:7;
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 ; :: according to 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, Th11;
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 Th21: :: 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 Th12;
hereby :: according to 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 MCART_1:7;
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 ; :: according to 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, Th12;
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 Th22: :: 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 Th13;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10
let c3 be set ;
assume E28: c3 in dom (PA (AddressParts c1)) ;
InsCode (goto c2) = 6 by MCART_1:7;
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 ; :: according to 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, Th13;
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 Th23: :: 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 Th14;
hereby :: according to 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 MCART_1:7;
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 ; :: according to 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, Th14;
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 Th24: :: 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 Th15;
hereby :: according to 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 MCART_1:7;
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 ; :: according to 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, Th15;
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 Th25: :: 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 MCART_1:7;
then dom (PA (AddressParts (InsCode (c1 := c2)))) = {1,2} by Th17;
then E30: 1 in dom (PA (AddressParts (InsCode (c1 := c2)))) by TARSKI:def 2;
hereby :: according to 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, MCART_1:7;
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, Th8
.= c6 by FINSEQ_1:61 ;
hence c3 in SCM-Data-Loc by AMI_3:def 2;
end;
let c3 be set ; :: according to 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 MCART_1:7;
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 Th8
.= c4 by FINSEQ_1:61 ;
hence c3 in (PA (AddressParts (InsCode (c1 := c2)))) . 1 by E30, E31, AMISTD_2:def 1;
end;

theorem Th26: :: 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 MCART_1:7;
then dom (PA (AddressParts (InsCode (c1 := c2)))) = {1,2} by Th17;
then E31: 2 in dom (PA (AddressParts (InsCode (c1 := c2)))) by TARSKI:def 2;
hereby :: according to 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, MCART_1:7;
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, Th8
.= c7 by FINSEQ_1:61 ;
hence c3 in SCM-Data-Loc by AMI_3:def 2;
end;
let c3 be set ; :: according to 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 MCART_1:7;
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 Th8
.= c4 by FINSEQ_1:61 ;
hence c3 in (PA (AddressParts (InsCode (c1 := c2)))) . 2 by E31, E32, AMISTD_2:def 1;
end;

theorem Th27: :: 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 MCART_1:7;
then dom (PA (AddressParts (InsCode (AddTo c1,c2)))) = {1,2} by Th18;
then E32: 1 in dom (PA (AddressParts (InsCode (AddTo c1,c2)))) by TARSKI:def 2;
hereby :: according to 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, MCART_1:7;
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, Th9
.= c6 by FINSEQ_1:61 ;
hence c3 in SCM-Data-Loc by AMI_3:def 2;
end;
let c3 be set ; :: according to 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 MCART_1:7;
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 Th9
.= c4 by FINSEQ_1:61 ;
hence c3 in (PA (AddressParts (InsCode (AddTo c1,c2)))) . 1 by E32, E33, AMISTD_2:def 1;
end;

theorem Th28: :: 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 MCART_1:7;
then dom (PA (AddressParts (InsCode (AddTo c1,c2)))) = {1,2} by Th18;
then E33: 2 in dom (PA (AddressParts (InsCode (AddTo c1,c2)))) <