:: by Piotr Rudnicki

::

:: Received June 4, 1998

:: Copyright (c) 1998-2017 Association of Mizar Users

set D = Data-Locations ;

theorem Th1: :: SFMASTR2:1

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for b being Int-Location

for I being really-closed Program of st I is_halting_on Initialized s,p & not b in UsedILoc I holds

(IExec (I,p,s)) . b = (Initialized s) . b

for p being Instruction-Sequence of SCM+FSA

for b being Int-Location

for I being really-closed Program of st I is_halting_on Initialized s,p & not b in UsedILoc I holds

(IExec (I,p,s)) . b = (Initialized s) . b

proof end;

theorem :: SFMASTR2:2

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for f being FinSeq-Location

for I being really-closed Program of st I is_halting_on Initialized s,p & not f in UsedI*Loc I holds

(IExec (I,p,s)) . f = (Initialized s) . f

for p being Instruction-Sequence of SCM+FSA

for f being FinSeq-Location

for I being really-closed Program of st I is_halting_on Initialized s,p & not f in UsedI*Loc I holds

(IExec (I,p,s)) . f = (Initialized s) . f

proof end;

theorem :: SFMASTR2:3

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for I being really-closed Program of st ( I is_halting_on Initialized s,p or I is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) & not a in UsedILoc I holds

(IExec (I,p,s)) . a = s . a

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for I being really-closed Program of st ( I is_halting_on Initialized s,p or I is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) & not a in UsedILoc I holds

(IExec (I,p,s)) . a = s . a

proof end;

definition

let a be Int-Location;

let I be MacroInstruction of SCM+FSA ;

coherence

while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(intloc 0))))) is MacroInstruction of SCM+FSA ;

;

end;
let I be MacroInstruction of SCM+FSA ;

func times* (a,I) -> MacroInstruction of SCM+FSA equals :: SFMASTR2:def 1

while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(intloc 0)))));

correctness while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(intloc 0)))));

coherence

while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(intloc 0))))) is MacroInstruction of SCM+FSA ;

;

:: deftheorem defines times* SFMASTR2:def 1 :

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds times* (a,I) = while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(intloc 0)))));

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds times* (a,I) = while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(intloc 0)))));

definition

let a be Int-Location;

let I be MacroInstruction of SCM+FSA ;

coherence

((1 -stRWNotIn ({a} \/ (UsedILoc I))) := a) ";" (times* (a,I)) is MacroInstruction of SCM+FSA ;

;

end;
let I be MacroInstruction of SCM+FSA ;

func times (a,I) -> MacroInstruction of SCM+FSA equals :: SFMASTR2:def 2

((1 -stRWNotIn ({a} \/ (UsedILoc I))) := a) ";" (times* (a,I));

correctness ((1 -stRWNotIn ({a} \/ (UsedILoc I))) := a) ";" (times* (a,I));

coherence

((1 -stRWNotIn ({a} \/ (UsedILoc I))) := a) ";" (times* (a,I)) is MacroInstruction of SCM+FSA ;

;

:: deftheorem defines times SFMASTR2:def 2 :

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds times (a,I) = ((1 -stRWNotIn ({a} \/ (UsedILoc I))) := a) ";" (times* (a,I));

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds times (a,I) = ((1 -stRWNotIn ({a} \/ (UsedILoc I))) := a) ";" (times* (a,I));

registration

let a be Int-Location;

let I be really-closed MacroInstruction of SCM+FSA ;

coherence

times* (a,I) is really-closed ;

end;
let I be really-closed MacroInstruction of SCM+FSA ;

coherence

times* (a,I) is really-closed ;

registration

let a be Int-Location;

let I be really-closed MacroInstruction of SCM+FSA ;

coherence

times (a,I) is really-closed ;

end;
let I be really-closed MacroInstruction of SCM+FSA ;

coherence

times (a,I) is really-closed ;

::$CT 2

theorem :: SFMASTR2:8

for b being Int-Location

for I being MacroInstruction of SCM+FSA holds {b} \/ (UsedILoc I) c= UsedILoc (times (b,I))

for I being MacroInstruction of SCM+FSA holds {b} \/ (UsedILoc I) c= UsedILoc (times (b,I))

proof end;

theorem :: SFMASTR2:9

for b being Int-Location

for I being MacroInstruction of SCM+FSA holds UsedI*Loc (times (b,I)) = UsedI*Loc I

for I being MacroInstruction of SCM+FSA holds UsedI*Loc (times (b,I)) = UsedI*Loc I

proof end;

registration
end;

definition

let p be Instruction-Sequence of SCM+FSA;

let s be State of SCM+FSA;

let I be MacroInstruction of SCM+FSA ;

let a be Int-Location;

coherence

StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc I))) := a),(Initialized s)))) is sequence of (product (the_Values_of SCM+FSA));

;

end;
let s be State of SCM+FSA;

let I be MacroInstruction of SCM+FSA ;

let a be Int-Location;

func StepTimes (a,I,p,s) -> sequence of (product (the_Values_of SCM+FSA)) equals :: SFMASTR2:def 3

StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc I))) := a),(Initialized s))));

correctness StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc I))) := a),(Initialized s))));

coherence

StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc I))) := a),(Initialized s)))) is sequence of (product (the_Values_of SCM+FSA));

;

:: deftheorem defines StepTimes SFMASTR2:def 3 :

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being MacroInstruction of SCM+FSA

for a being Int-Location holds StepTimes (a,I,p,s) = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc I))) := a),(Initialized s))));

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being MacroInstruction of SCM+FSA

for a being Int-Location holds StepTimes (a,I,p,s) = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(I ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc I))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc I))) := a),(Initialized s))));

theorem Th6: :: SFMASTR2:10

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for J being good MacroInstruction of SCM+FSA holds ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for J being good MacroInstruction of SCM+FSA holds ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1

proof end;

theorem Th7: :: SFMASTR2:11

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for J being good MacroInstruction of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) holds

((StepTimes (a,J,p,s)) . 0) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = s . a

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for J being good MacroInstruction of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) holds

((StepTimes (a,J,p,s)) . 0) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = s . a

proof end;

theorem Th8: :: SFMASTR2:12

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for k being Nat

for J being really-closed good MacroInstruction of SCM+FSA st ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 & J is_halting_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) holds

( ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 & ( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) > 0 implies ((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))) - 1 ) )

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for k being Nat

for J being really-closed good MacroInstruction of SCM+FSA st ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 & J is_halting_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) holds

( ((StepTimes (a,J,p,s)) . (k + 1)) . (intloc 0) = 1 & ( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) > 0 implies ((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))) - 1 ) )

proof end;

theorem Th9: :: SFMASTR2:13

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for I being MacroInstruction of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) holds

((StepTimes (a,I,p,s)) . 0) . a = s . a

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for I being MacroInstruction of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) holds

((StepTimes (a,I,p,s)) . 0) . a = s . a

proof end;

theorem :: SFMASTR2:14

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for f being FinSeq-Location

for I being MacroInstruction of SCM+FSA holds ((StepTimes (a,I,p,s)) . 0) . f = s . f

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for f being FinSeq-Location

for I being MacroInstruction of SCM+FSA holds ((StepTimes (a,I,p,s)) . 0) . f = s . f

proof end;

definition

let p be Instruction-Sequence of SCM+FSA;

let s be State of SCM+FSA;

let a be Int-Location;

let I be MacroInstruction of SCM+FSA ;

end;
let s be State of SCM+FSA;

let a be Int-Location;

let I be MacroInstruction of SCM+FSA ;

pred ProperTimesBody a,I,s,p means :: SFMASTR2:def 4

for k being Nat st k < s . a holds

I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I));

for k being Nat st k < s . a holds

I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I));

:: deftheorem defines ProperTimesBody SFMASTR2:def 4 :

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds

( ProperTimesBody a,I,s,p iff for k being Nat st k < s . a holds

I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) );

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being Int-Location

for I being MacroInstruction of SCM+FSA holds

( ProperTimesBody a,I,s,p iff for k being Nat st k < s . a holds

I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (times* (a,I)) );

theorem Th11: :: SFMASTR2:15

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for I being MacroInstruction of SCM+FSA st I is parahalting holds

ProperTimesBody a,I,s,p by SCMFSA7B:19;

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for I being MacroInstruction of SCM+FSA st I is parahalting holds

ProperTimesBody a,I,s,p by SCMFSA7B:19;

theorem Th12: :: SFMASTR2:16

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for J being really-closed good MacroInstruction of SCM+FSA st ProperTimesBody a,J,s,p holds

for k being Nat st k <= s . a holds

((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for J being really-closed good MacroInstruction of SCM+FSA st ProperTimesBody a,J,s,p holds

for k being Nat st k <= s . a holds

((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1

proof end;

theorem Th13: :: SFMASTR2:17

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for J being really-closed good MacroInstruction of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) & ProperTimesBody a,J,s,p holds

for k being Nat st k <= s . a holds

(((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))) + k = s . a

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for J being really-closed good MacroInstruction of SCM+FSA st ( s . (intloc 0) = 1 or a is read-write ) & ProperTimesBody a,J,s,p holds

for k being Nat st k <= s . a holds

(((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))) + k = s . a

proof end;

theorem Th14: :: SFMASTR2:18

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for J being really-closed good MacroInstruction of SCM+FSA st ProperTimesBody a,J,s,p & 0 <= s . a & ( s . (intloc 0) = 1 or a is read-write ) holds

for k being Nat st k >= s . a holds

( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = 0 & ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 )

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for J being really-closed good MacroInstruction of SCM+FSA st ProperTimesBody a,J,s,p & 0 <= s . a & ( s . (intloc 0) = 1 or a is read-write ) holds

for k being Nat st k >= s . a holds

( ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = 0 & ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 )

proof end;

theorem :: SFMASTR2:19

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for I being MacroInstruction of SCM+FSA st s . (intloc 0) = 1 holds

((StepTimes (a,I,p,s)) . 0) | ((UsedILoc I) \/ FinSeq-Locations) = s | ((UsedILoc I) \/ FinSeq-Locations)

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for I being MacroInstruction of SCM+FSA st s . (intloc 0) = 1 holds

((StepTimes (a,I,p,s)) . 0) | ((UsedILoc I) \/ FinSeq-Locations) = s | ((UsedILoc I) \/ FinSeq-Locations)

proof end;

theorem Th16: :: SFMASTR2:20

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for k being Nat

for J being really-closed good MacroInstruction of SCM+FSA st ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 & J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) & ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) > 0 holds

((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedILoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedILoc J) \/ FinSeq-Locations)

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for k being Nat

for J being really-closed good MacroInstruction of SCM+FSA st ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 & J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) & ((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) > 0 holds

((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedILoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedILoc J) \/ FinSeq-Locations)

proof end;

theorem :: SFMASTR2:21

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for k being Nat

for J being really-closed good MacroInstruction of SCM+FSA st ( ProperTimesBody a,J,s,p or J is parahalting ) & k < s . a & ( s . (intloc 0) = 1 or a is read-write ) holds

((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedILoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedILoc J) \/ FinSeq-Locations)

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for k being Nat

for J being really-closed good MacroInstruction of SCM+FSA st ( ProperTimesBody a,J,s,p or J is parahalting ) & k < s . a & ( s . (intloc 0) = 1 or a is read-write ) holds

((StepTimes (a,J,p,s)) . (k + 1)) | ((UsedILoc J) \/ FinSeq-Locations) = (IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k))) | ((UsedILoc J) \/ FinSeq-Locations)

proof end;

theorem :: SFMASTR2:22

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for I being really-closed MacroInstruction of SCM+FSA st s . a <= 0 & s . (intloc 0) = 1 holds

(IExec ((times (a,I)),p,s)) | ((UsedILoc I) \/ FinSeq-Locations) = s | ((UsedILoc I) \/ FinSeq-Locations)

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for I being really-closed MacroInstruction of SCM+FSA st s . a <= 0 & s . (intloc 0) = 1 holds

(IExec ((times (a,I)),p,s)) | ((UsedILoc I) \/ FinSeq-Locations) = s | ((UsedILoc I) \/ FinSeq-Locations)

proof end;

theorem Th19: :: SFMASTR2:23

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for k being Nat

for J being really-closed good MacroInstruction of SCM+FSA st s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) holds

DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k)

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for k being Nat

for J being really-closed good MacroInstruction of SCM+FSA st s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) holds

DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k)

proof end;

theorem :: SFMASTR2:24

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for J being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) holds

times (a,J) is_halting_on s,p

for p being Instruction-Sequence of SCM+FSA

for a being Int-Location

for J being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) holds

times (a,J) is_halting_on s,p

proof end;

definition

let d be read-write Int-Location;

coherence

times (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))) is MacroInstruction of SCM+FSA ;

;

end;
func triv-times d -> MacroInstruction of SCM+FSA equals :: SFMASTR2:def 5

times (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))));

correctness times (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))));

coherence

times (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0))))) is MacroInstruction of SCM+FSA ;

;

:: deftheorem defines triv-times SFMASTR2:def 5 :

for d being read-write Int-Location holds triv-times d = times (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))));

for d being read-write Int-Location holds triv-times d = times (d,((while=0 (d,(Macro (d := d)))) ";" (SubFrom (d,(intloc 0)))));

theorem :: SFMASTR2:25

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for d being read-write Int-Location st s . d <= 0 holds

(IExec ((triv-times d),p,s)) . d = s . d

for p being Instruction-Sequence of SCM+FSA

for d being read-write Int-Location st s . d <= 0 holds

(IExec ((triv-times d),p,s)) . d = s . d

proof end;

theorem :: SFMASTR2:26

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for d being read-write Int-Location st 0 <= s . d holds

(IExec ((triv-times d),p,s)) . d = 0

for p being Instruction-Sequence of SCM+FSA

for d being read-write Int-Location st 0 <= s . d holds

(IExec ((triv-times d),p,s)) . d = 0

proof end;