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


begin

definition
let la, lb be Int-Location;
let a, b be Integer;
:: original:-->
redefine func(la,lb) --> (a,b) ->  PartState of SCM+FSA;
coherence
 (la,lb) --> (a,b) is PartState of SCM+FSA
proofend;
end;

theorem Th1: :: SCMFSA10:1
for o being Object of SCM+FSA holds
( not o in Data-Locations or o is Int-Location or o is FinSeq-Location )
proofend;

theorem Th2: :: SCMFSA10:2
for a, b being Int-Location holds a := b = [1,{},<*a,b*>]
proofend;

theorem Th3: :: SCMFSA10:3
for a, b being Int-Location holds AddTo (a,b) = [2,{},<*a,b*>]
proofend;

theorem Th4: :: SCMFSA10:4
for a, b being Int-Location holds SubFrom (a,b) = [3,{},<*a,b*>]
proofend;

theorem Th5: :: SCMFSA10:5
for a, b being Int-Location holds MultBy (a,b) = [4,{},<*a,b*>]
proofend;

theorem Th6: :: SCMFSA10:6
for a, b being Int-Location holds Divide (a,b) = [5,{},<*a,b*>]
proofend;

theorem Th7: :: SCMFSA10:7
for a being Int-Location
for il being Element of NAT holds a =0_goto il = [7,<*il*>,<*a*>]
proofend;

theorem Th8: :: SCMFSA10:8
for a being Int-Location
for il being Element of NAT holds a >0_goto il = [8,<*il*>,<*a*>]
proofend;

theorem Th9: :: SCMFSA10:9
JumpPart (halt SCM+FSA) = {} ;

theorem Th10: :: SCMFSA10:10
for a, b being Int-Location holds JumpPart (a := b) = {}
proofend;

theorem Th11: :: SCMFSA10:11
for a, b being Int-Location holds JumpPart (AddTo (a,b)) = {}
proofend;

theorem Th12: :: SCMFSA10:12
for a, b being Int-Location holds JumpPart (SubFrom (a,b)) = {}
proofend;

theorem Th13: :: SCMFSA10:13
for a, b being Int-Location holds JumpPart (MultBy (a,b)) = {}
proofend;

theorem Th14: :: SCMFSA10:14
for a, b being Int-Location holds JumpPart (Divide (a,b)) = {}
proofend;

theorem Th15: :: SCMFSA10:15
for i1 being Element of NAT
for a being Int-Location holds JumpPart (a =0_goto i1) = <*i1*>
proofend;

theorem Th16: :: SCMFSA10:16
for i1 being Element of NAT
for a being Int-Location holds JumpPart (a >0_goto i1) = <*i1*>
proofend;

theorem :: SCMFSA10:17
for T being InsType of the InstructionsF of SCM+FSA st T = 0 holds
JumpParts T = {0}
proofend;

theorem :: SCMFSA10:18
for T being InsType of the InstructionsF of SCM+FSA st T = 1 holds
JumpParts T = {{}}
proofend;

theorem :: SCMFSA10:19
for T being InsType of the InstructionsF of SCM+FSA st T = 2 holds
JumpParts T = {{}}
proofend;

theorem :: SCMFSA10:20
for T being InsType of the InstructionsF of SCM+FSA st T = 3 holds
JumpParts T = {{}}
proofend;

theorem :: SCMFSA10:21
for T being InsType of the InstructionsF of SCM+FSA st T = 4 holds
JumpParts T = {{}}
proofend;

theorem :: SCMFSA10:22
for T being InsType of the InstructionsF of SCM+FSA st T = 5 holds
JumpParts T = {{}}
proofend;

theorem Th23: :: SCMFSA10:23
for T being InsType of the InstructionsF of SCM+FSA st T = 6 holds
dom (product" (JumpParts T)) = {1}
proofend;

theorem Th24: :: SCMFSA10:24
for T being InsType of the InstructionsF of SCM+FSA st T = 7 holds
dom (product" (JumpParts T)) = {1}
proofend;

theorem Th25: :: SCMFSA10:25
for T being InsType of the InstructionsF of SCM+FSA st T = 8 holds
dom (product" (JumpParts T)) = {1}
proofend;

theorem :: SCMFSA10:26
for T being InsType of the InstructionsF of SCM+FSA st T = 9 holds
JumpParts T = {{}}
proofend;

theorem :: SCMFSA10:27
for T being InsType of the InstructionsF of SCM+FSA st T = 10 holds
JumpParts T = {{}}
proofend;

theorem :: SCMFSA10:28
for T being InsType of the InstructionsF of SCM+FSA st T = 11 holds
JumpParts T = {{}}
proofend;

theorem :: SCMFSA10:29
for T being InsType of the InstructionsF of SCM+FSA st T = 12 holds
JumpParts T = {{}}
proofend;

theorem :: SCMFSA10:30
for i1 being Element of NAT holds (product" (JumpParts (InsCode (goto i1)))) . 1 = NAT
proofend;

theorem :: SCMFSA10:31
for i1 being Element of NAT
for a being Int-Location holds (product" (JumpParts (InsCode (a =0_goto i1)))) . 1 = NAT
proofend;

theorem :: SCMFSA10:32
for i1 being Element of NAT
for a being Int-Location holds (product" (JumpParts (InsCode (a >0_goto i1)))) . 1 = NAT
proofend;

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

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

registration
let a, b be Int-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 Int-Location;
cluster JUMP (a := b) ->  empty ;
coherence
 JUMP (a := b) is empty
proofend;
cluster JUMP (AddTo (a,b)) ->  empty ;
coherence
 JUMP (AddTo (a,b)) is empty
proofend;
cluster JUMP (SubFrom (a,b)) ->  empty ;
coherence
 JUMP (SubFrom (a,b)) is empty
proofend;
cluster JUMP (MultBy (a,b)) ->  empty ;
coherence
 JUMP (MultBy (a,b)) is empty
proofend;
cluster JUMP (Divide (a,b)) ->  empty ;
coherence
 JUMP (Divide (a,b)) is empty
proofend;
end;

theorem Th33: :: SCMFSA10:33
for i1, il being Element of NAT holds NIC ((goto i1),il) = {i1}
proofend;

theorem Th34: :: SCMFSA10:34
for i1 being Element of NAT holds JUMP (goto i1) = {i1}
proofend;

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

theorem Th35: :: SCMFSA10:35
for i1, il being Element of NAT
for a being Int-Location holds NIC ((a =0_goto i1),il) = {i1,(succ il)}
proofend;

theorem Th36: :: SCMFSA10:36
for i1 being Element of NAT
for a being Int-Location holds JUMP (a =0_goto i1) = {i1}
proofend;

registration
let a be Int-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 Th37: :: SCMFSA10:37
for i1, il being Element of NAT
for a being Int-Location holds NIC ((a >0_goto i1),il) = {i1,(succ il)}
proofend;

theorem Th38: :: SCMFSA10:38
for i1 being Element of NAT
for a being Int-Location holds JUMP (a >0_goto i1) = {i1}
proofend;

registration
let a be Int-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;

registration
let a, b be Int-Location;
let f be FinSeq-Location ;
clustera := (f,b) ->  sequential ;
coherence
 a := (f,b) is sequential
proofend;
end;

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

registration
let a, b be Int-Location;
let f be FinSeq-Location ;
cluster(f,b) := a ->  sequential ;
coherence
 (f,b) := a is sequential
proofend;
end;

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

registration
let a be Int-Location;
let f be FinSeq-Location ;
clustera :=len f ->  sequential ;
coherence
 a :=len f is sequential
proofend;
end;

registration
let a be Int-Location;
let f be FinSeq-Location ;
cluster JUMP (a :=len f) ->  empty ;
coherence
 JUMP (a :=len f) is empty
proofend;
end;

registration
let a be Int-Location;
let f be FinSeq-Location ;
clusterf :=<0,...,0> a ->  sequential ;
coherence
 f :=<0,...,0> a is sequential
proofend;
end;

registration
let a be Int-Location;
let f be FinSeq-Location ;
cluster JUMP (f :=<0,...,0> a) ->  empty ;
coherence
 JUMP (f :=<0,...,0> a) is empty
proofend;
end;

theorem Th39: :: SCMFSA10:39
for il being Element of NAT holds SUCC (il,SCM+FSA) = {il,(succ il)}
proofend;

theorem Th40: :: SCMFSA10:40
for k being Element of NAT holds
( k + 1 in SUCC (k,SCM+FSA) &amp; ( for j being Element of NAT st j in SUCC (k,SCM+FSA) holds
k <= j ) )
proofend;

registration
cluster SCM+FSA  ->  standard ;
coherence
 SCM+FSA is standard by Th40, AMISTD_1:3;
end;

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

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

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

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

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

registration
let a be Int-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:  intloc 0 <> intloc 1
by AMI_3:10;

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

Lm3:  fsloc 0 <> intloc 0
by SCMFSA_2:99;

Lm4:  fsloc 0 <> intloc 1
by SCMFSA_2:99;

registration
let a, b be Int-Location;
let f be FinSeq-Location ;
cluster(b := (f,a)) `1_3  ->  non jump-only for InsType of the InstructionsF of SCM+FSA;
coherence
 for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (b := (f,a)) holds
not b1 is jump-only
proofend;
cluster((f,a) := b) `1_3  ->  non jump-only for InsType of the InstructionsF of SCM+FSA;
coherence
 for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode ((f,a) := b) holds
not b1 is jump-only
proofend;
end;

registration
let a, b be Int-Location;
let f be FinSeq-Location ;
clusterb := (f,a) ->  non jump-only ;
coherence
 not b := (f,a) is jump-only
proofend;
cluster(f,a) := b ->  non jump-only ;
coherence
 not (f,a) := b is jump-only
proofend;
end;

registration
let a be Int-Location;
let f be FinSeq-Location ;
cluster(a :=len f) `1_3  ->  non jump-only for InsType of the InstructionsF of SCM+FSA;
coherence
 for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (a :=len f) holds
not b1 is jump-only
proofend;
cluster(f :=<0,...,0> a) `1_3  ->  non jump-only for InsType of the InstructionsF of SCM+FSA;
coherence
 for b1 being InsType of the InstructionsF of SCM+FSA st b1 = InsCode (f :=<0,...,0> a) holds
not b1 is jump-only
proofend;
end;

registration
let a be Int-Location;
let f be FinSeq-Location ;
clustera :=len f ->  non jump-only ;
coherence
 not a :=len f is jump-only
proofend;
clusterf :=<0,...,0> a ->  non jump-only ;
coherence
 not f :=<0,...,0> a is jump-only
proofend;
end;

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

theorem Th41: :: SCMFSA10:41
for i1 being Element of NAT
for k being Nat holds IncAddr ((goto i1),k) = goto (i1 + k)
proofend;

theorem Th42: :: SCMFSA10:42
for i1 being Element of NAT
for k being Nat
for a being Int-Location holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k)
proofend;

theorem Th43: :: SCMFSA10:43
for i1 being Element of NAT
for k being Nat
for a being Int-Location holds IncAddr ((a >0_goto i1),k) = a >0_goto (i1 + k)
proofend;

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