:: The Properties of Instructions of { \bf SCM } over Ring
:: by Artur Korni{\l}owicz
::
:: Received April 14, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

theorem Th1: :: SCMRING3:1
for R being Ring
for a being Data-Location of R holds Values a = the carrier of R
proofend;

definition
let R be Ring;
let la, lb be Data-Location of R;
let a, b be Element of R;
:: original:-->
redefine func(la,lb) --> (a,b) ->  FinPartState of (SCM R);
coherence
 (la,lb) --> (a,b) is FinPartState of (SCM R)
proofend;
end;

theorem Th2: :: SCMRING3:2
for R being Ring
for a being Data-Location of R holds a <> IC
proofend;

theorem :: SCMRING3:3
for R being Ring
for o being Object of (SCM R) holds
( o = IC or o is Data-Location of R )
proofend;

theorem :: SCMRING3:4
canceled;

theorem :: SCMRING3:5
for R being Ring
for a, b being Data-Location of R holds InsCode (a := b) = 1 by RECDEF_2:def_1;

theorem :: SCMRING3:6
for R being Ring
for a, b being Data-Location of R holds InsCode (AddTo (a,b)) = 2 by RECDEF_2:def_1;

theorem :: SCMRING3:7
for R being Ring
for a, b being Data-Location of R holds InsCode (SubFrom (a,b)) = 3 by RECDEF_2:def_1;

theorem :: SCMRING3:8
for R being Ring
for a, b being Data-Location of R holds InsCode (MultBy (a,b)) = 4 by RECDEF_2:def_1;

theorem :: SCMRING3:9
for R being Ring
for r being Element of R
for a being Data-Location of R holds InsCode (a := r) = 5 by RECDEF_2:def_1;

theorem Th10: :: SCMRING3:10
for R being Ring
for i1 being Element of NAT holds InsCode (goto (i1,R)) = 6 by RECDEF_2:def_1;

theorem Th11: :: SCMRING3:11
for R being Ring
for a being Data-Location of R
for i1 being Element of NAT holds InsCode (a =0_goto i1) = 7 by RECDEF_2:def_1;

theorem Th12: :: SCMRING3:12
for R being Ring
for I being Instruction of (SCM R) st InsCode I = 0 holds
I = halt (SCM R)
proofend;

theorem Th13: :: SCMRING3:13
for R being Ring
for I being Instruction of (SCM R) st InsCode I = 1 holds
ex a, b being Data-Location of R st I = a := b
proofend;

theorem Th14: :: SCMRING3:14
for R being Ring
for I being Instruction of (SCM R) st InsCode I = 2 holds
ex a, b being Data-Location of R st I = AddTo (a,b)
proofend;

theorem Th15: :: SCMRING3:15
for R being Ring
for I being Instruction of (SCM R) st InsCode I = 3 holds
ex a, b being Data-Location of R st I = SubFrom (a,b)
proofend;

theorem Th16: :: SCMRING3:16
for R being Ring
for I being Instruction of (SCM R) st InsCode I = 4 holds
ex a, b being Data-Location of R st I = MultBy (a,b)
proofend;

theorem Th17: :: SCMRING3:17
for R being Ring
for I being Instruction of (SCM R) st InsCode I = 5 holds
ex a being Data-Location of R ex r being Element of R st I = a := r
proofend;

theorem Th18: :: SCMRING3:18
for R being Ring
for I being Instruction of (SCM R) st InsCode I = 6 holds
ex i2 being Element of NAT st I = goto (i2,R)
proofend;

theorem Th19: :: SCMRING3:19
for R being Ring
for I being Instruction of (SCM R) st InsCode I = 7 holds
ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1
proofend;

Lm1:  for x, y being set st x in dom <*y*> holds
x = 1
proofend;

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

theorem :: SCMRING3:20
for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 0 holds
JumpParts T = {0}
proofend;

theorem :: SCMRING3:21
for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 1 holds
JumpParts T = {{}}
proofend;

theorem :: SCMRING3:22
for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 2 holds
JumpParts T = {{}}
proofend;

theorem :: SCMRING3:23
for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 3 holds
JumpParts T = {{}}
proofend;

theorem :: SCMRING3:24
for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 4 holds
JumpParts T = {{}}
proofend;

theorem :: SCMRING3:25
for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 5 holds
JumpParts T = {{}}
proofend;

theorem Th26: :: SCMRING3:26
for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 6 holds
dom (product" (JumpParts T)) = {1}
proofend;

theorem Th27: :: SCMRING3:27
for R being Ring
for T being InsType of the InstructionsF of (SCM R) st T = 7 holds
dom (product" (JumpParts T)) = {1}
proofend;

theorem :: SCMRING3:28
for R being Ring
for i1 being Element of NAT holds (product" (JumpParts (InsCode (goto (i1,R))))) . 1 = NAT
proofend;

theorem :: SCMRING3:29
for R being Ring
for a being Data-Location of R
for i1 being Element of NAT holds (product" (JumpParts (InsCode (a =0_goto i1)))) . 1 = NAT
proofend;

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

registration
let R be Ring;
cluster JUMP (halt (SCM R)) ->  empty ;
coherence
 JUMP (halt (SCM R)) is empty ;
end;

registration
let R be Ring;
let a, b be Data-Location of R;
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;
end;

registration
let R be Ring;
let a be Data-Location of R;
let r be Element of R;
clustera := r ->  sequential ;
coherence
 a := r is sequential
proofend;
end;

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

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

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

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

registration
let R be Ring;
let a be Data-Location of R;
let r be Element of R;
cluster JUMP (a := r) ->  empty ;
coherence
 JUMP (a := r) is empty
proofend;
end;

theorem Th30: :: SCMRING3:30
for R being Ring
for i1, il being Element of NAT holds NIC ((goto (i1,R)),il) = {i1}
proofend;

theorem Th31: :: SCMRING3:31
for R being Ring
for i1 being Element of NAT holds JUMP (goto (i1,R)) = {i1}
proofend;

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

theorem Th32: :: SCMRING3:32
for R being Ring
for a being Data-Location of R
for i1, il being Element of NAT holds
( i1 in NIC ((a =0_goto i1),il) &amp; NIC ((a =0_goto i1),il) c= {i1,(succ il)} )
proofend;

theorem :: SCMRING3:33
for R being non trivial Ring
for a being Data-Location of R
for il, i1 being Element of NAT holds NIC ((a =0_goto i1),il) = {i1,(succ il)}
proofend;

theorem Th34: :: SCMRING3:34
for R being Ring
for a being Data-Location of R
for i1 being Element of NAT holds JUMP (a =0_goto i1) = {i1}
proofend;

registration
let R be Ring;
let a be Data-Location of R;
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 Th35: :: SCMRING3:35
for R being Ring
for il being Element of NAT holds SUCC (il,(SCM R)) = {il,(succ il)}
proofend;

theorem Th36: :: SCMRING3:36
for R being Ring
for k being Element of NAT holds
( k + 1 in SUCC (k,(SCM R)) &amp; ( for j being Element of NAT st j in SUCC (k,(SCM R)) holds
k <= j ) )
proofend;

registration
let R be Ring;
cluster SCM R ->  standard ;
coherence
 SCM R is standard
proofend;
end;

definition
let R be Ring;
let k be Element of NAT ;
func dl. (R,k) ->  Data-Location of R equals :: SCMRING3:def 1
 dl. k;
coherence
 dl. k is Data-Location of R
proofend;
end;

:: deftheorem  defines dl. SCMRING3:def_1_:_
 for R being Ring
for k being Element of NAT holds dl. (R,k) = dl. k;

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

registration
let R be Ring;
cluster halt (SCM R) ->  jump-only ;
coherence
 halt (SCM R) is jump-only
proofend;
end;

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

registration
let R be Ring;
let i1 be Element of NAT ;
cluster goto (i1,R) ->  jump-only ;
coherence
 goto (i1,R) is jump-only
proofend;
end;

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

registration
let R be Ring;
let a be Data-Location of R;
let i1 be Element of NAT ;
clustera =0_goto i1 ->  jump-only ;
coherence
 a =0_goto i1 is jump-only
proofend;
end;

registration
let S be non trivial Ring;
let p, q be Data-Location of S;
cluster InsCode (p := q) ->  non jump-only for InsType of the InstructionsF of (SCM S);
coherence
 for b1 being InsType of the InstructionsF of (SCM S) st b1 = InsCode (p := q) holds
not b1 is jump-only
proofend;
end;

registration
let S be non trivial Ring;
let p, q be Data-Location of S;
clusterp := q ->  non jump-only ;
coherence
 not p := q is jump-only
proofend;
end;

registration
let S be non trivial Ring;
let p, q be Data-Location of S;
cluster InsCode (AddTo (p,q)) ->  non jump-only for InsType of the InstructionsF of (SCM S);
coherence
 for b1 being InsType of the InstructionsF of (SCM S) st b1 = InsCode (AddTo (p,q)) holds
not b1 is jump-only
proofend;
end;

registration
let S be non trivial Ring;
let p, q be Data-Location of S;
cluster AddTo (p,q) ->  non jump-only ;
coherence
 not AddTo (p,q) is jump-only
proofend;
end;

registration
let S be non trivial Ring;
let p, q be Data-Location of S;
cluster InsCode (SubFrom (p,q)) ->  non jump-only for InsType of the InstructionsF of (SCM S);
coherence
 for b1 being InsType of the InstructionsF of (SCM S) st b1 = InsCode (SubFrom (p,q)) holds
not b1 is jump-only
proofend;
end;

registration
let S be non trivial Ring;
let p, q be Data-Location of S;
cluster SubFrom (p,q) ->  non jump-only ;
coherence
 not SubFrom (p,q) is jump-only
proofend;
end;

registration
let S be non trivial Ring;
let p, q be Data-Location of S;
cluster InsCode (MultBy (p,q)) ->  non jump-only for InsType of the InstructionsF of (SCM S);
coherence
 for b1 being InsType of the InstructionsF of (SCM S) st b1 = InsCode (MultBy (p,q)) holds
not b1 is jump-only
proofend;
end;

registration
let S be non trivial Ring;
let p, q be Data-Location of S;
cluster MultBy (p,q) ->  non jump-only ;
coherence
 not MultBy (p,q) is jump-only
proofend;
end;

registration
let S be non trivial Ring;
let p be Data-Location of S;
let w be Element of S;
cluster InsCode (p := w) ->  non jump-only for InsType of the InstructionsF of (SCM S);
coherence
 for b1 being InsType of the InstructionsF of (SCM S) st b1 = InsCode (p := w) holds
not b1 is jump-only
proofend;
end;

registration
let S be non trivial Ring;
let p be Data-Location of S;
let w be Element of S;
clusterp := w ->  non jump-only ;
coherence
 not p := w is jump-only
proofend;
end;

registration
let R be Ring;
let i1 be Element of NAT ;
cluster goto (i1,R) ->  non sequential ;
coherence
 not goto (i1,R) is sequential
proofend;
end;

registration
let R be Ring;
let a be Data-Location of R;
let i1 be Element of NAT ;
clustera =0_goto i1 ->  non sequential ;
coherence
 not a =0_goto i1 is sequential
proofend;
end;

registration
let R be Ring;
let i1 be Element of NAT ;
cluster goto (i1,R) ->  non ins-loc-free ;
coherence
 not goto (i1,R) is ins-loc-free
proofend;
end;

registration
let R be Ring;
let a be Data-Location of R;
let i1 be Element of NAT ;
clustera =0_goto i1 ->  non ins-loc-free ;
coherence
 not a =0_goto i1 is ins-loc-free
proofend;
end;

registration
let R be Ring;
cluster SCM R ->  with_explicit_jumps ;
coherence
 SCM R is with_explicit_jumps
proofend;
end;

theorem Th37: :: SCMRING3:37
for R being Ring
for i1 being Element of NAT
for k being Nat holds IncAddr ((goto (i1,R)),k) = goto ((i1 + k),R)
proofend;

theorem Th38: :: SCMRING3:38
for R being Ring
for a being Data-Location of R
for i1 being Element of NAT
for k being Nat holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)
proofend;

registration
let R be Ring;
cluster SCM R ->  IC-relocable ;
coherence
 SCM R is IC-relocable
proofend;
end;

theorem :: SCMRING3:39
for R being Ring
for I being Instruction of (SCM R) holds InsCode I <= 7
proofend;