:: by Piotr Rudnicki

::

:: Received June 3, 1998

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

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

set SAt = Start-At (0,SCM+FSA);

theorem :: SCMFSA9A:7

for b being Int-Location

for I, J being MacroInstruction of SCM+FSA holds UsedILoc (if=0 (b,I,J)) = ({b} \/ (UsedILoc I)) \/ (UsedILoc J)

for I, J being MacroInstruction of SCM+FSA holds UsedILoc (if=0 (b,I,J)) = ({b} \/ (UsedILoc I)) \/ (UsedILoc J)

proof end;

theorem :: SCMFSA9A:8

for I, J being MacroInstruction of SCM+FSA

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

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

proof end;

theorem :: SCMFSA9A:9

for b being Int-Location

for I, J being MacroInstruction of SCM+FSA holds UsedILoc (if>0 (b,I,J)) = ({b} \/ (UsedILoc I)) \/ (UsedILoc J)

for I, J being MacroInstruction of SCM+FSA holds UsedILoc (if>0 (b,I,J)) = ({b} \/ (UsedILoc I)) \/ (UsedILoc J)

proof end;

theorem :: SCMFSA9A:10

for b being Int-Location

for I, J being MacroInstruction of SCM+FSA holds UsedI*Loc (if>0 (b,I,J)) = (UsedI*Loc I) \/ (UsedI*Loc J)

for I, J being MacroInstruction of SCM+FSA holds UsedI*Loc (if>0 (b,I,J)) = (UsedI*Loc I) \/ (UsedI*Loc J)

proof end;

Lm1: for a being Int-Location

for I being MacroInstruction of SCM+FSA holds (if=0 (a,(I ';' (goto 0)))) . ((card (I ';' (goto 0))) + 1) = goto ((card (I ';' (goto 0))) + 1)

proof end;

Lm2: for a being Int-Location

for I being MacroInstruction of SCM+FSA holds (if>0 (a,(I ';' (goto 0)))) . ((card (I ';' (goto 0))) + 1) = goto ((card (I ';' (goto 0))) + 1)

proof end;

Lm3: for a being Int-Location

for I being MacroInstruction of SCM+FSA holds UsedILoc (if=0 (a,(I ';' (goto 0)))) = UsedILoc ((if=0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)))

proof end;

Lm4: for a being Int-Location

for I being MacroInstruction of SCM+FSA holds UsedI*Loc (if=0 (a,(I ';' (goto 0)))) = UsedI*Loc ((if=0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)))

proof end;

theorem :: SCMFSA9A:11

for b being Int-Location

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

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

proof end;

theorem :: SCMFSA9A:12

for b being Int-Location

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

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

proof end;

definition

let p be Instruction-Sequence of SCM+FSA;

let s be State of SCM+FSA;

let a be read-write Int-Location;

let I be MacroInstruction of SCM+FSA ;

end;
let s be State of SCM+FSA;

let a be read-write Int-Location;

let I be MacroInstruction of SCM+FSA ;

pred ProperBodyWhile=0 a,I,s,p means :: SCMFSA9A:def 1

for k being Nat st ((StepWhile=0 (a,I,p,s)) . k) . a = 0 holds

I is_halting_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I));

for k being Nat st ((StepWhile=0 (a,I,p,s)) . k) . a = 0 holds

I is_halting_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I));

pred WithVariantWhile=0 a,I,s,p means :: SCMFSA9A:def 2

ex f being Function of (product (the_Values_of SCM+FSA)),NAT st

for k being Nat holds

( f . ((StepWhile=0 (a,I,p,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,p,s)) . k) or ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 );

ex f being Function of (product (the_Values_of SCM+FSA)),NAT st

for k being Nat holds

( f . ((StepWhile=0 (a,I,p,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,p,s)) . k) or ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 );

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

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being MacroInstruction of SCM+FSA holds

( ProperBodyWhile=0 a,I,s,p iff for k being Nat st ((StepWhile=0 (a,I,p,s)) . k) . a = 0 holds

I is_halting_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I)) );

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being MacroInstruction of SCM+FSA holds

( ProperBodyWhile=0 a,I,s,p iff for k being Nat st ((StepWhile=0 (a,I,p,s)) . k) . a = 0 holds

I is_halting_on (StepWhile=0 (a,I,p,s)) . k,p +* (while=0 (a,I)) );

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

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being MacroInstruction of SCM+FSA holds

( WithVariantWhile=0 a,I,s,p iff ex f being Function of (product (the_Values_of SCM+FSA)),NAT st

for k being Nat holds

( f . ((StepWhile=0 (a,I,p,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,p,s)) . k) or ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 ) );

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being MacroInstruction of SCM+FSA holds

( WithVariantWhile=0 a,I,s,p iff ex f being Function of (product (the_Values_of SCM+FSA)),NAT st

for k being Nat holds

( f . ((StepWhile=0 (a,I,p,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,p,s)) . k) or ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 ) );

theorem Th13: :: SCMFSA9A:13

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being parahalting MacroInstruction of SCM+FSA holds ProperBodyWhile=0 a,I,s,p by SCMFSA7B:19;

for s being State of SCM+FSA

for a being read-write Int-Location

for I being parahalting MacroInstruction of SCM+FSA holds ProperBodyWhile=0 a,I,s,p by SCMFSA7B:19;

theorem Th14: :: SCMFSA9A:14

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st ProperBodyWhile=0 a,I,s,p & WithVariantWhile=0 a,I,s,p holds

while=0 (a,I) is_halting_on s,p

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st ProperBodyWhile=0 a,I,s,p & WithVariantWhile=0 a,I,s,p holds

while=0 (a,I) is_halting_on s,p

proof end;

theorem Th15: :: SCMFSA9A:15

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed parahalting MacroInstruction of SCM+FSA st WithVariantWhile=0 a,I,s,p holds

while=0 (a,I) is_halting_on s,p

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed parahalting MacroInstruction of SCM+FSA st WithVariantWhile=0 a,I,s,p holds

while=0 (a,I) is_halting_on s,p

proof end;

theorem Th16: :: SCMFSA9A:16

for p being Instruction-Sequence of SCM+FSA

for a being read-write Int-Location

for I being MacroInstruction of SCM+FSA

for s being 0 -started State of SCM+FSA st while=0 (a,I) c= p & s . a <> 0 holds

( LifeSpan (p,s) = 3 & ( for k being Nat holds DataPart (Comput (p,s,k)) = DataPart s ) )

for a being read-write Int-Location

for I being MacroInstruction of SCM+FSA

for s being 0 -started State of SCM+FSA st while=0 (a,I) c= p & s . a <> 0 holds

( LifeSpan (p,s) = 3 & ( for k being Nat holds DataPart (Comput (p,s,k)) = DataPart s ) )

proof end;

theorem Th17: :: SCMFSA9A:17

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st I is_halting_on s,p & s . a = 0 holds

DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),((LifeSpan ((p +* I),(Initialize s))) + 2))) = DataPart (Comput ((p +* I),(Initialize s),(LifeSpan ((p +* I),(Initialize s)))))

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st I is_halting_on s,p & s . a = 0 holds

DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),((LifeSpan ((p +* I),(Initialize s))) + 2))) = DataPart (Comput ((p +* I),(Initialize s),(LifeSpan ((p +* I),(Initialize s)))))

proof end;

theorem Th18: :: SCMFSA9A:18

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being MacroInstruction of SCM+FSA

for k being Nat st ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 holds

DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart ((StepWhile=0 (a,I,p,s)) . k)

for s being State of SCM+FSA

for a being read-write Int-Location

for I being MacroInstruction of SCM+FSA

for k being Nat st ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 holds

DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart ((StepWhile=0 (a,I,p,s)) . k)

proof end;

theorem Th19: :: SCMFSA9A:19

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for k being Nat

for I being really-closed MacroInstruction of SCM+FSA st ( I is_halting_on Initialized ((StepWhile=0 (a,I,p,s)) . k),p +* (while=0 (a,I)) or I is parahalting ) & ((StepWhile=0 (a,I,p,s)) . k) . a = 0 & ((StepWhile=0 (a,I,p,s)) . k) . (intloc 0) = 1 holds

DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart (IExec (I,(p +* (while=0 (a,I))),((StepWhile=0 (a,I,p,s)) . k)))

for s being State of SCM+FSA

for a being read-write Int-Location

for k being Nat

for I being really-closed MacroInstruction of SCM+FSA st ( I is_halting_on Initialized ((StepWhile=0 (a,I,p,s)) . k),p +* (while=0 (a,I)) or I is parahalting ) & ((StepWhile=0 (a,I,p,s)) . k) . a = 0 & ((StepWhile=0 (a,I,p,s)) . k) . (intloc 0) = 1 holds

DataPart ((StepWhile=0 (a,I,p,s)) . (k + 1)) = DataPart (IExec (I,(p +* (while=0 (a,I))),((StepWhile=0 (a,I,p,s)) . k)))

proof end;

theorem :: SCMFSA9A:20

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

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

for k being Nat holds ((StepWhile=0 (a,Ig,p,s)) . k) . (intloc 0) = 1

for s being State of SCM+FSA

for a being read-write Int-Location

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

for k being Nat holds ((StepWhile=0 (a,Ig,p,s)) . k) . (intloc 0) = 1

proof end;

theorem :: SCMFSA9A:21

for p1, p2 being Instruction-Sequence of SCM+FSA

for s1, s2 being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st ProperBodyWhile=0 a,I,s1,p1 & DataPart s1 = DataPart s2 holds

for k being Nat holds DataPart ((StepWhile=0 (a,I,p1,s1)) . k) = DataPart ((StepWhile=0 (a,I,p2,s2)) . k)

for s1, s2 being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st ProperBodyWhile=0 a,I,s1,p1 & DataPart s1 = DataPart s2 holds

for k being Nat holds DataPart ((StepWhile=0 (a,I,p1,s1)) . k) = DataPart ((StepWhile=0 (a,I,p2,s2)) . k)

proof end;

definition

let p be Instruction-Sequence of SCM+FSA;

let s be State of SCM+FSA;

let a be read-write Int-Location;

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

assume that

A1: ( ProperBodyWhile=0 a,I,s,p or I is parahalting ) and

A2: WithVariantWhile=0 a,I,s,p ;

ex b_{1}, k being Nat st

( b_{1} = k & ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 & ( for i being Nat st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds

k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) )

for b_{1}, b_{2} being Nat st ex k being Nat st

( b_{1} = k & ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 & ( for i being Nat st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds

k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) ) & ex k being Nat st

( b_{2} = k & ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 & ( for i being Nat st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds

k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) ) holds

b_{1} = b_{2}

end;
let s be State of SCM+FSA;

let a be read-write Int-Location;

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

assume that

A1: ( ProperBodyWhile=0 a,I,s,p or I is parahalting ) and

A2: WithVariantWhile=0 a,I,s,p ;

func ExitsAtWhile=0 (a,I,p,s) -> Nat means :Def3: :: SCMFSA9A:def 3

ex k being Nat st

( it = k & ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 & ( for i being Nat st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds

k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) );

existence ex k being Nat st

( it = k & ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 & ( for i being Nat st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds

k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) );

ex b

( b

k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) )

proof end;

uniqueness for b

( b

k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) ) & ex k being Nat st

( b

k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) ) holds

b

proof end;

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

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st ( ProperBodyWhile=0 a,I,s,p or I is parahalting ) & WithVariantWhile=0 a,I,s,p holds

for b_{5} being Nat holds

( b_{5} = ExitsAtWhile=0 (a,I,p,s) iff ex k being Nat st

( b_{5} = k & ((StepWhile=0 (a,I,p,s)) . k) . a <> 0 & ( for i being Nat st ((StepWhile=0 (a,I,p,s)) . i) . a <> 0 holds

k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) ) );

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st ( ProperBodyWhile=0 a,I,s,p or I is parahalting ) & WithVariantWhile=0 a,I,s,p holds

for b

( b

( b

k <= i ) & DataPart (Comput ((p +* (while=0 (a,I))),(Initialize s),(LifeSpan ((p +* (while=0 (a,I))),(Initialize s))))) = DataPart ((StepWhile=0 (a,I,p,s)) . k) ) );

theorem :: SCMFSA9A:22

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

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

DataPart (IExec ((while=0 (a,I)),p,s)) = DataPart s

for s being State of SCM+FSA

for a being read-write Int-Location

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

DataPart (IExec ((while=0 (a,I)),p,s)) = DataPart s

proof end;

theorem :: SCMFSA9A:23

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st ( ProperBodyWhile=0 a,I, Initialized s,p or I is parahalting ) & WithVariantWhile=0 a,I, Initialized s,p holds

DataPart (IExec ((while=0 (a,I)),p,s)) = DataPart ((StepWhile=0 (a,I,p,(Initialized s))) . (ExitsAtWhile=0 (a,I,p,(Initialized s))))

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st ( ProperBodyWhile=0 a,I, Initialized s,p or I is parahalting ) & WithVariantWhile=0 a,I, Initialized s,p holds

DataPart (IExec ((while=0 (a,I)),p,s)) = DataPart ((StepWhile=0 (a,I,p,(Initialized s))) . (ExitsAtWhile=0 (a,I,p,(Initialized s))))

proof end;

Lm5: for a being Int-Location

for I being MacroInstruction of SCM+FSA holds UsedILoc (if>0 (a,(I ';' (goto 0)))) = UsedILoc ((if>0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)))

proof end;

Lm6: for a being Int-Location

for I being MacroInstruction of SCM+FSA holds UsedI*Loc (if>0 (a,(I ';' (goto 0)))) = UsedI*Loc ((if>0 (a,(I ';' (goto 0)))) +* (((card I) + 2),(goto 0)))

proof end;

theorem Th24: :: SCMFSA9A:24

for b being Int-Location

for I being MacroInstruction of SCM+FSA holds UsedILoc (while>0 (b,I)) = {b} \/ (UsedILoc I)

for I being MacroInstruction of SCM+FSA holds UsedILoc (while>0 (b,I)) = {b} \/ (UsedILoc I)

proof end;

theorem Th25: :: SCMFSA9A:25

for b being Int-Location

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

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

proof end;

definition

let p be Instruction-Sequence of SCM+FSA;

let s be State of SCM+FSA;

let a be read-write Int-Location;

let I be MacroInstruction of SCM+FSA ;

end;
let s be State of SCM+FSA;

let a be read-write Int-Location;

let I be MacroInstruction of SCM+FSA ;

pred ProperBodyWhile>0 a,I,s,p means :: SCMFSA9A:def 4

for k being Nat st ((StepWhile>0 (a,I,p,s)) . k) . a > 0 holds

I is_halting_on (StepWhile>0 (a,I,p,s)) . k,p +* (while>0 (a,I));

for k being Nat st ((StepWhile>0 (a,I,p,s)) . k) . a > 0 holds

I is_halting_on (StepWhile>0 (a,I,p,s)) . k,p +* (while>0 (a,I));

pred WithVariantWhile>0 a,I,s,p means :: SCMFSA9A:def 5

ex f being Function of (product (the_Values_of SCM+FSA)),NAT st

for k being Nat holds

( f . ((StepWhile>0 (a,I,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,p,s)) . k) or ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 );

ex f being Function of (product (the_Values_of SCM+FSA)),NAT st

for k being Nat holds

( f . ((StepWhile>0 (a,I,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,p,s)) . k) or ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 );

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

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being MacroInstruction of SCM+FSA holds

( ProperBodyWhile>0 a,I,s,p iff for k being Nat st ((StepWhile>0 (a,I,p,s)) . k) . a > 0 holds

I is_halting_on (StepWhile>0 (a,I,p,s)) . k,p +* (while>0 (a,I)) );

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being MacroInstruction of SCM+FSA holds

( ProperBodyWhile>0 a,I,s,p iff for k being Nat st ((StepWhile>0 (a,I,p,s)) . k) . a > 0 holds

I is_halting_on (StepWhile>0 (a,I,p,s)) . k,p +* (while>0 (a,I)) );

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

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being MacroInstruction of SCM+FSA holds

( WithVariantWhile>0 a,I,s,p iff ex f being Function of (product (the_Values_of SCM+FSA)),NAT st

for k being Nat holds

( f . ((StepWhile>0 (a,I,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,p,s)) . k) or ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 ) );

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being MacroInstruction of SCM+FSA holds

( WithVariantWhile>0 a,I,s,p iff ex f being Function of (product (the_Values_of SCM+FSA)),NAT st

for k being Nat holds

( f . ((StepWhile>0 (a,I,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,p,s)) . k) or ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 ) );

theorem Th26: :: SCMFSA9A:26

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being parahalting MacroInstruction of SCM+FSA holds ProperBodyWhile>0 a,I,s,p by SCMFSA7B:19;

for s being State of SCM+FSA

for a being read-write Int-Location

for I being parahalting MacroInstruction of SCM+FSA holds ProperBodyWhile>0 a,I,s,p by SCMFSA7B:19;

theorem Th27: :: SCMFSA9A:27

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st ProperBodyWhile>0 a,I,s,p & WithVariantWhile>0 a,I,s,p holds

while>0 (a,I) is_halting_on s,p

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st ProperBodyWhile>0 a,I,s,p & WithVariantWhile>0 a,I,s,p holds

while>0 (a,I) is_halting_on s,p

proof end;

theorem Th28: :: SCMFSA9A:28

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed parahalting MacroInstruction of SCM+FSA st WithVariantWhile>0 a,I,s,p holds

while>0 (a,I) is_halting_on s,p

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed parahalting MacroInstruction of SCM+FSA st WithVariantWhile>0 a,I,s,p holds

while>0 (a,I) is_halting_on s,p

proof end;

theorem Th29: :: SCMFSA9A:29

for p being Instruction-Sequence of SCM+FSA

for a being read-write Int-Location

for I being MacroInstruction of SCM+FSA

for s being 0 -started State of SCM+FSA st while>0 (a,I) c= p & s . a <= 0 holds

( LifeSpan (p,s) = 3 & ( for k being Nat holds DataPart (Comput (p,s,k)) = DataPart s ) )

for a being read-write Int-Location

for I being MacroInstruction of SCM+FSA

for s being 0 -started State of SCM+FSA st while>0 (a,I) c= p & s . a <= 0 holds

( LifeSpan (p,s) = 3 & ( for k being Nat holds DataPart (Comput (p,s,k)) = DataPart s ) )

proof end;

theorem Th30: :: SCMFSA9A:30

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st I is_halting_on s,p & s . a > 0 holds

DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),((LifeSpan ((p +* I),(Initialize s))) + 2))) = DataPart (Comput ((p +* I),(Initialize s),(LifeSpan ((p +* I),(Initialize s)))))

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st I is_halting_on s,p & s . a > 0 holds

DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),((LifeSpan ((p +* I),(Initialize s))) + 2))) = DataPart (Comput ((p +* I),(Initialize s),(LifeSpan ((p +* I),(Initialize s)))))

proof end;

theorem Th31: :: SCMFSA9A:31

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being MacroInstruction of SCM+FSA

for k being Nat st ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 holds

DataPart ((StepWhile>0 (a,I,p,s)) . (k + 1)) = DataPart ((StepWhile>0 (a,I,p,s)) . k)

for s being State of SCM+FSA

for a being read-write Int-Location

for I being MacroInstruction of SCM+FSA

for k being Nat st ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 holds

DataPart ((StepWhile>0 (a,I,p,s)) . (k + 1)) = DataPart ((StepWhile>0 (a,I,p,s)) . k)

proof end;

theorem Th32: :: SCMFSA9A:32

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for k being Nat

for I being really-closed MacroInstruction of SCM+FSA st ( I is_halting_on Initialized ((StepWhile>0 (a,I,p,s)) . k),p +* (while>0 (a,I)) or I is parahalting ) & ((StepWhile>0 (a,I,p,s)) . k) . a > 0 & ((StepWhile>0 (a,I,p,s)) . k) . (intloc 0) = 1 holds

DataPart ((StepWhile>0 (a,I,p,s)) . (k + 1)) = DataPart (IExec (I,(p +* (while>0 (a,I))),((StepWhile>0 (a,I,p,s)) . k)))

for s being State of SCM+FSA

for a being read-write Int-Location

for k being Nat

for I being really-closed MacroInstruction of SCM+FSA st ( I is_halting_on Initialized ((StepWhile>0 (a,I,p,s)) . k),p +* (while>0 (a,I)) or I is parahalting ) & ((StepWhile>0 (a,I,p,s)) . k) . a > 0 & ((StepWhile>0 (a,I,p,s)) . k) . (intloc 0) = 1 holds

DataPart ((StepWhile>0 (a,I,p,s)) . (k + 1)) = DataPart (IExec (I,(p +* (while>0 (a,I))),((StepWhile>0 (a,I,p,s)) . k)))

proof end;

theorem Th33: :: SCMFSA9A:33

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

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

for k being Nat holds ((StepWhile>0 (a,Ig,p,s)) . k) . (intloc 0) = 1

for s being State of SCM+FSA

for a being read-write Int-Location

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

for k being Nat holds ((StepWhile>0 (a,Ig,p,s)) . k) . (intloc 0) = 1

proof end;

theorem Th34: :: SCMFSA9A:34

for p1, p2 being Instruction-Sequence of SCM+FSA

for s1, s2 being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st ProperBodyWhile>0 a,I,s1,p1 & DataPart s1 = DataPart s2 holds

for k being Nat holds DataPart ((StepWhile>0 (a,I,p1,s1)) . k) = DataPart ((StepWhile>0 (a,I,p2,s2)) . k)

for s1, s2 being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st ProperBodyWhile>0 a,I,s1,p1 & DataPart s1 = DataPart s2 holds

for k being Nat holds DataPart ((StepWhile>0 (a,I,p1,s1)) . k) = DataPart ((StepWhile>0 (a,I,p2,s2)) . k)

proof end;

definition

let p be Instruction-Sequence of SCM+FSA;

let s be State of SCM+FSA;

let a be read-write Int-Location;

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

assume that

A1: ( ProperBodyWhile>0 a,I,s,p or I is parahalting ) and

A2: WithVariantWhile>0 a,I,s,p ;

ex b_{1}, k being Nat st

( b_{1} = k & ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 & ( for i being Nat st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds

k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) )

for b_{1}, b_{2} being Nat st ex k being Nat st

( b_{1} = k & ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 & ( for i being Nat st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds

k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) ) & ex k being Nat st

( b_{2} = k & ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 & ( for i being Nat st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds

k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) ) holds

b_{1} = b_{2}

end;
let s be State of SCM+FSA;

let a be read-write Int-Location;

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

assume that

A1: ( ProperBodyWhile>0 a,I,s,p or I is parahalting ) and

A2: WithVariantWhile>0 a,I,s,p ;

func ExitsAtWhile>0 (a,I,p,s) -> Nat means :Def6: :: SCMFSA9A:def 6

ex k being Nat st

( it = k & ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 & ( for i being Nat st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds

k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) );

existence ex k being Nat st

( it = k & ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 & ( for i being Nat st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds

k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) );

ex b

( b

k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) )

proof end;

uniqueness for b

( b

k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) ) & ex k being Nat st

( b

k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) ) holds

b

proof end;

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

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st ( ProperBodyWhile>0 a,I,s,p or I is parahalting ) & WithVariantWhile>0 a,I,s,p holds

for b_{5} being Nat holds

( b_{5} = ExitsAtWhile>0 (a,I,p,s) iff ex k being Nat st

( b_{5} = k & ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 & ( for i being Nat st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds

k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) ) );

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st ( ProperBodyWhile>0 a,I,s,p or I is parahalting ) & WithVariantWhile>0 a,I,s,p holds

for b

( b

( b

k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) ) );

theorem Th35: :: SCMFSA9A:35

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

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

DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart s

for s being State of SCM+FSA

for a being read-write Int-Location

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

DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart s

proof end;

theorem Th36: :: SCMFSA9A:36

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st ( ProperBodyWhile>0 a,I, Initialized s,p or I is parahalting ) & WithVariantWhile>0 a,I, Initialized s,p holds

DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart ((StepWhile>0 (a,I,p,(Initialized s))) . (ExitsAtWhile>0 (a,I,p,(Initialized s))))

for s being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st ( ProperBodyWhile>0 a,I, Initialized s,p or I is parahalting ) & WithVariantWhile>0 a,I, Initialized s,p holds

DataPart (IExec ((while>0 (a,I)),p,s)) = DataPart ((StepWhile>0 (a,I,p,(Initialized s))) . (ExitsAtWhile>0 (a,I,p,(Initialized s))))

proof end;

theorem Th37: :: SCMFSA9A:37

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for I being MacroInstruction of SCM+FSA

for k being Nat st ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 holds

for n being Nat st k <= n holds

DataPart ((StepWhile>0 (a,I,p,s)) . n) = DataPart ((StepWhile>0 (a,I,p,s)) . k)

for s being State of SCM+FSA

for a being read-write Int-Location

for I being MacroInstruction of SCM+FSA

for k being Nat st ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 holds

for n being Nat st k <= n holds

DataPart ((StepWhile>0 (a,I,p,s)) . n) = DataPart ((StepWhile>0 (a,I,p,s)) . k)

proof end;

theorem :: SCMFSA9A:38

for p1, p2 being Instruction-Sequence of SCM+FSA

for s1, s2 being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st DataPart s1 = DataPart s2 & ProperBodyWhile>0 a,I,s1,p1 holds

ProperBodyWhile>0 a,I,s2,p2

for s1, s2 being State of SCM+FSA

for a being read-write Int-Location

for I being really-closed MacroInstruction of SCM+FSA st DataPart s1 = DataPart s2 & ProperBodyWhile>0 a,I,s1,p1 holds

ProperBodyWhile>0 a,I,s2,p2

proof end;

Lm7: for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being really-closed Program of st s . (intloc 0) = 1 holds

( I is_halting_on s,p iff I is_halting_on Initialized s,p )

proof end;

theorem Th39: :: SCMFSA9A:39

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for Ig being good really-closed MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ProperBodyWhile>0 a,Ig,s,p & WithVariantWhile>0 a,Ig,s,p holds

for i, j being Nat st i <> j & i <= ExitsAtWhile>0 (a,Ig,p,s) & j <= ExitsAtWhile>0 (a,Ig,p,s) holds

( (StepWhile>0 (a,Ig,p,s)) . i <> (StepWhile>0 (a,Ig,p,s)) . j & DataPart ((StepWhile>0 (a,Ig,p,s)) . i) <> DataPart ((StepWhile>0 (a,Ig,p,s)) . j) )

for s being State of SCM+FSA

for a being read-write Int-Location

for Ig being good really-closed MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ProperBodyWhile>0 a,Ig,s,p & WithVariantWhile>0 a,Ig,s,p holds

for i, j being Nat st i <> j & i <= ExitsAtWhile>0 (a,Ig,p,s) & j <= ExitsAtWhile>0 (a,Ig,p,s) holds

( (StepWhile>0 (a,Ig,p,s)) . i <> (StepWhile>0 (a,Ig,p,s)) . j & DataPart ((StepWhile>0 (a,Ig,p,s)) . i) <> DataPart ((StepWhile>0 (a,Ig,p,s)) . j) )

proof end;

canceled;

::$CD

theorem Th40: :: SCMFSA9A:40

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write Int-Location

for Ig being good really-closed MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ProperBodyWhile>0 a,Ig,s,p & WithVariantWhile>0 a,Ig,s,p holds

ex f being Function of (product (the_Values_of SCM+FSA)),NAT st

( f is on_data_only & ( for k being Nat holds

( f . ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,Ig,p,s)) . k) or ((StepWhile>0 (a,Ig,p,s)) . k) . a <= 0 ) ) )

for s being State of SCM+FSA

for a being read-write Int-Location

for Ig being good really-closed MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ProperBodyWhile>0 a,Ig,s,p & WithVariantWhile>0 a,Ig,s,p holds

ex f being Function of (product (the_Values_of SCM+FSA)),NAT st

( f is on_data_only & ( for k being Nat holds

( f . ((StepWhile>0 (a,Ig,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,Ig,p,s)) . k) or ((StepWhile>0 (a,Ig,p,s)) . k) . a <= 0 ) ) )

proof end;

theorem :: SCMFSA9A:41

for p1, p2 being Instruction-Sequence of SCM+FSA

for s1, s2 being State of SCM+FSA

for a being read-write Int-Location

for Ig being good really-closed MacroInstruction of SCM+FSA st s1 . (intloc 0) = 1 & DataPart s1 = DataPart s2 & ProperBodyWhile>0 a,Ig,s1,p1 & WithVariantWhile>0 a,Ig,s1,p1 holds

WithVariantWhile>0 a,Ig,s2,p2

for s1, s2 being State of SCM+FSA

for a being read-write Int-Location

for Ig being good really-closed MacroInstruction of SCM+FSA st s1 . (intloc 0) = 1 & DataPart s1 = DataPart s2 & ProperBodyWhile>0 a,Ig,s1,p1 & WithVariantWhile>0 a,Ig,s1,p1 holds

WithVariantWhile>0 a,Ig,s2,p2

proof end;

definition

let N, result be Int-Location;

coherence

(((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}))))))))) is MacroInstruction of SCM+FSA ;

;

end;
func Fusc_macro (N,result) -> MacroInstruction of SCM+FSA equals :: SCMFSA9A:def 7

(((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 (((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})))))))));

coherence

(((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}))))))))) is MacroInstruction of SCM+FSA ;

;

:: deftheorem defines Fusc_macro SCMFSA9A:def 7 :

for N, result being Int-Location holds Fusc_macro (N,result) = (((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})))))))));

for N, result being Int-Location holds Fusc_macro (N,result) = (((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})))))))));

:: set next = 1-stRWNotIn {N, result};

:: set aux = 2-ndRWNotIn {N, result};

:: set rem2 = 3-rdRWNotIn {N, result};

:: while and if do not allocate memory, no need to save anything

:: set aux = 2-ndRWNotIn {N, result};

:: set rem2 = 3-rdRWNotIn {N, result};

:: while and if do not allocate memory, no need to save anything

registration
end;

theorem :: SCMFSA9A:42

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for N, result being read-write Int-Location st N <> result holds

for n being Element of NAT st n = s . N holds

( (IExec ((Fusc_macro (N,result)),p,s)) . result = Fusc n & (IExec ((Fusc_macro (N,result)),p,s)) . N = n )

for s being State of SCM+FSA

for N, result being read-write Int-Location st N <> result holds

for n being Element of NAT st n = s . N holds

( (IExec ((Fusc_macro (N,result)),p,s)) . result = Fusc n & (IExec ((Fusc_macro (N,result)),p,s)) . N = n )

proof end;

theorem :: SCMFSA9A:43

for I, J being MacroInstruction of SCM+FSA

for a being Int-Location holds

( UsedILoc (if=0 (a,I,J)) = ({a} \/ (UsedILoc I)) \/ (UsedILoc J) & UsedILoc (if>0 (a,I,J)) = ({a} \/ (UsedILoc I)) \/ (UsedILoc J) )

for a being Int-Location holds

( UsedILoc (if=0 (a,I,J)) = ({a} \/ (UsedILoc I)) \/ (UsedILoc J) & UsedILoc (if>0 (a,I,J)) = ({a} \/ (UsedILoc I)) \/ (UsedILoc J) )

proof end;

theorem :: SCMFSA9A:44

for b being Int-Location

for I being MacroInstruction of SCM+FSA holds UsedILoc (Times (b,I)) = {b,(intloc 0)} \/ (UsedILoc I)

for I being MacroInstruction of SCM+FSA holds UsedILoc (Times (b,I)) = {b,(intloc 0)} \/ (UsedILoc I)

proof end;

theorem :: SCMFSA9A:45

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;

set D = Data-Locations ;

:: registration

:: let I be good Program of SCM+FSA, a be Int-Location;

:: cluster Times(a, I) -> good;

:: coherence;

:: end;

:: let I be good Program of SCM+FSA, a be Int-Location;

:: cluster Times(a, I) -> good;

:: coherence;

:: 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 read-write Int-Location;

coherence

StepWhile>0 (a,(I ";" (SubFrom (a,(intloc 0)))),p,(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 read-write Int-Location;

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

StepWhile>0 (a,(I ";" (SubFrom (a,(intloc 0)))),p,(Initialized s));

correctness StepWhile>0 (a,(I ";" (SubFrom (a,(intloc 0)))),p,(Initialized s));

coherence

StepWhile>0 (a,(I ";" (SubFrom (a,(intloc 0)))),p,(Initialized s)) is sequence of (product (the_Values_of SCM+FSA));

;

:: deftheorem defines StepTimes SCMFSA9A:def 8 :

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 read-write Int-Location holds StepTimes (a,I,p,s) = StepWhile>0 (a,(I ";" (SubFrom (a,(intloc 0)))),p,(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 read-write Int-Location holds StepTimes (a,I,p,s) = StepWhile>0 (a,(I ";" (SubFrom (a,(intloc 0)))),p,(Initialized s));

theorem :: SCMFSA9A:46

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for J being good MacroInstruction of SCM+FSA

for a being read-write Int-Location holds ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1

for p being Instruction-Sequence of SCM+FSA

for J being good MacroInstruction of SCM+FSA

for a being read-write Int-Location holds ((StepTimes (a,J,p,s)) . 0) . (intloc 0) = 1

proof end;

theorem :: SCMFSA9A:47

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for J being good MacroInstruction of SCM+FSA

for a being read-write Int-Location holds ((StepTimes (a,J,p,s)) . 0) . a = s . a

for p being Instruction-Sequence of SCM+FSA

for J being good MacroInstruction of SCM+FSA

for a being read-write Int-Location holds ((StepTimes (a,J,p,s)) . 0) . a = s . a

proof end;

registration

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

let a be Int-Location;

coherence

Times (a,I) is really-closed ;

end;
let a be Int-Location;

coherence

Times (a,I) is really-closed ;

theorem Th48: :: SCMFSA9A:48

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for k being Nat

for a being read-write Int-Location

for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & ((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) . a > 0 implies ((StepTimes (a,J,p,s)) . (k + 1)) . a = (((StepTimes (a,J,p,s)) . k) . a) - 1 ) )

for p being Instruction-Sequence of SCM+FSA

for k being Nat

for a being read-write Int-Location

for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & ((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) . a > 0 implies ((StepTimes (a,J,p,s)) . (k + 1)) . a = (((StepTimes (a,J,p,s)) . k) . a) - 1 ) )

proof end;

theorem :: SCMFSA9A:49

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for f being FinSeq-Location

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location holds ((StepTimes (a,I,p,s)) . 0) . f = s . f

for p being Instruction-Sequence of SCM+FSA

for f being FinSeq-Location

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location 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 read-write Int-Location;

let I be MacroInstruction of SCM+FSA ;

end;
let s be State of SCM+FSA;

let a be read-write Int-Location;

let I be MacroInstruction of SCM+FSA ;

pred ProperTimesBody a,I,s,p means :: SCMFSA9A:def 9

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 SCMFSA9A:def 9 :

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being read-write 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 read-write 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 Th50: :: SCMFSA9A:50

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location st I is parahalting holds

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

for p being Instruction-Sequence of SCM+FSA

for I being MacroInstruction of SCM+FSA

for a being read-write Int-Location st I is parahalting holds

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

theorem Th51: :: SCMFSA9A:51

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being read-write Int-Location

for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & 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 read-write Int-Location

for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & 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 Th52: :: SCMFSA9A:52

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being read-write Int-Location

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

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

(((StepTimes (a,J,p,s)) . k) . a) + k = s . a

for p being Instruction-Sequence of SCM+FSA

for a being read-write Int-Location

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

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

(((StepTimes (a,J,p,s)) . k) . a) + k = s . a

proof end;

theorem Th53: :: SCMFSA9A:53

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being read-write Int-Location

for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & ProperTimesBody a,J,s,p & 0 <= s . a holds

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

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

for p being Instruction-Sequence of SCM+FSA

for a being read-write Int-Location

for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & ProperTimesBody a,J,s,p & 0 <= s . a holds

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

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

proof end;

theorem :: SCMFSA9A:54

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for k being Nat

for a being read-write Int-Location

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

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

for p being Instruction-Sequence of SCM+FSA

for k being Nat

for a being read-write Int-Location

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

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

proof end;

theorem Th55: :: SCMFSA9A:55

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for a being read-write Int-Location

for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & 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 read-write Int-Location

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

Times (a,J) is_halting_on s,p

proof end;

theorem Th56: :: SCMFSA9A:56

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being good really-closed parahalting MacroInstruction of SCM+FSA

for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 holds

Times (a,I) is_halting_on s,P by Th55;

for s being State of SCM+FSA

for I being good really-closed parahalting MacroInstruction of SCM+FSA

for a being read-write Int-Location st not I destroys a & s . (intloc 0) = 1 holds

Times (a,I) is_halting_on s,P by Th55;

theorem :: SCMFSA9A:57

for I being good really-closed parahalting MacroInstruction of SCM+FSA

for a being read-write Int-Location st not I destroys a holds

Initialize ((intloc 0) .--> 1) is Times (a,I) -halted

for a being read-write Int-Location st not I destroys a holds

Initialize ((intloc 0) .--> 1) is Times (a,I) -halted

proof end;

theorem :: SCMFSA9A:58