:: On the Instructions of { \bf SCM }
:: by Artur Korni{\l}owicz
::
:: Received May 8, 2001
:: Copyright (c) 2001-2012 Association of Mizar Users


begin

theorem :: AMI_6:1
for T being InsType of the InstructionsF of SCM holds
( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 )
proofend;

theorem Th2: :: AMI_6:2
JumpPart (halt SCM) = {} ;

theorem :: AMI_6:3
for T being InsType of the InstructionsF of SCM st T = 0 holds
JumpParts T = {0}
proofend;

theorem :: AMI_6:4
for T being InsType of the InstructionsF of SCM st T = 1 holds
JumpParts T = {{}}
proofend;

theorem :: AMI_6:5
for T being InsType of the InstructionsF of SCM st T = 2 holds
JumpParts T = {{}}
proofend;

theorem :: AMI_6:6
for T being InsType of the InstructionsF of SCM st T = 3 holds
JumpParts T = {{}}
proofend;

theorem :: AMI_6:7
for T being InsType of the InstructionsF of SCM st T = 4 holds
JumpParts T = {{}}
proofend;

theorem :: AMI_6:8
for T being InsType of the InstructionsF of SCM st T = 5 holds
JumpParts T = {{}}
proofend;

theorem Th9: :: AMI_6:9
for T being InsType of the InstructionsF of SCM st T = 6 holds
dom (product" (JumpParts T)) = {1}
proofend;

theorem Th10: :: AMI_6:10
for T being InsType of the InstructionsF of SCM st T = 7 holds
dom (product" (JumpParts T)) = {1}
proofend;

theorem Th11: :: AMI_6:11
for T being InsType of the InstructionsF of SCM st T = 8 holds
dom (product" (JumpParts T)) = {1}
proofend;

theorem :: AMI_6:12
for k1 being Nat holds (product" (JumpParts (InsCode (SCM-goto k1)))) . 1 = NAT
proofend;

theorem :: AMI_6:13
for a being Data-Location
for k1 being Nat holds (product" (JumpParts (InsCode (a =0_goto k1)))) . 1 = NAT
proofend;

theorem :: AMI_6:14
for a being Data-Location
for k1 being Nat holds (product" (JumpParts (InsCode (a >0_goto k1)))) . 1 = NAT
proofend;

Lm1:  for i being Instruction of SCM st ( for l being Element of NAT holds NIC (i,l) = {(succ l)} ) holds
JUMP i is empty
proofend;

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

registration
let a, b be Data-Location;
clustera := b ->  sequential ;
coherence
 a := b is sequential
proofend;
cluster AddTo (a,b) ->  sequential ;
coherence
 AddTo (a,b) is sequential
proofend;
cluster SubFrom (a,b) ->  sequential ;
coherence
 SubFrom (a,b) is sequential
proofend;
cluster MultBy (a,b) ->  sequential ;
coherence
 MultBy (a,b) is sequential
proofend;
cluster Divide (a,b) ->  sequential ;
coherence
 Divide (a,b) is sequential
proofend;
end;

registration
let a, b be Data-Location;
cluster JUMP (a := b) ->  empty ;
coherence
 JUMP (a := b) is empty
proofend;
end;

registration
let a, b be Data-Location;
cluster JUMP (AddTo (a,b)) ->  empty ;
coherence
 JUMP (AddTo (a,b)) is empty
proofend;
end;

registration
let a, b be Data-Location;
cluster JUMP (SubFrom (a,b)) ->  empty ;
coherence
 JUMP (SubFrom (a,b)) is empty
proofend;
end;

registration
let a, b be Data-Location;
cluster JUMP (MultBy (a,b)) ->  empty ;
coherence
 JUMP (MultBy (a,b)) is empty
proofend;
end;

registration
let a, b be Data-Location;
cluster JUMP (Divide (a,b)) ->  empty ;
coherence
 JUMP (Divide (a,b)) is empty
proofend;
end;

theorem Th15: :: AMI_6:15
for il being Element of NAT
for k being Nat holds NIC ((SCM-goto k),il) = {k}
proofend;

theorem Th16: :: AMI_6:16
for k being Nat holds JUMP (SCM-goto k) = {k}
proofend;

registration
let i1 be Element of NAT ;
cluster JUMP (SCM-goto i1) -> 1 -element ;
coherence
 JUMP (SCM-goto i1) is 1 -element
proofend;
end;

theorem Th17: :: AMI_6:17
for a being Data-Location
for il being Element of NAT
for k being Nat holds NIC ((a =0_goto k),il) = {k,(succ il)}
proofend;

theorem Th18: :: AMI_6:18
for a being Data-Location
for k being Nat holds JUMP (a =0_goto k) = {k}
proofend;

registration
let a be Data-Location;
let i1 be Element of NAT ;
cluster JUMP (a =0_goto i1) -> 1 -element ;
coherence
 JUMP (a =0_goto i1) is 1 -element
proofend;
end;

theorem Th19: :: AMI_6:19
for a being Data-Location
for il being Element of NAT
for k being Nat holds NIC ((a >0_goto k),il) = {k,(succ il)}
proofend;

theorem Th20: :: AMI_6:20
for a being Data-Location
for k being Nat holds JUMP (a >0_goto k) = {k}
proofend;

registration
let a be Data-Location;
let i1 be Element of NAT ;
cluster JUMP (a >0_goto i1) -> 1 -element ;
coherence
 JUMP (a >0_goto i1) is 1 -element
proofend;
end;

theorem Th21: :: AMI_6:21
for il being Element of NAT holds SUCC (il,SCM) = {il,(succ il)}
proofend;

theorem Th22: :: AMI_6:22
for k being Element of NAT holds
( k + 1 in SUCC (k,SCM) & ( for j being Element of NAT st j in SUCC (k,SCM) holds
k <= j ) )
proofend;

registration
cluster SCM  ->  standard ;
coherence
 SCM is standard by Th22, AMISTD_1:3;
end;

registration
cluster InsCode (halt SCM) ->  jump-only for InsType of the InstructionsF of SCM;
coherence
 for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (halt SCM) holds
b1 is jump-only
proofend;
end;

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

registration
let i1 be Element of NAT ;
cluster InsCode (SCM-goto i1) ->  jump-only for InsType of the InstructionsF of SCM;
coherence
 for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (SCM-goto i1) holds
b1 is jump-only
proofend;
end;

registration
let i1 be Element of NAT ;
cluster SCM-goto i1 ->  non ins-loc-free jump-only non sequential ;
coherence
 ( SCM-goto i1 is jump-only &amp; not SCM-goto i1 is sequential &amp; not SCM-goto i1 is ins-loc-free )
proofend;
end;

registration
let a be Data-Location;
let i1 be Element of NAT ;
cluster InsCode (a =0_goto i1) ->  jump-only for InsType of the InstructionsF of SCM;
coherence
 for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (a =0_goto i1) holds
b1 is jump-only
proofend;
cluster InsCode (a >0_goto i1) ->  jump-only for InsType of the InstructionsF of SCM;
coherence
 for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (a >0_goto i1) holds
b1 is jump-only
proofend;
end;

registration
let a be Data-Location;
let i1 be Element of NAT ;
clustera =0_goto i1 ->  non ins-loc-free jump-only non sequential ;
coherence
 ( a =0_goto i1 is jump-only &amp; not a =0_goto i1 is sequential &amp; not a =0_goto i1 is ins-loc-free )
proofend;
clustera >0_goto i1 ->  non ins-loc-free jump-only non sequential ;
coherence
 ( a >0_goto i1 is jump-only &amp; not a >0_goto i1 is sequential &amp; not a >0_goto i1 is ins-loc-free )
proofend;
end;

Lm2:  dl. 0 <> dl. 1
by AMI_3:10;

registration
let a, b be Data-Location;
cluster InsCode (a := b) ->  non jump-only for InsType of the InstructionsF of SCM;
coherence
 for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (a := b) holds
not b1 is jump-only
proofend;
cluster InsCode (AddTo (a,b)) ->  non jump-only for InsType of the InstructionsF of SCM;
coherence
 for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (AddTo (a,b)) holds
not b1 is jump-only
proofend;
cluster InsCode (SubFrom (a,b)) ->  non jump-only for InsType of the InstructionsF of SCM;
coherence
 for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (SubFrom (a,b)) holds
not b1 is jump-only
proofend;
cluster InsCode (MultBy (a,b)) ->  non jump-only for InsType of the InstructionsF of SCM;
coherence
 for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (MultBy (a,b)) holds
not b1 is jump-only
proofend;
cluster InsCode (Divide (a,b)) ->  non jump-only for InsType of the InstructionsF of SCM;
coherence
 for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (Divide (a,b)) holds
not b1 is jump-only
proofend;
end;

registration
let a, b be Data-Location;
clustera := b ->  non jump-only ;
coherence
 not a := b is jump-only
proofend;
cluster AddTo (a,b) ->  non jump-only ;
coherence
 not AddTo (a,b) is jump-only
proofend;
cluster SubFrom (a,b) ->  non jump-only ;
coherence
 not SubFrom (a,b) is jump-only
proofend;
cluster MultBy (a,b) ->  non jump-only ;
coherence
 not MultBy (a,b) is jump-only
proofend;
cluster Divide (a,b) ->  non jump-only ;
coherence
 not Divide (a,b) is jump-only
proofend;
end;

registration
cluster SCM  ->  with_explicit_jumps ;
coherence
 SCM is with_explicit_jumps
proofend;
end;

theorem Th23: :: AMI_6:23
for i1 being Element of NAT
for k being Nat holds IncAddr ((SCM-goto i1),k) = SCM-goto (i1 + k)
proofend;

theorem Th24: :: AMI_6:24
for a being Data-Location
for i1 being Element of NAT
for k being Nat holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)
proofend;

theorem Th25: :: AMI_6:25
for a being Data-Location
for i1 being Element of NAT
for k being Nat holds IncAddr ((a >0_goto i1),k) = a >0_goto (i1 + k)
proofend;

registration
cluster SCM  ->  IC-relocable ;
coherence
 SCM is IC-relocable
proofend;
end;