:: AMI_6 semantic presentation

theorem Th1: :: AMI_6:1
for b1 being Data-Location holds not b1 in the Instruction-Locations of SCM
proof end;

theorem Th2: :: AMI_6:2
SCM-Data-Loc <> the Instruction-Locations of SCM
proof end;

theorem Th3: :: AMI_6:3
for b1 being Object of SCM holds
( b1 = IC SCM or b1 in the Instruction-Locations of SCM or b1 is Data-Location )
proof end;

theorem Th4: :: AMI_6:4
for b1, b2 being Instruction-Location of SCM st b1 <> b2 holds
Next b1 <> Next b2
proof end;

theorem Th5: :: AMI_6:5
for b1 being Data-Location
for b2, b3 being State of SCM st b2,b3 equal_outside the Instruction-Locations of SCM holds
b2 . b1 = b3 . b1
proof 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 st b6 = b5 & b4 = b3 +* ((IC b2),b5 --> b6,b7) holds
( b4 . b5 = b7 & IC b4 = b5 & IC (Following b4) = (Exec (b4 . (IC b4)),b4) . (IC b2) )
proof end;

Lemma7: for b1, b2 being set st b1 in dom <*b2*> holds
b1 = 1
proof end;

Lemma8: for b1, b2, b3 being set holds
( not b1 in dom <*b2,b3*> or b1 = 1 or b1 = 2 )
proof end;

Lemma9: for b1 being InsType of SCM holds
( b1 = 0 or b1 = 1 or b1 = 2 or b1 = 3 or b1 = 4 or b1 = 5 or b1 = 6 or b1 = 7 or b1 = 8 )
proof 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*>
proof end;

theorem Th9: :: AMI_6:9
for b1, b2 being Data-Location holds AddressPart (AddTo b1,b2) = <*b1,b2*>
proof end;

theorem Th10: :: AMI_6:10
for b1, b2 being Data-Location holds AddressPart (SubFrom b1,b2) = <*b1,b2*>
proof end;

theorem Th11: :: AMI_6:11
for b1, b2 being Data-Location holds AddressPart (MultBy b1,b2) = <*b1,b2*>
proof end;

theorem Th12: :: AMI_6:12
for b1, b2 being Data-Location holds AddressPart (Divide b1,b2) = <*b1,b2*>
proof end;

theorem Th13: :: AMI_6:13
for b1 being Instruction-Location of SCM holds AddressPart (goto b1) = <*b1*>
proof end;

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*>
proof end;

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*>
proof end;

theorem Th16: :: AMI_6:16
for b1 being InsType of SCM st b1 = 0 holds
AddressParts b1 = {0}
proof end;

registration
let c1 be InsType of SCM ;
cluster AddressParts a1 -> non empty ;
coherence
not AddressParts c1 is empty
proof end;
end;

theorem Th17: :: AMI_6:17
for b1 being InsType of SCM st b1 = 1 holds
dom (PA (AddressParts b1)) = {1,2}
proof end;

theorem Th18: :: AMI_6:18
for b1 being InsType of SCM st b1 = 2 holds
dom (PA (AddressParts b1)) = {1,2}
proof end;

theorem Th19: :: AMI_6:19
for b1 being InsType of SCM st b1 = 3 holds
dom (PA (AddressParts b1)) = {1,2}
proof end;

theorem Th20: :: AMI_6:20
for b1 being InsType of SCM st b1 = 4 holds
dom (PA (AddressParts b1)) = {1,2}
proof end;

theorem Th21: :: AMI_6:21
for b1 being InsType of SCM st b1 = 5 holds
dom (PA (AddressParts b1)) = {1,2}
proof end;

theorem Th22: :: AMI_6:22
for b1 being InsType of SCM st b1 = 6 holds
dom (PA (AddressParts b1)) = {1}
proof end;

theorem Th23: :: AMI_6:23
for b1 being InsType of SCM st b1 = 7 holds
dom (PA (AddressParts b1)) = {1,2}
proof end;

theorem Th24: :: AMI_6:24
for b1 being InsType of SCM st b1 = 8 holds
dom (PA (AddressParts b1)) = {1,2}
proof end;

theorem Th25: :: AMI_6:25
for b1, b2 being Data-Location holds (PA (AddressParts (InsCode (b1 := b2)))) . 1 = SCM-Data-Loc
proof end;

theorem Th26: :: AMI_6:26
for b1, b2 being Data-Location holds (PA (AddressParts (InsCode (b1 := b2)))) . 2 = SCM-Data-Loc
proof end;

theorem Th27: :: AMI_6:27
for b1, b2 being Data-Location holds (PA (AddressParts (InsCode (AddTo b1,b2)))) . 1 = SCM-Data-Loc
proof end;

theorem Th28: :: AMI_6:28
for b1, b2 being Data-Location holds (PA (AddressParts (InsCode (AddTo b1,b2)))) . 2 = SCM-Data-Loc
proof end;

theorem Th29: :: AMI_6:29
for b1, b2 being Data-Location holds (PA (AddressParts (InsCode (SubFrom b1,b2)))) . 1 = SCM-Data-Loc
proof end;

theorem Th30: :: AMI_6:30
for b1, b2 being Data-Location holds (PA (AddressParts (InsCode (SubFrom b1,b2)))) . 2 = SCM-Data-Loc
proof end;

theorem Th31: :: AMI_6:31
for b1, b2 being Data-Location holds (PA (AddressParts (InsCode (MultBy b1,b2)))) . 1 = SCM-Data-Loc
proof end;

theorem Th32: :: AMI_6:32
for b1, b2 being Data-Location holds (PA (AddressParts (InsCode (MultBy b1,b2)))) . 2 = SCM-Data-Loc
proof end;

theorem Th33: :: AMI_6:33
for b1, b2 being Data-Location holds (PA (AddressParts (InsCode (Divide b1,b2)))) . 1 = SCM-Data-Loc
proof end;

theorem Th34: :: AMI_6:34
for b1, b2 being Data-Location holds (PA (AddressParts (InsCode (Divide b1,b2)))) . 2 = SCM-Data-Loc
proof end;

theorem Th35: :: AMI_6:35
for b1 being Instruction-Location of SCM holds (PA (AddressParts (InsCode (goto b1)))) . 1 = the Instruction-Locations of SCM
proof end;

theorem Th36: :: AMI_6:36
for b1 being Data-Location
for b2 being Instruction-Location of SCM holds (PA (AddressParts (InsCode (b1 =0_goto b2)))) . 1 = the Instruction-Locations of SCM
proof end;

theorem Th37: :: AMI_6:37
for b1 being Data-Location
for b2 being Instruction-Location of SCM holds (PA (AddressParts (InsCode (b1 =0_goto b2)))) . 2 = SCM-Data-Loc
proof end;

theorem Th38: :: AMI_6:38
for b1 being Data-Location
for b2 being Instruction-Location of SCM holds (PA (AddressParts (InsCode (b1 >0_goto b2)))) . 1 = the Instruction-Locations of SCM
proof end;

theorem Th39: :: AMI_6:39
for b1 being Data-Location
for b2 being Instruction-Location of SCM holds (PA (AddressParts (InsCode (b1 >0_goto b2)))) . 2 = SCM-Data-Loc
proof end;

Lemma43: for b1 being Instruction-Location of SCM
for b2 being Instruction of SCM st ( for b3 being State of SCM st IC b3 = b1 & b3 . b1 = b2 holds
(Exec b2,b3) . (IC SCM ) = Next (IC b3) ) holds
NIC b2,b1 = {(Next b1)}
proof end;

Lemma44: for b1 being Instruction of SCM st ( for b2 being Instruction-Location of SCM holds NIC b1,b2 = {(Next b2)} ) holds
JUMP b1 is empty
proof end;

theorem Th40: :: AMI_6:40
for b1 being Instruction-Location of SCM holds NIC (halt SCM ),b1 = {b1}
proof end;

registration
cluster JUMP (halt SCM ) -> empty ;
coherence
JUMP (halt SCM ) is empty
proof end;
end;

theorem Th41: :: AMI_6:41
for b1, b2 being Data-Location
for b3 being Instruction-Location of SCM holds NIC (b1 := b2),b3 = {(Next b3)}
proof end;

registration
let c1, c2 be Data-Location ;
cluster JUMP (a1 := a2) -> empty ;
coherence
JUMP (c1 := c2) is empty
proof end;
end;

theorem Th42: :: AMI_6:42
for b1, b2 being Data-Location
for b3 being Instruction-Location of SCM holds NIC (AddTo b1,b2),b3 = {(Next b3)}
proof end;

registration
let c1, c2 be Data-Location ;
cluster JUMP (AddTo a1,a2) -> empty ;
coherence
JUMP (AddTo c1,c2) is empty
proof end;
end;

theorem Th43: :: AMI_6:43
for b1, b2 being Data-Location
for b3 being Instruction-Location of SCM holds NIC (SubFrom b1,b2),b3 = {(Next b3)}
proof end;

registration
let c1, c2 be Data-Location ;
cluster JUMP (SubFrom a1,a2) -> empty ;
coherence
JUMP (SubFrom c1,c2) is empty
proof end;
end;

theorem Th44: :: AMI_6:44
for b1, b2 being Data-Location
for b3 being Instruction-Location of SCM holds NIC (MultBy b1,b2),b3 = {(Next b3)}
proof end;

registration
let c1, c2 be Data-Location ;
cluster JUMP (MultBy a1,a2) -> empty ;
coherence
JUMP (MultBy c1,c2) is empty
proof end;
end;

theorem Th45: :: AMI_6:45
for b1, b2 being Data-Location
for b3 being Instruction-Location of SCM holds NIC (Divide b1,b2),b3 = {(Next b3)}
proof end;

registration
let c1, c2 be Data-Location ;
cluster JUMP (Divide a1,a2) -> empty ;
coherence
JUMP (Divide c1,c2) is empty
proof end;
end;

theorem Th46: :: AMI_6:46
for b1, b2 being Instruction-Location of SCM holds NIC (goto b1),b2 = {b1}
proof end;

theorem Th47: :: AMI_6:47
for b1 being Instruction-Location of SCM holds JUMP (goto b1) = {b1}
proof end;

registration
let c1 be Instruction-Location of SCM ;
cluster JUMP (goto a1) -> non empty trivial ;
coherence
( not JUMP (goto c1) is empty & JUMP (goto c1) is trivial )
proof end;
end;

theorem Th48: :: AMI_6:48
for b1 being Data-Location
for b2, b3 being Instruction-Location of SCM holds NIC (b1 =0_goto b2),b3 = {b2,(Next b3)}
proof end;

theorem Th49: :: AMI_6:49
for b1 being Data-Location
for b2 being Instruction-Location of SCM holds JUMP (b1 =0_goto b2) = {b2}
proof end;

registration
let c1 be Data-Location ;
let c2 be Instruction-Location of SCM ;
cluster JUMP (a1 =0_goto a2) -> non empty trivial ;
coherence
( not JUMP (c1 =0_goto c2) is empty & JUMP (c1 =0_goto c2) is trivial )
proof end;
end;

theorem Th50: :: AMI_6:50
for b1 being Data-Location
for b2, b3 being Instruction-Location of SCM holds NIC (b1 >0_goto b2),b3 = {b2,(Next b3)}
proof end;

theorem Th51: :: AMI_6:51
for b1 being Data-Location
for b2 being Instruction-Location of SCM holds JUMP (b1 >0_goto b2) = {b2}
proof end;

registration
let c1 be Data-Location ;
let c2 be Instruction-Location of SCM ;
cluster JUMP (a1 >0_goto a2) -> non empty trivial ;
coherence
( not JUMP (c1 >0_goto c2) is empty & JUMP (c1 >0_goto c2) is trivial )
proof end;
end;

theorem Th52: :: AMI_6:52
for b1 being Instruction-Location of SCM holds SUCC b1 = {b1,(Next b1)}
proof end;

theorem Th53: :: AMI_6:53
for b1 being Function of NAT ,the Instruction-Locations of SCM st ( for b2 being Nat holds b1 . b2 = il. b2 ) holds
( b1 is bijective & ( for b2 being Nat holds
( b1 . (b2 + 1) in SUCC (b1 . b2) & ( for b3 being Nat st b1 . b3 in SUCC (b1 . b2) holds
b2 <= b3 ) ) ) )
proof end;

registration
cluster SCM -> standard ;
coherence
SCM is standard
proof end;
end;

theorem Th54: :: AMI_6:54
for b1 being natural number holds il. SCM ,b1 = il. b1
proof end;

theorem Th55: :: AMI_6:55
for b1 being natural number holds Next (il. SCM ,b1) = il. SCM ,(b1 + 1)
proof end;

theorem Th56: :: AMI_6:56
for b1 being Instruction-Location of SCM holds Next b1 = NextLoc b1
proof end;

registration
cluster InsCode (halt SCM ) -> jump-only ;
coherence
InsCode (halt SCM ) is jump-only
proof end;
end;

registration
cluster halt SCM -> jump-only ;
coherence
halt SCM is jump-only
proof end;
end;

registration
let c1 be Instruction-Location of SCM ;
cluster InsCode (goto a1) -> jump-only ;
coherence
InsCode (goto c1) is jump-only
proof end;
end;

registration
let c1 be Instruction-Location of SCM ;
cluster goto a1 -> jump-only non sequential non ins-loc-free ;
coherence
( goto c1 is jump-only & not goto c1 is sequential & not goto c1 is ins-loc-free )
proof end;
end;

registration
let c1 be Data-Location ;
let c2 be Instruction-Location of SCM ;
cluster InsCode (a1 =0_goto a2) -> jump-only ;
coherence
InsCode (c1 =0_goto c2) is jump-only
proof end;
cluster InsCode (a1 >0_goto a2) -> jump-only ;
coherence
InsCode (c1 >0_goto c2) is jump-only
proof end;
end;

registration
let c1 be Data-Location ;
let c2 be Instruction-Location of SCM ;
cluster a1 =0_goto a2 -> jump-only non sequential non ins-loc-free ;
coherence
( c1 =0_goto c2 is jump-only & not c1 =0_goto c2 is sequential & not c1 =0_goto c2 is ins-loc-free )
proof end;
cluster a1 >0_goto a2 -> jump-only non sequential non ins-loc-free ;
coherence
( c1 >0_goto c2 is jump-only & not c1 >0_goto c2 is sequential & not c1 >0_goto c2 is ins-loc-free )
proof end;
end;

registration
let c1, c2 be Data-Location ;
cluster InsCode (a1 := a2) -> non jump-only ;
coherence
not InsCode (c1 := c2) is jump-only
proof end;
cluster InsCode (AddTo a1,a2) -> non jump-only ;
coherence
not InsCode (AddTo c1,c2) is jump-only
proof end;
cluster InsCode (SubFrom a1,a2) -> non jump-only ;
coherence
not InsCode (SubFrom c1,c2) is jump-only
proof end;
cluster InsCode (MultBy a1,a2) -> non jump-only ;
coherence
not InsCode (MultBy c1,c2) is jump-only
proof end;
cluster InsCode (Divide a1,a2) -> non jump-only ;
coherence
not InsCode (Divide c1,c2) is jump-only
proof end;
end;

registration
let c1, c2 be Data-Location ;
cluster a1 := a2 -> non jump-only sequential ;
coherence
( not c1 := c2 is jump-only & c1 := c2 is sequential )
proof end;
cluster AddTo a1,a2 -> non jump-only sequential ;
coherence
( not AddTo c1,c2 is jump-only & AddTo c1,c2 is sequential )
proof end;
cluster SubFrom a1,a2 -> non jump-only sequential ;
coherence
( not SubFrom c1,c2 is jump-only & SubFrom c1,c2 is sequential )
proof end;
cluster MultBy a1,a2 -> non jump-only sequential ;
coherence
( not MultBy c1,c2 is jump-only & MultBy c1,c2 is sequential )
proof end;
cluster Divide a1,a2 -> non jump-only sequential ;
coherence
( not Divide c1,c2 is jump-only & Divide c1,c2 is sequential )
proof end;
end;

registration
cluster SCM -> standard homogeneous with_explicit_jumps without_implicit_jumps ;
coherence
( SCM is homogeneous & SCM is with_explicit_jumps & SCM is without_implicit_jumps )
proof end;
end;

registration
cluster SCM -> standard homogeneous with_explicit_jumps without_implicit_jumps regular ;
coherence
SCM is regular
proof end;
end;

theorem Th57: :: AMI_6:57
for b1 being Instruction-Location of SCM
for b2 being natural number holds IncAddr (goto b1),b2 = goto (il. SCM ,((locnum b1) + b2))
proof end;

theorem Th58: :: AMI_6:58
for b1 being Data-Location
for b2 being Instruction-Location of SCM
for b3 being natural number holds IncAddr (b1 =0_goto b2),b3 = b1 =0_goto (il. SCM ,((locnum b2) + b3))
proof end;

theorem Th59: :: AMI_6:59
for b1 being Data-Location
for b2 being Instruction-Location of SCM
for b3 being natural number holds IncAddr (b1 >0_goto b2),b3 = b1 >0_goto (il. SCM ,((locnum b2) + b3))
proof end;

registration
cluster SCM -> standard homogeneous with_explicit_jumps without_implicit_jumps regular IC-good Exec-preserving ;
coherence
( SCM is IC-good & SCM is Exec-preserving )
proof end;
end;