:: SCMFSA10 semantic presentation

theorem Th1: :: SCMFSA10:1

for b₁ being Function
for b₂, b₃, b₄, b₅, b₆, b₇ being set st b₂ <> b₄ & b₂ <> b₆ holds
(((b₁ +* (b₂ .--> b₃)) +* (b₄ .--> b₅)) +* (b₆ .--> b₇)) . b₂ = b₃

proof end;

theorem Th2: :: SCMFSA10:2

for b₁, b₂ being set holds <*b₁*> +* 1,b₂ = <*b₂*>

proof end;

definition

let c₁, c₂ be Int-Location ;
let c₃, c₄ be Integer;
redefine func --> as c₁,c₂ --> c₃,c₄ -> FinPartState of SCM+FSA ;
coherence

proof end;

end;

theorem Th3: :: SCMFSA10:3

for b₁ being Int-Location holds not b₁ in the Instruction-Locations of SCM+FSA

proof end;

theorem Th4: :: SCMFSA10:4

for b₁ being FinSeq-Location holds not b₁ in the Instruction-Locations of SCM+FSA

proof end;

theorem Th5: :: SCMFSA10:5

SCM+FSA-Data-Loc <> the Instruction-Locations of SCM+FSA

proof end;

theorem Th6: :: SCMFSA10:6

SCM+FSA-Data*-Loc <> the Instruction-Locations of SCM+FSA

proof end;

theorem Th7: :: SCMFSA10:7

for b₁ being Object of SCM+FSA holds
( b₁ = IC SCM+FSA or b₁ in the Instruction-Locations of SCM+FSA or b₁ is Int-Location or b₁ is FinSeq-Location )

proof end;

theorem Th8: :: SCMFSA10:8

for b₁, b₂ being Instruction-Location of SCM+FSA st b₁ <> b₂ holds
Next b₁ <> Next b₂

proof end;

theorem Th9: :: SCMFSA10:9

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

proof end;

theorem Th10: :: SCMFSA10:10

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

proof end;

theorem Th11: :: SCMFSA10:11

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

proof end;

theorem Th12: :: SCMFSA10:12

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

proof end;

theorem Th13: :: SCMFSA10:13

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

proof end;

theorem Th14: :: SCMFSA10:14

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

proof end;

theorem Th15: :: SCMFSA10:15

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

proof end;

theorem Th16: :: SCMFSA10:16

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

proof end;

Lemma17: for b₁, b₂ being set st b₁ in dom <*b₂*> holds
b₁ = 1

proof end;

Lemma18: for b₁, b₂, b₃ being set holds
( not b₁ in dom <*b₂,b₃*> or b₁ = 1 or b₁ = 2 )

proof end;

Lemma19: for b₁, b₂, b₃, b₄ being set holds
( not b₁ in dom <*b₂,b₃,b₄*> or b₁ = 1 or b₁ = 2 or b₁ = 3 )

proof end;

Lemma20: for b₁ being InsType of SCM+FSA holds
( b₁ = 0 or b₁ = 1 or b₁ = 2 or b₁ = 3 or b₁ = 4 or b₁ = 5 or b₁ = 6 or b₁ = 7 or b₁ = 8 or b₁ = 9 or b₁ = 10 or b₁ = 11 or b₁ = 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 b₁, b₂ being Int-Location holds AddressPart (b₁ := b₂) = <*b₁,b₂*>

proof end;

theorem Th19: :: SCMFSA10:19

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

proof end;

theorem Th20: :: SCMFSA10:20

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

proof end;

theorem Th21: :: SCMFSA10:21

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

proof end;

theorem Th22: :: SCMFSA10:22

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

proof end;

theorem Th23: :: SCMFSA10:23

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

proof end;

theorem Th24: :: SCMFSA10:24

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

proof end;

theorem Th25: :: SCMFSA10:25

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

proof end;

theorem Th26: :: SCMFSA10:26

for b₁, b₂ being Int-Location
for b₃ being FinSeq-Location holds AddressPart (b₁ := b₃,b₂) = <*b₁,b₃,b₂*>

proof end;

theorem Th27: :: SCMFSA10:27

for b₁, b₂ being Int-Location
for b₃ being FinSeq-Location holds AddressPart (b₃,b₁ := b₂) = <*b₂,b₃,b₁*>

proof end;

theorem Th28: :: SCMFSA10:28

for b₁ being Int-Location
for b₂ being FinSeq-Location holds AddressPart (b₁ :=len b₂) = <*b₁,b₂*>

proof end;

theorem Th29: :: SCMFSA10:29

for b₁ being Int-Location
for b₂ being FinSeq-Location holds AddressPart (b₂ :=<0,...,0> b₁) = <*b₁,b₂*>

proof end;

theorem Th30: :: SCMFSA10:30

for b₁ being InsType of SCM+FSA st b₁ = 0 holds
AddressParts b₁ = {0}

proof end;

registration

let c₁ be InsType of SCM+FSA ;
cluster AddressParts a₁ -> non empty ;
coherence

proof end;

end;

theorem Th31: :: SCMFSA10:31

for b₁ being InsType of SCM+FSA st b₁ = 1 holds
dom (PA (AddressParts b₁)) = {1,2}

proof end;

theorem Th32: :: SCMFSA10:32

for b₁ being InsType of SCM+FSA st b₁ = 2 holds
dom (PA (AddressParts b₁)) = {1,2}

proof end;

theorem Th33: :: SCMFSA10:33

for b₁ being InsType of SCM+FSA st b₁ = 3 holds
dom (PA (AddressParts b₁)) = {1,2}

proof end;

theorem Th34: :: SCMFSA10:34

for b₁ being InsType of SCM+FSA st b₁ = 4 holds
dom (PA (AddressParts b₁)) = {1,2}

proof end;

theorem Th35: :: SCMFSA10:35

for b₁ being InsType of SCM+FSA st b₁ = 5 holds
dom (PA (AddressParts b₁)) = {1,2}

proof end;

theorem Th36: :: SCMFSA10:36

for b₁ being InsType of SCM+FSA st b₁ = 6 holds
dom (PA (AddressParts b₁)) = {1}

proof end;

theorem Th37: :: SCMFSA10:37

for b₁ being InsType of SCM+FSA st b₁ = 7 holds
dom (PA (AddressParts b₁)) = {1,2}

proof end;

theorem Th38: :: SCMFSA10:38

for b₁ being InsType of SCM+FSA st b₁ = 8 holds
dom (PA (AddressParts b₁)) = {1,2}

proof end;

theorem Th39: :: SCMFSA10:39

for b₁ being InsType of SCM+FSA st b₁ = 9 holds
dom (PA (AddressParts b₁)) = {1,2,3}

proof end;

theorem Th40: :: SCMFSA10:40

for b₁ being InsType of SCM+FSA st b₁ = 10 holds
dom (PA (AddressParts b₁)) = {1,2,3}

proof end;

theorem Th41: :: SCMFSA10:41

for b₁ being InsType of SCM+FSA st b₁ = 11 holds
dom (PA (AddressParts b₁)) = {1,2}

proof end;

theorem Th42: :: SCMFSA10:42

for b₁ being InsType of SCM+FSA st b₁ = 12 holds
dom (PA (AddressParts b₁)) = {1,2}

proof end;

theorem Th43: :: SCMFSA10:43

for b₁, b₂ being Int-Location holds (PA (AddressParts (InsCode (b₁ := b₂)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th44: :: SCMFSA10:44

for b₁, b₂ being Int-Location holds (PA (AddressParts (InsCode (b₁ := b₂)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th45: :: SCMFSA10:45

for b₁, b₂ being Int-Location holds (PA (AddressParts (InsCode (AddTo b₁,b₂)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th46: :: SCMFSA10:46

for b₁, b₂ being Int-Location holds (PA (AddressParts (InsCode (AddTo b₁,b₂)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th47: :: SCMFSA10:47

for b₁, b₂ being Int-Location holds (PA (AddressParts (InsCode (SubFrom b₁,b₂)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th48: :: SCMFSA10:48

for b₁, b₂ being Int-Location holds (PA (AddressParts (InsCode (SubFrom b₁,b₂)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th49: :: SCMFSA10:49

for b₁, b₂ being Int-Location holds (PA (AddressParts (InsCode (MultBy b₁,b₂)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th50: :: SCMFSA10:50

for b₁, b₂ being Int-Location holds (PA (AddressParts (InsCode (MultBy b₁,b₂)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th51: :: SCMFSA10:51

for b₁, b₂ being Int-Location holds (PA (AddressParts (InsCode (Divide b₁,b₂)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th52: :: SCMFSA10:52

for b₁, b₂ being Int-Location holds (PA (AddressParts (InsCode (Divide b₁,b₂)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th53: :: SCMFSA10:53

for b₁ being Instruction-Location of SCM+FSA holds (PA (AddressParts (InsCode (goto b₁)))) . 1 = the Instruction-Locations of SCM+FSA

proof end;

theorem Th54: :: SCMFSA10:54

for b₁ being Int-Location
for b₂ being Instruction-Location of SCM+FSA holds (PA (AddressParts (InsCode (b₁ =0_goto b₂)))) . 1 = the Instruction-Locations of SCM+FSA

proof end;

theorem Th55: :: SCMFSA10:55

for b₁ being Int-Location
for b₂ being Instruction-Location of SCM+FSA holds (PA (AddressParts (InsCode (b₁ =0_goto b₂)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th56: :: SCMFSA10:56

for b₁ being Int-Location
for b₂ being Instruction-Location of SCM+FSA holds (PA (AddressParts (InsCode (b₁ >0_goto b₂)))) . 1 = the Instruction-Locations of SCM+FSA

proof end;

theorem Th57: :: SCMFSA10:57

for b₁ being Int-Location
for b₂ being Instruction-Location of SCM+FSA holds (PA (AddressParts (InsCode (b₁ >0_goto b₂)))) . 2 = SCM+FSA-Data-Loc

proof end;

theorem Th58: :: SCMFSA10:58

for b₁, b₂ being Int-Location
for b₃ being FinSeq-Location holds (PA (AddressParts (InsCode (b₁ := b₃,b₂)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th59: :: SCMFSA10:59

for b₁, b₂ being Int-Location
for b₃ being FinSeq-Location holds (PA (AddressParts (InsCode (b₁ := b₃,b₂)))) . 2 = SCM+FSA-Data*-Loc

proof end;

theorem Th60: :: SCMFSA10:60

for b₁, b₂ being Int-Location
for b₃ being FinSeq-Location holds (PA (AddressParts (InsCode (b₁ := b₃,b₂)))) . 3 = SCM+FSA-Data-Loc

proof end;

theorem Th61: :: SCMFSA10:61

for b₁, b₂ being Int-Location
for b₃ being FinSeq-Location holds (PA (AddressParts (InsCode (b₃,b₁ := b₂)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th62: :: SCMFSA10:62

for b₁, b₂ being Int-Location
for b₃ being FinSeq-Location holds (PA (AddressParts (InsCode (b₃,b₁ := b₂)))) . 2 = SCM+FSA-Data*-Loc

proof end;

theorem Th63: :: SCMFSA10:63

for b₁, b₂ being Int-Location
for b₃ being FinSeq-Location holds (PA (AddressParts (InsCode (b₃,b₁ := b₂)))) . 3 = SCM+FSA-Data-Loc

proof end;

theorem Th64: :: SCMFSA10:64

for b₁ being Int-Location
for b₂ being FinSeq-Location holds (PA (AddressParts (InsCode (b₁ :=len b₂)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th65: :: SCMFSA10:65

for b₁ being Int-Location
for b₂ being FinSeq-Location holds (PA (AddressParts (InsCode (b₁ :=len b₂)))) . 2 = SCM+FSA-Data*-Loc

proof end;

theorem Th66: :: SCMFSA10:66

for b₁ being Int-Location
for b₂ being FinSeq-Location holds (PA (AddressParts (InsCode (b₂ :=<0,...,0> b₁)))) . 1 = SCM+FSA-Data-Loc

proof end;

theorem Th67: :: SCMFSA10:67

for b₁ being Int-Location
for b₂ being FinSeq-Location holds (PA (AddressParts (InsCode (b₂ :=<0,...,0> b₁)))) . 2 = SCM+FSA-Data*-Loc

proof end;

Lemma72: for b₁ being Instruction-Location of SCM+FSA
for b₂ being Instruction of SCM+FSA st ( for b₃ being State of SCM+FSA st IC b₃ = b₁ & b₃ . b₁ = b₂ holds
(Exec b₂,b₃) . (IC SCM+FSA ) = Next (IC b₃) ) holds
NIC b₂,b₁ = {(Next b₁)}

proof end;

Lemma73: for b₁ being Instruction of SCM+FSA st ( for b₂ being Instruction-Location of SCM+FSA holds NIC b₁,b₂ = {(Next b₂)} ) holds
JUMP b₁ is empty

proof end;

theorem Th68: :: SCMFSA10:68

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

proof end;

registration

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

proof end;

end;

theorem Th69: :: SCMFSA10:69

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

proof end;

registration

let c₁, c₂ be Int-Location ;
cluster JUMP (a₁ := a₂) -> empty ;
coherence

proof end;

end;

theorem Th70: :: SCMFSA10:70

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

proof end;

registration

let c₁, c₂ be Int-Location ;
cluster JUMP (AddTo a₁,a₂) -> empty ;
coherence

proof end;

end;

theorem Th71: :: SCMFSA10:71

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

proof end;

registration

let c₁, c₂ be Int-Location ;
cluster JUMP (SubFrom a₁,a₂) -> empty ;
coherence

proof end;

end;

theorem Th72: :: SCMFSA10:72

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

proof end;

registration

let c₁, c₂ be Int-Location ;
cluster JUMP (MultBy a₁,a₂) -> empty ;
coherence

proof end;

end;

theorem Th73: :: SCMFSA10:73

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

proof end;

registration

let c₁, c₂ be Int-Location ;
cluster JUMP (Divide a₁,a₂) -> empty ;
coherence

proof end;

end;

theorem Th74: :: SCMFSA10:74

for b₁, b₂ being Instruction-Location of SCM+FSA holds NIC (goto b₁),b₂ = {b₁}

proof end;

theorem Th75: :: SCMFSA10:75

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

proof end;

registration

let c₁ be Instruction-Location of SCM+FSA ;
cluster JUMP (goto a₁) -> non empty trivial ;
coherence

proof end;

end;

theorem Th76: :: SCMFSA10:76

for b₁ being Int-Location
for b₂, b₃ being Instruction-Location of SCM+FSA holds NIC (b₁ =0_goto b₂),b₃ = {b₂,(Next b₃)}

proof end;

theorem Th77: :: SCMFSA10:77

for b₁ being Int-Location
for b₂ being Instruction-Location of SCM+FSA holds JUMP (b₁ =0_goto b₂) = {b₂}

proof end;

registration

let c₁ be Int-Location ;
let c₂ be Instruction-Location of SCM+FSA ;
cluster JUMP (a₁ =0_goto a₂) -> non empty trivial ;
coherence

proof end;

end;

theorem Th78: :: SCMFSA10:78

for b₁ being Int-Location
for b₂, b₃ being Instruction-Location of SCM+FSA holds NIC (b₁ >0_goto b₂),b₃ = {b₂,(Next b₃)}

proof end;

theorem Th79: :: SCMFSA10:79

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

proof end;

registration

let c₁ be Int-Location ;
let c₂ be Instruction-Location of SCM+FSA ;
cluster JUMP (a₁ >0_goto a₂) -> non empty trivial ;
coherence

proof end;

end;

theorem Th80: :: SCMFSA10:80

for b₁, b₂ being Int-Location
for b₃ being FinSeq-Location
for b₄ being Instruction-Location of SCM+FSA holds NIC (b₁ := b₃,b₂),b₄ = {(Next b₄)}

proof end;

registration

let c₁, c₂ be Int-Location ;
let c₃ be FinSeq-Location ;
cluster JUMP (a₁ := a₃,a₂) -> empty ;
coherence

proof end;

end;

theorem Th81: :: SCMFSA10:81

for b₁, b₂ being Int-Location
for b₃ being FinSeq-Location
for b₄ being Instruction-Location of SCM+FSA holds NIC (b₃,b₁ := b₂),b₄ = {(Next b₄)}

proof end;

registration

let c₁, c₂ be Int-Location ;
let c₃ be FinSeq-Location ;
cluster JUMP (a₃,a₂ := a₁) -> empty ;
coherence

proof end;

end;

theorem Th82: :: SCMFSA10:82

for b₁ being Int-Location
for b₂ being FinSeq-Location
for b₃ being Instruction-Location of SCM+FSA holds NIC (b₁ :=len b₂),b₃ = {(Next b₃)}

proof end;

registration

let c₁ be Int-Location ;
let c₂ be FinSeq-Location ;
cluster JUMP (a₁ :=len a₂) -> empty ;
coherence

proof end;

end;

theorem Th83: :: SCMFSA10:83

for b₁ being Int-Location
for b₂ being FinSeq-Location
for b₃ being Instruction-Location of SCM+FSA holds NIC (b₂ :=<0,...,0> b₁),b₃ = {(Next b₃)}

proof end;

registration

let c₁ be Int-Location ;
let c₂ be FinSeq-Location ;
cluster JUMP (a₂ :=<0,...,0> a₁) -> empty ;
coherence

proof end;

end;

theorem Th84: :: SCMFSA10:84

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

proof end;

theorem Th85: :: SCMFSA10:85

for b₁ being Function of NAT ,the Instruction-Locations of SCM+FSA st ( for b₂ being Nat holds b₁ . b₂ = insloc b₂ ) holds
( b₁ is bijective & ( for b₂ being Nat holds
( b₁ . (b₂ + 1) in SUCC (b₁ . b₂) & ( for b₃ being Nat st b₁ . b₃ in SUCC (b₁ . b₂) holds
b₂ <= b₃ ) ) ) )

proof end;

registration

cluster SCM+FSA -> standard ;
coherence

proof end;

end;

theorem Th86: :: SCMFSA10:86

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

proof end;

theorem Th87: :: SCMFSA10:87