:: SCMFSA6C semantic presentation

set c₁ = Start-At (insloc 0);

theorem Th1: :: SCMFSA6C:1

for b₁ being Int-Location
for b₂ being State of SCM+FSA
for b₃ being parahalting keeping_0 Macro-Instruction
for b₄ being parahalting Macro-Instruction holds (IExec (b₃ ';' b₄),b₂) . b₁ = (IExec b₄,(IExec b₃,b₂)) . b₁

proof end;

theorem Th2: :: SCMFSA6C:2

for b₁ being FinSeq-Location
for b₂ being State of SCM+FSA
for b₃ being parahalting keeping_0 Macro-Instruction
for b₄ being parahalting Macro-Instruction holds (IExec (b₃ ';' b₄),b₂) . b₁ = (IExec b₄,(IExec b₃,b₂)) . b₁

proof end;

definition

let c₂ be Instruction of SCM+FSA ;
attr a₁ is parahalting means :Def1: :: SCMFSA6C:def 1
Macro a₁ is parahalting;
attr a₁ is keeping_0 means :Def2: :: SCMFSA6C:def 2
Macro a₁ is keeping_0;

end;

:: deftheorem Def1 defines parahalting SCMFSA6C:def 1 :

:: deftheorem Def2 defines keeping_0 SCMFSA6C:def 2 :

Lemma3: Macro (halt SCM+FSA ) is parahalting

proof end;

Lemma4: ( Macro (halt SCM+FSA ) is keeping_0 & Macro (halt SCM+FSA ) is parahalting )

proof end;

registration

cluster halt SCM+FSA -> parahalting keeping_0 ;
coherence

proof end;

end;

registration

cluster parahalting keeping_0 Element of the Instructions of SCM+FSA ;
existence

proof end;

end;

registration

let c₂ be parahalting Instruction of SCM+FSA ;
cluster Macro a₁ -> parahalting ;
coherence by Def1;

end;

registration

let c₂ be keeping_0 Instruction of SCM+FSA ;
cluster Macro a₁ -> keeping_0 ;
coherence by Def2;

end;

registration

let c₂, c₃ be Int-Location ;
cluster a₁ := a₂ -> parahalting ;
coherence

proof end;

cluster AddTo a₁,a₂ -> parahalting ;
coherence

proof end;

cluster SubFrom a₁,a₂ -> parahalting ;
coherence

proof end;

cluster MultBy a₁,a₂ -> parahalting ;
coherence

proof end;

cluster Divide a₁,a₂ -> parahalting ;
coherence

proof end;

let c₄ be FinSeq-Location ;
cluster a₂ := a₃,a₁ -> parahalting ;
coherence

proof end;

cluster a₃,a₁ := a₂ -> parahalting keeping_0 ;
coherence

proof end;

end;

registration

let c₂ be Int-Location ;
let c₃ be FinSeq-Location ;
cluster a₁ :=len a₂ -> parahalting ;
coherence

proof end;

cluster a₂ :=<0,...,0> a₁ -> parahalting keeping_0 ;
coherence

proof end;

end;

registration

let c₂ be read-write Int-Location ;
let c₃ be Int-Location ;
cluster a₁ := a₂ -> parahalting keeping_0 ;
coherence

proof end;

cluster AddTo a₁,a₂ -> parahalting keeping_0 ;
coherence

proof end;

cluster SubFrom a₁,a₂ -> parahalting keeping_0 ;
coherence

proof end;

cluster MultBy a₁,a₂ -> parahalting keeping_0 ;
coherence

proof end;

end;

registration

let c₂, c₃ be read-write Int-Location ;
cluster Divide a₁,a₂ -> parahalting keeping_0 ;
coherence

proof end;

end;

registration

let c₂ be Int-Location ;
let c₃ be FinSeq-Location ;
let c₄ be read-write Int-Location ;
cluster a₃ := a₂,a₁ -> parahalting keeping_0 ;
coherence

proof end;

end;

registration

let c₂ be FinSeq-Location ;
let c₃ be read-write Int-Location ;
cluster a₂ :=len a₁ -> parahalting keeping_0 ;
coherence

proof end;

end;

registration

let c₂ be parahalting Instruction of SCM+FSA ;
let c₃ be parahalting Macro-Instruction;
cluster a₁ ';' a₂ -> parahalting ;
coherence

proof end;

end;

registration

let c₂ be parahalting Macro-Instruction;
let c₃ be parahalting Instruction of SCM+FSA ;
cluster a₁ ';' a₂ -> parahalting ;
coherence

proof end;

end;

registration

let c₂, c₃ be parahalting Instruction of SCM+FSA ;
cluster a₁ ';' a₂ -> parahalting ;
coherence

proof end;

end;

registration

let c₂ be keeping_0 Instruction of SCM+FSA ;
let c₃ be keeping_0 Macro-Instruction;
cluster a₁ ';' a₂ -> keeping_0 ;
coherence

proof end;

end;

registration

let c₂ be keeping_0 Macro-Instruction;
let c₃ be keeping_0 Instruction of SCM+FSA ;
cluster a₁ ';' a₂ -> keeping_0 ;
coherence

proof end;

end;

registration

let c₂, c₃ be keeping_0 Instruction of SCM+FSA ;
cluster a₁ ';' a₂ -> keeping_0 ;
coherence

proof end;

end;

definition

let c₂ be State of SCM+FSA ;
func Initialize c₁ -> State of SCM+FSA equals :: SCMFSA6C:def 3
(a₁ +* ((intloc 0) .--> 1)) +* (Start-At (insloc 0));
coherence

proof end;

end;

:: deftheorem Def3 defines Initialize SCMFSA6C:def 3 :

theorem Th3: :: SCMFSA6C:3

for b₁ being State of SCM+FSA holds
( IC (Initialize b₁) = insloc 0 & (Initialize b₁) . (intloc 0) = 1 & ( for b₂ being read-write Int-Location holds (Initialize b₁) . b₂ = b₁ . b₂ ) & ( for b₂ being FinSeq-Location holds (Initialize b₁) . b₂ = b₁ . b₂ ) & ( for b₂ being Instruction-Location of SCM+FSA holds (Initialize b₁) . b₂ = b₁ . b₂ ) )

proof end;

theorem Th4: :: SCMFSA6C:4

for b₁, b₂ being State of SCM+FSA holds
( b₁,b₂ equal_outside the Instruction-Locations of SCM+FSA iff b₁ | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) = b₂ | ((Int-Locations \/ FinSeq-Locations ) \/ {(IC SCM+FSA )}) )

proof end;

theorem Th5: :: SCMFSA6C:5

for b₁ being Instruction of SCM+FSA
for b₂, b₃ being State of SCM+FSA st b₂ | (Int-Locations \/ FinSeq-Locations ) = b₃ | (Int-Locations \/ FinSeq-Locations ) holds
(Exec b₁,b₂) | (Int-Locations \/ FinSeq-Locations ) = (Exec b₁,b₃) | (Int-Locations \/ FinSeq-Locations )

proof end;

E8: now

let c₂ be parahalting keeping_0 Macro-Instruction;
let c₃ be State of SCM+FSA ;
set c₄ = IExec c₂,c₃;
set c₅ = Int-Locations \/ FinSeq-Locations ;

now

E9: ( dom (Initialize (IExec c₂,c₃)) = the carrier of SCM+FSA & dom (IExec c₂,c₃) = the carrier of SCM+FSA ) by AMI_3:36;
hence E10: dom ((Initialize (IExec c₂,c₃)) | (Int-Locations \/ FinSeq-Locations )) = (dom (IExec c₂,c₃)) /\ (Int-Locations \/ FinSeq-Locations ) by RELAT_1:90;
let c₆ be set ;
assume E11: c₆ in dom ((Initialize (IExec c₂,c₃)) | (Int-Locations \/ FinSeq-Locations )) ;
dom (Initialize (IExec c₂,c₃)) = (Int-Locations \/ FinSeq-Locations ) \/ ({(IC SCM+FSA )} \/ the Instruction-Locations of SCM+FSA ) by E9, SCMFSA_2:8, XBOOLE_1:4;
then E12: dom ((Initialize (IExec c₂,c₃)) | (Int-Locations \/ FinSeq-Locations )) = Int-Locations \/ FinSeq-Locations by E9, E10, XBOOLE_1:21;

per cases by E11, E12, XBOOLE_0:def 2;

suppose c₆ in Int-Locations ;

then reconsider c₇ = c₆ as Int-Location by SCMFSA_2:11;

hereby

per cases ;

suppose E13: not c₇ is read-only ;

thus ((Initialize (IExec c₂,c₃)) | (Int-Locations \/ FinSeq-Locations )) . c₆ = (Initialize (IExec c₂,c₃)) . c₆ by E11, E12, FUNCT_1:72
.= (IExec c₂,c₃) . c₆ by E13, Th3 ;

end;

suppose c₇ is read-only ;

then E13: c₇ = intloc 0 by SF_MASTR:def 5;
thus ((Initialize (IExec c₂,c₃)) | (Int-Locations \/ FinSeq-Locations )) . c₆ = (Initialize (IExec c₂,c₃)) . c₇ by E11, E12, FUNCT_1:72
.= 1 by E13, Th3
.= (IExec c₂,c₃) . c₆ by E13, SCMFSA6B:35 ;

end;

suppose c₆ in FinSeq-Locations ;

then reconsider c₇ = c₆ as FinSeq-Location by SCMFSA_2:12;
thus ((Initialize (IExec c₂,c₃)) | (Int-Locations \/ FinSeq-Locations )) . c₆ = (Initialize (IExec c₂,c₃)) . c₇ by E11, E12, FUNCT_1:72
.= (IExec c₂,c₃) . c₆ by Th3 ;

end;

hence (Initialize (IExec c₂,c₃)) | (Int-Locations \/ FinSeq-Locations ) = (IExec c₂,c₃) | (Int-Locations \/ FinSeq-Locations ) by FUNCT_1:68;

end;

theorem Th6: :: SCMFSA6C:6

for b₁ being State of SCM+FSA
for b₂ being parahalting Instruction of SCM+FSA holds Exec b₂,(Initialize b₁) = IExec (Macro b₂),b₁

proof end;

theorem Th7: :: SCMFSA6C:7

for b₁ being Int-Location
for b₂ being State of SCM+FSA
for b₃ being parahalting keeping_0 Macro-Instruction
for b₄ being parahalting Instruction of SCM+FSA holds (IExec (b₃ ';' b₄),b₂) . b₁ = (Exec b₄,(IExec b₃,b₂)) . b₁

proof end;

theorem Th8: :: SCMFSA6C:8

for b₁ being FinSeq-Location
for b₂ being State of SCM+FSA
for b₃ being parahalting keeping_0 Macro-Instruction
for b₄ being parahalting Instruction of SCM+FSA holds (IExec (b₃ ';' b₄),b₂) . b₁ = (Exec b₄,(IExec b₃,b₂)) . b₁

proof end;

theorem Th9: :: SCMFSA6C:9

for b₁ being Int-Location
for b₂ being State of SCM+FSA
for b₃ being parahalting keeping_0 Instruction of SCM+FSA
for b₄ being parahalting Instruction of SCM+FSA holds (IExec (b₃ ';' b₄),b₂) . b₁ = (Exec b₄,(Exec b₃,(Initialize b₂))) . b₁

proof end;

theorem Th10: :: SCMFSA6C:10

for b₁ being FinSeq-Location
for b₂ being State of SCM+FSA
for b₃ being parahalting keeping_0 Instruction of SCM+FSA
for b₄ being parahalting Instruction of SCM+FSA holds (IExec (b₃ ';' b₄),b₂) . b₁ = (Exec b₄,(Exec b₃,(Initialize b₂))) . b₁

proof end;

definition

let c₂, c₃ be Int-Location ;
func swap c₁,c₂ -> Macro-Instruction equals :: SCMFSA6C:def 4
(((FirstNotUsed (Macro (a₁ := a₂))) := a₁) ';' (a₁ := a₂)) ';' (a₂ := (FirstNotUsed (Macro (a₁ := a₂))));
correctness ;

end;

:: deftheorem Def4 defines swap SCMFSA6C:def 4 :

registration

let c₂, c₃ be Int-Location ;
cluster swap a₁,a₂ -> parahalting ;
coherence ;

end;

registration

let c₂, c₃ be read-write Int-Location ;
cluster swap a₁,a₂ -> parahalting keeping_0 ;
coherence ;

end;

theorem Th11: :: SCMFSA6C:11

for b₁ being State of SCM+FSA
for b₂, b₃ being read-write Int-Location holds
( (IExec (swap b₂,b₃),b₁) . b₂ = b₁ . b₃ & (IExec (swap b₂,b₃),b₁) . b₃ = b₁ . b₂ )

proof end;

theorem Th12: :: SCMFSA6C:12

for b₁, b₂ being Int-Location holds UsedInt*Loc (swap b₁,b₂) = {}

proof end;