:: AMI_5 semantic presentation

theorem :: AMI_5:1

canceled;

theorem :: AMI_5:2

canceled;

theorem :: AMI_5:3

for b₁, b₂ being Nat holds
( b₂ <> 0 implies (b₁ * b₂) div b₂ = b₁ )

let c₁, c₂ be Nat;
assume c₂ <> 0 ;
then ( ( c₁ * c₂ = (c₂ * c₁) + 0 & 0 < c₂ ) or ( c₁ = 0 & c₂ = 0 ) ) by NAT_1:19;
hence (c₁ * c₂) div c₂ = c₁ by NAT_1:def 1;

end;

theorem :: AMI_5:4

for b₁, b₂ being natural number holds
( b₁ >= b₂ implies (b₁ -' b₂) + b₂ = b₁ )

proof

let c₁, c₂ be natural number ;
assume c₁ >= c₂ ;
then ex b₁ being Nat st c₁ = c₂ + b₁ by NAT_1:28;
hence (c₁ -' c₂) + c₂ = c₁ by BINARITH:39;

end;

theorem :: AMI_5:5

canceled;

theorem :: AMI_5:6

canceled;

theorem :: AMI_5:7

canceled;

theorem :: AMI_5:8

canceled;

theorem :: AMI_5:9

canceled;

theorem :: AMI_5:10

canceled;

theorem :: AMI_5:11

canceled;

theorem :: AMI_5:12

canceled;

theorem :: AMI_5:13

canceled;

theorem :: AMI_5:14

canceled;

theorem E1: :: AMI_5:15

for b₁ being Data-Location
for b₂ being State of SCM holds
( (Exec (Divide b₁,b₁),b₂) . (IC SCM ) = Next (IC b₂) & (Exec (Divide b₁,b₁),b₂) . b₁ = (b₂ . b₁) mod (b₂ . b₁) & for b₃ being Data-Location holds
( b₃ <> b₁ implies (Exec (Divide b₁,b₁),b₂) . b₃ = b₂ . b₃ ) )

proof

let c₁ be Data-Location ;
let c₂ be State of SCM ;
reconsider c₃ = c₁ as Element of SCM-Data-Loc by AMI_3:def 2;
reconsider c₄ = Divide c₁,c₁ as Element of SCM-Instr by AMI_3:def 1;
reconsider c₅ = c₂ as SCM-State by AMI_3:def 1;
set c₆ = SCM-Chg c₅,(c₄ address_1 ),((c₅ . (c₄ address_1 )) div (c₅ . (c₄ address_2 )));
set c₇ = SCM-Chg (SCM-Chg c₅,(c₄ address_1 ),((c₅ . (c₄ address_1 )) div (c₅ . (c₄ address_2 )))),(c₄ address_2 ),((c₅ . (c₄ address_1 )) mod (c₅ . (c₄ address_2 )));
reconsider c₈ = 5 as Element of Segm 9 by GR_CY_1:10;
E2: c₄ = [c₈,<*c₃,c₃*>] ;
E3: Exec (Divide c₁,c₁),c₂ = SCM-Exec-Res c₄,c₅ by AMI_3:7
.= SCM-Chg (SCM-Chg (SCM-Chg c₅,(c₄ address_1 ),((c₅ . (c₄ address_1 )) div (c₅ . (c₄ address_2 )))),(c₄ address_2 ),((c₅ . (c₄ address_1 )) mod (c₅ . (c₄ address_2 )))),(Next (IC c₅)) by E2, AMI_2:def 16 ;
E4: ( c₄ address_1 = c₃ & c₄ address_2 = c₃ ) by E2, AMI_2:23;
thus (Exec (Divide c₁,c₁),c₂) . (IC SCM ) = Next (IC c₂) by AMI_3:12;
thus (Exec (Divide c₁,c₁),c₂) . c₁ = (SCM-Chg (SCM-Chg c₅,(c₄ address_1 ),((c₅ . (c₄ address_1 )) div (c₅ . (c₄ address_2 )))),(c₄ address_2 ),((c₅ . (c₄ address_1 )) mod (c₅ . (c₄ address_2 )))) . c₃ by E3, AMI_2:17
.= (c₂ . c₁) mod (c₂ . c₁) by E4, AMI_2:20 ;
thus for b₁ being Data-Location holds
( b₁ <> c₁ implies (Exec (Divide c₁,c₁),c₂) . b₁ = c₂ . b₁ ) by AMI_3:12;

end;

theorem E2: :: AMI_5:16

for b₁ being set holds
( b₁ in SCM-Data-Loc implies b₁ is Data-Location ) by AMI_3:def 1, AMI_3:def 2;

theorem :: AMI_5:17

canceled;

theorem E3: :: AMI_5:18

for b₁ being Data-Location holds
ex b₂ being Nat st b₁ = dl. b₂

proof

let c₁ be Data-Location ;
c₁ in SCM-Data-Loc by AMI_3:def 2;
then consider c₂ being Nat such that
E4: c₁ = (2 * c₂) + 1 by AMI_2:def 2;
consider c₃ being Nat such that
E5: c₂ = c₃ ;
take c₃ ;
thus c₁ = dl. c₃ by E4, E5;

end;

theorem E4: :: AMI_5:19

for b₁ being Instruction-Location of SCM holds
ex b₂ being Nat st b₁ = il. b₂

proof

let c₁ be Instruction-Location of SCM ;
c₁ in SCM-Instr-Loc by AMI_3:def 1;
then consider c₂ being Nat such that
E5: ( c₁ = 2 * c₂ & c₂ > 0 ) by AMI_2:def 3;
consider c₃ being Nat such that
E6: c₂ = c₃ + 1 by E5, NAT_1:22;
take c₃ ;
thus c₁ = (2 * c₃) + (2 * 1) by E5, E6
.= il. c₃ ;

end;

theorem E5: :: AMI_5:20

for b₁ being Data-Location holds
b₁ <> IC SCM

proof

let c₁ be Data-Location ;
consider c₂ being Nat such that
E6: c₁ = dl. c₂ by E3;
thus c₁ <> IC SCM by E6, AMI_3:57;

end;

theorem :: AMI_5:21

canceled;

theorem E6: :: AMI_5:22

for b₁ being Instruction-Location of SCM
for b₂ being Data-Location holds
b₁ <> b₂

proof

let c₁ be Instruction-Location of SCM ;
let c₂ be Data-Location ;
consider c₃ being Nat such that
E7: c₁ = il. c₃ by E4;
consider c₄ being Nat such that
E8: c₂ = dl. c₄ by E3;
thus c₁ <> c₂ by E7, E8, AMI_3:56;

end;

theorem E7: :: AMI_5:23

the carrier of SCM = ({(IC SCM )} \/ SCM-Data-Loc ) \/ SCM-Instr-Loc

proof

E8: NAT c= ({0} \/ { ((2 * b₁) + 1) where B is Nat : verum } ) \/ { (2 * b₁) where B is Nat : b₁ > 0 }

proof

let c₁ be set ; :: uses TARSKI:def 3
assume c₁ in NAT ;
then reconsider c₂ = c₁ as Nat ;
E9: not ( not c₂ div 2 = 0 & not c₂ div 2 > 0 ) by NAT_1:19;
c₂ mod 2 < 2 by NAT_1:46;
then ( c₂ mod 2 = 0 or c₂ mod 2 = 1 ) by NAT_1:71;
then E10: ( c₂ = (2 * (c₂ div 2)) + 0 or c₂ = (2 * (c₂ div 2)) + 1 ) by NAT_1:47;

per cases not ( not c₁ = 0 & for b₁ being Nat holds
not c₁ = (2 * b₁) + 1 & for b₁ being Nat holds
not ( c₁ = 2 * b₁ & b₁ > 0 ) ) by E9, E10;

suppose c₁ = 0 ;

then c₁ in {0} by TARSKI:def 1;
then c₁ in {0} \/ { ((2 * b₁) + 1) where B is Nat : verum } by XBOOLE_0:def 2;
hence c₁ in ({0} \/ { ((2 * b₁) + 1) where B is Nat : verum } ) \/ { (2 * b₁) where B is Nat : b₁ > 0 } by XBOOLE_0:def 2;

end;

suppose ex b₁ being Nat st c₁ = (2 * b₁) + 1 ;

then c₁ in { ((2 * b₁) + 1) where B is Nat : verum } ;
then c₁ in {0} \/ { ((2 * b₁) + 1) where B is Nat : verum } by XBOOLE_0:def 2;
hence c₁ in ({0} \/ { ((2 * b₁) + 1) where B is Nat : verum } ) \/ { (2 * b₁) where B is Nat : b₁ > 0 } by XBOOLE_0:def 2;

end;

suppose ex b₁ being Nat st
( c₁ = 2 * b₁ & b₁ > 0 ) ;

then c₁ in { (2 * b₁) where B is Nat : b₁ > 0 } ;
hence c₁ in ({0} \/ { ((2 * b₁) + 1) where B is Nat : verum } ) \/ { (2 * b₁) where B is Nat : b₁ > 0 } by XBOOLE_0:def 2;

end;

{(IC SCM )} c= NAT by AMI_3:4, ZFMISC_1:37;
then {(IC SCM )} \/ SCM-Data-Loc c= NAT by XBOOLE_1:8;
then ({(IC SCM )} \/ SCM-Data-Loc ) \/ SCM-Instr-Loc c= NAT by XBOOLE_1:8;
hence the carrier of SCM = ({(IC SCM )} \/ SCM-Data-Loc ) \/ SCM-Instr-Loc by E8, AMI_2:def 2, AMI_2:def 3, AMI_3:def 1, XBOOLE_0:def 10;

end;

theorem :: AMI_5:24

for b₁ being State of SCM
for b₂ being Data-Location
for b₃ being Instruction-Location of SCM holds
( b₂ in dom b₁ & b₃ in dom b₁ )

proof

let c₁ be State of SCM ;
let c₂ be Data-Location ;
let c₃ be Instruction-Location of SCM ;
c₂ in SCM-Data-Loc by AMI_3:def 2;
then c₂ in {(IC SCM )} \/ SCM-Data-Loc by XBOOLE_0:def 2;
then c₂ in ({(IC SCM )} \/ SCM-Data-Loc ) \/ SCM-Instr-Loc by XBOOLE_0:def 2;
hence c₂ in dom c₁ by E7, AMI_3:36;
c₃ in ({(IC SCM )} \/ SCM-Data-Loc ) \/ SCM-Instr-Loc by AMI_3:def 1, XBOOLE_0:def 2;
hence c₃ in dom c₁ by E7, AMI_3:36;

end;

theorem E8: :: AMI_5:25

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite AMI-Struct of b₁
for b₃ being State of b₂ holds IC b₂ in dom b₃

proof

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite AMI-Struct of c₁;
let c₃ be State of c₂;
dom c₃ = the carrier of c₂ by AMI_3:36;
hence IC c₂ in dom c₃ ;

end;

theorem :: AMI_5:26

for b₁, b₂ being State of SCM holds
( ( IC b₁ = IC b₂ & for b₃ being Data-Location holds b₁ . b₃ = b₂ . b₃ & for b₃ being Instruction-Location of SCM holds b₁ . b₃ = b₂ . b₃ ) implies ( b₁ = b₂ ) )

proof

let c₁, c₂ be State of SCM ;
assume that E9: IC c₁ = IC c₂
and E10: for b₁ being Data-Location holds c₁ . b₁ = c₂ . b₁
and E11: for b₁ being Instruction-Location of SCM holds c₁ . b₁ = c₂ . b₁ ;
consider c₃ being Function such that
E12: ( c₁ = c₃ & dom c₃ = dom SCM-OK & for b₁ being set holds
( b₁ in dom SCM-OK implies c₃ . b₁ in SCM-OK . b₁ ) ) by AMI_3:def 1, CARD_3:def 5;
consider c₄ being Function such that
E13: ( c₂ = c₄ & dom c₄ = dom SCM-OK & for b₁ being set holds
( b₁ in dom SCM-OK implies c₄ . b₁ in SCM-OK . b₁ ) ) by AMI_3:def 1, CARD_3:def 5;
E14: ( NAT = dom c₃ & NAT = dom c₄ ) by E12, E13, FUNCT_2:def 1;

now

let c₅ be set ;
assume E15: c₅ in NAT ;
E16: ( c₅ in {(IC SCM )} \/ SCM-Data-Loc or c₅ in SCM-Instr-Loc ) by E15, E7, AMI_3:def 1, XBOOLE_0:def 2;

per cases not ( not c₅ in {(IC SCM )} & not c₅ in SCM-Data-Loc & not c₅ in SCM-Instr-Loc ) by E16, XBOOLE_0:def 2;

suppose c₅ in {(IC SCM )} ;

then E17: c₅ = IC SCM by TARSKI:def 1;
c₁ . (IC SCM ) = IC c₂ by E9
.= c₂ . (IC SCM ) ;
hence c₃ . c₅ = c₄ . c₅ by E12, E13, E17;

end;

suppose c₅ in SCM-Data-Loc ;

then c₅ is Data-Location by E2;
hence c₃ . c₅ = c₄ . c₅ by E10, E12, E13;

end;

suppose c₅ in SCM-Instr-Loc ;

hence c₃ . c₅ = c₄ . c₅ by E11, E12, E13, AMI_3:def 1;

end;

hence c₁ = c₂ by E12, E13, E14, FUNCT_1:9;

end;

theorem E9: :: AMI_5:27

for b₁ being State of SCM holds SCM-Data-Loc c= dom b₁

proof

let c₁ be State of SCM ;
SCM-Data-Loc c= SCM-Data-Loc \/ SCM-Instr-Loc by XBOOLE_1:10;
then SCM-Data-Loc c= {(IC SCM )} \/ (SCM-Data-Loc \/ SCM-Instr-Loc ) by XBOOLE_1:10;
then SCM-Data-Loc c= ({(IC SCM )} \/ SCM-Data-Loc ) \/ SCM-Instr-Loc by XBOOLE_1:4;
hence SCM-Data-Loc c= dom c₁ by E7, AMI_3:36;

end;

theorem E10: :: AMI_5:28

for b₁ being State of SCM holds SCM-Instr-Loc c= dom b₁

proof

let c₁ be State of SCM ;
SCM-Instr-Loc c= ({(IC SCM )} \/ SCM-Data-Loc ) \/ SCM-Instr-Loc by XBOOLE_1:10;
hence SCM-Instr-Loc c= dom c₁ by E7, AMI_3:36;

end;

theorem :: AMI_5:29

for b₁ being State of SCM holds dom (b₁ | SCM-Data-Loc ) = SCM-Data-Loc

proof

let c₁ be State of SCM ;
SCM-Data-Loc c= dom c₁ by E9;
hence dom (c₁ | SCM-Data-Loc ) = SCM-Data-Loc by RELAT_1:91;

end;

theorem :: AMI_5:30

for b₁ being State of SCM holds dom (b₁ | SCM-Instr-Loc ) = SCM-Instr-Loc

proof

let c₁ be State of SCM ;
SCM-Instr-Loc c= dom c₁ by E10;
hence dom (c₁ | SCM-Instr-Loc ) = SCM-Instr-Loc by RELAT_1:91;

end;

theorem E11: :: AMI_5:31

not SCM-Data-Loc is finite

proof

deffunc H₁( Element of NAT ) -> Element of NAT = (2 * a₁) + 1;
consider c₁ being Function of NAT , NAT such that
E12: for b₁ being Element of NAT holds c₁ . b₁ = H₁(b₁) from FUNCT_2:sch 4();
E13: dom c₁ = NAT by FUNCT_2:def 1;
NAT , SCM-Data-Loc are_equipotent

proof

take c₁ ; :: uses WELLORD2:def 4
thus c₁ is one-to-one

proof

let c₂, c₃ be set ; :: uses FUNCT_1:def 8
assume that E14: c₂ in dom c₁
and E15: c₃ in dom c₁
and E16: c₁ . c₂ = c₁ . c₃ ;
reconsider c₄ = c₂, c₅ = c₃ as Nat by E14, E15, FUNCT_2:def 1;
dl. c₄ = (2 * c₄) + 1
.= c₁ . c₄ by E12
.= (2 * c₅) + 1 by E12, E16
.= dl. c₅ ;
hence c₂ = c₃ by AMI_3:52;

end;

thus dom c₁ = NAT by FUNCT_2:def 1;
thus rng c₁ c= SCM-Data-Loc :: uses XBOOLE_0:def 10

proof

let c₂ be set ; :: uses TARSKI:def 3
assume c₂ in rng c₁ ;
then consider c₃ being set such that
E14: c₃ in dom c₁
and E15: c₂ = c₁ . c₃ by FUNCT_1:def 5;
reconsider c₄ = c₃ as Nat by E14, FUNCT_2:def 1;
c₂ = (2 * c₄) + 1 by E12, E15
.= dl. c₄ ;
hence c₂ in SCM-Data-Loc by AMI_3:def 2;

end;

thus SCM-Data-Loc c= rng c₁

proof

let c₂ be set ; :: uses TARSKI:def 3
assume E14: c₂ in SCM-Data-Loc ;
reconsider c₃ = c₂ as Data-Location by E14, AMI_3:def 1, AMI_3:def 2;
consider c₄ being Nat such that
E15: c₃ = dl. c₄ by E3;
c₂ = (2 * c₄) + 1 by E15
.= c₁ . c₄ by E12 ;
hence c₂ in rng c₁ by E13, FUNCT_1:def 5;

end;

hence not SCM-Data-Loc is finite by CARD_1:68, CARD_4:15;

end;

theorem E12: :: AMI_5:32

not the Instruction-Locations of SCM is finite

proof

deffunc H₁( Element of NAT ) -> Element of NAT = (2 * a₁) + 2;
consider c₁ being Function of NAT , NAT such that
E13: for b₁ being Element of NAT holds c₁ . b₁ = H₁(b₁) from FUNCT_2:sch 4();
E14: dom c₁ = NAT by FUNCT_2:def 1;
NAT , SCM-Instr-Loc are_equipotent

proof

take c₁ ; :: uses WELLORD2:def 4
thus c₁ is one-to-one

proof

let c₂, c₃ be set ; :: uses FUNCT_1:def 8
assume that E15: c₂ in dom c₁
and E16: c₃ in dom c₁
and E17: c₁ . c₂ = c₁ . c₃ ;
reconsider c₄ = c₂, c₅ = c₃ as Nat by E15, E16, FUNCT_2:def 1;
il. c₄ = (2 * c₄) + 2
.= c₁ . c₄ by E13
.= (2 * c₅) + 2 by E13, E17
.= il. c₅ ;
hence c₂ = c₃ by AMI_3:53;

end;

thus dom c₁ = NAT by FUNCT_2:def 1;
thus rng c₁ c= SCM-Instr-Loc :: uses XBOOLE_0:def 10

proof

let c₂ be set ; :: uses TARSKI:def 3
assume c₂ in rng c₁ ;
then consider c₃ being set such that
E15: c₃ in dom c₁
and E16: c₂ = c₁ . c₃ by FUNCT_1:def 5;
reconsider c₄ = c₃ as Nat by E15, FUNCT_2:def 1;
c₂ = (2 * c₄) + 2 by E13, E16
.= il. c₄ ;
hence c₂ in SCM-Instr-Loc by AMI_3:def 1;

end;

thus SCM-Instr-Loc c= rng c₁

proof

let c₂ be set ; :: uses TARSKI:def 3
assume c₂ in SCM-Instr-Loc ;
then reconsider c₃ = c₂ as Instruction-Location of SCM by AMI_3:def 1;
consider c₄ being Nat such that
E15: c₃ = il. c₄ by E4;
c₂ = (2 * c₄) + 2 by E15
.= c₁ . c₄ by E13 ;
hence c₂ in rng c₁ by E14, FUNCT_1:def 5;

end;

hence not the Instruction-Locations of SCM is finite by AMI_3:def 1, CARD_1:68, CARD_4:15;

end;

registration

cluster SCM-Data-Loc -> infinite ;
coherence by E11;
cluster the Instruction-Locations of SCM -> infinite ;
coherence by E12;

end;

theorem E13: :: AMI_5:33

SCM-Data-Loc misses SCM-Instr-Loc

proof

{ ((2 * b₁) + 1) where B is Nat : verum } /\ { (2 * b₁) where B is Nat : b₁ > 0 } = {}

proof

consider c₁ being Element of { ((2 * b₁) + 1) where B is Nat : verum } /\ { (2 * b₁) where B is Nat : b₁ > 0 } ;
assume { ((2 * b₁) + 1) where B is Nat : verum } /\ { (2 * b₁) where B is Nat : b₁ > 0 } <> {} ;
then E14: ( c₁ in { ((2 * b₁) + 1) where B is Nat : verum } & c₁ in { (2 * b₁) where B is Nat : b₁ > 0 } ) by XBOOLE_0:def 3;
then consider c₂ being Nat such that
E15: c₁ = (2 * c₂) + 1 ;
consider c₃ being Nat such that
E16: ( c₁ = 2 * c₃ & c₃ > 0 ) by E14;
consider c₄ being Nat such that
E17: c₃ = c₄ + 1 by E16, NAT_1:22;
c₁ = (2 * c₄) + (2 * 1) by E16, E17
.= (2 * c₄) + 2 ;
then ( c₁ = dl. c₂ & c₁ = il. c₄ ) by E15;
hence not verum by SCM_1:7;

end;

hence SCM-Data-Loc misses SCM-Instr-Loc by AMI_2:def 2, AMI_2:def 3, XBOOLE_0:def 7;

end;

theorem :: AMI_5:34

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite AMI-Struct of b₁
for b₃ being State of b₂ holds Start-At (IC b₃) = b₃ | {(IC b₂)}

proof

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite AMI-Struct of c₁;
let c₃ be State of c₂;
E14: IC c₂ in dom c₃ by E8;
thus Start-At (IC c₃) = (IC c₂) .--> (IC c₃)
.= (IC c₂) .--> (c₃ . (IC c₂))
.= {[(IC c₂),(c₃ . (IC c₂))]} by AMI_1:19
.= c₃ | {(IC c₂)} by E14, GRFUNC_1:89 ;

end;

theorem E14: :: AMI_5:35

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite AMI-Struct of b₁
for b₃ being Instruction-Location of b₂ holds Start-At b₃ = {[(IC b₂),b₃]}

proof

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite AMI-Struct of c₁;
let c₃ be Instruction-Location of c₂;
thus Start-At c₃ = (IC c₂) .--> c₃
.= {(IC c₂)} --> c₃ by CQC_LANG:def 2
.= [:{(IC c₂)},{c₃}:] by FUNCOP_1:def 2
.= {[(IC c₂),c₃]} by ZFMISC_1:35 ;

end;

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
let c₃ be Element of the Instructions of c₂;
func InsCode a₃ -> InsType of a₂ equals :: AMI_5:def 1
a₃ `1 ;
coherence

proof

reconsider c₄ = c₃ as Instruction of c₂ ;
c₄ `1 in the Instruction-Codes of c₂ ;
hence c₃ `1 is InsType of c₂ ;

end;

:: deftheorem defines InsCode AMI_5:def 1 :

registration

let c₁ be Instruction of SCM ;
cluster InsCode a₁ -> natural ;
coherence

proof

InsCode c₁ in Segm 9 by AMI_3:def 1;
hence InsCode c₁ is natural by ORDINAL2:def 21;

end;

definition

let c₁ be Instruction of SCM ;
func @ a₁ -> Element of SCM-Instr equals :: AMI_5:def 2
a₁;
coherence by AMI_3:def 1;

end;

:: deftheorem defines @ AMI_5:def 2 :

definition

let c₁ be Element of SCM-Instr-Loc ;
func a₁ @ -> Instruction-Location of SCM equals :: AMI_5:def 3
a₁;
coherence by AMI_3:def 1;

end;

:: deftheorem defines @ AMI_5:def 3 :

definition

let c₁ be Element of SCM-Data-Loc ;
func a₁ @ -> Data-Location equals :: AMI_5:def 4
a₁;
coherence by AMI_3:def 1, AMI_3:def 2;

end;

:: deftheorem defines @ AMI_5:def 4 :

theorem E15: :: AMI_5:36

for b₁ being Instruction of SCM holds InsCode b₁ <= 8

proof

let c₁ be Instruction of SCM ;
InsCode c₁ < 8 + 1 by AMI_3:def 1, GR_CY_1:10;
hence InsCode c₁ <= 8 by NAT_1:38;

end;

theorem E16: :: AMI_5:37

InsCode (halt SCM ) = 0

proof

thus InsCode (halt SCM ) = (halt SCM ) `1
.= 0 by AMI_3:71, MCART_1:7 ;

end;

theorem :: AMI_5:38

for b₁, b₂ being Data-Location holds InsCode (b₁ := b₂) = 1

proof

let c₁, c₂ be Data-Location ;
thus InsCode (c₁ := c₂) = (c₁ := c₂) `1
.= 1 by MCART_1:7 ;

end;

theorem :: AMI_5:39

for b₁, b₂ being Data-Location holds InsCode (AddTo b₁,b₂) = 2

proof

let c₁, c₂ be Data-Location ;
thus InsCode (AddTo c₁,c₂) = (AddTo c₁,c₂) `1
.= 2 by MCART_1:7 ;

end;

theorem :: AMI_5:40

for b₁, b₂ being Data-Location holds InsCode (SubFrom b₁,b₂) = 3

proof

let c₁, c₂ be Data-Location ;
thus InsCode (SubFrom c₁,c₂) = (SubFrom c₁,c₂) `1
.= 3 by MCART_1:7 ;

end;

theorem :: AMI_5:41

for b₁, b₂ being Data-Location holds InsCode (MultBy b₁,b₂) = 4

proof

let c₁, c₂ be Data-Location ;
thus InsCode (MultBy c₁,c₂) = (MultBy c₁,c₂) `1
.= 4 by MCART_1:7 ;

end;

theorem :: AMI_5:42

for b₁, b₂ being Data-Location holds InsCode (Divide b₁,b₂) = 5

proof

let c₁, c₂ be Data-Location ;
thus InsCode (Divide c₁,c₂) = (Divide c₁,c₂) `1
.= 5 by MCART_1:7 ;

end;

theorem :: AMI_5:43

for b₁ being Instruction-Location of SCM holds InsCode (goto b₁) = 6

proof

let c₁ be Instruction-Location of SCM ;
thus InsCode (goto c₁) = (goto c₁) `1
.= 6 by MCART_1:7 ;

end;

theorem :: AMI_5:44

for b₁ being Data-Location
for b₂ being Instruction-Location of SCM holds InsCode (b₁ =0_goto b₂) = 7

proof

let c₁ be Data-Location ;
let c₂ be Instruction-Location of SCM ;
thus InsCode (c₁ =0_goto c₂) = (c₁ =0_goto c₂) `1
.= 7 by MCART_1:7 ;

end;

theorem :: AMI_5:45

for b₁ being Data-Location
for b₂ being Instruction-Location of SCM holds InsCode (b₁ >0_goto b₂) = 8

proof

let c₁ be Data-Location ;
let c₂ be Instruction-Location of SCM ;
thus InsCode (c₁ >0_goto c₂) = (c₁ >0_goto c₂) `1
.= 8 by MCART_1:7 ;

end;

theorem E17: :: AMI_5:46

for b₁ being Instruction of SCM holds
( InsCode b₁ = 0 implies b₁ = halt SCM )

proof

let c₁ be Instruction of SCM ;
assume E18: InsCode c₁ = 0 ;

E19: now

assume c₁ in { [b₁,<*b₂,b₃*>] where B is Element of Segm 9, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc : b₁ in {1,2,3,4,5} } ;
then consider c₂ being Element of Segm 9, c₃, c₄ being Element of SCM-Data-Loc such that
E20: c₁ = [c₂,<*c₃,c₄*>]
and E21: c₂ in {1,2,3,4,5} ;
InsCode c₁ = c₁ `1
.= c₂ by E20, MCART_1:7 ;
hence not verum by E18, E21, ENUMSET1:def 3;

end;

E20: now

assume c₁ in { [b₁,<*b₂,b₃*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b₁ in {7,8} } ;
then consider c₂ being Element of Segm 9, c₃ being Element of SCM-Instr-Loc , c₄ being Element of SCM-Data-Loc such that
E21: c₁ = [c₂,<*c₃,c₄*>]
and E22: c₂ in {7,8} ;
InsCode c₁ = c₁ `1
.= c₂ by E21, MCART_1:7 ;
hence not verum by E18, E22, TARSKI:def 2;

end;

E21: now

assume c₁ in { [b₁,<*b₂*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b₁ = 6 } ;
then consider c₂ being Element of Segm 9, c₃ being Element of SCM-Instr-Loc such that
E22: c₁ = [c₂,<*c₃*>]
and E23: c₂ = 6 ;
InsCode c₁ = c₁ `1
.= c₂ by E22, MCART_1:7 ;
hence not verum by E18, E23;

end;

c₁ in ({[SCM-Halt ,{} ]} \/ { [b₁,<*b₂*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b₁ = 6 } ) \/ { [b₁,<*b₂,b₃*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b₁ in {7,8} } by E19, AMI_2:def 4, AMI_3:def 1, XBOOLE_0:def 2;
then c₁ in {[SCM-Halt ,{} ]} \/ { [b₁,<*b₂*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b₁ = 6 } by E20, XBOOLE_0:def 2;
then c₁ in {[SCM-Halt ,{} ]} by E21, XBOOLE_0:def 2;
hence c₁ = halt SCM by AMI_2:def 1, AMI_3:71, TARSKI:def 1;

end;

theorem E18: :: AMI_5:47

for b₁ being Instruction of SCM holds
not ( InsCode b₁ = 1 & for b₂, b₃ being Data-Location holds
not b₁ = b₂ := b₃ )

proof

let c₁ be Instruction of SCM ;
assume E19: InsCode c₁ = 1 ;
E20: not c₁ in {[SCM-Halt ,{} ]} by E19, E16, AMI_2:def 1, AMI_3:71, TARSKI:def 1;

E21: now

assume c₁ in { [b₁,<*b₂,b₃*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b₁ in {7,8} } ;
then consider c₂ being Element of Segm 9, c₃ being Element of SCM-Instr-Loc , c₄ being Element of SCM-Data-Loc such that
E22: c₁ = [c₂,<*c₃,c₄*>]
and E23: c₂ in {7,8} ;
InsCode c₁ = c₁ `1
.= c₂ by E22, MCART_1:7 ;
hence not verum by E19, E23, TARSKI:def 2;

end;

now

end;

then not c₁ in {[SCM-Halt ,{} ]} \/ { [b₁,<*b₂*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b₁ = 6 } by E20, XBOOLE_0:def 2;
then not c₁ in ({[SCM-Halt ,{} ]} \/ { [b₁,<*b₂*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b₁ = 6 } ) \/ { [b₁,<*b₂,b₃*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b₁ in {7,8} } by E21, XBOOLE_0:def 2;
then c₁ in { [b₁,<*b₂,b₃*>] where B is Element of Segm 9, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc : b₁ in {1,2,3,4,5} } by AMI_2:def 4, AMI_3:def 1, XBOOLE_0:def 2;
then consider c₂ being Element of Segm 9, c₃, c₄ being Element of SCM-Data-Loc such that
E22: c₁ = [c₂,<*c₃,c₄*>]
and c₂ in {1,2,3,4,5} ;
E23: InsCode c₁ = c₁ `1
.= c₂ by E22, MCART_1:7 ;
reconsider c₅ = c₃ @ , c₆ = c₄ @ as Data-Location ;
take c₅ ;
take c₆ ;
( c₃ = c₃ @ & c₄ = c₄ @ ) ;
hence c₁ = c₅ := c₆ by E19, E22, E23;

end;

theorem E19: :: AMI_5:48

for b₁ being Instruction of SCM holds
not ( InsCode b₁ = 2 & for b₂, b₃ being Data-Location holds
not b₁ = AddTo b₂,b₃ )

proof

let c₁ be Instruction of SCM ;
assume E20: InsCode c₁ = 2 ;
E21: not c₁ in {[SCM-Halt ,{} ]} by E20, E16, AMI_2:def 1, AMI_3:71, TARSKI:def 1;

E22: now

assume c₁ in { [b₁,<*b₂,b₃*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b₁ in {7,8} } ;
then consider c₂ being Element of Segm 9, c₃ being Element of SCM-Instr-Loc , c₄ being Element of SCM-Data-Loc such that
E23: c₁ = [c₂,<*c₃,c₄*>]
and E24: c₂ in {7,8} ;
InsCode c₁ = c₁ `1
.= c₂ by E23, MCART_1:7 ;
hence not verum by E20, E24, TARSKI:def 2;

end;

now

assume c₁ in { [b₁,<*b₂*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b₁ = 6 } ;
then consider c₂ being Element of Segm 9, c₃ being Element of SCM-Instr-Loc such that
E23: c₁ = [c₂,<*c₃*>]
and E24: c₂ = 6 ;
InsCode c₁ = c₁ `1
.= c₂ by E23, MCART_1:7 ;
hence not verum by E20, E24;

end;

then not c₁ in {[SCM-Halt ,{} ]} \/ { [b₁,<*b₂*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b₁ = 6 } by E21, XBOOLE_0:def 2;
then not c₁ in ({[SCM-Halt ,{} ]} \/ { [b₁,<*b₂*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc : b₁ = 6 } ) \/ { [b₁,<*b₂,b₃*>] where B is Element of Segm 9, B is Element of SCM-Instr-Loc , B is Element of SCM-Data-Loc : b₁ in {7,8} } by E22, XBOOLE_0:def 2;
then c₁ in { [b₁,<*b₂,b₃*>] where B is Element of Segm 9, B is Element of SCM-Data-Loc , B is Element of SCM-Data-Loc : b₁ in {1,2,3,4,5} } by AMI_2:def 4, AMI_3:def 1, XBOOLE_0:def 2;
then consider c₂ being Element of Segm 9, c₃, c₄ being Element of SCM-Data-Loc such that
E23: c₁ = [c₂,<*c₃,c₄*>]
and c₂ in {1,2,3,4,5} ;
E24: InsCode c₁ = c₁ `1
.= c₂ by E23, MCART_1:7 ;
reconsider c₅ = c₃ @ , c₆ = c₄ @ as Data-Location ;
take c₅ ;
take c₆ ;
( c₃ = c₃ @ & c₄ = c₄ @ ) ;
hence c₁ = AddTo c₅,c₆ by E20, E23, E24;

end;

theorem E20: :: AMI_5:49

for b₁ being Instruction of SCM holds
not (