:: SCMFSA_9 semantic presentation

theorem Th1: :: SCMFSA_9:1

for b₁ being Macro-Instruction
for b₂ being Int-Location holds card (if=0 b₂,(b₁ ';' (Goto (insloc 0))),SCM+FSA-Stop ) = (card b₁) + 6

proof end;

theorem Th2: :: SCMFSA_9:2

for b₁ being Macro-Instruction
for b₂ being Int-Location holds card (if>0 b₂,(b₁ ';' (Goto (insloc 0))),SCM+FSA-Stop ) = (card b₁) + 6

proof end;

definition

let c₁ be Int-Location ;
let c₂ be Macro-Instruction;
func while=0 c₁,c₂ -> Macro-Instruction equals :: SCMFSA_9:def 1
(if=0 a₁,(a₂ ';' (Goto (insloc 0))),SCM+FSA-Stop ) +* ((insloc ((card a₂) + 4)) .--> (goto (insloc 0)));
correctness

proof end;

func while>0 c₁,c₂ -> Macro-Instruction equals :: SCMFSA_9:def 2
(if>0 a₁,(a₂ ';' (Goto (insloc 0))),SCM+FSA-Stop ) +* ((insloc ((card a₂) + 4)) .--> (goto (insloc 0)));
correctness

proof end;

end;

:: deftheorem Def1 defines while=0 SCMFSA_9:def 1 :

:: deftheorem Def2 defines while>0 SCMFSA_9:def 2 :

theorem Th3: :: SCMFSA_9:3

for b₁ being Macro-Instruction
for b₂ being Int-Location holds card (if=0 b₂,SCM+FSA-Stop ,(if>0 b₂,SCM+FSA-Stop ,(b₁ ';' (Goto (insloc 0))))) = (card b₁) + 11

proof end;

definition

let c₁ be Int-Location ;
let c₂ be Macro-Instruction;
func while<0 c₁,c₂ -> Macro-Instruction equals :: SCMFSA_9:def 3
(if=0 a₁,SCM+FSA-Stop ,(if>0 a₁,SCM+FSA-Stop ,(a₂ ';' (Goto (insloc 0))))) +* ((insloc ((card a₂) + 4)) .--> (goto (insloc 0)));
correctness

proof end;

end;

:: deftheorem Def3 defines while<0 SCMFSA_9:def 3 :

theorem Th4: :: SCMFSA_9:4

for b₁ being Macro-Instruction
for b₂ being Int-Location holds card (while=0 b₂,b₁) = (card b₁) + 6

proof end;

theorem Th5: :: SCMFSA_9:5

for b₁ being Macro-Instruction
for b₂ being Int-Location holds card (while>0 b₂,b₁) = (card b₁) + 6

proof end;

theorem Th6: :: SCMFSA_9:6

for b₁ being Macro-Instruction
for b₂ being Int-Location holds card (while<0 b₂,b₁) = (card b₁) + 11

proof end;

theorem Th7: :: SCMFSA_9:7

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;

theorem Th8: :: SCMFSA_9:8

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;

theorem Th9: :: SCMFSA_9:9

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

theorem Th10: :: SCMFSA_9:10

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

proof end;

theorem Th11: :: SCMFSA_9:11

for b₁ being Int-Location
for b₂ being Macro-Instruction holds
( (while=0 b₁,b₂) . (insloc 0) = b₁ =0_goto (insloc 4) & (while=0 b₁,b₂) . (insloc 1) = goto (insloc 2) & (while>0 b₁,b₂) . (insloc 0) = b₁ >0_goto (insloc 4) & (while>0 b₁,b₂) . (insloc 1) = goto (insloc 2) )

proof end;

theorem Th12: :: SCMFSA_9:12

for b₁ being Int-Location
for b₂ being Macro-Instruction
for b₃ being Nat st b₃ < 6 holds
insloc b₃ in dom (while=0 b₁,b₂)

proof end;

theorem Th13: :: SCMFSA_9:13

for b₁ being Int-Location
for b₂ being Macro-Instruction
for b₃ being Nat st b₃ < 6 holds
insloc ((card b₂) + b₃) in dom (while=0 b₁,b₂)

proof end;

theorem Th14: :: SCMFSA_9:14

for b₁ being Int-Location
for b₂ being Macro-Instruction holds (while=0 b₁,b₂) . (insloc ((card b₂) + 5)) = halt SCM+FSA

proof end;

theorem Th15: :: SCMFSA_9:15

for b₁ being Int-Location
for b₂ being Macro-Instruction holds (while=0 b₁,b₂) . (insloc 3) = goto (insloc ((card b₂) + 5))

proof end;

theorem Th16: :: SCMFSA_9:16

for b₁ being Int-Location
for b₂ being Macro-Instruction holds (while=0 b₁,b₂) . (insloc 2) = goto (insloc 3)

proof end;

theorem Th17: :: SCMFSA_9:17

for b₁ being Int-Location
for b₂ being Macro-Instruction
for b₃ being Nat st b₃ < (card b₂) + 6 holds
insloc b₃ in dom (while=0 b₁,b₂)

proof end;

theorem Th18: :: SCMFSA_9:18

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

proof end;

theorem Th19: :: SCMFSA_9:19

for b₁ being Int-Location
for b₂ being Macro-Instruction
for b₃ being State of SCM+FSA
for b₄ being Nat st b₂ is_closed_on b₃ & b₂ is_halting_on b₃ & b₄ < LifeSpan (b₃ +* (b₂ +* (Start-At (insloc 0)))) & IC ((Computation (b₃ +* ((while=0 b₁,b₂) +* (Start-At (insloc 0))))) . (1 + b₄)) = (IC ((Computation (b₃ +* (b₂ +* (Start-At (insloc 0))))) . b₄)) + 4 & ((Computation (b₃ +* ((while=0 b₁,b₂) +* (Start-At (insloc 0))))) . (1 + b₄)) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b₃ +* (b₂ +* (Start-At (insloc 0))))) . b₄) | (Int-Locations \/ FinSeq-Locations ) holds
( IC ((Computation (b₃ +* ((while=0 b₁,b₂) +* (Start-At (insloc 0))))) . ((1 + b₄) + 1)) = (IC ((Computation (b₃ +* (b₂ +* (Start-At (insloc 0))))) . (b₄ + 1))) + 4 & ((Computation (b₃ +* ((while=0 b₁,b₂) +* (Start-At (insloc 0))))) . ((1 + b₄) + 1)) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b₃ +* (b₂ +* (Start-At (insloc 0))))) . (b₄ + 1)) | (Int-Locations \/ FinSeq-Locations ) )

proof end;

theorem Th20: :: SCMFSA_9:20

for b₁ being Int-Location
for b₂ being Macro-Instruction
for b₃ being State of SCM+FSA st b₂ is_closed_on b₃ & b₂ is_halting_on b₃ & IC ((Computation (b₃ +* ((while=0 b₁,b₂) +* (Start-At (insloc 0))))) . (1 + (LifeSpan (b₃ +* (b₂ +* (Start-At (insloc 0))))))) = (IC ((Computation (b₃ +* (b₂ +* (Start-At (insloc 0))))) . (LifeSpan (b₃ +* (b₂ +* (Start-At (insloc 0))))))) + 4 holds
CurInstr ((Computation (b₃ +* ((while=0 b₁,b₂) +* (Start-At (insloc 0))))) . (1 + (LifeSpan (b₃ +* (b₂ +* (Start-At (insloc 0))))))) = goto (insloc ((card b₂) + 4))

proof end;

theorem Th21: :: SCMFSA_9:21

for b₁ being Int-Location
for b₂ being Macro-Instruction holds (while=0 b₁,b₂) . (insloc ((card b₂) + 4)) = goto (insloc 0)

proof end;

theorem Th22: :: SCMFSA_9:22

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction
for b₃ being read-write Int-Location st b₂ is_closed_on b₁ & b₂ is_halting_on b₁ & b₁ . b₃ = 0 holds
( IC ((Computation (b₁ +* ((while=0 b₃,b₂) +* (Start-At (insloc 0))))) . ((LifeSpan (b₁ +* (b₂ +* (Start-At (insloc 0))))) + 3)) = insloc 0 & ( for b₄ being Nat st b₄ <= (LifeSpan (b₁ +* (b₂ +* (Start-At (insloc 0))))) + 3 holds
IC ((Computation (b₁ +* ((while=0 b₃,b₂) +* (Start-At (insloc 0))))) . b₄) in dom (while=0 b₃,b₂) ) )

proof end;

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

definition

let c₂ be State of SCM+FSA ;
let c₃ be Macro-Instruction;
let c₄ be read-write Int-Location ;
func StepWhile=0 c₃,c₂,c₁ -> Function of NAT , product the Object-Kind of SCM+FSA means :Def4: :: SCMFSA_9:def 4
( a₄ . 0 = a₁ & ( for b₁ being Nat holds a₄ . (b₁ + 1) = (Computation ((a₄ . b₁) +* ((while=0 a₃,a₂) +* (Start-At (insloc 0))))) . ((LifeSpan ((a₄ . b₁) +* (a₂ +* (Start-At (insloc 0))))) + 3) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines StepWhile=0 SCMFSA_9:def 4 :

theorem Th23: :: SCMFSA_9:23

canceled;

theorem Th24: :: SCMFSA_9:24

canceled;

theorem Th25: :: SCMFSA_9:25

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction
for b₃ being read-write Int-Location
for b₄ being Nat holds (StepWhile=0 b₃,b₂,b₁) . (b₄ + 1) = (StepWhile=0 b₃,b₂,((StepWhile=0 b₃,b₂,b₁) . b₄)) . 1

proof end;

scheme :: SCMFSA_9:sch 1
s1{ F₁( Nat) -> Nat, F₂() -> Nat } :

ex b₁ being Nat st
( F₁(b₁) = 0 & ( for b₂ being Nat st F₁(b₂) = 0 holds
b₁ <= b₂ ) )

provided

E23: F₁(0) = F₂() and
E24: for b₁ being Nat holds
( F₁((b₁ + 1)) < F₁(b₁) or F₁(b₁) = 0 )

proof end;

theorem Th26: :: SCMFSA_9:26

for b₁, b₂ being Function holds (b₁ +* b₂) +* b₂ = b₁ +* b₂

proof end;

theorem Th27: :: SCMFSA_9:27

for b₁, b₂, b₃ being Function
for b₄ being set st (b₁ +* b₂) | b₄ = b₃ | b₄ holds
(b₃ +* b₂) | b₄ = (b₁ +* b₂) | b₄

proof end;

theorem Th28: :: SCMFSA_9:28

for b₁, b₂, b₃ being Function
for b₄ being set st b₁ | b₄ = b₃ | b₄ holds
(b₃ +* b₂) | b₄ = (b₁ +* b₂) | b₄

proof end;

theorem Th29: :: SCMFSA_9:29

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

proof end;

theorem Th30: :: SCMFSA_9:30

for b₁ being Macro-Instruction
for b₂ being read-write Int-Location
for b₃ being State of SCM+FSA holds (StepWhile=0 b₂,b₁,b₃) . (0 + 1) = (Computation (b₃ +* ((while=0 b₂,b₁) +* (Start-At (insloc 0))))) . ((LifeSpan (b₃ +* (b₁ +* (Start-At (insloc 0))))) + 3)

proof end;

theorem Th31: :: SCMFSA_9:31

for b₁ being Macro-Instruction
for b₂ being read-write Int-Location
for b₃ being State of SCM+FSA
for b₄, b₅ being Nat st IC ((StepWhile=0 b₂,b₁,b₃) . b₄) = insloc 0 & (StepWhile=0 b₂,b₁,b₃) . b₄ = (Computation (b₃ +* ((while=0 b₂,b₁) +* (Start-At (insloc 0))))) . b₅ holds
( (StepWhile=0 b₂,b₁,b₃) . b₄ = ((StepWhile=0 b₂,b₁,b₃) . b₄) +* ((while=0 b₂,b₁) +* (Start-At (insloc 0))) & (StepWhile=0 b₂,b₁,b₃) . (b₄ + 1) = (Computation (b₃ +* ((while=0 b₂,b₁) +* (Start-At (insloc 0))))) . (b₅ + ((LifeSpan (((StepWhile=0 b₂,b₁,b₃) . b₄) +* (b₁ +* (Start-At (insloc 0))))) + 3)) )

proof end;

theorem Th32: :: SCMFSA_9:32

for b₁ being Macro-Instruction
for b₂ being read-write Int-Location
for b₃ being State of SCM+FSA st ( for b₄ being Nat holds
( b₁ is_closed_on (StepWhile=0 b₂,b₁,b₃) . b₄ & b₁ is_halting_on (StepWhile=0 b₂,b₁,b₃) . b₄ ) ) & ex b₄ being Function of product the Object-Kind of SCM+FSA , NAT st
for b₅ being Nat holds
( ( b₄ . ((StepWhile=0 b₂,b₁,b₃) . (b₅ + 1)) < b₄ . ((StepWhile=0 b₂,b₁,b₃) . b₅) or b₄ . ((StepWhile=0 b₂,b₁,b₃) . b₅) = 0 ) & ( b₄ . ((StepWhile=0 b₂,b₁,b₃) . b₅) = 0 implies ((StepWhile=0 b₂,b₁,b₃) . b₅) . b₂ <> 0 ) & ( ((StepWhile=0 b₂,b₁,b₃) . b₅) . b₂ <> 0 implies b₄ . ((StepWhile=0 b₂,b₁,b₃) . b₅) = 0 ) ) holds
( while=0 b₂,b₁ is_halting_on b₃ & while=0 b₂,b₁ is_closed_on b₃ )

proof end;

theorem Th33: :: SCMFSA_9:33

for b₁ being parahalting Macro-Instruction
for b₂ being read-write Int-Location
for b₃ being State of SCM+FSA st ex b₄ being Function of product the Object-Kind of SCM+FSA , NAT st
for b₅ being Nat holds
( ( b₄ . ((StepWhile=0 b₂,b₁,b₃) . (b₅ + 1)) < b₄ . ((StepWhile=0 b₂,b₁,b₃) . b₅) or b₄ . ((StepWhile=0 b₂,b₁,b₃) . b₅) = 0 ) & ( b₄ . ((StepWhile=0 b₂,b₁,b₃) . b₅) = 0 implies ((StepWhile=0 b₂,b₁,b₃) . b₅) . b₂ <> 0 ) & ( ((StepWhile=0 b₂,b₁,b₃) . b₅) . b₂ <> 0 implies b₄ . ((StepWhile=0 b₂,b₁,b₃) . b₅) = 0 ) ) holds
( while=0 b₂,b₁ is_halting_on b₃ & while=0 b₂,b₁ is_closed_on b₃ )

proof end;

theorem Th34: :: SCMFSA_9:34

for b₁ being parahalting Macro-Instruction
for b₂ being read-write Int-Location st ex b₃ being Function of product the Object-Kind of SCM+FSA , NAT st
for b₄ being State of SCM+FSA holds
( ( b₃ . ((StepWhile=0 b₂,b₁,b₄) . 1) < b₃ . b₄ or b₃ . b₄ = 0 ) & ( b₃ . b₄ = 0 implies b₄ . b₂ <> 0 ) & ( b₄ . b₂ <> 0 implies b₃ . b₄ = 0 ) ) holds
while=0 b₂,b₁ is parahalting

proof end;

theorem Th35: :: SCMFSA_9:35

for b₁, b₂ being Instruction-Location of SCM+FSA
for b₃ being Int-Location holds b₁ .--> (goto b₂) does_not_destroy b₃

proof end;

theorem Th36: :: SCMFSA_9:36

for b₁ being Instruction of SCM+FSA st b₁ does_not_destroy intloc 0 holds
Macro b₁ is good

proof end;

registration

let c₂, c₃ be good Macro-Instruction;
let c₄ be Int-Location ;
cluster if=0 a₃,a₁,a₂ -> good ;
correctness

proof end;

end;

registration

let c₂ be good Macro-Instruction;
let c₃ be Int-Location ;
cluster while=0 a₂,a₁ -> good ;
correctness

proof end;

end;

theorem Th37: :: SCMFSA_9:37

for b₁ being Int-Location
for b₂ being Macro-Instruction
for b₃ being Nat st b₃ < 6 holds
insloc b₃ in dom (while>0 b₁,b₂)

proof end;

theorem Th38: :: SCMFSA_9:38

for b₁ being Int-Location
for b₂ being Macro-Instruction
for b₃ being Nat st b₃ < 6 holds
insloc ((card b₂) + b₃) in dom (while>0 b₁,b₂)

proof end;

theorem Th39: :: SCMFSA_9:39

for b₁ being Int-Location
for b₂ being Macro-Instruction holds (while>0 b₁,b₂) . (insloc ((card b₂) + 5)) = halt SCM+FSA

proof end;

theorem Th40: :: SCMFSA_9:40

for b₁ being Int-Location
for b₂ being Macro-Instruction holds (while>0 b₁,b₂) . (insloc 3) = goto (insloc ((card b₂) + 5))

proof end;

theorem Th41: :: SCMFSA_9:41

for b₁ being Int-Location
for b₂ being Macro-Instruction holds (while>0 b₁,b₂) . (insloc 2) = goto (insloc 3)

proof end;

theorem Th42: :: SCMFSA_9:42

for b₁ being Int-Location
for b₂ being Macro-Instruction
for b₃ being Nat st b₃ < (card b₂) + 6 holds
insloc b₃ in dom (while>0 b₁,b₂)

proof end;

theorem Th43: :: SCMFSA_9:43

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

proof end;

theorem Th44: :: SCMFSA_9:44

for b₁ being Int-Location
for b₂ being Macro-Instruction
for b₃ being State of SCM+FSA
for b₄ being Nat st b₂ is_closed_on b₃ & b₂ is_halting_on b₃ & b₄ < LifeSpan (b₃ +* (b₂ +* (Start-At (insloc 0)))) & IC ((Computation (b₃ +* ((while>0 b₁,b₂) +* (Start-At (insloc 0))))) . (1 + b₄)) = (IC ((Computation (b₃ +* (b₂ +* (Start-At (insloc 0))))) . b₄)) + 4 & ((Computation (b₃ +* ((while>0 b₁,b₂) +* (Start-At (insloc 0))))) . (1 + b₄)) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b₃ +* (b₂ +* (Start-At (insloc 0))))) . b₄) | (Int-Locations \/ FinSeq-Locations ) holds
( IC ((Computation (b₃ +* ((while>0 b₁,b₂) +* (Start-At (insloc 0))))) . ((1 + b₄) + 1)) = (IC ((Computation (b₃ +* (b₂ +* (Start-At (insloc 0))))) . (b₄ + 1))) + 4 & ((Computation (b₃ +* ((while>0 b₁,b₂) +* (Start-At (insloc 0))))) . ((1 + b₄) + 1)) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (b₃ +* (b₂ +* (Start-At (insloc 0))))) . (b₄ + 1)) | (Int-Locations \/ FinSeq-Locations ) )

proof end;

theorem Th45: :: SCMFSA_9:45

for b₁ being Int-Location
for b₂ being Macro-Instruction
for b₃ being State of SCM+FSA st b₂ is_closed_on b₃ & b₂ is_halting_on b₃ & IC ((Computation (b₃ +* ((while>0 b₁,b₂) +* (Start-At (insloc 0))))) . (1 + (LifeSpan (b₃ +* (b₂ +* (Start-At (insloc 0))))))) = (IC ((Computation (b₃ +* (b₂ +* (Start-At (insloc 0))))) . (LifeSpan (b₃ +* (b₂ +* (Start-At (insloc 0))))))) + 4 holds
CurInstr ((Computation (b₃ +* ((while>0 b₁,b₂) +* (Start-At (insloc 0))))) . (1 + (LifeSpan (b₃ +* (b₂ +* (Start-At (insloc 0))))))) = goto (insloc ((card b₂) + 4))

proof end;

theorem Th46: :: SCMFSA_9:46

for b₁ being Int-Location
for b₂ being Macro-Instruction holds (while>0 b₁,b₂) . (insloc ((card b₂) + 4)) = goto (insloc 0)

proof end;

theorem Th47: :: SCMFSA_9:47

for b₁ being State of SCM+FSA
for b₂ being Macro-Instruction
for b₃ being read-write Int-Location st b₂ is_closed_on b₁ & b₂ is_halting_on b₁ & b₁ . b₃ > 0 holds
( IC ((Computation (b₁ +* ((while>0 b₃,b₂) +* (Start-At (insloc 0))))) . ((LifeSpan (b₁ +* (b₂ +* (Start-At (insloc 0))))) + 3)) = insloc 0 & ( for b₄ being Nat st b₄ <= (LifeSpan (b₁ +* (b₂ +* (Start-At (insloc 0))))) + 3 holds
IC ((Computation (b₁ +* ((while>0 b₃,b₂) +* (Start-At (insloc 0))))) . b₄) in dom (while>0 b₃,b₂) ) )

proof end;

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

definition

let c₃ be State of SCM+FSA ;
let c₄ be Macro-Instruction;
let c₅ be read-write Int-Location ;
func StepWhile>0 c₃,c₂,c₁ -> Function of NAT , product the Object-Kind of SCM+FSA means :Def5: :: SCMFSA_9:def 5
( a₄ . 0 = a₁ & ( for b₁ being Nat holds a₄ . (b₁ + 1) = (Computation ((a₄ . b₁) +* ((while>0 a₃,a₂) +* (Start-At (insloc 0))))) . ((LifeSpan ((a₄ . b₁) +* (a₂ +* (Start-At (insloc 0))))) + 3) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines StepWhile>0 SCMFSA_9:def 5 :

theorem Th48: :: SCMFSA_9:48

canceled;

theorem Th49: :: SCMFSA_9:49

canceled;

theorem Th50: :: SCMFSA_9:50

for b₁ being Nat
for b₂ being State of SCM+FSA
for b₃ being Macro-Instruction
for b₄ being read-write Int-Location holds (StepWhile>0 b₄,b₃,b₂) . (b₁ + 1) = (StepWhile>0 b₄,b₃,((StepWhile>0 b₄,b₃,b₂) . b₁)) . 1

proof end;

theorem Th51: :: SCMFSA_9:51

for b₁ being Macro-Instruction
for b₂ being read-write Int-Location
for b₃ being State of SCM+FSA holds (StepWhile>0 b₂,b₁,b₃) . (0 + 1) = (Computation (b₃ +* ((while>0 b₂,b₁) +* (Start-At (insloc 0))))) . ((LifeSpan (b₃ +* (b₁ +* (Start-At (insloc 0))))) + 3)

proof end;

theorem Th52: :: SCMFSA_9:52

for b₁ being Macro-Instruction
for b₂ being read-write Int-Location
for b₃ being State of SCM+FSA
for b₄, b₅ being Nat st IC ((StepWhile>0 b₂,b₁,b₃) . b₄) = insloc 0 & (StepWhile>0 b₂,b₁,b₃) . b₄ = (Computation (b₃ +* ((while>0 b₂,b₁) +* (Start-At (insloc 0))))) . b₅ holds
( (StepWhile>0 b₂,b₁,b₃) . b₄ = ((StepWhile>0 b₂,b₁,b₃) . b₄) +* ((while>0 b₂,b₁) +* (Start-At (insloc 0))) & (StepWhile>0 b₂,b₁,b₃) . (b₄ + 1) = (Computation (b₃ +* ((while>0 b₂,b₁) +* (Start-At (insloc 0))))) . (b₅ + ((LifeSpan (((StepWhile>0 b₂,b₁,b₃) . b₄) +* (b₁ +* (Start-At (insloc 0))))) + 3)) )

proof end;

theorem Th53: :: SCMFSA_9:53

for b₁ being Macro-Instruction
for b₂ being read-write Int-Location
for b₃ being State of SCM+FSA st ( for b₄ being Nat holds
( b₁ is_closed_on (StepWhile>0 b₂,b₁,b₃) . b₄ & b₁ is_halting_on (StepWhile>0 b₂,b₁,b₃) . b₄ ) ) & ex b₄ being Function of product the Object-Kind of SCM+FSA , NAT st
for b₅ being Nat holds
( ( b₄ . ((StepWhile>0 b₂,b₁,b₃) . (b₅ + 1)) < b₄ . ((StepWhile>0 b₂,b₁,b₃) . b₅) or b₄ . ((StepWhile>0 b₂,b₁,b₃) . b₅) = 0 ) & ( b₄ . ((StepWhile>0 b₂,b₁,b₃) . b₅) = 0 implies ((StepWhile>0 b₂,b₁,b₃) . b₅) . b₂ <= 0 ) & ( ((StepWhile>0 b₂,b₁,b₃) . b₅) . b₂ <= 0 implies b₄ . ((StepWhile>0 b₂,b₁,b₃) . b₅) = 0 ) ) holds
( while>0 b₂,b₁ is_halting_on b₃ & while>0 b₂,b₁ is_closed_on b₃ )

proof end;

theorem Th54: :: SCMFSA_9:54

for b₁ being parahalting Macro-Instruction
for b₂ being read-write Int-Location
for b₃ being State of SCM+FSA st ex b₄ being Function of product the Object-Kind of SCM+FSA , NAT st
for b₅ being Nat holds
( ( b₄ . ((StepWhile>0 b₂,b₁,b₃) . (b₅ + 1)) < b₄ . ((StepWhile>0 b₂,b₁,b₃) . b₅) or b₄ . ((StepWhile>0 b₂,b₁,b₃) . b₅) = 0 ) & ( b₄ . ((StepWhile>0 b₂,b₁,b₃) . b₅) = 0 implies ((StepWhile>0 b₂,b₁,b₃) . b₅) . b₂ <= 0 ) & ( ((StepWhile>0 b₂,b₁,b₃) . b₅) . b₂ <= 0 implies b₄ . ((StepWhile>0 b₂,b₁,b₃) . b₅) = 0 ) ) holds
( while>0 b₂,b₁ is_halting_on b₃ & while>0 b₂,b₁ is_closed_on b₃ )

proof end;

theorem Th55: :: SCMFSA_9:55

for b₁ being parahalting Macro-Instruction
for b₂ being read-write Int-Location st ex b₃ being Function of product the Object-Kind of SCM+FSA , NAT st
for b₄ being State of SCM+FSA holds
( ( b₃ . ((StepWhile>0 b₂,b₁,b₄) . 1) < b₃ . b₄ or b₃ . b₄ = 0 ) & ( b₃ . b₄ = 0 implies b₄ . b₂ <= 0 ) & ( b₄ . b₂ <= 0 implies b₃ . b₄ = 0 ) ) holds
while>0 b₂,b₁ is parahalting

proof end;

registration

let c₃, c₄ be good Macro-Instruction;
let c₅ be Int-Location ;
cluster if>0 a₃,a₁,a₂ -> good ;
coherence

proof end;

end;

registration

let c₃ be good Macro-Instruction;
let c₄ be Int-Location ;
cluster while>0 a₂,a₁ -> good ;
correctness

proof end;

end;