:: AMI_3 semantic presentation

definition
func SCM -> strict AMI-Struct of {INT } equals :: AMI_3:def 1
 AMI-Struct(# NAT ,0,SCM-Instr-Loc ,(Segm 9),SCM-Instr ,SCM-OK ,SCM-Exec #);
coherence
AMI-Struct(# NAT ,0,SCM-Instr-Loc ,(Segm 9),SCM-Instr ,SCM-OK ,SCM-Exec #) is strict AMI-Struct of {INT } ;
end;

:: deftheorem defines SCM AMI_3:def 1 :
SCM = AMI-Struct(# NAT ,0,SCM-Instr-Loc ,(Segm 9),SCM-Instr ,SCM-OK ,SCM-Exec #);

registration
cluster SCM -> non empty strict non void ;
coherence
( not SCM is empty & not SCM is void ) by AMI_1:def 3, STRUCT_0:def 1;
end;

theorem E1: :: AMI_3:1
SCM is data-oriented
proof
set c1 = SCM ;
let c2 be set ; :: according to AMI_1:def 12,TARSKI:def 3
assume E2: c2 in the Object-Kind of SCM " {the Instructions of SCM } ;
then reconsider c3 = c2 as Nat by FUNCT_2:46;
SCM-OK . c3 in {SCM-Instr } by E2, FUNCT_2:46;
then SCM-OK . c3 = SCM-Instr by TARSKI:def 1;
then consider c4 being Nat such that
E3: c3 = (2 * c4) + (2 * 1) by AMI_2:9;
( c3 = 2 * (c4 + 1) & c4 + 1 > 0 ) by E3, NAT_1:19;
hence c2 in the Instruction-Locations of SCM by AMI_2:def 3;
end;

theorem E2: :: AMI_3:2
SCM is definite
proof
let c1 be Instruction-Location of SCM ; :: according to AMI_1:def 14
reconsider c2 = c1 as Element of SCM-Instr-Loc ;
thus ObjectKind c1 = SCM-OK . c2
.= the Instructions of SCM by AMI_2:11 ;
end;

registration
cluster SCM -> non empty strict non void IC-Ins-separated data-oriented definite ;
coherence
( SCM is IC-Ins-separated & SCM is data-oriented & SCM is definite )
proof
SCM is IC-Ins-separated
proof
ObjectKind (IC SCM ) = SCM-OK . (IC SCM )
.= the Instruction-Locations of SCM by AMI_2:def 5 ;
hence SCM is IC-Ins-separated by AMI_1:def 11;
end;
hence ( SCM is IC-Ins-separated & SCM is data-oriented & SCM is definite ) by E1, E2;
end;
end;

definition
mode Data-Location -> Object of SCM means :E3: :: AMI_3:def 2
a1 in SCM-Data-Loc ;
existence
ex b1 being Object of SCM st b1 in SCM-Data-Loc
proof
consider c1 being Element of SCM-Data-Loc ;
reconsider c2 = c1 as Object of SCM ;
take c2 ;
thus c2 in SCM-Data-Loc ;
end;
end;

:: deftheorem E3 defines Data-Location AMI_3:def 2 :
for b1 being Object of SCM holds
( b1 is Data-Location iff b1 in SCM-Data-Loc );

definition
let c1 be State of SCM ;
let c2 be Data-Location ;
redefine func . as c1 . c2 -> Integer;
coherence
c1 . c2 is Integer
proof
reconsider c3 = c1 as SCM-State ;
reconsider c4 = c2 as Element of SCM-Data-Loc by E3;
c3 . c4 = c1 . c2 ;
hence c1 . c2 is Integer ;
end;
end;

definition
let c1, c2 be Data-Location ;
func c1 := c2 -> Instruction of SCM equals :: AMI_3:def 3
[1,<*a1,a2*>];
correctness
coherence
[1,<*c1,c2*>] is Instruction of SCM ;
proof
reconsider c3 = c1, c4 = c2 as Element of SCM-Data-Loc by E3;
1 in {1,2,3,4,5} by ENUMSET1:def 3;
then [1,<*c3,c4*>] in SCM-Instr by AMI_2:5;
hence [1,<*c1,c2*>] is Instruction of SCM ;
end;
func AddTo c1,c2 -> Instruction of SCM equals :: AMI_3:def 4
[2,<*a1,a2*>];
correctness
coherence
[2,<*c1,c2*>] is Instruction of SCM ;
proof
reconsider c3 = c1, c4 = c2 as Element of SCM-Data-Loc by E3;
2 in {1,2,3,4,5} by ENUMSET1:def 3;
then [2,<*c3,c4*>] in SCM-Instr by AMI_2:5;
hence [2,<*c1,c2*>] is Instruction of SCM ;
end;
func SubFrom c1,c2 -> Instruction of SCM equals :: AMI_3:def 5
[3,<*a1,a2*>];
correctness
coherence
[3,<*c1,c2*>] is Instruction of SCM ;
proof
reconsider c3 = c1, c4 = c2 as Element of SCM-Data-Loc by E3;
3 in {1,2,3,4,5} by ENUMSET1:def 3;
then [3,<*c3,c4*>] in SCM-Instr by AMI_2:5;
hence [3,<*c1,c2*>] is Instruction of SCM ;
end;
func MultBy c1,c2 -> Instruction of SCM equals :: AMI_3:def 6
[4,<*a1,a2*>];
correctness
coherence
[4,<*c1,c2*>] is Instruction of SCM ;
proof
reconsider c3 = c1, c4 = c2 as Element of SCM-Data-Loc by E3;
4 in {1,2,3,4,5} by ENUMSET1:def 3;
then [4,<*c3,c4*>] in SCM-Instr by AMI_2:5;
hence [4,<*c1,c2*>] is Instruction of SCM ;
end;
func Divide c1,c2 -> Instruction of SCM equals :: AMI_3:def 7
[5,<*a1,a2*>];
correctness
coherence
[5,<*c1,c2*>] is Instruction of SCM ;
proof
reconsider c3 = c1, c4 = c2 as Element of SCM-Data-Loc by E3;
5 in {1,2,3,4,5} by ENUMSET1:def 3;
then [5,<*c3,c4*>] in SCM-Instr by AMI_2:5;
hence [5,<*c1,c2*>] is Instruction of SCM ;
end;
end;

:: deftheorem defines := AMI_3:def 3 :
for b1, b2 being Data-Location holds b1 := b2 = [1,<*b1,b2*>];

:: deftheorem defines AddTo AMI_3:def 4 :
for b1, b2 being Data-Location holds AddTo b1,b2 = [2,<*b1,b2*>];

:: deftheorem defines SubFrom AMI_3:def 5 :
for b1, b2 being Data-Location holds SubFrom b1,b2 = [3,<*b1,b2*>];

:: deftheorem defines MultBy AMI_3:def 6 :
for b1, b2 being Data-Location holds MultBy b1,b2 = [4,<*b1,b2*>];

:: deftheorem defines Divide AMI_3:def 7 :
for b1, b2 being Data-Location holds Divide b1,b2 = [5,<*b1,b2*>];

definition
let c1 be Instruction-Location of SCM ;
func goto c1 -> Instruction of SCM equals :: AMI_3:def 8
[6,<*a1*>];
correctness
coherence
[6,<*c1*>] is Instruction of SCM ;
by AMI_2:3;
let c2 be Data-Location ;
func c2 =0_goto c1 -> Instruction of SCM equals :: AMI_3:def 9
[7,<*a1,a2*>];
correctness
coherence
[7,<*c1,c2*>] is Instruction of SCM ;
proof
reconsider c3 = c1 as Element of SCM-Instr-Loc ;
reconsider c4 = c2 as Element of SCM-Data-Loc by E3;
7 in {7,8} by TARSKI:def 2;
then [7,<*c3,c4*>] in SCM-Instr by AMI_2:4;
hence [7,<*c1,c2*>] is Instruction of SCM ;
end;
func c2 >0_goto c1 -> Instruction of SCM equals :: AMI_3:def 10
[8,<*a1,a2*>];
correctness
coherence
[8,<*c1,c2*>] is Instruction of SCM ;
proof
reconsider c3 = c1 as Element of SCM-Instr-Loc ;
reconsider c4 = c2 as Element of SCM-Data-Loc by E3;
8 in {7,8} by TARSKI:def 2;
then [8,<*c3,c4*>] in SCM-Instr by AMI_2:4;
hence [8,<*c1,c2*>] is Instruction of SCM ;
end;
end;

:: deftheorem defines goto AMI_3:def 8 :
for b1 being Instruction-Location of SCM holds goto b1 = [6,<*b1*>];

:: deftheorem defines =0_goto AMI_3:def 9 :
for b1 being Instruction-Location of SCM
for b2 being Data-Location holds b2 =0_goto b1 = [7,<*b1,b2*>];

:: deftheorem defines >0_goto AMI_3:def 10 :
for b1 being Instruction-Location of SCM
for b2 being Data-Location holds b2 >0_goto b1 = [8,<*b1,b2*>];

theorem :: AMI_3:3
canceled;

theorem :: AMI_3:4
IC SCM = 0 ;

theorem E4: :: AMI_3:5
for b1 being State of SCM
for b2 being SCM-State holds
( b2 = b1 implies IC b1 = IC b2 ) by AMI_2:def 6;

definition
let c1 be Instruction-Location of SCM ;
func Next c1 -> Instruction-Location of SCM means :E5: :: AMI_3:def 11
ex b1 being Element of SCM-Instr-Loc st
( b1 = a1 & a2 = Next b1 );
existence
ex b1 being Instruction-Location of SCM ex b2 being Element of SCM-Instr-Loc st
( b2 = c1 & b1 = Next b2 )
proof
reconsider c2 = c1 as Element of SCM-Instr-Loc ;
Next c2 is Instruction-Location of SCM ;
hence ex b1 being Instruction-Location of SCM ex b2 being Element of SCM-Instr-Loc st
( b2 = c1 & b1 = Next b2 ) ;
end;
correctness
uniqueness
for b1, b2 being Instruction-Location of SCM holds
( ( ) implies ( ( for b3 being Element of SCM-Instr-Loc holds
not ( b3 = c1 & b1 = Next b3 ) ) or ( for b3 being Element of SCM-Instr-Loc holds
not ( b3 = c1 & b2 = Next b3 ) ) or b1 = b2 ) );
;
end;

:: deftheorem E5 defines Next AMI_3:def 11 :
for b1, b2 being Instruction-Location of SCM holds
( b2 = Next b1 iff ex b3 being Element of SCM-Instr-Loc st
( b3 = b1 & b2 = Next b3 ) );

theorem E6: :: AMI_3:6
for b1 being Instruction-Location of SCM
for b2 being Element of SCM-Instr-Loc holds
( b2 = b1 implies Next b2 = Next b1 ) by E5;

theorem E7: :: AMI_3:7
for b1 being Instruction of SCM
for b2 being State of SCM
for b3 being Element of SCM-Instr holds
( b3 = b1 implies for b4 being SCM-State holds
( b4 = b2 implies Exec b1,b2 = SCM-Exec-Res b3,b4 ) ) by AMI_2:def 17;

theorem E8: :: AMI_3:8
for b1, b2 being Data-Location
for b3 being State of SCM holds
( (Exec (b1 := b2),b3) . (IC SCM ) = Next (IC b3) & (Exec (b1 := b2),b3) . b1 = b3 . b2 & ( for b4 being Data-Location holds
( b4 <> b1 implies (Exec (b1 := b2),b3) . b4 = b3 . b4 ) ) )
proof
let c1, c2 be Data-Location ;
let c3 be State of SCM ;
reconsider c4 = c1, c5 = c2 as Element of SCM-Data-Loc by E3;
reconsider c6 = c1 := c2 as Element of SCM-Instr ;
reconsider c7 = c3 as SCM-State ;
set c8 = SCM-Chg c7,(c6 address_1 ),(c7 . (c6 address_2 ));
reconsider c9 = 1 as Element of Segm 9 by GR_CY_1:10;
E9: c6 = [c9,<*c4,c5*>] ;
E10: IC c3 = IC c7 by E4;
E11: Exec (c1 := c2),c3 = SCM-Exec-Res c6,c7 by E7
.= SCM-Chg (SCM-Chg c7,(c6 address_1 ),(c7 . (c6 address_2 ))),(Next (IC c7)) by E9, AMI_2:def 16 ;
E12: ( c6 address_1 = c4 & c6 address_2 = c5 ) by E9, AMI_2:23;
thus (Exec (c1 := c2),c3) . (IC SCM ) = Next (IC c7) by E11, AMI_2:16
.= Next (IC c3) by E10, E6 ;
thus (Exec (c1 := c2),c3) . c1 = (SCM-Chg c7,(c6 address_1 ),(c7 . (c6 address_2 ))) . c4 by E11, AMI_2:17
.= c3 . c2 by E12, AMI_2:20 ;
let c10 be Data-Location ;
reconsider c11 = c10 as Element of SCM-Data-Loc by E3;
assume E13: c10 <> c1 ;
thus (Exec (c1 := c2),c3) . c10 = (SCM-Chg c7,(c6 address_1 ),(c7 . (c6 address_2 ))) . c11 by E11, AMI_2:17
.= c3 . c10 by E12, E13, AMI_2:21 ;
end;

theorem E9: :: AMI_3:9
for b1, b2 being Data-Location
for b3 being State of SCM holds
( (Exec (AddTo b1,b2),b3) . (IC SCM ) = Next (IC b3) & (Exec (AddTo b1,b2),b3) . b1 = (b3 . b1) + (b3 . b2) & ( for b4 being Data-Location holds
( b4 <> b1 implies (Exec (AddTo b1,b2),b3) . b4 = b3 . b4 ) ) )
proof
let c1, c2 be Data-Location ;
let c3 be State of SCM ;
reconsider c4 = c1, c5 = c2 as Element of SCM-Data-Loc by E3;
reconsider c6 = AddTo c1,c2 as Element of SCM-Instr ;
reconsider c7 = c3 as SCM-State ;
set c8 = SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) + (c7 . (c6 address_2 )));
reconsider c9 = 2 as Element of Segm 9 by GR_CY_1:10;
E10: c6 = [c9,<*c4,c5*>] ;
E11: IC c3 = IC c7 by E4;
E12: Exec (AddTo c1,c2),c3 = SCM-Exec-Res c6,c7 by E7
.= SCM-Chg (SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) + (c7 . (c6 address_2 )))),(Next (IC c7)) by E10, AMI_2:def 16 ;
E13: ( c6 address_1 = c4 & c6 address_2 = c5 ) by E10, AMI_2:23;
thus (Exec (AddTo c1,c2),c3) . (IC SCM ) = Next (IC c7) by E12, AMI_2:16
.= Next (IC c3) by E11, E6 ;
thus (Exec (AddTo c1,c2),c3) . c1 = (SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) + (c7 . (c6 address_2 )))) . c4 by E12, AMI_2:17
.= (c3 . c1) + (c3 . c2) by E13, AMI_2:20 ;
let c10 be Data-Location ;
reconsider c11 = c10 as Element of SCM-Data-Loc by E3;
assume E14: c10 <> c1 ;
thus (Exec (AddTo c1,c2),c3) . c10 = (SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) + (c7 . (c6 address_2 )))) . c11 by E12, AMI_2:17
.= c3 . c10 by E13, E14, AMI_2:21 ;
end;

theorem E10: :: AMI_3:10
for b1, b2 being Data-Location
for b3 being State of SCM holds
( (Exec (SubFrom b1,b2),b3) . (IC SCM ) = Next (IC b3) & (Exec (SubFrom b1,b2),b3) . b1 = (b3 . b1) - (b3 . b2) & ( for b4 being Data-Location holds
( b4 <> b1 implies (Exec (SubFrom b1,b2),b3) . b4 = b3 . b4 ) ) )
proof
let c1, c2 be Data-Location ;
let c3 be State of SCM ;
reconsider c4 = c1, c5 = c2 as Element of SCM-Data-Loc by E3;
reconsider c6 = SubFrom c1,c2 as Element of SCM-Instr ;
reconsider c7 = c3 as SCM-State ;
set c8 = SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) - (c7 . (c6 address_2 )));
reconsider c9 = 3 as Element of Segm 9 by GR_CY_1:10;
E11: c6 = [c9,<*c4,c5*>] ;
E12: IC c3 = IC c7 by E4;
E13: Exec (SubFrom c1,c2),c3 = SCM-Exec-Res c6,c7 by E7
.= SCM-Chg (SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) - (c7 . (c6 address_2 )))),(Next (IC c7)) by E11, AMI_2:def 16 ;
E14: ( c6 address_1 = c4 & c6 address_2 = c5 ) by E11, AMI_2:23;
thus (Exec (SubFrom c1,c2),c3) . (IC SCM ) = Next (IC c7) by E13, AMI_2:16
.= Next (IC c3) by E12, E6 ;
thus (Exec (SubFrom c1,c2),c3) . c1 = (SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) - (c7 . (c6 address_2 )))) . c4 by E13, AMI_2:17
.= (c3 . c1) - (c3 . c2) by E14, AMI_2:20 ;
let c10 be Data-Location ;
reconsider c11 = c10 as Element of SCM-Data-Loc by E3;
assume E15: c10 <> c1 ;
thus (Exec (SubFrom c1,c2),c3) . c10 = (SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) - (c7 . (c6 address_2 )))) . c11 by E13, AMI_2:17
.= c3 . c10 by E14, E15, AMI_2:21 ;
end;

theorem E11: :: AMI_3:11
for b1, b2 being Data-Location
for b3 being State of SCM holds
( (Exec (MultBy b1,b2),b3) . (IC SCM ) = Next (IC b3) & (Exec (MultBy b1,b2),b3) . b1 = (b3 . b1) * (b3 . b2) & ( for b4 being Data-Location holds
( b4 <> b1 implies (Exec (MultBy b1,b2),b3) . b4 = b3 . b4 ) ) )
proof
let c1, c2 be Data-Location ;
let c3 be State of SCM ;
reconsider c4 = c1, c5 = c2 as Element of SCM-Data-Loc by E3;
reconsider c6 = MultBy c1,c2 as Element of SCM-Instr ;
reconsider c7 = c3 as SCM-State ;
set c8 = SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) * (c7 . (c6 address_2 )));
reconsider c9 = 4 as Element of Segm 9 by GR_CY_1:10;
E12: c6 = [c9,<*c4,c5*>] ;
E13: IC c3 = IC c7 by E4;
E14: Exec (MultBy c1,c2),c3 = SCM-Exec-Res c6,c7 by E7
.= SCM-Chg (SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) * (c7 . (c6 address_2 )))),(Next (IC c7)) by E12, AMI_2:def 16 ;
E15: ( c6 address_1 = c4 & c6 address_2 = c5 ) by E12, AMI_2:23;
thus (Exec (MultBy c1,c2),c3) . (IC SCM ) = Next (IC c7) by E14, AMI_2:16
.= Next (IC c3) by E13, E6 ;
thus (Exec (MultBy c1,c2),c3) . c1 = (SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) * (c7 . (c6 address_2 )))) . c4 by E14, AMI_2:17
.= (c3 . c1) * (c3 . c2) by E15, AMI_2:20 ;
let c10 be Data-Location ;
reconsider c11 = c10 as Element of SCM-Data-Loc by E3;
assume E16: c10 <> c1 ;
thus (Exec (MultBy c1,c2),c3) . c10 = (SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) * (c7 . (c6 address_2 )))) . c11 by E14, AMI_2:17
.= c3 . c10 by E15, E16, AMI_2:21 ;
end;

theorem E12: :: AMI_3:12
for b1, b2 being Data-Location
for b3 being State of SCM holds
( (Exec (Divide b1,b2),b3) . (IC SCM ) = Next (IC b3) & ( b1 <> b2 implies (Exec (Divide b1,b2),b3) . b1 = (b3 . b1) div (b3 . b2) ) & (Exec (Divide b1,b2),b3) . b2 = (b3 . b1) mod (b3 . b2) & ( for b4 being Data-Location holds
( ( ) implies ( not b4 <> b1 or not b4 <> b2 or (Exec (Divide b1,b2),b3) . b4 = b3 . b4 ) ) ) )
proof
let c1, c2 be Data-Location ;
let c3 be State of SCM ;
reconsider c4 = c1, c5 = c2 as Element of SCM-Data-Loc by E3;
reconsider c6 = Divide c1,c2 as Element of SCM-Instr ;
reconsider c7 = c3 as SCM-State ;
set c8 = SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) div (c7 . (c6 address_2 )));
set c9 = SCM-Chg (SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) div (c7 . (c6 address_2 )))),(c6 address_2 ),((c7 . (c6 address_1 )) mod (c7 . (c6 address_2 )));
reconsider c10 = 5 as Element of Segm 9 by GR_CY_1:10;
E13: c6 = [c10,<*c4,c5*>] ;
E14: IC c3 = IC c7 by E4;
E15: Exec (Divide c1,c2),c3 = SCM-Exec-Res c6,c7 by E7
.= SCM-Chg (SCM-Chg (SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) div (c7 . (c6 address_2 )))),(c6 address_2 ),((c7 . (c6 address_1 )) mod (c7 . (c6 address_2 )))),(Next (IC c7)) by E13, AMI_2:def 16 ;
E16: ( c6 address_1 = c4 & c6 address_2 = c5 ) by E13, AMI_2:23;
thus (Exec (Divide c1,c2),c3) . (IC SCM ) = Next (IC c7) by E15, AMI_2:16
.= Next (IC c3) by E14, E6 ;
hereby
assume E17: c1 <> c2 ;
thus (Exec (Divide c1,c2),c3) . c1 = (SCM-Chg (SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) div (c7 . (c6 address_2 )))),(c6 address_2 ),((c7 . (c6 address_1 )) mod (c7 . (c6 address_2 )))) . c4 by E15, AMI_2:17
.= (SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) div (c7 . (c6 address_2 )))) . c4 by E16, E17, AMI_2:21
.= (c3 . c1) div (c3 . c2) by E16, AMI_2:20 ;
end;
thus (Exec (Divide c1,c2),c3) . c2 = (SCM-Chg (SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) div (c7 . (c6 address_2 )))),(c6 address_2 ),((c7 . (c6 address_1 )) mod (c7 . (c6 address_2 )))) . c5 by E15, AMI_2:17
.= (c3 . c1) mod (c3 . c2) by E16, AMI_2:20 ;
let c11 be Data-Location ;
reconsider c12 = c11 as Element of SCM-Data-Loc by E3;
assume E17: ( c11 <> c1 & c11 <> c2 ) ;
thus (Exec (Divide c1,c2),c3) . c11 = (SCM-Chg (SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) div (c7 . (c6 address_2 )))),(c6 address_2 ),((c7 . (c6 address_1 )) mod (c7 . (c6 address_2 )))) . c12 by E15, AMI_2:17
.= (SCM-Chg c7,(c6 address_1 ),((c7 . (c6 address_1 )) div (c7 . (c6 address_2 )))) . c12 by E16, E17, AMI_2:21
.= c3 . c11 by E16, E17, AMI_2:21 ;
end;

theorem :: AMI_3:13
for b1 being Data-Location
for b2 being Instruction-Location of SCM
for b3 being State of SCM holds
( (Exec (goto b2),b3) . (IC SCM ) = b2 & (Exec (goto b2),b3) . b1 = b3 . b1 )
proof
let c1 be Data-Location ;
let c2 be Instruction-Location of SCM ;
let c3 be State of SCM ;
reconsider c4 = c2 as Element of SCM-Instr-Loc ;
reconsider c5 = goto c2 as Element of SCM-Instr ;
reconsider c6 = c3 as SCM-State ;
reconsider c7 = 6 as Element of Segm 9 by GR_CY_1:10;
E13: c5 = [c7,<*c4*>] ;
E14: Exec (goto c2),c3 = SCM-Exec-Res c5,c6 by E7
.= SCM-Chg c6,(c5 jump_address ) by AMI_2:def 16 ;
c5 jump_address = c4 by E13, AMI_2:24;
hence (Exec (goto c2),c3) . (IC SCM ) = c2 by E14, AMI_2:16;
reconsider c8 = c1 as Element of SCM-Data-Loc by E3;
thus (Exec (goto c2),c3) . c1 = c6 . c8 by E14, AMI_2:17
.= c3 . c1 ;
end;

theorem E13: :: AMI_3:14
for b1, b2 being Data-Location
for b3 being Instruction-Location of SCM
for b4 being State of SCM holds
( ( b4 . b1 = 0 implies (Exec (b1 =0_goto b3),b4) . (IC SCM ) = b3 ) & ( b4 . b1 <> 0 implies (Exec (b1 =0_goto b3),b4) . (IC SCM ) = Next (IC b4) ) & (Exec (b1 =0_goto b3),b4) . b2 = b4 . b2 )
proof
let c1, c2 be Data-Location ;
let c3 be Instruction-Location of SCM ;
let c4 be State of SCM ;
reconsider c5 = c3 as Element of SCM-Instr-Loc ;
reconsider c6 = c1 as Element of SCM-Data-Loc by E3;
reconsider c7 = c1 =0_goto c3 as Element of SCM-Instr ;
reconsider c8 = c4 as SCM-State ;
reconsider c9 = 7 as Element of Segm 9 by GR_CY_1:10;
E14: c7 = [c9,<*c5,c6*>] ;
E15: IC c4 = IC c8 by E4;
E16: Exec (c1 =0_goto c3),c4 = SCM-Exec-Res c7,c8 by E7
.= SCM-Chg c8,(IFEQ (c8 . (c7 cond_address )),0,(c7 cjump_address ),(Next (IC c8))) by E14, AMI_2:def 16 ;
thus ( c4 . c1 = 0 implies (Exec (c1 =0_goto c3),c4) . (IC SCM ) = c3 )
proof
assume c4 . c1 = 0 ;
then E17: c8 . (c7 cond_address ) = 0 by E14, AMI_2:25;
thus (Exec (c1 =0_goto c3),c4) . (IC SCM ) = IFEQ (c8 . (c7 cond_address )),0,(c7 cjump_address ),(Next (IC c8)) by E16, AMI_2:16
.= c7 cjump_address by E17, CQC_LANG:def 1
.= c3 by E14, AMI_2:25 ;
end;
thus ( c4 . c1 <> 0 implies (Exec (c1 =0_goto c3),c4) . (IC SCM ) = Next (IC c4) )
proof
assume c4 . c1 <> 0 ;
then E17: c8 . (c7 cond_address ) <> 0 by E14, AMI_2:25;
thus (Exec (c1 =0_goto c3),c4) . (IC SCM ) = IFEQ (c8 . (c7 cond_address )),0,(c7 cjump_address ),(Next (IC c8)) by E16, AMI_2:16
.= Next (IC c8) by E17, CQC_LANG:def 1
.= Next (IC c4) by E15, E6 ;
end;
reconsider c10 = c2 as Element of SCM-Data-Loc by E3;
thus (Exec (c1 =0_goto c3),c4) . c2 = c8 . c10 by E16, AMI_2:17
.= c4 . c2 ;
end;

theorem E14: :: AMI_3:15
for b1, b2 being Data-Location
for b3 being Instruction-Location of SCM
for b4 being State of SCM holds
( ( b4 . b1 > 0 implies (Exec (b1 >0_goto b3),b4) . (IC SCM ) = b3 ) & ( b4 . b1 <= 0 implies (Exec (b1 >0_goto b3),b4) . (IC SCM ) = Next (IC b4) ) & (Exec (b1 >0_goto b3),b4) . b2 = b4 . b2 )
proof
let c1, c2 be Data-Location ;
let c3 be Instruction-Location of SCM ;
let c4 be State of SCM ;
reconsider c5 = c3 as Element of SCM-Instr-Loc ;
reconsider c6 = c1 as Element of SCM-Data-Loc by E3;
reconsider c7 = c1 >0_goto c3 as Element of SCM-Instr ;
reconsider c8 = c4 as SCM-State ;
reconsider c9 = 8 as Element of Segm 9 by GR_CY_1:10;
E15: c7 = [c9,<*c5,c6*>] ;
E16: IC c4 = IC c8 by E4;
E17: Exec (c1 >0_goto c3),c4 = SCM-Exec-Res c7,c8 by E7
.= SCM-Chg c8,(IFGT (c8 . (c7 cond_address )),0,(c7 cjump_address ),(Next (IC c8))) by E15, AMI_2:def 16 ;
thus ( c4 . c1 > 0 implies (Exec (c1 >0_goto c3),c4) . (IC SCM ) = c3 )
proof
assume c4 . c1 > 0 ;
then E18: c8 . (c7 cond_address ) > 0 by E15, AMI_2:25;
thus (Exec (c1 >0_goto c3),c4) . (IC SCM ) = IFGT (c8 . (c7 cond_address )),0,(c7 cjump_address ),(Next (IC c8)) by E17, AMI_2:16
.= c7 cjump_address by E18, AMI_2:def 14
.= c3 by E15, AMI_2:25 ;
end;
thus ( c4 . c1 <= 0 implies (Exec (c1 >0_goto c3),c4) . (IC SCM ) = Next (IC c4) )
proof
assume c4 . c1 <= 0 ;
then E18: c8 . (c7 cond_address ) <= 0 by E15, AMI_2:25;
thus (Exec (c1 >0_goto c3),c4) . (IC SCM ) = IFGT (c8 . (c7 cond_address )),0,(c7 cjump_address ),(Next (IC c8)) by E17, AMI_2:16
.= Next (IC c8) by E18, AMI_2:def 14
.= Next (IC c4) by E16, E6 ;
end;
reconsider c10 = c2 as Element of SCM-Data-Loc by E3;
thus (Exec (c1 >0_goto c3),c4) . c2 = c8 . c10 by E17, AMI_2:17
.= c4 . c2 ;
end;

E15: for b1 being Instruction of SCM holds
not ( ex b2 being State of SCM st (Exec b1,b2) . (IC SCM ) = Next (IC b2) & b1 is halting )
proof
let c1 be Instruction of SCM ;
given c2 being State of SCM such that E16: