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

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

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

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

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

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

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

theorem Th7: :: SCMFSA10:7
for a being Int-Location
for il being Nat holds a =0_goto il = [7,<*il*>,<*a*>]
proof end;

theorem Th8: :: SCMFSA10:8
for a being Int-Location
for il being Nat holds a >0_goto il = [8,<*il*>,<*a*>]
proof end;

theorem Th9: :: SCMFSA10:9

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

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

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

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

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

theorem Th15: :: SCMFSA10:15
for i1 being Nat
for a being Int-Location holds JumpPart (a =0_goto i1) = <*i1*>
proof end;

theorem Th16: :: SCMFSA10:16
for i1 being Nat
for a being Int-Location holds JumpPart (a >0_goto i1) = <*i1*>
proof end;

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem :: SCMFSA10:30
for i1 being Nat holds (product" (JumpParts (InsCode (goto i1)))) . 1 = NAT
proof end;

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

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

Lm1: for i being Instruction of SCM+FSA st ( for l being Nat holds NIC (i,l) = {(l + 1)} ) holds
JUMP i is empty

proof end;

registration
coherence
JUMP () is empty
;
end;

registration
let a, b be Int-Location;
cluster a := b -> sequential ;
coherence
a := b is sequential
by SCMFSA_2:63;
cluster AddTo (a,b) -> sequential ;
coherence
by SCMFSA_2:64;
cluster SubFrom (a,b) -> sequential ;
coherence
SubFrom (a,b) is sequential
by SCMFSA_2:65;
cluster MultBy (a,b) -> sequential ;
coherence
MultBy (a,b) is sequential
by SCMFSA_2:66;
cluster Divide (a,b) -> sequential ;
coherence
Divide (a,b) is sequential
by SCMFSA_2:67;
end;

registration
let a, b be Int-Location;
cluster JUMP (a := b) -> empty ;
coherence
JUMP (a := b) is empty
proof end;
cluster JUMP (AddTo (a,b)) -> empty ;
coherence
proof end;
cluster JUMP (SubFrom (a,b)) -> empty ;
coherence
JUMP (SubFrom (a,b)) is empty
proof end;
cluster JUMP (MultBy (a,b)) -> empty ;
coherence
JUMP (MultBy (a,b)) is empty
proof end;
cluster JUMP (Divide (a,b)) -> empty ;
coherence
JUMP (Divide (a,b)) is empty
proof end;
end;

theorem Th33: :: SCMFSA10:33
for il, i1 being Nat holds NIC ((goto i1),il) = {i1}
proof end;

theorem Th34: :: SCMFSA10:34
for i1 being Nat holds JUMP (goto i1) = {i1}
proof end;

registration
let i1 be Nat;
cluster JUMP (goto i1) -> 1 -element ;
coherence
JUMP (goto i1) is 1 -element
proof end;
end;

theorem Th35: :: SCMFSA10:35
for il, i1 being Nat
for a being Int-Location holds NIC ((a =0_goto i1),il) = {i1,(il + 1)}
proof end;

theorem Th36: :: SCMFSA10:36
for i1 being Nat
for a being Int-Location holds JUMP (a =0_goto i1) = {i1}
proof end;

registration
let a be Int-Location;
let i1 be Nat;
cluster JUMP (a =0_goto i1) -> 1 -element ;
coherence
JUMP (a =0_goto i1) is 1 -element
proof end;
end;

theorem Th37: :: SCMFSA10:37
for il, i1 being Nat
for a being Int-Location holds NIC ((a >0_goto i1),il) = {i1,(il + 1)}
proof end;

theorem Th38: :: SCMFSA10:38
for i1 being Nat
for a being Int-Location holds JUMP (a >0_goto i1) = {i1}
proof end;

registration
let a be Int-Location;
let i1 be Nat;
cluster JUMP (a >0_goto i1) -> 1 -element ;
coherence
JUMP (a >0_goto i1) is 1 -element
proof end;
end;

registration
let a, b be Int-Location;
let f be FinSeq-Location ;
cluster a := (f,b) -> sequential ;
coherence
a := (f,b) is sequential
by SCMFSA_2:72;
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
proof end;
end;

registration
let a, b be Int-Location;
let f be FinSeq-Location ;
cluster (f,b) := a -> sequential ;
coherence
(f,b) := a is sequential
by SCMFSA_2:73;
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
proof end;
end;

registration
let a be Int-Location;
let f be FinSeq-Location ;
coherence
a :=len f is sequential
by SCMFSA_2:74;
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
proof end;
end;

registration
let a be Int-Location;
let f be FinSeq-Location ;
coherence by SCMFSA_2:75;
end;

registration
let a be Int-Location;
let f be FinSeq-Location ;
cluster JUMP () -> empty ;
coherence
JUMP () is empty
proof end;
end;

theorem Th39: :: SCMFSA10:39
for il being Nat holds SUCC (il,SCM+FSA) = {il,(il + 1)}
proof end;

theorem Th40: :: SCMFSA10:40
for k being Nat holds
( k + 1 in SUCC (k,SCM+FSA) & ( for j being Nat st j in SUCC (k,SCM+FSA) holds
k <= j ) )
proof end;

registration
coherence by ;
end;

registration
cluster () 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 () holds
b1 is jump-only
proof end;
end;

registration
coherence ;
end;

registration
let i1 be 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
proof end;
end;

registration
let i1 be Nat;
cluster goto i1 -> non ins-loc-free jump-only non sequential ;
coherence
( goto i1 is jump-only & not goto i1 is sequential & not goto i1 is ins-loc-free )
proof end;
end;

registration
let a be Int-Location;
let i1 be 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
proof end;
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
proof end;
end;

registration
let a be Int-Location;
let i1 be Nat;
cluster a =0_goto i1 -> non ins-loc-free jump-only non sequential ;
coherence
( a =0_goto i1 is jump-only & not a =0_goto i1 is sequential & not a =0_goto i1 is ins-loc-free )
proof end;
cluster a >0_goto i1 -> non ins-loc-free jump-only non sequential ;
coherence
( a >0_goto i1 is jump-only & not a >0_goto i1 is sequential & not a >0_goto i1 is ins-loc-free )
proof end;
end;

Lm2:
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
proof end;
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
proof end;
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
proof end;
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
proof end;
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
proof end;
end;

Lm3:
by SCMFSA_2:99;

Lm4:
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
proof end;
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
proof end;
end;

registration
let a, b be Int-Location;
let f be FinSeq-Location ;
cluster b := (f,a) -> non jump-only ;
coherence
not b := (f,a) is jump-only
;
cluster (f,a) := b -> non jump-only ;
coherence
not (f,a) := b is jump-only
;
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
proof end;
cluster () `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 () holds
not b1 is jump-only
proof end;
end;

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

registration
coherence
proof end;
end;

theorem Th41: :: SCMFSA10:41
for i1, k being Nat holds IncAddr ((goto i1),k) = goto (i1 + k)
proof end;

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

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

registration
coherence
proof end;
end;