:: SCMFSA7B semantic presentation

set c₁ = the Instruction-Locations of SCM+FSA ;

theorem Th1: :: SCMFSA7B:1

for b₁ being FinSequence of the Instructions of SCM+FSA holds dom (Load b₁) = { (insloc b₂) where B is Nat : b₂ < len b₁ }

proof end;

theorem Th2: :: SCMFSA7B:2

for b₁ being FinSequence of the Instructions of SCM+FSA holds rng (Load b₁) = rng b₁

proof end;

registration

let c₂ be FinSequence of the Instructions of SCM+FSA ;
cluster Load a₁ -> programmed initial ;
coherence

proof end;

end;

theorem Th3: :: SCMFSA7B:3

for b₁ being Instruction of SCM+FSA holds Load <*b₁*> = (insloc 0) .--> b₁

proof end;

theorem Th4: :: SCMFSA7B:4

for b₁ being Instruction of SCM+FSA holds dom (Macro b₁) = {(insloc 0),(insloc 1)}

proof end;

theorem Th5: :: SCMFSA7B:5

for b₁ being Instruction of SCM+FSA holds Macro b₁ = Load <*b₁,(halt SCM+FSA )*>

proof end;

theorem Th6: :: SCMFSA7B:6

for b₁ being Instruction of SCM+FSA holds card (Macro b₁) = 2

proof end;

theorem Th7: :: SCMFSA7B:7

for b₁ being Instruction of SCM+FSA holds
( ( b₁ = halt SCM+FSA implies (Directed (Macro b₁)) . (insloc 0) = goto (insloc 2) ) & ( b₁ <> halt SCM+FSA implies (Directed (Macro b₁)) . (insloc 0) = b₁ ) )

proof end;

theorem Th8: :: SCMFSA7B:8

for b₁ being Instruction of SCM+FSA holds (Directed (Macro b₁)) . (insloc 1) = goto (insloc 2)

proof end;

registration

let c₂ be Int-Location ;
let c₃ be Integer;
cluster a₁ := a₂ -> programmed initial ;
coherence

proof end;

end;

Lemma6: for b₁ being State of SCM+FSA st IC b₁ = insloc 0 holds
for b₂ being Int-Location
for b₃ being Integer st b₂ := b₃ c= b₁ holds
b₁ is halting

proof end;

registration

let c₂ be Int-Location ;
let c₃ be Integer;
cluster a₁ := a₂ -> programmed initial parahalting ;
correctness

proof end;

end;

theorem Th9: :: SCMFSA7B:9

for b₁ being State of SCM+FSA
for b₂ being read-write Int-Location
for b₃ being Integer holds
( (IExec (b₂ := b₃),b₁) . b₂ = b₃ & ( for b₄ being read-write Int-Location st b₄ <> b₂ holds
(IExec (b₂ := b₃),b₁) . b₄ = b₁ . b₄ ) & ( for b₄ being FinSeq-Location holds (IExec (b₂ := b₃),b₁) . b₄ = b₁ . b₄ ) )

proof end;

Lemma7: for b₁, b₂, b₃, b₄ being FinSequence holds ((b₁ ^ b₂) ^ b₃) ^ b₄ = b₁ ^ ((b₂ ^ b₃) ^ b₄)

proof end;

Lemma8: for b₁, b₂, b₃ being FinSequence holds
( ((len b₁) + (len b₂)) + (len b₃) = len ((b₁ ^ b₂) ^ b₃) & ((len b₁) + (len b₂)) + (len b₃) = len (b₁ ^ (b₂ ^ b₃)) & (len b₁) + ((len b₂) + (len b₃)) = len (b₁ ^ (b₂ ^ b₃)) & (len b₁) + ((len b₂) + (len b₃)) = len ((b₁ ^ b₂) ^ b₃) )

proof end;

Lemma9: for b₁ being State of SCM+FSA st IC b₁ = insloc 0 & b₁ . (intloc 0) = 1 holds
for b₂ being FinSeq-Location
for b₃ being FinSequence of INT st b₂ := b₃ c= b₁ holds
( b₁ is halting & (Result b₁) . b₂ = b₃ & ( for b₄ being Int-Location st b₄ <> intloc 1 & b₄ <> intloc 2 holds
(Result b₁) . b₄ = b₁ . b₄ ) & ( for b₄ being FinSeq-Location st b₄ <> b₂ holds
(Result b₁) . b₄ = b₁ . b₄ ) )

proof end;

Lemma10: for b₁ being State of SCM+FSA
for b₂ being Nat st IC b₁ = insloc b₂ holds
for b₃ being Int-Location
for b₄ being Integer st ( for b₅ being Nat st b₅ < len (aSeq b₃,b₄) holds
(aSeq b₃,b₄) . (b₅ + 1) = b₁ . (insloc (b₂ + b₅)) ) holds
for b₅ being Nat st b₅ <= len (aSeq b₃,b₄) holds
IC ((Computation b₁) . b₅) = insloc (b₂ + b₅)

proof end;

Lemma11: for b₁ being State of SCM+FSA st IC b₁ = insloc 0 holds
for b₂ being Int-Location
for b₃ being Integer st Load (aSeq b₂,b₃) c= b₁ holds
for b₄ being Nat st b₄ <= len (aSeq b₂,b₃) holds
IC ((Computation b₁) . b₄) = insloc b₄

proof end;

Lemma12: for b₁ being State of SCM+FSA st IC b₁ = insloc 0 holds
for b₂ being FinSeq-Location
for b₃ being FinSequence of INT st b₂ := b₃ c= b₁ holds
b₁ is halting

proof end;

registration

let c₂ be FinSeq-Location ;
let c₃ be FinSequence of INT ;
cluster a₁ := a₂ -> programmed initial ;
coherence

proof end;

end;

registration

let c₂ be FinSeq-Location ;
let c₃ be FinSequence of INT ;
cluster a₁ := a₂ -> programmed initial parahalting ;
correctness

proof end;

end;

theorem Th10: :: SCMFSA7B:10

for b₁ being State of SCM+FSA
for b₂ being FinSeq-Location
for b₃ being FinSequence of INT holds
( (IExec (b₂ := b₃),b₁) . b₂ = b₃ & ( for b₄ being read-write Int-Location st b₄ <> intloc 1 & b₄ <> intloc 2 holds
(IExec (b₂ := b₃),b₁) . b₄ = b₁ . b₄ ) & ( for b₄ being FinSeq-Location st b₄ <> b₂ holds
(IExec (b₂ := b₃),b₁) . b₄ = b₁ . b₄ ) )

proof end;

definition

let c₂ be Instruction of SCM+FSA ;
let c₃ be Int-Location ;
pred c₁ does_not_refer c₂ means :: SCMFSA7B:def 1
for b₁ being Int-Location
for b₂ being Instruction-Location of SCM+FSA
for b₃ being FinSeq-Location holds
( b₁ := a₂ <> a₁ & AddTo b₁,a₂ <> a₁ & SubFrom b₁,a₂ <> a₁ & MultBy b₁,a₂ <> a₁ & Divide b₁,a₂ <> a₁ & Divide a₂,b₁ <> a₁ & a₂ =0_goto b₂ <> a₁ & a₂ >0_goto b₂ <> a₁ & b₁ := b₃,a₂ <> a₁ & b₃,b₁ := a₂ <> a₁ & b₃,a₂ := b₁ <> a₁ & b₃ :=<0,...,0> a₂ <> a₁ );

end;

:: deftheorem Def1 defines does_not_refer SCMFSA7B:def 1 :

definition

let c₂ be programmed FinPartState of SCM+FSA ;
let c₃ be Int-Location ;
pred c₁ does_not_refer c₂ means :: SCMFSA7B:def 2
for b₁ being Instruction of SCM+FSA st b₁ in rng a₁ holds
b₁ does_not_refer a₂;

end;

:: deftheorem Def2 defines does_not_refer SCMFSA7B:def 2 :

definition

let c₂ be Instruction of SCM+FSA ;
let c₃ be Int-Location ;
pred c₁ does_not_destroy c₂ means :Def3: :: SCMFSA7B:def 3
for b₁ being Int-Location
for b₂ being FinSeq-Location holds
( a₂ := b₁ <> a₁ & AddTo a₂,b₁ <> a₁ & SubFrom a₂,b₁ <> a₁ & MultBy a₂,b₁ <> a₁ & Divide a₂,b₁ <> a₁ & Divide b₁,a₂ <> a₁ & a₂ := b₂,b₁ <> a₁ & a₂ :=len b₂ <> a₁ );

end;

:: deftheorem Def3 defines does_not_destroy SCMFSA7B:def 3 :

definition

let c₂ be FinPartState of SCM+FSA ;
let c₃ be Int-Location ;
pred c₁ does_not_destroy c₂ means :Def4: :: SCMFSA7B:def 4
for b₁ being Instruction of SCM+FSA st b₁ in rng a₁ holds
b₁ does_not_destroy a₂;

end;

:: deftheorem Def4 defines does_not_destroy SCMFSA7B:def 4 :

definition

let c₂ be FinPartState of SCM+FSA ;
attr a₁ is good means :Def5: :: SCMFSA7B:def 5
a₁ does_not_destroy intloc 0;

end;

:: deftheorem Def5 defines good SCMFSA7B:def 5 :

definition

let c₂ be FinPartState of SCM+FSA ;
attr a₁ is halt-free means :Def6: :: SCMFSA7B:def 6
not halt SCM+FSA in rng a₁;

end;

:: deftheorem Def6 defines halt-free SCMFSA7B:def 6 :

registration

cluster good halt-free FinPartState of SCM+FSA ;
existence

proof end;

end;

theorem Th11: :: SCMFSA7B:11

for b₁ being Int-Location holds halt SCM+FSA does_not_destroy b₁

proof end;

theorem Th12: :: SCMFSA7B:12

for b₁, b₂, b₃ being Int-Location st b₁ <> b₂ holds
b₂ := b₃ does_not_destroy b₁

proof end;

theorem Th13: :: SCMFSA7B:13

for b₁, b₂, b₃ being Int-Location st b₁ <> b₂ holds
AddTo b₂,b₃ does_not_destroy b₁

proof end;

theorem Th14: :: SCMFSA7B:14

for b₁, b₂, b₃ being Int-Location st b₁ <> b₂ holds
SubFrom b₂,b₃ does_not_destroy b₁

proof end;

theorem Th15: :: SCMFSA7B:15

for b₁, b₂, b₃ being Int-Location st b₁ <> b₂ holds
MultBy b₂,b₃ does_not_destroy b₁

proof end;

theorem Th16: :: SCMFSA7B:16

for b₁, b₂, b₃ being Int-Location st b₁ <> b₂ & b₁ <> b₃ holds
Divide b₂,b₃ does_not_destroy b₁

proof end;

theorem Th17: :: SCMFSA7B:17

for b₁ being Int-Location
for b₂ being Instruction-Location of SCM+FSA holds goto b₂ does_not_destroy b₁

proof end;

theorem Th18: :: SCMFSA7B:18

for b₁, b₂ being Int-Location
for b₃ being Instruction-Location of SCM+FSA holds b₂ =0_goto b₃ does_not_destroy b₁

proof end;

theorem Th19: :: SCMFSA7B:19

for b₁, b₂ being Int-Location
for b₃ being Instruction-Location of SCM+FSA holds b₂ >0_goto b₃ does_not_destroy b₁

proof end;

theorem Th20: :: SCMFSA7B:20

for b₁, b₂, b₃ being Int-Location
for b₄ being FinSeq-Location st b₁ <> b₂ holds
b₂ := b₄,b₃ does_not_destroy b₁

proof end;

theorem Th21: :: SCMFSA7B:21

for b₁, b₂, b₃ being Int-Location
for b₄ being FinSeq-Location holds b₄,b₃ := b₂ does_not_destroy b₁

proof end;

theorem Th22: :: SCMFSA7B:22

for b₁, b₂ being Int-Location
for b₃ being FinSeq-Location st b₁ <> b₂ holds
b₂ :=len b₃ does_not_destroy b₁

proof end;

theorem Th23: :: SCMFSA7B:23

for b₁, b₂ being Int-Location
for b₃ being FinSeq-Location holds b₃ :=<0,...,0> b₂ does_not_destroy b₁

proof end;

definition

let c₂ be FinPartState of SCM+FSA ;
let c₃ be State of SCM+FSA ;
pred c₁ is_closed_on c₂ means :Def7: :: SCMFSA7B:def 7
for b₁ being Nat holds IC ((Computation (a₂ +* (a₁ +* (Start-At (insloc 0))))) . b₁) in dom a₁;
pred c₁ is_halting_on c₂ means :Def8: :: SCMFSA7B:def 8
a₂ +* (a₁ +* (Start-At (insloc 0))) is halting;

end;

:: deftheorem Def7 defines is_closed_on SCMFSA7B:def 7 :

:: deftheorem Def8 defines is_halting_on SCMFSA7B:def 8 :

theorem Th24: :: SCMFSA7B:24

for b₁ being Macro-Instruction holds
( b₁ is paraclosed iff for b₂ being State of SCM+FSA holds b₁ is_closed_on b₂ )

proof end;

theorem Th25: :: SCMFSA7B:25

for b₁ being Macro-Instruction holds
( b₁ is parahalting iff for b₂ being State of SCM+FSA holds b₁ is_halting_on b₂ )

proof end;

theorem Th26: :: SCMFSA7B:26

for b₁ being Instruction of SCM+FSA
for b₂ being Int-Location
for b₃ being State of SCM+FSA st b₁ does_not_destroy b₂ holds
(Exec b₁,b₃) . b₂ = b₃ . b₂

proof end;

theorem Th27: :: SCMFSA7B:27

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction
for b₃ being Int-Location st b₂ does_not_destroy b₃ & b₂ is_closed_on b₁ holds
for b₄ being Nat holds ((Computation (b₁ +* (b₂ +* (Start-At (insloc 0))))) . b₄) . b₃ = b₁ . b₃

proof end;

theorem Th28: :: SCMFSA7B:28

SCM+FSA-Stop does_not_destroy intloc 0

proof end;

Lemma27: SCM+FSA-Stop is parahalting

proof end;

registration

cluster parahalting good FinPartState of SCM+FSA ;
existence

proof end;

end;

registration

cluster SCM+FSA-Stop -> parahalting good ;
coherence by Def5, Lemma27, Th28;

end;

registration

cluster paraclosed good -> keeping_0 FinPartState of SCM+FSA ;
correctness

proof end;

end;

theorem Th29: :: SCMFSA7B:29

for b₁ being Int-Location
for b₂ being Integer holds rng (aSeq b₁,b₂) c= {(b₁ := (intloc 0)),(AddTo b₁,(intloc 0)),(SubFrom b₁,(intloc 0))}

proof end;

theorem Th30: :: SCMFSA7B:30

for b₁ being Int-Location
for b₂ being Integer holds rng (b₁ := b₂) c= {(halt SCM+FSA ),(b₁ := (intloc 0)),(AddTo b₁,(intloc 0)),(SubFrom b₁,(intloc 0))}

proof end;

registration

let c₂ be read-write Int-Location ;
let c₃ be Integer;
cluster a₁ := a₂ -> programmed initial parahalting keeping_0 good ;
correctness

proof end;

end;

registration

let c₂ be read-write Int-Location ;
let c₃ be Integer;
cluster a₁ := a₂ -> programmed initial parahalting keeping_0 good ;
correctness ;

end;