:: SCMFSA9A semantic presentation

scheme :: SCMFSA9A:sch 1
MinPred{ F₁( Nat) -> Nat, P₁[ set ] } :

ex k being Nat st
( P₁[k] & ( for n being Nat st P₁[n] holds
k <= n ) )

provided

A1: for k being Nat holds
( F₁((k + 1)) < F₁(k) or P₁[k] )

proof end;

theorem Th1: :: SCMFSA9A:1

for n being natural number holds
( not n is even iff ex k being Nat st n = (2 * k) + 1 )

proof end;

theorem :: SCMFSA9A:2

canceled;

theorem :: SCMFSA9A:3

canceled;

theorem Th4: :: SCMFSA9A:4

for i, j being Integer st 0 < i & 1 < j holds
i div j < i

proof end;

theorem :: SCMFSA9A:5

canceled;

theorem Th6: :: SCMFSA9A:6

for N being non empty with_non-empty_elements set
for S being non empty non void halting IC-Ins-separated definite AMI-Struct of N
for s being State of S
for k being Nat st CurInstr ((Computation s) . k) = halt S holds
(Computation s) . (LifeSpan s) = (Computation s) . k

proof end;

theorem Th7: :: SCMFSA9A:7

for l being Instruction-Location of SCM+FSA
for i being Instruction of SCM+FSA holds UsedIntLoc (l .--> i) = UsedIntLoc i

proof end;

theorem Th8: :: SCMFSA9A:8

for l being Instruction-Location of SCM+FSA
for i being Instruction of SCM+FSA holds UsedInt*Loc (l .--> i) = UsedInt*Loc i

proof end;

theorem Th9: :: SCMFSA9A:9

UsedIntLoc SCM+FSA-Stop = {} by Th7, SCMFSA_4:def 5, SF_MASTR:17;

theorem Th10: :: SCMFSA9A:10

UsedInt*Loc SCM+FSA-Stop = {}

proof end;

theorem Th11: :: SCMFSA9A:11

for l being Instruction-Location of SCM+FSA holds UsedIntLoc (Goto l) = {}

proof end;

theorem Th12: :: SCMFSA9A:12

for l being Instruction-Location of SCM+FSA holds UsedInt*Loc (Goto l) = {}

proof end;

set D = Int-Locations \/ FinSeq-Locations ;

set SAt = Start-At (insloc 0);

set IL = the Instruction-Locations of SCM+FSA ;

theorem Th13: :: SCMFSA9A:13

for b being Int-Location
for I, J being Macro-Instruction holds UsedIntLoc (if=0 b,I,J) = ({b} \/ (UsedIntLoc I)) \/ (UsedIntLoc J)

proof end;

theorem Th14: :: SCMFSA9A:14

for I, J being Macro-Instruction
for a being Int-Location holds UsedInt*Loc (if=0 a,I,J) = (UsedInt*Loc I) \/ (UsedInt*Loc J)

proof end;

theorem Th15: :: SCMFSA9A:15

for b being Int-Location
for I, J being Macro-Instruction holds UsedIntLoc (if>0 b,I,J) = ({b} \/ (UsedIntLoc I)) \/ (UsedIntLoc J)

proof end;

theorem Th16: :: SCMFSA9A:16

for b being Int-Location
for I, J being Macro-Instruction holds UsedInt*Loc (if>0 b,I,J) = (UsedInt*Loc I) \/ (UsedInt*Loc J)

proof end;

Lm1: for a being Int-Location
for I being Macro-Instruction holds
( insloc ((card I) + 4) in dom (if=0 a,(I ';' (Goto (insloc 0))),SCM+FSA-Stop ) & (if=0 a,(I ';' (Goto (insloc 0))),SCM+FSA-Stop ) . (insloc ((card I) + 4)) = goto ((insloc 0) + ((card I) + 4)) )

proof end;

Lm2: for a being Int-Location
for I being Macro-Instruction holds UsedIntLoc (if=0 a,(I ';' (Goto (insloc 0))),SCM+FSA-Stop ) = UsedIntLoc ((if=0 a,(I ';' (Goto (insloc 0))),SCM+FSA-Stop ) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0))))

proof end;

Lm3: for a being Int-Location
for I being Macro-Instruction holds UsedInt*Loc (if=0 a,(I ';' (Goto (insloc 0))),SCM+FSA-Stop ) = UsedInt*Loc ((if=0 a,(I ';' (Goto (insloc 0))),SCM+FSA-Stop ) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0))))

proof end;

theorem :: SCMFSA9A:17

for b being Int-Location
for I being Macro-Instruction holds UsedIntLoc (while=0 b,I) = {b} \/ (UsedIntLoc I)

proof end;

theorem :: SCMFSA9A:18

for b being Int-Location
for I being Macro-Instruction holds UsedInt*Loc (while=0 b,I) = UsedInt*Loc I

proof end;

definition

let s be State of SCM+FSA ;
let a be read-write Int-Location ;
let I be Macro-Instruction;
pred ProperBodyWhile=0 a,I,s means :Def1: :: SCMFSA9A:def 1
for k being Nat st ((StepWhile=0 a,I,s) . k) . a = 0 holds
( I is_closed_on (StepWhile=0 a,I,s) . k & I is_halting_on (StepWhile=0 a,I,s) . k );
pred WithVariantWhile=0 a,I,s means :Def2: :: SCMFSA9A:def 2
ex f being Function of product the Object-Kind of SCM+FSA , NAT st
for k being Nat holds
( f . ((StepWhile=0 a,I,s) . (k + 1)) < f . ((StepWhile=0 a,I,s) . k) or ((StepWhile=0 a,I,s) . k) . a <> 0 );

end;

:: deftheorem Def1 defines ProperBodyWhile=0 SCMFSA9A:def 1 :

:: deftheorem Def2 defines WithVariantWhile=0 SCMFSA9A:def 2 :

theorem Th19: :: SCMFSA9A:19

for s being State of SCM+FSA
for a being read-write Int-Location
for I being parahalting Macro-Instruction holds ProperBodyWhile=0 a,I,s

proof end;

theorem Th20: :: SCMFSA9A:20

for s being State of SCM+FSA
for a being read-write Int-Location
for I being Macro-Instruction st ProperBodyWhile=0 a,I,s & WithVariantWhile=0 a,I,s holds
( while=0 a,I is_halting_on s & while=0 a,I is_closed_on s )

proof end;

theorem Th21: :: SCMFSA9A:21

for s being State of SCM+FSA
for a being read-write Int-Location
for I being parahalting Macro-Instruction st WithVariantWhile=0 a,I,s holds
( while=0 a,I is_halting_on s & while=0 a,I is_closed_on s )

proof end;

theorem Th22: :: SCMFSA9A:22

for s being State of SCM+FSA
for a being read-write Int-Location
for I being Macro-Instruction st (while=0 a,I) +* (Start-At (insloc 0)) c= s & s . a <> 0 holds
( LifeSpan s = 4 & ( for k being Nat holds ((Computation s) . k) | (Int-Locations \/ FinSeq-Locations ) = s | (Int-Locations \/ FinSeq-Locations ) ) )

proof end;

theorem Th23: :: SCMFSA9A:23

for s being State of SCM+FSA
for a being read-write Int-Location
for I being Macro-Instruction st I is_closed_on s & I is_halting_on s & s . a = 0 holds
((Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0))))) . ((LifeSpan (s +* (I +* (Start-At (insloc 0))))) + 3)) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (s +* (I +* (Start-At (insloc 0))))) . (LifeSpan (s +* (I +* (Start-At (insloc 0)))))) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th24: :: SCMFSA9A:24

for s being State of SCM+FSA
for a being read-write Int-Location
for I being Macro-Instruction
for k being Nat st ((StepWhile=0 a,I,s) . k) . a <> 0 holds
((StepWhile=0 a,I,s) . (k + 1)) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile=0 a,I,s) . k) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th25: :: SCMFSA9A:25

for s being State of SCM+FSA
for a being read-write Int-Location
for I being Macro-Instruction
for k being Nat st ( ( I is_halting_on Initialize ((StepWhile=0 a,I,s) . k) & I is_closed_on Initialize ((StepWhile=0 a,I,s) . k) ) or I is parahalting ) & ((StepWhile=0 a,I,s) . k) . a = 0 & ((StepWhile=0 a,I,s) . k) . (intloc 0) = 1 holds
((StepWhile=0 a,I,s) . (k + 1)) | (Int-Locations \/ FinSeq-Locations ) = (IExec I,((StepWhile=0 a,I,s) . k)) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem :: SCMFSA9A:26

for s being State of SCM+FSA
for a being read-write Int-Location
for Ig being good Macro-Instruction st ( ProperBodyWhile=0 a,Ig,s or Ig is parahalting ) & s . (intloc 0) = 1 holds
for k being Nat holds ((StepWhile=0 a,Ig,s) . k) . (intloc 0) = 1

proof end;

theorem :: SCMFSA9A:27

for s1, s2 being State of SCM+FSA
for a being read-write Int-Location
for I being Macro-Instruction st ProperBodyWhile=0 a,I,s1 & s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) holds
for k being Nat holds ((StepWhile=0 a,I,s1) . k) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile=0 a,I,s2) . k) | (Int-Locations \/ FinSeq-Locations )

proof end;

definition

let s be State of SCM+FSA ;
let a be read-write Int-Location ;
let I be Macro-Instruction;
assume that
A1: ( ProperBodyWhile=0 a,I,s or I is parahalting ) and
A2: WithVariantWhile=0 a,I,s ;
func ExitsAtWhile=0 a,I,s -> Nat means :Def3: :: SCMFSA9A:def 3
ex k being Nat st
( it = k & ((StepWhile=0 a,I,s) . k) . a <> 0 & ( for i being Nat st ((StepWhile=0 a,I,s) . i) . a <> 0 holds
k <= i ) & ((Computation (s +* ((while=0 a,I) +* (Start-At (insloc 0))))) . (LifeSpan (s +* ((while=0 a,I) +* (Start-At (insloc 0)))))) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile=0 a,I,s) . k) | (Int-Locations \/ FinSeq-Locations ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines ExitsAtWhile=0 SCMFSA9A:def 3 :

theorem :: SCMFSA9A:28

for s being State of SCM+FSA
for a being read-write Int-Location
for I being Macro-Instruction st s . (intloc 0) = 1 & s . a <> 0 holds
(IExec (while=0 a,I),s) | (Int-Locations \/ FinSeq-Locations ) = s | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem :: SCMFSA9A:29

for s being State of SCM+FSA
for a being read-write Int-Location
for I being Macro-Instruction st ( ProperBodyWhile=0 a,I, Initialize s or I is parahalting ) & WithVariantWhile=0 a,I, Initialize s holds
(IExec (while=0 a,I),s) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile=0 a,I,(Initialize s)) . (ExitsAtWhile=0 a,I,(Initialize s))) | (Int-Locations \/ FinSeq-Locations )

proof end;

Lm4: for a being Int-Location
for I being Macro-Instruction holds
( insloc ((card I) + 4) in dom (if>0 a,(I ';' (Goto (insloc 0))),SCM+FSA-Stop ) & (if>0 a,(I ';' (Goto (insloc 0))),SCM+FSA-Stop ) . (insloc ((card I) + 4)) = goto ((insloc 0) + ((card I) + 4)) )

proof end;

Lm5: for a being Int-Location
for I being Macro-Instruction holds UsedIntLoc (if>0 a,(I ';' (Goto (insloc 0))),SCM+FSA-Stop ) = UsedIntLoc ((if>0 a,(I ';' (Goto (insloc 0))),SCM+FSA-Stop ) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0))))

proof end;

Lm6: for a being Int-Location
for I being Macro-Instruction holds UsedInt*Loc (if>0 a,(I ';' (Goto (insloc 0))),SCM+FSA-Stop ) = UsedInt*Loc ((if>0 a,(I ';' (Goto (insloc 0))),SCM+FSA-Stop ) +* ((insloc ((card I) + 4)) .--> (goto (insloc 0))))

proof end;

theorem :: SCMFSA9A:30

for b being Int-Location
for I being Macro-Instruction holds UsedIntLoc (while>0 b,I) = {b} \/ (UsedIntLoc I)

proof end;

theorem :: SCMFSA9A:31

for b being Int-Location
for I being Macro-Instruction holds UsedInt*Loc (while>0 b,I) = UsedInt*Loc I

proof end;

definition

let s be State of SCM+FSA ;
let a be read-write Int-Location ;
let I be Macro-Instruction;
pred ProperBodyWhile>0 a,I,s means :Def4: :: SCMFSA9A:def 4
for k being Nat st ((StepWhile>0 a,I,s) . k) . a > 0 holds
( I is_closed_on (StepWhile>0 a,I,s) . k & I is_halting_on (StepWhile>0 a,I,s) . k );
pred WithVariantWhile>0 a,I,s means :Def5: :: SCMFSA9A:def 5
ex f being Function of product the Object-Kind of SCM+FSA , NAT st
for k being Nat holds
( f . ((StepWhile>0 a,I,s) . (k + 1)) < f . ((StepWhile>0 a,I,s) . k) or ((StepWhile>0 a,I,s) . k) . a <= 0 );

end;

:: deftheorem Def4 defines ProperBodyWhile>0 SCMFSA9A:def 4 :

:: deftheorem Def5 defines WithVariantWhile>0 SCMFSA9A:def 5 :

theorem Th32: :: SCMFSA9A:32

for s being State of SCM+FSA
for a being read-write Int-Location
for I being parahalting Macro-Instruction holds ProperBodyWhile>0 a,I,s

proof end;

theorem Th33: :: SCMFSA9A:33

for s being State of SCM+FSA
for a being read-write Int-Location
for I being Macro-Instruction st ProperBodyWhile>0 a,I,s & WithVariantWhile>0 a,I,s holds
( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s )

proof end;

theorem Th34: :: SCMFSA9A:34

for s being State of SCM+FSA
for a being read-write Int-Location
for I being parahalting Macro-Instruction st WithVariantWhile>0 a,I,s holds
( while>0 a,I is_halting_on s & while>0 a,I is_closed_on s )

proof end;

theorem Th35: :: SCMFSA9A:35

for s being State of SCM+FSA
for a being read-write Int-Location
for I being Macro-Instruction st (while>0 a,I) +* (Start-At (insloc 0)) c= s & s . a <= 0 holds
( LifeSpan s = 4 & ( for k being Nat holds ((Computation s) . k) | (Int-Locations \/ FinSeq-Locations ) = s | (Int-Locations \/ FinSeq-Locations ) ) )

proof end;

theorem Th36: :: SCMFSA9A:36

for s being State of SCM+FSA
for a being read-write Int-Location
for I being Macro-Instruction st I is_closed_on s & I is_halting_on s & s . a > 0 holds
((Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0))))) . ((LifeSpan (s +* (I +* (Start-At (insloc 0))))) + 3)) | (Int-Locations \/ FinSeq-Locations ) = ((Computation (s +* (I +* (Start-At (insloc 0))))) . (LifeSpan (s +* (I +* (Start-At (insloc 0)))))) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th37: :: SCMFSA9A:37

for s being State of SCM+FSA
for a being read-write Int-Location
for I being Macro-Instruction
for k being Nat st ((StepWhile>0 a,I,s) . k) . a <= 0 holds
((StepWhile>0 a,I,s) . (k + 1)) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile>0 a,I,s) . k) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th38: :: SCMFSA9A:38

for s being State of SCM+FSA
for a being read-write Int-Location
for I being Macro-Instruction
for k being Nat st ( ( I is_halting_on Initialize ((StepWhile>0 a,I,s) . k) & I is_closed_on Initialize ((StepWhile>0 a,I,s) . k) ) or I is parahalting ) & ((StepWhile>0 a,I,s) . k) . a > 0 & ((StepWhile>0 a,I,s) . k) . (intloc 0) = 1 holds
((StepWhile>0 a,I,s) . (k + 1)) | (Int-Locations \/ FinSeq-Locations ) = (IExec I,((StepWhile>0 a,I,s) . k)) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th39: :: SCMFSA9A:39

for s being State of SCM+FSA
for a being read-write Int-Location
for Ig being good Macro-Instruction st ( ProperBodyWhile>0 a,Ig,s or Ig is parahalting ) & s . (intloc 0) = 1 holds
for k being Nat holds ((StepWhile>0 a,Ig,s) . k) . (intloc 0) = 1

proof end;

theorem Th40: :: SCMFSA9A:40

for s1, s2 being State of SCM+FSA
for a being read-write Int-Location
for I being Macro-Instruction st ProperBodyWhile>0 a,I,s1 & s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) holds
for k being Nat holds ((StepWhile>0 a,I,s1) . k) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile>0 a,I,s2) . k) | (Int-Locations \/ FinSeq-Locations )

proof end;

definition

let s be State of SCM+FSA ;
let a be read-write Int-Location ;
let I be Macro-Instruction;
assume that
A1: ( ProperBodyWhile>0 a,I,s or I is parahalting ) and
A2: WithVariantWhile>0 a,I,s ;
func ExitsAtWhile>0 a,I,s -> Nat means :Def6: :: SCMFSA9A:def 6
ex k being Nat st
( it = k & ((StepWhile>0 a,I,s) . k) . a <= 0 & ( for i being Nat st ((StepWhile>0 a,I,s) . i) . a <= 0 holds
k <= i ) & ((Computation (s +* ((while>0 a,I) +* (Start-At (insloc 0))))) . (LifeSpan (s +* ((while>0 a,I) +* (Start-At (insloc 0)))))) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile>0 a,I,s) . k) | (Int-Locations \/ FinSeq-Locations ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines ExitsAtWhile>0 SCMFSA9A:def 6 :

theorem :: SCMFSA9A:41

for s being State of SCM+FSA
for a being read-write Int-Location
for I being Macro-Instruction st s . (intloc 0) = 1 & s . a <= 0 holds
(IExec (while>0 a,I),s) | (Int-Locations \/ FinSeq-Locations ) = s | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th42: :: SCMFSA9A:42

for s being State of SCM+FSA
for a being read-write Int-Location
for I being Macro-Instruction st ( ProperBodyWhile>0 a,I, Initialize s or I is parahalting ) & WithVariantWhile>0 a,I, Initialize s holds
(IExec (while>0 a,I),s) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile>0 a,I,(Initialize s)) . (ExitsAtWhile>0 a,I,(Initialize s))) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem Th43: :: SCMFSA9A:43

for s being State of SCM+FSA
for a being read-write Int-Location
for I being Macro-Instruction
for k being Nat st ((StepWhile>0 a,I,s) . k) . a <= 0 holds
for n being Nat st k <= n holds
((StepWhile>0 a,I,s) . n) | (Int-Locations \/ FinSeq-Locations ) = ((StepWhile>0 a,I,s) . k) | (Int-Locations \/ FinSeq-Locations )

proof end;

theorem :: SCMFSA9A:44

for s1, s2 being State of SCM+FSA
for a being read-write Int-Location
for I being Macro-Instruction st s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) & ProperBodyWhile>0 a,I,s1 holds
ProperBodyWhile>0 a,I,s2

proof end;

Lm7: for s being State of SCM+FSA
for I being Macro-Instruction st s . (intloc 0) = 1 holds
( I is_closed_on s iff I is_closed_on Initialize s )

proof end;

Lm8: for s being State of SCM+FSA
for I being Macro-Instruction st s . (intloc 0) = 1 holds
( I is_closed_on s & I is_halting_on s iff ( I is_closed_on Initialize s & I is_halting_on Initialize s ) )

proof end;

theorem Th45: :: SCMFSA9A:45

for s being State of SCM+FSA
for a being read-write Int-Location
for Ig being good Macro-Instruction st s . (intloc 0) = 1 & ProperBodyWhile>0 a,Ig,s & WithVariantWhile>0 a,Ig,s holds
for i, j being Nat st i <> j & i <= ExitsAtWhile>0 a,Ig,s & j <= ExitsAtWhile>0 a,Ig,s holds
( (StepWhile>0 a,Ig,s) . i <> (StepWhile>0 a,Ig,s) . j & ((StepWhile>0 a,Ig,s) . i) | (Int-Locations \/ FinSeq-Locations ) <> ((StepWhile>0 a,Ig,s) . j) | (Int-Locations \/ FinSeq-Locations ) )

proof end;

definition

let f be Function of product the Object-Kind of SCM+FSA , NAT ;
attr f is on_data_only means :Def7: :: SCMFSA9A:def 7
for s1, s2 being State of SCM+FSA st s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) holds
f . s1 = f . s2;

end;

:: deftheorem Def7 defines on_data_only SCMFSA9A:def 7 :

theorem Th46: :: SCMFSA9A:46

for s being State of SCM+FSA
for a being read-write Int-Location
for Ig being good Macro-Instruction st s . (intloc 0) = 1 & ProperBodyWhile>0 a,Ig,s & WithVariantWhile>0 a,Ig,s holds
ex f being Function of product the Object-Kind of SCM+FSA , NAT st
( f is on_data_only & ( for k being Nat holds
( f . ((StepWhile>0 a,Ig,s) . (k + 1)) < f . ((StepWhile>0 a,Ig,s) . k) or ((StepWhile>0 a,Ig,s) . k) . a <= 0 ) ) )

proof end;

theorem :: SCMFSA9A:47

for s1, s2 being State of SCM+FSA
for a being read-write Int-Location
for Ig being good Macro-Instruction st s1 . (intloc 0) = 1 & s1 | (Int-Locations \/ FinSeq-Locations ) = s2 | (Int-Locations \/ FinSeq-Locations ) & ProperBodyWhile>0 a,Ig,s1 & WithVariantWhile>0 a,Ig,s1 holds
WithVariantWhile>0 a,Ig,s2

proof end;

definition

let N, result be Int-Location ;
set next = 1 -stRWNotIn {N,result};
set aux = 2 -ndRWNotIn {N,result};
set rem2 = 3 -rdRWNotIn {N,result};
func Fusc_macro N,result -> Macro-Instruction equals :: SCMFSA9A:def 8
(((SubFrom result,result) ';' ((1 -stRWNotIn {N,result}) := (intloc 0))) ';' ((2 -ndRWNotIn {N,result}) := N)) ';' (while>0 (2 -ndRWNotIn {N,result}),((((3 -rdRWNotIn {N,result}) := 2) ';' (Divide (2 -ndRWNotIn {N,result}),(3 -rdRWNotIn {N,result}))) ';' (if=0 (3 -rdRWNotIn {N,result}),(Macro (AddTo (1 -stRWNotIn {N,result}),result)),(Macro (AddTo result,(1 -stRWNotIn {N,result}))))));
correctness ;

end;

:: deftheorem defines Fusc_macro SCMFSA9A:def 8 :

theorem :: SCMFSA9A:48

for s being State of SCM+FSA
for N, result being read-write Int-Location st N <> result holds
for n being Nat st n = s . N holds
( (IExec (Fusc_macro N,result),s) . result = Fusc n & (IExec (Fusc_macro N,result),s) . N = n )

proof end;