:: by Piotr Rudnicki

::

:: Received June 3, 1998

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

definition
end;

:: deftheorem Def1 defines good SFMASTR1:def 1 :

for i being Instruction of SCM+FSA holds

( i is good iff Macro i is good );

for i being Instruction of SCM+FSA holds

( i is good iff Macro i is good );

registration

let a be read-write Int-Location;

let b be Int-Location;

coherence

a := b is good by SCMFSA7B:6, SCMFSA8C:70;

coherence

AddTo (a,b) is good by SCMFSA7B:7, SCMFSA8C:70;

coherence

SubFrom (a,b) is good by SCMFSA7B:8, SCMFSA8C:70;

coherence

MultBy (a,b) is good by SCMFSA7B:9, SCMFSA8C:70;

end;
let b be Int-Location;

coherence

a := b is good by SCMFSA7B:6, SCMFSA8C:70;

coherence

AddTo (a,b) is good by SCMFSA7B:7, SCMFSA8C:70;

coherence

SubFrom (a,b) is good by SCMFSA7B:8, SCMFSA8C:70;

coherence

MultBy (a,b) is good by SCMFSA7B:9, SCMFSA8C:70;

registration

ex b_{1} being Instruction of SCM+FSA st

( b_{1} is good & b_{1} is sequential )
end;

cluster with_explicit_jumps IC-relocable sequential good for Element of the InstructionsF of SCM+FSA;

existence ex b

( b

proof end;

registration
end;

registration

let a be Int-Location;

let l be Element of NAT ;

coherence

a =0_goto l is good by SCMFSA7B:12, SCMFSA8C:70;

coherence

a >0_goto l is good by SCMFSA7B:13, SCMFSA8C:70;

end;
let l be Element of NAT ;

coherence

a =0_goto l is good by SCMFSA7B:12, SCMFSA8C:70;

coherence

a >0_goto l is good by SCMFSA7B:13, SCMFSA8C:70;

registration

let a be Int-Location;

let f be FinSeq-Location ;

let b be read-write Int-Location;

coherence

b := (f,a) is good by SCMFSA7B:14, SCMFSA8C:70;

end;
let f be FinSeq-Location ;

let b be read-write Int-Location;

coherence

b := (f,a) is good by SCMFSA7B:14, SCMFSA8C:70;

registration

let f be FinSeq-Location ;

let b be read-write Int-Location;

coherence

b :=len f is good by SCMFSA7B:16, SCMFSA8C:70;

end;
let b be read-write Int-Location;

coherence

b :=len f is good by SCMFSA7B:16, SCMFSA8C:70;

registration

let f be FinSeq-Location ;

let a be Int-Location;

coherence

f :=<0,...,0> a is good by SCMFSA7B:17, SCMFSA8C:70;

let b be Int-Location;

coherence

(f,a) := b is good by SCMFSA7B:15, SCMFSA8C:70;

end;
let a be Int-Location;

coherence

f :=<0,...,0> a is good by SCMFSA7B:17, SCMFSA8C:70;

let b be Int-Location;

coherence

(f,a) := b is good by SCMFSA7B:15, SCMFSA8C:70;

registration
end;

registration
end;

registration

let i be good Instruction of SCM+FSA;

let I be good Program of SCM+FSA;

coherence

i ";" I is good ;

coherence

I ";" i is good ;

end;
let I be good Program of SCM+FSA;

coherence

i ";" I is good ;

coherence

I ";" i is good ;

registration

let I be good MacroInstruction of SCM+FSA ;

let a be read-write Int-Location;

coherence

Times (a,I) is good ;

end;
let a be read-write Int-Location;

coherence

Times (a,I) is good ;

theorem :: SFMASTR1:1

for a being Int-Location

for I being Program of SCM+FSA st not a in UsedILoc I holds

not I destroys a

for I being Program of SCM+FSA st not a in UsedILoc I holds

not I destroys a

proof end;

set D = Data-Locations ;

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

::$CT

theorem Th2: :: SFMASTR1:3

for P being Instruction-Sequence of SCM+FSA

for S being State of SCM+FSA

for I, J being really-closed Program of SCM+FSA st I is_halting_on Initialized S,P & J is_halting_on IExec (I,P,S),P holds

I ";" J is_halting_on Initialized S,P

for S being State of SCM+FSA

for I, J being really-closed Program of SCM+FSA st I is_halting_on Initialized S,P & J is_halting_on IExec (I,P,S),P holds

I ";" J is_halting_on Initialized S,P

proof end;

theorem Th3: :: SFMASTR1:4

for p being Instruction-Sequence of SCM+FSA

for J being Program of SCM+FSA

for I being really-closed Program of SCM+FSA

for s being 0 -started State of SCM+FSA st I c= p & p halts_on s holds

for m being Nat st m <= LifeSpan (p,s) holds

Comput (p,s,m) = Comput ((p +* (I ";" J)),s,m)

for J being Program of SCM+FSA

for I being really-closed Program of SCM+FSA

for s being 0 -started State of SCM+FSA st I c= p & p halts_on s holds

for m being Nat st m <= LifeSpan (p,s) holds

Comput (p,s,m) = Comput ((p +* (I ";" J)),s,m)

proof end;

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

for I being good really-closed Program of SCM+FSA

for J being really-closed Program of SCM+FSA

for s being State of SCM+FSA st s . (intloc 0) = 1 & I is_halting_on s,p & J is_halting_on IExec (I,p,s),p & Initialize ((intloc 0) .--> 1) c= s & I ";" J c= p holds

( IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I & DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = DataPart (Initialized (Comput ((p +* I),s,(LifeSpan ((p +* I),s))))) & Reloc (J,(card I)) c= p & (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) . (intloc 0) = 1 & p halts_on s & LifeSpan (p,s) = ((LifeSpan ((p +* I),s)) + 1) + (LifeSpan (((p +* I) +* J),(Initialized (Result ((p +* I),s))))) & ( J is good implies (Result (p,s)) . (intloc 0) = 1 ) )

proof end;

theorem Th4: :: SFMASTR1:5

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for Ig being good really-closed Program of SCM+FSA

for J being really-closed Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p holds

LifeSpan ((p +* (Ig ";" J)),(Initialized s)) = ((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s))))))

for s being State of SCM+FSA

for Ig being good really-closed Program of SCM+FSA

for J being really-closed Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p holds

LifeSpan ((p +* (Ig ";" J)),(Initialized s)) = ((LifeSpan ((p +* Ig),(Initialized s))) + 1) + (LifeSpan (((p +* Ig) +* J),(Initialized (Result ((p +* Ig),(Initialized s))))))

proof end;

theorem Th5: :: SFMASTR1:6

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for Ig being good really-closed Program of SCM+FSA

for J being really-closed Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p holds

IExec ((Ig ";" J),p,s) = (IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA))

for s being State of SCM+FSA

for Ig being good really-closed Program of SCM+FSA

for J being really-closed Program of SCM+FSA st Ig is_halting_on Initialized s,p & J is_halting_on IExec (Ig,p,s),p holds

IExec ((Ig ";" J),p,s) = (IExec (J,p,(IExec (Ig,p,s)))) +* (Start-At (((IC (IExec (J,p,(IExec (Ig,p,s))))) + (card Ig)),SCM+FSA))

proof end;

theorem Th6: :: SFMASTR1:7

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for a being Int-Location

for Ig being good really-closed Program of SCM+FSA

for J being really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) & ( J is parahalting or J is_halting_on IExec (Ig,p,s),p ) holds

(IExec ((Ig ";" J),p,s)) . a = (IExec (J,p,(IExec (Ig,p,s)))) . a

for s being State of SCM+FSA

for a being Int-Location

for Ig being good really-closed Program of SCM+FSA

for J being really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) & ( J is parahalting or J is_halting_on IExec (Ig,p,s),p ) holds

(IExec ((Ig ";" J),p,s)) . a = (IExec (J,p,(IExec (Ig,p,s)))) . a

proof end;

theorem Th7: :: SFMASTR1:8

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for f being FinSeq-Location

for Ig being good really-closed Program of SCM+FSA

for J being really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) & ( J is parahalting or J is_halting_on IExec (Ig,p,s),p ) holds

(IExec ((Ig ";" J),p,s)) . f = (IExec (J,p,(IExec (Ig,p,s)))) . f

for s being State of SCM+FSA

for f being FinSeq-Location

for Ig being good really-closed Program of SCM+FSA

for J being really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) & ( J is parahalting or J is_halting_on IExec (Ig,p,s),p ) holds

(IExec ((Ig ";" J),p,s)) . f = (IExec (J,p,(IExec (Ig,p,s)))) . f

proof end;

theorem :: SFMASTR1:9

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for Ig being good really-closed Program of SCM+FSA

for J being really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) & ( J is parahalting or J is_halting_on IExec (Ig,p,s),p ) holds

DataPart (IExec ((Ig ";" J),p,s)) = DataPart (IExec (J,p,(IExec (Ig,p,s))))

for s being State of SCM+FSA

for Ig being good really-closed Program of SCM+FSA

for J being really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) & ( J is parahalting or J is_halting_on IExec (Ig,p,s),p ) holds

DataPart (IExec ((Ig ";" J),p,s)) = DataPart (IExec (J,p,(IExec (Ig,p,s))))

proof end;

theorem Th9: :: SFMASTR1:10

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for Ig being good really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) holds

DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s))

for s being State of SCM+FSA

for Ig being good really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) holds

DataPart (Initialized (IExec (Ig,p,s))) = DataPart (IExec (Ig,p,s))

proof end;

theorem Th10: :: SFMASTR1:11

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for j being sequential Instruction of SCM+FSA

for a being Int-Location

for Ig being good really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) holds

(IExec ((Ig ";" j),p,s)) . a = (Exec (j,(IExec (Ig,p,s)))) . a

for s being State of SCM+FSA

for j being sequential Instruction of SCM+FSA

for a being Int-Location

for Ig being good really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) holds

(IExec ((Ig ";" j),p,s)) . a = (Exec (j,(IExec (Ig,p,s)))) . a

proof end;

theorem Th11: :: SFMASTR1:12

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for j being sequential Instruction of SCM+FSA

for f being FinSeq-Location

for Ig being good really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) holds

(IExec ((Ig ";" j),p,s)) . f = (Exec (j,(IExec (Ig,p,s)))) . f

for s being State of SCM+FSA

for j being sequential Instruction of SCM+FSA

for f being FinSeq-Location

for Ig being good really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) holds

(IExec ((Ig ";" j),p,s)) . f = (Exec (j,(IExec (Ig,p,s)))) . f

proof end;

theorem :: SFMASTR1:13

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for j being sequential Instruction of SCM+FSA

for Ig being good really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) holds

DataPart (IExec ((Ig ";" j),p,s)) = DataPart (Exec (j,(IExec (Ig,p,s))))

for s being State of SCM+FSA

for j being sequential Instruction of SCM+FSA

for Ig being good really-closed Program of SCM+FSA st ( Ig is parahalting or Ig is_halting_on Initialized s,p ) holds

DataPart (IExec ((Ig ";" j),p,s)) = DataPart (Exec (j,(IExec (Ig,p,s))))

proof end;

theorem Th13: :: SFMASTR1:14

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for i being sequential good Instruction of SCM+FSA

for a being Int-Location

for J being really-closed Program of SCM+FSA st ( J is parahalting or J is_halting_on Exec (i,(Initialized s)),p ) holds

(IExec ((i ";" J),p,s)) . a = (IExec (J,p,(Exec (i,(Initialized s))))) . a

for s being State of SCM+FSA

for i being sequential good Instruction of SCM+FSA

for a being Int-Location

for J being really-closed Program of SCM+FSA st ( J is parahalting or J is_halting_on Exec (i,(Initialized s)),p ) holds

(IExec ((i ";" J),p,s)) . a = (IExec (J,p,(Exec (i,(Initialized s))))) . a

proof end;

theorem Th14: :: SFMASTR1:15

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for i being sequential good Instruction of SCM+FSA

for f being FinSeq-Location

for J being really-closed Program of SCM+FSA st ( J is parahalting or J is_halting_on Exec (i,(Initialized s)),p ) holds

(IExec ((i ";" J),p,s)) . f = (IExec (J,p,(Exec (i,(Initialized s))))) . f

for s being State of SCM+FSA

for i being sequential good Instruction of SCM+FSA

for f being FinSeq-Location

for J being really-closed Program of SCM+FSA st ( J is parahalting or J is_halting_on Exec (i,(Initialized s)),p ) holds

(IExec ((i ";" J),p,s)) . f = (IExec (J,p,(Exec (i,(Initialized s))))) . f

proof end;

theorem :: SFMASTR1:16

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for i being sequential good Instruction of SCM+FSA

for J being really-closed Program of SCM+FSA st ( J is parahalting or J is_halting_on Exec (i,(Initialized s)),p ) holds

DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s)))))

for s being State of SCM+FSA

for i being sequential good Instruction of SCM+FSA

for J being really-closed Program of SCM+FSA st ( J is parahalting or J is_halting_on Exec (i,(Initialized s)),p ) holds

DataPart (IExec ((i ";" J),p,s)) = DataPart (IExec (J,p,(Exec (i,(Initialized s)))))

proof end;

definition

let n be Element of NAT ;

let p be preProgram of SCM+FSA;

correctness

coherence

n -thRWNotIn (UsedILoc p) is Int-Location;

;

end;
let p be preProgram of SCM+FSA;

correctness

coherence

n -thRWNotIn (UsedILoc p) is Int-Location;

;

:: deftheorem defines -thNotUsed SFMASTR1:def 4 :

for n being Element of NAT

for p being preProgram of SCM+FSA holds n -thNotUsed p = n -thRWNotIn (UsedILoc p);

for n being Element of NAT

for p being preProgram of SCM+FSA holds n -thNotUsed p = n -thRWNotIn (UsedILoc p);

notation

let n be Element of NAT ;

let p be preProgram of SCM+FSA;

synonym n -stNotUsed p for n -thNotUsed p;

synonym n -ndNotUsed p for n -thNotUsed p;

synonym n -rdNotUsed p for n -thNotUsed p;

end;
let p be preProgram of SCM+FSA;

synonym n -stNotUsed p for n -thNotUsed p;

synonym n -ndNotUsed p for n -thNotUsed p;

synonym n -rdNotUsed p for n -thNotUsed p;

registration

let n be Element of NAT ;

let p be preProgram of SCM+FSA;

coherence

not n -thNotUsed p is read-only ;

end;
let p be preProgram of SCM+FSA;

coherence

not n -thNotUsed p is read-only ;