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

begin

definition

let la, lb be Int-Location ;
let a, b be Integer;
:: original: -->
redefine func la,lb --> a,b -> FinPartState of ;
coherence
la,lb --> a,b is FinPartState of

proof end;

end;

theorem :: SCMFSA10:1

canceled;

theorem :: SCMFSA10:2

canceled;

theorem Th3: :: SCMFSA10:3

for a being Int-Location holds not a in NAT

proof end;

theorem Th4: :: SCMFSA10:4

for f being FinSeq-Location holds not f in NAT

proof end;

theorem Th5: :: SCMFSA10:5

SCM+FSA-Data-Loc <> NAT

proof end;

theorem Th6: :: SCMFSA10:6

SCM+FSA-Data*-Loc <> NAT

proof end;

theorem Th7: :: SCMFSA10:7

for o being Object of holds
( o = IC SCM+FSA or o in NAT or o is Int-Location or o is FinSeq-Location )

proof end;

theorem :: SCMFSA10:8

canceled;

theorem Th9: :: SCMFSA10:9

for a, b being Int-Location holds a := b = [1,<*a,b*>]

proof end;

theorem Th10: :: SCMFSA10:10

for a, b being Int-Location holds AddTo a,b = [2,<*a,b*>]

proof end;

theorem Th11: :: SCMFSA10:11

for a, b being Int-Location holds SubFrom a,b = [3,<*a,b*>]

proof end;

theorem Th12: :: SCMFSA10:12

for a, b being Int-Location holds MultBy a,b = [4,<*a,b*>]

proof end;

theorem Th13: :: SCMFSA10:13

for a, b being Int-Location holds Divide a,b = [5,<*a,b*>]

proof end;

theorem Th14: :: SCMFSA10:14

for il being Instruction-Location of SCM+FSA holds goto il = [6,<*il*>]

proof end;

theorem Th15: :: SCMFSA10:15

for a being Int-Location
for il being Instruction-Location of SCM+FSA holds a =0_goto il = [7,<*il,a*>]

proof end;

theorem Th16: :: SCMFSA10:16

for a being Int-Location
for il being Instruction-Location of SCM+FSA holds a >0_goto il = [8,<*il,a*>]

proof end;

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

proof end;

Lm2: for x, y, z being set holds
( not x in dom <*y,z*> or x = 1 or x = 2 )

proof end;

Lm3: for x, y, z, t being set holds
( not x in dom <*y,z,t*> or x = 1 or x = 2 or x = 3 )

proof end;

Lm4: for T being InsType of 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 or T = 9 or T = 10 or T = 11 or T = 12 )

proof end;

theorem Th17: :: SCMFSA10:17

AddressPart (halt SCM+FSA ) = {} by AMI_3:71, MCART_1:def 2, SCMFSA_2:123;

theorem Th18: :: SCMFSA10:18

for a, b being Int-Location holds AddressPart (a := b) = <*a,b*>

proof end;

theorem Th19: :: SCMFSA10:19

for a, b being Int-Location holds AddressPart (AddTo a,b) = <*a,b*>

proof end;

theorem Th20: :: SCMFSA10:20

for a, b being Int-Location holds AddressPart (SubFrom a,b) = <*a,b*>

proof end;

theorem Th21: :: SCMFSA10:21

for a, b being Int-Location holds AddressPart (MultBy a,b) = <*a,b*>

proof end;

theorem Th22: :: SCMFSA10:22

for a, b being Int-Location holds AddressPart (Divide a,b) = <*a,b*>

proof end;

theorem Th23: :: SCMFSA10:23

for i1 being Instruction-Location of SCM+FSA holds AddressPart (goto i1) = <*i1*>

proof end;

theorem Th24: :: SCMFSA10:24

for i1 being Instruction-Location of SCM+FSA
for a being Int-Location holds AddressPart (a =0_goto i1) = <*i1,a*>

proof end;

theorem Th25: :: SCMFSA10:25

for i1 being Instruction-Location of SCM+FSA
for a being Int-Location holds AddressPart (a >0_goto i1) = <*i1,a*>

proof end;

theorem :: SCMFSA10:26

for b, a being Int-Location
for f being FinSeq-Location holds AddressPart (b := f,a) = <*b,f,a*> by MCART_1:def 2;

theorem :: SCMFSA10:27

for a, b being Int-Location
for f being FinSeq-Location holds AddressPart (f,a := b) = <*b,f,a*> by MCART_1:def 2;

theorem :: SCMFSA10:28

for a being Int-Location
for f being FinSeq-Location holds AddressPart (a :=len f) = <*a,f*> by MCART_1:def 2;

theorem :: SCMFSA10:29

for a being Int-Location
for f being FinSeq-Location holds AddressPart (f :=<0,...,0> a) = <*a,f*> by MCART_1:def 2;

theorem Th30: :: SCMFSA10:30

for T being InsType of st T = 0 holds
AddressParts T = {0 }

proof end;

registration

let T be InsType of ;
cluster AddressParts T -> non empty ;
coherence
not AddressParts T is empty

proof end;

end;

theorem Th31: :: SCMFSA10:31

for T being InsType of st T = 1 holds
dom (product" (AddressParts T)) = {1,2}

proof end;

theorem Th32: :: SCMFSA10:32

for T being InsType of st T = 2 holds
dom (product" (AddressParts T)) = {1,2}

proof end;

theorem Th33: :: SCMFSA10:33

for T being InsType of st T = 3 holds
dom (product" (AddressParts T)) = {1,2}

proof end;

theorem Th34: :: SCMFSA10:34

for T being InsType of st T = 4 holds
dom (product" (AddressParts T)) = {1,2}

proof end;

theorem Th35: :: SCMFSA10:35

for T being InsType of st T = 5 holds
dom (product" (AddressParts T)) = {1,2}

proof end;

theorem Th36: :: SCMFSA10:36

for T being InsType of st T = 6 holds
dom (product" (AddressParts T)) = {1}

proof end;

theorem Th37: :: SCMFSA10:37

for T being InsType of st T = 7 holds
dom (product" (AddressParts T)) = {1,2}

proof end;

theorem Th38: :: SCMFSA10:38

for T being InsType of st T = 8 holds
dom (product" (AddressParts T)) = {1,2}

proof end;

theorem Th39: :: SCMFSA10:39

for T being InsType of st T = 9 holds
dom (product" (AddressParts T)) = {1,2,3}

proof end;

theorem Th40: :: SCMFSA10:40

for T being InsType of st T = 10 holds
dom (product" (AddressParts T)) = {1,2,3}

proof end;

theorem Th41: :: SCMFSA10:41

for T being InsType of st T = 11 holds
dom (product" (AddressParts T)) = {1,2}

proof end;

theorem Th42: :: SCMFSA10:42

for T being InsType of st T = 12 holds
dom (product" (AddressParts T)) = {1,2}

proof end;

theorem Th43: :: SCMFSA10:43

for a, b being Int-Location holds (product" (AddressParts (InsCode (a := b)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th44: :: SCMFSA10:44

for a, b being Int-Location holds (product" (AddressParts (InsCode (a := b)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th45: :: SCMFSA10:45

for a, b being Int-Location holds (product" (AddressParts (InsCode (AddTo a,b)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th46: :: SCMFSA10:46

for a, b being Int-Location holds (product" (AddressParts (InsCode (AddTo a,b)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th47: :: SCMFSA10:47

for a, b being Int-Location holds (product" (AddressParts (InsCode (SubFrom a,b)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th48: :: SCMFSA10:48

for a, b being Int-Location holds (product" (AddressParts (InsCode (SubFrom a,b)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th49: :: SCMFSA10:49

for a, b being Int-Location holds (product" (AddressParts (InsCode (MultBy a,b)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th50: :: SCMFSA10:50

for a, b being Int-Location holds (product" (AddressParts (InsCode (MultBy a,b)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th51: :: SCMFSA10:51

for a, b being Int-Location holds (product" (AddressParts (InsCode (Divide a,b)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th52: :: SCMFSA10:52

for a, b being Int-Location holds (product" (AddressParts (InsCode (Divide a,b)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th53: :: SCMFSA10:53

for i1 being Instruction-Location of SCM+FSA holds (product" (AddressParts (InsCode (goto i1)))) . 1 = NAT

proof end;

theorem Th54: :: SCMFSA10:54

for i1 being Instruction-Location of SCM+FSA
for a being Int-Location holds (product" (AddressParts (InsCode (a =0_goto i1)))) . 1 = NAT

proof end;

theorem Th55: :: SCMFSA10:55

for i1 being Instruction-Location of SCM+FSA
for a being Int-Location holds (product" (AddressParts (InsCode (a =0_goto i1)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th56: :: SCMFSA10:56

for i1 being Instruction-Location of SCM+FSA
for a being Int-Location holds (product" (AddressParts (InsCode (a >0_goto i1)))) . 1 = NAT

proof end;

theorem Th57: :: SCMFSA10:57

for i1 being Instruction-Location of SCM+FSA
for a being Int-Location holds (product" (AddressParts (InsCode (a >0_goto i1)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th58: :: SCMFSA10:58

for b, a being Int-Location
for f being FinSeq-Location holds (product" (AddressParts (InsCode (b := f,a)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th59: :: SCMFSA10:59

for b, a being Int-Location
for f being FinSeq-Location holds (product" (AddressParts (InsCode (b := f,a)))) . 2 = SCM+FSA-Data*-Loc

proof end;

theorem Th60: :: SCMFSA10:60

for b, a being Int-Location
for f being FinSeq-Location holds (product" (AddressParts (InsCode (b := f,a)))) . 3 = SCM+FSA-Data-Loc

proof end;

theorem Th61: :: SCMFSA10:61

for a, b being Int-Location
for f being FinSeq-Location holds (product" (AddressParts (InsCode (f,a := b)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th62: :: SCMFSA10:62

for a, b being Int-Location
for f being FinSeq-Location holds (product" (AddressParts (InsCode (f,a := b)))) . 2 = SCM+FSA-Data*-Loc

proof end;

theorem Th63: :: SCMFSA10:63

for a, b being Int-Location
for f being FinSeq-Location holds (product" (AddressParts (InsCode (f,a := b)))) . 3 = SCM+FSA-Data-Loc

proof end;

theorem Th64: :: SCMFSA10:64

for a being Int-Location
for f being FinSeq-Location holds (product" (AddressParts (InsCode (a :=len f)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th65: :: SCMFSA10:65

for a being Int-Location
for f being FinSeq-Location holds (product" (AddressParts (InsCode (a :=len f)))) . 2 = SCM+FSA-Data*-Loc

proof end;

theorem Th66: :: SCMFSA10:66

for a being Int-Location
for f being FinSeq-Location holds (product" (AddressParts (InsCode (f :=<0,...,0> a)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th67: :: SCMFSA10:67

for a being Int-Location
for f being FinSeq-Location holds (product" (AddressParts (InsCode (f :=<0,...,0> a)))) . 2 = SCM+FSA-Data*-Loc

proof end;

Lm5: for l being Instruction-Location of SCM+FSA
for i being Instruction of st ( for s being State of st IC s = l & s . l = i holds
(Exec i,s) . (IC SCM+FSA ) = Next (IC s) ) holds
NIC i,l = {(Next l)}

proof end;

Lm6: for i being Instruction of st ( for l being Instruction-Location of SCM+FSA holds NIC i,l = {(Next l)} ) holds
JUMP i is empty

proof end;

theorem Th68: :: SCMFSA10:68

for il being Instruction-Location of SCM+FSA holds NIC (halt SCM+FSA ),il = {il}

proof end;

registration

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

end;

theorem Th69: :: SCMFSA10:69

for il being Instruction-Location of SCM+FSA
for a, b being Int-Location holds NIC (a := b),il = {(Next il)}

proof end;

registration

let a, b be Int-Location ;
cluster JUMP (a := b) -> empty ;
coherence
JUMP (a := b) is empty

proof end;

end;

theorem Th70: :: SCMFSA10:70

for il being Instruction-Location of SCM+FSA
for a, b being Int-Location holds NIC (AddTo a,b),il = {(Next il)}

proof end;

registration

let a, b be Int-Location ;
cluster JUMP (AddTo a,b) -> empty ;
coherence
JUMP (AddTo a,b) is empty

proof end;

end;

theorem Th71: :: SCMFSA10:71

for il being Instruction-Location of SCM+FSA
for a, b being Int-Location holds NIC (SubFrom a,b),il = {(Next il)}

proof end;

registration

let a, b be Int-Location ;
cluster JUMP (SubFrom a,b) -> empty ;
coherence
JUMP (SubFrom a,b) is empty

proof end;

end;

theorem Th72: :: SCMFSA10:72

for il being Instruction-Location of SCM+FSA
for a, b being Int-Location holds NIC (MultBy a,b),il = {(Next il)}

proof end;

registration

let a, b be Int-Location ;
cluster JUMP (MultBy a,b) -> empty ;
coherence
JUMP (MultBy a,b) is empty

proof end;

end;

theorem Th73: :: SCMFSA10:73

for il being Instruction-Location of SCM+FSA
for a, b being Int-Location holds NIC (Divide a,b),il = {(Next il)}

proof end;

registration

let a, b be Int-Location ;
cluster JUMP (Divide a,b) -> empty ;
coherence
JUMP (Divide a,b) is empty

proof end;

end;

theorem Th74: :: SCMFSA10:74

for i1, il being Instruction-Location of SCM+FSA holds NIC (goto i1),il = {i1}

proof end;

theorem Th75: :: SCMFSA10:75

for i1 being Instruction-Location of SCM+FSA holds JUMP (goto i1) = {i1}

proof end;

registration

let i1 be Instruction-Location of SCM+FSA ;
cluster JUMP (goto i1) -> non empty trivial ;
coherence
( not JUMP (goto i1) is empty & JUMP (goto i1) is trivial )

proof end;

end;

theorem Th76: :: SCMFSA10:76

for i1, il being Instruction-Location of SCM+FSA
for a being Int-Location holds NIC (a =0_goto i1),il = {i1,(Next il)}

proof end;

theorem Th77: :: SCMFSA10:77

for i1 being Instruction-Location of SCM+FSA
for a being Int-Location holds JUMP (a =0_goto i1) = {i1}

proof end;

registration

let a be Int-Location ;
let i1 be Instruction-Location of SCM+FSA ;
cluster JUMP (a =0_goto i1) -> non empty trivial ;
coherence
( not JUMP (a =0_goto i1) is empty & JUMP (a =0_goto i1) is trivial )

proof end;

end;

theorem Th78: :: SCMFSA10:78

for i1, il being Instruction-Location of SCM+FSA
for a being Int-Location holds NIC (a >0_goto i1),il = {i1,(Next il)}

proof end;

theorem Th79: :: SCMFSA10:79

for i1 being Instruction-Location of SCM+FSA
for a being Int-Location holds JUMP (a >0_goto i1) = {i1}

proof end;

registration

let a be Int-Location ;
let i1 be Instruction-Location of SCM+FSA ;
cluster JUMP (a >0_goto i1) -> non empty trivial ;
coherence
( not JUMP (a >0_goto i1) is empty & JUMP (a >0_goto i1) is trivial )

proof end;

end;

theorem Th80: :: SCMFSA10:80

for il being Instruction-Location of SCM+FSA
for a, b being Int-Location
for f being FinSeq-Location holds NIC (a := f,b),il = {(Next il)}

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

theorem Th81: :: SCMFSA10:81

for il being Instruction-Location of SCM+FSA
for b, a being Int-Location
for f being FinSeq-Location holds NIC (f,b := a),il = {(Next il)}

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

theorem Th82: :: SCMFSA10:82

for il being Instruction-Location of SCM+FSA
for a being Int-Location
for f being FinSeq-Location holds NIC (a :=len f),il = {(Next il)}

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

theorem Th83: :: SCMFSA10:83

for il being Instruction-Location of SCM+FSA
for a being Int-Location
for f being FinSeq-Location holds NIC (f :=<0,...,0> a),il = {(Next il)}

proof 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

proof end;

end;

theorem Th84: :: SCMFSA10:84

for il being Instruction-Location of SCM+FSA holds SUCC il = {il,(Next il)}

proof end;

theorem Th85: :: SCMFSA10:85

for f being IL-Function of NAT , SCM+FSA st ( for k being Element of NAT holds f . k = insloc k ) holds
( f is bijective & ( for k being Element of NAT holds
( f . (k + 1) in SUCC (f . k) & ( for j being Element of NAT st f . j in SUCC (f . k) holds
k <= j ) ) ) )

proof end;

registration

cluster SCM+FSA -> standard ;
coherence
SCM+FSA is standard

proof end;

end;

theorem Th86: :: SCMFSA10:86

for k being natural number holds il. SCM+FSA ,k = insloc k

proof end;

theorem Th87: :: SCMFSA10:87

for k being natural number holds Next (il. SCM+FSA ,k) = il. SCM+FSA ,(k + 1)

proof end;

theorem Th88: :: SCMFSA10:88

for il being Instruction-Location of SCM+FSA holds Next il = NextLoc il

proof end;

registration

cluster (halt SCM+FSA ) `1 -> jump-only InsType of ;
coherence
for b₁ being InsType of st b₁ = InsCode (halt SCM+FSA ) holds
b₁ is jump-only

proof end;

end;

registration

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

proof end;

end;

registration

let i1 be Instruction-Location of SCM+FSA ;
cluster (goto i1) `1 -> jump-only InsType of ;
coherence
for b₁ being InsType of st b₁ = InsCode (goto i1) holds
b₁ is jump-only

proof end;

end;

registration

let i1 be Instruction-Location of SCM+FSA ;
cluster goto i1 -> jump-only non sequential non ins-loc-free ;
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 Instruction-Location of SCM+FSA ;
cluster (a =0_goto i1) `1 -> jump-only InsType of ;
coherence
for b₁ being InsType of st b₁ = InsCode (a =0_goto i1) holds
b₁ is jump-only

proof end;

cluster (a >0_goto i1) `1 -> jump-only InsType of ;
coherence
for b₁ being InsType of st b₁ = InsCode (a >0_goto i1) holds
b₁ is jump-only

proof end;

end;

registration

let a be Int-Location ;
let i1 be Instruction-Location of SCM+FSA ;
cluster a =0_goto i1 -> jump-only non sequential non ins-loc-free ;
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 -> jump-only non sequential non ins-loc-free ;
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;

Lm7: intloc 0 <> intloc 1
by AMI_3:52;

registration

let a, b be Int-Location ;
cluster (a := b) `1 -> non jump-only InsType of ;
coherence
for b₁ being InsType of st b₁ = InsCode (a := b) holds
not b₁ is jump-only

proof end;

cluster (AddTo a,b) `1 -> non jump-only InsType of ;
coherence
for b₁ being InsType of st b₁ = InsCode (AddTo a,b) holds
not b₁ is jump-only

proof end;

cluster (SubFrom a,b) `1 -> non jump-only InsType of ;
coherence
for b₁ being InsType of st b₁ = InsCode (SubFrom a,b) holds
not b₁ is jump-only

proof end;

cluster (MultBy a,b) `1 -> non jump-only InsType of ;
coherence
for b₁ being InsType of st b₁ = InsCode (MultBy a,b) holds
not b₁ is jump-only

proof end;

cluster (Divide a,b) `1 -> non jump-only InsType of ;
coherence
for b₁ being InsType of st b₁ = InsCode (Divide a,b) holds
not b₁ is jump-only

proof end;

end;

registration

let a, b be Int-Location ;
cluster a := b -> non jump-only sequential ;
coherence
( not a := b is jump-only & a := b is sequential )

proof end;

cluster AddTo a,b -> non jump-only sequential ;
coherence
( not AddTo a,b is jump-only & AddTo a,b is sequential )

proof end;

cluster SubFrom a,b -> non jump-only sequential ;
coherence
( not SubFrom a,b is jump-only & SubFrom a,b is sequential )

proof end;

cluster MultBy a,b -> non jump-only sequential ;
coherence
( not MultBy a,b is jump-only & MultBy a,b is sequential )

proof end;

cluster Divide a,b -> non jump-only sequential ;
coherence
( not Divide a,b is jump-only & Divide a,b is sequential )

proof end;

end;

Lm8: fsloc 0 <> intloc 0
by SCMFSA_2:126;

Lm9: fsloc 0 <> intloc 1
by SCMFSA_2:126;

registration

let a, b be Int-Location ;
let f be FinSeq-Location ;
cluster (b := f,a) `1 -> non jump-only InsType of ;
coherence
for b₁ being InsType of st b₁ = InsCode (b := f,a) holds
not b₁ is jump-only

proof end;

cluster (f,a := b) `1 -> non jump-only InsType of ;
coherence
for b₁ being InsType of st b₁ = InsCode (f,a := b) holds
not b₁ 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 sequential ;
coherence
( not b := f,a is jump-only & b := f,a is sequential )

proof end;

cluster f,a := b -> non jump-only sequential ;
coherence
( not f,a := b is jump-only & f,a := b is sequential )

proof end;

end;

registration

let a be Int-Location ;
let f be FinSeq-Location ;
cluster (a :=len f) `1 -> non jump-only InsType of ;
coherence
for b₁ being InsType of st b₁ = InsCode (a :=len f) holds
not b₁ is jump-only

proof end;

cluster (f :=<0,...,0> a) `1 -> non jump-only InsType of ;
coherence
for b₁ being InsType of st b₁ = InsCode (f :=<0,...,0> a) holds
not b₁ is jump-only

proof end;

end;

registration

let a be Int-Location ;
let f be FinSeq-Location ;
cluster a :=len f -> non jump-only sequential ;
coherence
( not a :=len f is jump-only & a :=len f is sequential )

proof end;

cluster f :=<0,...,0> a -> non jump-only sequential ;
coherence
( not f :=<0,...,0> a is jump-only & f :=<0,...,0> a is sequential )

proof end;

end;

registration

cluster SCM+FSA -> homogeneous with_explicit_jumps without_implicit_jumps ;
coherence
( SCM+FSA is homogeneous & SCM+FSA is with_explicit_jumps & SCM+FSA is without_implicit_jumps )

proof end;

end;

registration

cluster SCM+FSA -> regular ;
coherence
SCM+FSA is regular

proof end;

end;

theorem Th89: :: SCMFSA10:89

for i1 being Instruction-Location of SCM+FSA
for k being natural number holds IncAddr (goto i1),k = goto (il. SCM+FSA ,((locnum i1) + k))

proof end;

theorem Th90: :: SCMFSA10:90

for i1 being Instruction-Location of SCM+FSA
for k being natural number
for a being Int-Location holds IncAddr (a =0_goto i1),k = a =0_goto (il. SCM+FSA ,((locnum i1) + k))

proof end;

theorem Th91: :: SCMFSA10:91

for i1 being Instruction-Location of SCM+FSA
for k being natural number
for a being Int-Location holds IncAddr (a >0_goto i1),k = a >0_goto (il. SCM+FSA ,((locnum i1) + k))

proof end;

registration

cluster SCM+FSA -> IC-good Exec-preserving ;
coherence
( SCM+FSA is IC-good & SCM+FSA is Exec-preserving )

proof end;

end;