:: SCMFSA8B semantic presentation

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

set c₂ = Int-Locations \/ FinSeq-Locations ;

Lemma1: for b₁ being Instruction-Location of SCM+FSA holds goto b₁ <> halt SCM+FSA
by SCMFSA_2:47, SCMFSA_2:124;

Lemma2: for b₁ being Int-Location
for b₂ being Instruction-Location of SCM+FSA holds b₁ =0_goto b₂ <> halt SCM+FSA
by SCMFSA_2:48, SCMFSA_2:124;

Lemma3: for b₁ being Int-Location
for b₂ being Instruction-Location of SCM+FSA holds b₁ >0_goto b₂ <> halt SCM+FSA
by SCMFSA_2:49, SCMFSA_2:124;

Lemma4: for b₁, b₂ being Macro-Instruction holds ProgramPart (Relocated b₂,(card b₁)) c= b₁ ';' b₂

proof end;

theorem Th1: :: SCMFSA8B:1

for b₁ being State of SCM+FSA holds IC SCM+FSA in dom b₁

proof end;

theorem Th2: :: SCMFSA8B:2

for b₁ being State of SCM+FSA
for b₂ being Instruction-Location of SCM+FSA holds b₂ in dom b₁

proof end;

theorem Th3: :: SCMFSA8B:3

for b₁ being Macro-Instruction
for b₂ being State of SCM+FSA st b₁ is_closed_on b₂ holds
insloc 0 in dom b₁

proof end;

theorem Th4: :: SCMFSA8B:4

for b₁ being State of SCM+FSA
for b₂, b₃ being Instruction-Location of SCM+FSA holds (b₁ +* (Start-At b₂)) +* (Start-At b₃) = b₁ +* (Start-At b₃)

proof end;

theorem Th5: :: SCMFSA8B:5

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction holds (Initialize b₁) | (Int-Locations \/ FinSeq-Locations ) = (b₁ +* (Initialized b₂)) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th6: :: SCMFSA8B:6

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

proof end;

theorem Th7: :: SCMFSA8B:7

for b₁, b₂ being State of SCM+FSA
for b₃, b₄ being Macro-Instruction st b₁ | (Int-Locations \/ FinSeq-Locations ) = b₂ | (Int-Locations \/ FinSeq-Locations ) holds
b₁ +* (b₃ +* (Start-At (insloc 0))),b₂ +* (b₄ +* (Start-At (insloc 0))) equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem Th8: :: SCMFSA8B:8

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

proof end;

theorem Th9: :: SCMFSA8B:9

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction holds
( b₂ is_closed_on Initialize b₁ iff b₂ is_closed_on b₁ +* (Initialized b₃) )

proof end;

theorem Th10: :: SCMFSA8B:10

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being Instruction-Location of SCM+FSA holds
( b₂ is_closed_on b₁ iff b₂ is_closed_on b₁ +* (b₂ +* (Start-At b₄)) )

proof end;

theorem Th11: :: SCMFSA8B:11

for b₁, b₂ being State of SCM+FSA
for b₃ being Macro-Instruction st b₃ +* (Start-At (insloc 0)) c= b₁ & b₃ is_closed_on b₁ holds
for b₄ being Nat st ProgramPart (Relocated b₃,b₄) c= b₂ & IC b₂ = insloc b₄ & b₁ | (Int-Locations \/ FinSeq-Locations ) = b₂ | (Int-Locations \/ FinSeq-Locations ) holds
for b₅ being Nat holds
( (IC ((Computation b₁) . b₅)) + b₄ = IC ((Computation b₂) . b₅) & IncAddr (CurInstr ((Computation b₁) . b₅)),b₄ = CurInstr ((Computation b₂) . b₅) & ((Computation b₁) . b₅) | (Int-Locations \/ FinSeq-Locations ) = ((Computation b₂) . b₅) | (Int-Locations \/ FinSeq-Locations ) )

proof end;

theorem Th12: :: SCMFSA8B:12

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

proof end;

theorem Th13: :: SCMFSA8B:13

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

proof end;

definition

let c₃ be Int-Location ;
let c₄, c₅ be Macro-Instruction;
func if=0 c₁,c₂,c₃ -> Macro-Instruction equals :: SCMFSA8B:def 1
((((a₁ =0_goto (insloc ((card a₃) + 3))) ';' a₃) ';' (Goto (insloc ((card a₂) + 1)))) ';' a₂) ';' SCM+FSA-Stop ;
coherence ;
func if>0 c₁,c₂,c₃ -> Macro-Instruction equals :: SCMFSA8B:def 2
((((a₁ >0_goto (insloc ((card a₃) + 3))) ';' a₃) ';' (Goto (insloc ((card a₂) + 1)))) ';' a₂) ';' SCM+FSA-Stop ;
coherence ;

end;

:: deftheorem Def1 defines if=0 SCMFSA8B:def 1 :

:: deftheorem Def2 defines if>0 SCMFSA8B:def 2 :

definition

let c₃ be Int-Location ;
let c₄, c₅ be Macro-Instruction;
func if<0 c₁,c₂,c₃ -> Macro-Instruction equals :: SCMFSA8B:def 3
if=0 a₁,a₃,(if>0 a₁,a₃,a₂);
coherence ;

end;

:: deftheorem Def3 defines if<0 SCMFSA8B:def 3 :

Lemma18: for b₁ being Int-Location
for b₂, b₃ being Macro-Instruction holds
( insloc 0 in dom (if=0 b₁,b₂,b₃) & insloc 1 in dom (if=0 b₁,b₂,b₃) & insloc 0 in dom (if>0 b₁,b₂,b₃) & insloc 1 in dom (if>0 b₁,b₂,b₃) )

proof end;

Lemma19: for b₁ being Int-Location
for b₂, b₃ being Macro-Instruction holds
( (if=0 b₁,b₂,b₃) . (insloc 0) = b₁ =0_goto (insloc ((card b₃) + 3)) & (if=0 b₁,b₂,b₃) . (insloc 1) = goto (insloc 2) & (if>0 b₁,b₂,b₃) . (insloc 0) = b₁ >0_goto (insloc ((card b₃) + 3)) & (if>0 b₁,b₂,b₃) . (insloc 1) = goto (insloc 2) )

proof end;

theorem Th14: :: SCMFSA8B:14

for b₁, b₂ being Macro-Instruction
for b₃ being Int-Location holds card (if=0 b₃,b₁,b₂) = ((card b₁) + (card b₂)) + 4

proof end;

theorem Th15: :: SCMFSA8B:15

for b₁, b₂ being Macro-Instruction
for b₃ being Int-Location holds card (if>0 b₃,b₁,b₂) = ((card b₁) + (card b₂)) + 4

proof end;

theorem Th16: :: SCMFSA8B:16

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ = 0 & b₂ is_closed_on b₁ & b₂ is_halting_on b₁ holds
( if=0 b₄,b₂,b₃ is_closed_on b₁ & if=0 b₄,b₂,b₃ is_halting_on b₁ )

proof end;

theorem Th17: :: SCMFSA8B:17

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ = 0 & b₂ is_closed_on Initialize b₁ & b₂ is_halting_on Initialize b₁ holds
IExec (if=0 b₄,b₂,b₃),b₁ = (IExec b₂,b₁) +* (Start-At (insloc (((card b₂) + (card b₃)) + 3)))

proof end;

theorem Th18: :: SCMFSA8B:18

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ <> 0 & b₃ is_closed_on b₁ & b₃ is_halting_on b₁ holds
( if=0 b₄,b₂,b₃ is_closed_on b₁ & if=0 b₄,b₂,b₃ is_halting_on b₁ )

proof end;

theorem Th19: :: SCMFSA8B:19

for b₁, b₂ being Macro-Instruction
for b₃ being read-write Int-Location
for b₄ being State of SCM+FSA st b₄ . b₃ <> 0 & b₂ is_closed_on Initialize b₄ & b₂ is_halting_on Initialize b₄ holds
IExec (if=0 b₃,b₁,b₂),b₄ = (IExec b₂,b₄) +* (Start-At (insloc (((card b₁) + (card b₂)) + 3)))

proof end;

theorem Th20: :: SCMFSA8B:20

for b₁ being State of SCM+FSA
for b₂, b₃ being parahalting Macro-Instruction
for b₄ being read-write Int-Location holds
( if=0 b₄,b₂,b₃ is parahalting & ( b₁ . b₄ = 0 implies IExec (if=0 b₄,b₂,b₃),b₁ = (IExec b₂,b₁) +* (Start-At (insloc (((card b₂) + (card b₃)) + 3))) ) & ( b₁ . b₄ <> 0 implies IExec (if=0 b₄,b₂,b₃),b₁ = (IExec b₃,b₁) +* (Start-At (insloc (((card b₂) + (card b₃)) + 3))) ) )

proof end;

theorem Th21: :: SCMFSA8B:21

for b₁ being State of SCM+FSA
for b₂, b₃ being parahalting Macro-Instruction
for b₄ being read-write Int-Location holds
( IC (IExec (if=0 b₄,b₂,b₃),b₁) = insloc (((card b₂) + (card b₃)) + 3) & ( b₁ . b₄ = 0 implies ( ( for b₅ being Int-Location holds (IExec (if=0 b₄,b₂,b₃),b₁) . b₅ = (IExec b₂,b₁) . b₅ ) & ( for b₅ being FinSeq-Location holds (IExec (if=0 b₄,b₂,b₃),b₁) . b₅ = (IExec b₂,b₁) . b₅ ) ) ) & ( b₁ . b₄ <> 0 implies ( ( for b₅ being Int-Location holds (IExec (if=0 b₄,b₂,b₃),b₁) . b₅ = (IExec b₃,b₁) . b₅ ) & ( for b₅ being FinSeq-Location holds (IExec (if=0 b₄,b₂,b₃),b₁) . b₅ = (IExec b₃,b₁) . b₅ ) ) ) )

proof end;

theorem Th22: :: SCMFSA8B:22

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ > 0 & b₂ is_closed_on b₁ & b₂ is_halting_on b₁ holds
( if>0 b₄,b₂,b₃ is_closed_on b₁ & if>0 b₄,b₂,b₃ is_halting_on b₁ )

proof end;

theorem Th23: :: SCMFSA8B:23

for b₁, b₂ being Macro-Instruction
for b₃ being read-write Int-Location
for b₄ being State of SCM+FSA st b₄ . b₃ > 0 & b₁ is_closed_on Initialize b₄ & b₁ is_halting_on Initialize b₄ holds
IExec (if>0 b₃,b₁,b₂),b₄ = (IExec b₁,b₄) +* (Start-At (insloc (((card b₁) + (card b₂)) + 3)))

proof end;

theorem Th24: :: SCMFSA8B:24

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ <= 0 & b₃ is_closed_on b₁ & b₃ is_halting_on b₁ holds
( if>0 b₄,b₂,b₃ is_closed_on b₁ & if>0 b₄,b₂,b₃ is_halting_on b₁ )

proof end;

theorem Th25: :: SCMFSA8B:25

for b₁, b₂ being Macro-Instruction
for b₃ being read-write Int-Location
for b₄ being State of SCM+FSA st b₄ . b₃ <= 0 & b₂ is_closed_on Initialize b₄ & b₂ is_halting_on Initialize b₄ holds
IExec (if>0 b₃,b₁,b₂),b₄ = (IExec b₂,b₄) +* (Start-At (insloc (((card b₁) + (card b₂)) + 3)))

proof end;

theorem Th26: :: SCMFSA8B:26

for b₁ being State of SCM+FSA
for b₂, b₃ being parahalting Macro-Instruction
for b₄ being read-write Int-Location holds
( if>0 b₄,b₂,b₃ is parahalting & ( b₁ . b₄ > 0 implies IExec (if>0 b₄,b₂,b₃),b₁ = (IExec b₂,b₁) +* (Start-At (insloc (((card b₂) + (card b₃)) + 3))) ) & ( b₁ . b₄ <= 0 implies IExec (if>0 b₄,b₂,b₃),b₁ = (IExec b₃,b₁) +* (Start-At (insloc (((card b₂) + (card b₃)) + 3))) ) )

proof end;

theorem Th27: :: SCMFSA8B:27

for b₁ being State of SCM+FSA
for b₂, b₃ being parahalting Macro-Instruction
for b₄ being read-write Int-Location holds
( IC (IExec (if>0 b₄,b₂,b₃),b₁) = insloc (((card b₂) + (card b₃)) + 3) & ( b₁ . b₄ > 0 implies ( ( for b₅ being Int-Location holds (IExec (if>0 b₄,b₂,b₃),b₁) . b₅ = (IExec b₂,b₁) . b₅ ) & ( for b₅ being FinSeq-Location holds (IExec (if>0 b₄,b₂,b₃),b₁) . b₅ = (IExec b₂,b₁) . b₅ ) ) ) & ( b₁ . b₄ <= 0 implies ( ( for b₅ being Int-Location holds (IExec (if>0 b₄,b₂,b₃),b₁) . b₅ = (IExec b₃,b₁) . b₅ ) & ( for b₅ being FinSeq-Location holds (IExec (if>0 b₄,b₂,b₃),b₁) . b₅ = (IExec b₃,b₁) . b₅ ) ) ) )

proof end;

theorem Th28: :: SCMFSA8B:28

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ < 0 & b₂ is_closed_on b₁ & b₂ is_halting_on b₁ holds
( if<0 b₄,b₂,b₃ is_closed_on b₁ & if<0 b₄,b₂,b₃ is_halting_on b₁ )

proof end;

theorem Th29: :: SCMFSA8B:29

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ < 0 & b₂ is_closed_on Initialize b₁ & b₂ is_halting_on Initialize b₁ holds
IExec (if<0 b₄,b₂,b₃),b₁ = (IExec b₂,b₁) +* (Start-At (insloc ((((card b₂) + (card b₃)) + (card b₃)) + 7)))

proof end;

theorem Th30: :: SCMFSA8B:30

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ = 0 & b₃ is_closed_on b₁ & b₃ is_halting_on b₁ holds
( if<0 b₄,b₂,b₃ is_closed_on b₁ & if<0 b₄,b₂,b₃ is_halting_on b₁ ) by Th16;

theorem Th31: :: SCMFSA8B:31

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ = 0 & b₃ is_closed_on Initialize b₁ & b₃ is_halting_on Initialize b₁ holds
IExec (if<0 b₄,b₂,b₃),b₁ = (IExec b₃,b₁) +* (Start-At (insloc ((((card b₂) + (card b₃)) + (card b₃)) + 7)))

proof end;

theorem Th32: :: SCMFSA8B:32

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ > 0 & b₃ is_closed_on b₁ & b₃ is_halting_on b₁ holds
( if<0 b₄,b₂,b₃ is_closed_on b₁ & if<0 b₄,b₂,b₃ is_halting_on b₁ )

proof end;

theorem Th33: :: SCMFSA8B:33

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being read-write Int-Location st b₁ . b₄ > 0 & b₃ is_closed_on Initialize b₁ & b₃ is_halting_on Initialize b₁ holds
IExec (if<0 b₄,b₂,b₃),b₁ = (IExec b₃,b₁) +* (Start-At (insloc ((((card b₂) + (card b₃)) + (card b₃)) + 7)))

proof end;

theorem Th34: :: SCMFSA8B:34

for b₁ being State of SCM+FSA
for b₂, b₃ being parahalting Macro-Instruction
for b₄ being read-write Int-Location holds
( if<0 b₄,b₂,b₃ is parahalting & ( b₁ . b₄ < 0 implies IExec (if<0 b₄,b₂,b₃),b₁ = (IExec b₂,b₁) +* (Start-At (insloc ((((card b₂) + (card b₃)) + (card b₃)) + 7))) ) & ( b₁ . b₄ >= 0 implies IExec (if<0 b₄,b₂,b₃),b₁ = (IExec b₃,b₁) +* (Start-At (insloc ((((card b₂) + (card b₃)) + (card b₃)) + 7))) ) )

proof end;

registration

let c₃, c₄ be parahalting Macro-Instruction;
let c₅ be read-write Int-Location ;
cluster if=0 a₃,a₁,a₂ -> parahalting ;
correctness by Th20;
cluster if>0 a₃,a₁,a₂ -> parahalting ;
correctness by Th26;

end;

definition

let c₃, c₄ be Int-Location ;
let c₅, c₆ be Macro-Instruction;
func if=0 c₁,c₂,c₃,c₄ -> Macro-Instruction equals :: SCMFSA8B:def 4
(SubFrom a₁,a₂) ';' (if=0 a₁,a₃,a₄);
coherence ;
func if>0 c₁,c₂,c₃,c₄ -> Macro-Instruction equals :: SCMFSA8B:def 5
(SubFrom a₁,a₂) ';' (if>0 a₁,a₃,a₄);
coherence ;

end;

:: deftheorem Def4 defines if=0 SCMFSA8B:def 4 :

:: deftheorem Def5 defines if>0 SCMFSA8B:def 5 :

notation

let c₃, c₄ be Int-Location ;
let c₅, c₆ be Macro-Instruction;
synonym if<0 c₂,c₁,c₃,c₄ for if>0 c₁,c₂,c₃,c₄;

end;

registration

let c₃, c₄ be parahalting Macro-Instruction;
let c₅, c₆ be read-write Int-Location ;
cluster if=0 a₃,a₄,a₁,a₂ -> parahalting ;
correctness ;
cluster if>0 a₃,a₄,a₁,a₂ -> parahalting ;
correctness ;

end;

theorem Th35: :: SCMFSA8B:35

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction holds (Result (b₁ +* (Initialized b₂))) | (Int-Locations \/ FinSeq-Locations ) = (IExec b₂,b₁) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th36: :: SCMFSA8B:36

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction
for b₃ being Int-Location holds Result (b₁ +* (Initialized b₂)), IExec b₂,b₁ equal_outside the Instruction-Locations of SCM+FSA

proof end;

theorem Th37: :: SCMFSA8B:37

for b₁, b₂ being State of SCM+FSA
for b₃ being Instruction of SCM+FSA
for b₄ being Int-Location st ( for b₅ being Int-Location st b₄ <> b₅ holds
b₁ . b₅ = b₂ . b₅ ) & ( for b₅ being FinSeq-Location holds b₁ . b₅ = b₂ . b₅ ) & b₃ does_not_refer b₄ & IC b₁ = IC b₂ holds
( ( for b₅ being Int-Location st b₄ <> b₅ holds
(Exec b₃,b₁) . b₅ = (Exec b₃,b₂) . b₅ ) & ( for b₅ being FinSeq-Location holds (Exec b₃,b₁) . b₅ = (Exec b₃,b₂) . b₅ ) & IC (Exec b₃,b₁) = IC (Exec b₃,b₂) )

proof end;

theorem Th38: :: SCMFSA8B:38

for b₁, b₂ being State of SCM+FSA
for b₃ being Macro-Instruction
for b₄ being Int-Location st b₃ does_not_refer b₄ & ( for b₅ being Int-Location st b₄ <> b₅ holds
b₁ . b₅ = b₂ . b₅ ) & ( for b₅ being FinSeq-Location holds b₁ . b₅ = b₂ . b₅ ) & b₃ is_closed_on b₁ & b₃ is_halting_on b₁ holds
for b₅ being Nat holds
( ( for b₆ being Int-Location st b₄ <> b₆ holds
((Computation (b₁ +* (b₃ +* (Start-At (insloc 0))))) . b₅) . b₆ = ((Computation (b₂ +* (b₃ +* (Start-At (insloc 0))))) . b₅) . b₆ ) & ( for b₆ being FinSeq-Location holds ((Computation (b₁ +* (b₃ +* (Start-At (insloc 0))))) . b₅) . b₆ = ((Computation (b₂ +* (b₃ +* (Start-At (insloc 0))))) . b₅) . b₆ ) & IC ((Computation (b₁ +* (b₃ +* (Start-At (insloc 0))))) . b₅) = IC ((Computation (b₂ +* (b₃ +* (Start-At (insloc 0))))) . b₅) & CurInstr ((Computation (b₁ +* (b₃ +* (Start-At (insloc 0))))) . b₅) = CurInstr ((Computation (b₂ +* (b₃ +* (Start-At (insloc 0))))) . b₅) )

proof end;

theorem Th39: :: SCMFSA8B:39

for b₁ being State of SCM+FSA
for b₂, b₃ being Macro-Instruction
for b₄ being Instruction-Location of SCM+FSA holds
( b₂ is_closed_on b₁ & b₂ is_halting_on b₁ iff ( b₂ is_closed_on b₁ +* (b₂ +* (Start-At b₄)) & b₂ is_halting_on b₁ +* (b₂ +* (Start-At b₄)) ) )

proof end;

theorem Th40: :: SCMFSA8B:40

proof end;

theorem Th41: :: SCMFSA8B:41

for b₁, b₂ being State of SCM+FSA
for b₃ being Macro-Instruction
for b₄ being Int-Location st ( for b₅ being read-write Int-Location st b₄ <> b₅ holds
b₁ . b₅ = b₂ . b₅ ) & ( for b₅ being FinSeq-Location holds b₁ . b₅ = b₂ . b₅ ) & b₃ does_not_refer b₄ & b₃ is_closed_on Initialize b₁ & b₃ is_halting_on Initialize b₁ holds
( ( for b₅ being Int-Location st b₄ <> b₅ holds
(IExec b₃,b₁) . b₅ = (IExec b₃,b₂) . b₅ ) & ( for b₅ being FinSeq-Location holds (IExec b₃,b₁) . b₅ = (IExec b₃,b₂) . b₅ ) & IC (IExec b₃,b₁) = IC (IExec b₃,b₂) )

proof end;

theorem Th42: :: SCMFSA8B:42

for b₁ being State of SCM+FSA
for b₂, b₃ being parahalting Macro-Instruction
for b₄, b₅ being read-write Int-Location st b₂ does_not_refer b₄ & b₃ does_not_refer b₄ holds
( IC (IExec (if=0 b₄,b₅,b₂,b₃),b₁) = insloc (((card b₂) + (card b₃)) + 5) & ( b₁ . b₄ = b₁ . b₅ implies ( ( for b₆ being Int-Location st b₄ <> b₆ holds
(IExec (if=0 b₄,b₅,b₂,b₃),b₁) . b₆ = (IExec b₂,b₁) . b₆ ) & ( for b₆ being FinSeq-Location holds (IExec (if=0 b₄,b₅,b₂,b₃),b₁) . b₆ = (IExec b₂,b₁) . b₆ ) ) ) & ( b₁ . b₄ <> b₁ . b₅ implies ( ( for b₆ being Int-Location st b₄ <> b₆ holds
(IExec (if=0 b₄,b₅,b₂,b₃),b₁) . b₆ = (IExec b₃,b₁) . b₆ ) & ( for b₆ being FinSeq-Location holds (IExec (if=0 b₄,b₅,b₂,b₃),b₁) . b₆ = (IExec b₃,b₁) . b₆ ) ) ) )

proof end;

theorem Th43: :: SCMFSA8B:43

for b₁ being State of SCM+FSA
for b₂, b₃ being parahalting Macro-Instruction
for b₄, b₅ being read-write Int-Location st b₂ does_not_refer b₄ & b₃ does_not_refer b₄ holds
( IC (IExec (if>0 b₄,b₅,b₂,b₃),b₁) = insloc (((card b₂) + (card b₃)) + 5) & ( b₁ . b₄ > b₁ . b₅ implies ( ( for b₆ being Int-Location st b₄ <> b₆ holds
(IExec (if>0 b₄,b₅,b₂,b₃),b₁) . b₆ = (IExec b₂,b₁) . b₆ ) & ( for b₆ being FinSeq-Location holds (IExec (if>0 b₄,b₅,b₂,b₃),b₁) . b₆ = (IExec b₂,b₁) . b₆ ) ) ) & ( b₁ . b₄ <= b₁ . b₅ implies ( ( for b₆ being Int-Location st b₄ <> b₆ holds
(IExec (if>0 b₄,b₅,b₂,b₃),b₁) . b₆ = (IExec b₃,b₁) . b₆ ) & ( for b₆ being FinSeq-Location holds (IExec (if>0 b₄,b₅,b₂,b₃),b₁) . b₆ = (IExec b₃,b₁) . b₆ ) ) ) )

proof end;