:: by JingChao Chen and Yatsuka Nakamura

::

:: Received June 17, 1998

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

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

set iS = Initialize ((intloc 0) .--> 1);

reconsider EP = {} as PartState of SCM+FSA by FUNCT_1:104, RELAT_1:171;

Lm1: IC (Initialize ((intloc 0) .--> 1)) = 0

by MEMSTR_0:def 11;

Lm2: dom (Initialize ((intloc 0) .--> 1)) = (dom ((intloc 0) .--> 1)) \/ (dom (Start-At (0,SCM+FSA))) by FUNCT_4:def 1

.= {(intloc 0)} \/ (dom (Start-At (0,SCM+FSA))) by FUNCOP_1:13

.= {(intloc 0)} \/ {(IC )} by FUNCOP_1:13 ;

canceled;

::$CD

definition

let I be Program of SCM+FSA;

end;
attr I is InitHalting means :Def1: :: SCM_HALT:def 1

for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds

for P being Instruction-Sequence of SCM+FSA st I c= P holds

P halts_on s;

for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds

for P being Instruction-Sequence of SCM+FSA st I c= P holds

P halts_on s;

attr I is keepInt0_1 means :Def2: :: SCM_HALT:def 2

for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds

for p being Instruction-Sequence of SCM+FSA st I c= p holds

for k being Nat holds (Comput (p,s,k)) . (intloc 0) = 1;

for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds

for p being Instruction-Sequence of SCM+FSA st I c= p holds

for k being Nat holds (Comput (p,s,k)) . (intloc 0) = 1;

:: deftheorem Def1 defines InitHalting SCM_HALT:def 1 :

for I being Program of SCM+FSA holds

( I is InitHalting iff for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds

for P being Instruction-Sequence of SCM+FSA st I c= P holds

P halts_on s );

for I being Program of SCM+FSA holds

( I is InitHalting iff for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds

for P being Instruction-Sequence of SCM+FSA st I c= P holds

P halts_on s );

:: deftheorem Def2 defines keepInt0_1 SCM_HALT:def 2 :

for I being Program of SCM+FSA holds

( I is keepInt0_1 iff for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds

for p being Instruction-Sequence of SCM+FSA st I c= p holds

for k being Nat holds (Comput (p,s,k)) . (intloc 0) = 1 );

for I being Program of SCM+FSA holds

( I is keepInt0_1 iff for s being State of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s holds

for p being Instruction-Sequence of SCM+FSA st I c= p holds

for k being Nat holds (Comput (p,s,k)) . (intloc 0) = 1 );

::$CT

registration

ex b_{1} being Program of SCM+FSA st b_{1} is InitHalting
by Th1;

end;

cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V34() V63() V73() V167() InitHalting for set ;

existence ex b

registration

for b_{1} being Program of SCM+FSA st b_{1} is parahalting holds

b_{1} is InitHalting
end;

cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V34() V73() parahalting -> InitHalting for set ;

coherence for b

b

proof end;

registration

for b_{1} being Program of SCM+FSA st b_{1} is keeping_0 holds

b_{1} is keepInt0_1
end;

cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V34() V73() keeping_0 -> keepInt0_1 for set ;

coherence for b

b

proof end;

::$CT

theorem :: SCM_HALT:4

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

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

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

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

for p being Instruction-Sequence of SCM+FSA

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

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

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

proof end;

theorem :: SCM_HALT:5

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

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

for f being FinSeq-Location st not f in UsedI*Loc I holds

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

for p being Instruction-Sequence of SCM+FSA

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

for f being FinSeq-Location st not f in UsedI*Loc I holds

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

proof end;

registration

for b_{1} being Program of SCM+FSA st b_{1} is InitHalting holds

not b_{1} is empty
;

end;

cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V34() V73() InitHalting -> for set ;

coherence for b

not b

theorem Th4: :: SCM_HALT:6

for s1, s2 being State of SCM+FSA

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

for J being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & J c= p1 holds

for n being Nat st Reloc (J,n) c= p2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Nat holds

( (IC (Comput (p1,s1,i))) + n = IC (Comput (p2,s2,i)) & IncAddr ((CurInstr (p1,(Comput (p1,s1,i)))),n) = CurInstr (p2,(Comput (p2,s2,i))) & DataPart (Comput (p1,s1,i)) = DataPart (Comput (p2,s2,i)) )

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

for J being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & J c= p1 holds

for n being Nat st Reloc (J,n) c= p2 & IC s2 = n & DataPart s1 = DataPart s2 holds

for i being Nat holds

( (IC (Comput (p1,s1,i))) + n = IC (Comput (p2,s2,i)) & IncAddr ((CurInstr (p1,(Comput (p1,s1,i)))),n) = CurInstr (p2,(Comput (p2,s2,i))) & DataPart (Comput (p1,s1,i)) = DataPart (Comput (p2,s2,i)) )

proof end;

theorem Th5: :: SCM_HALT:7

for s1, s2 being State of SCM+FSA

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

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & Initialize ((intloc 0) .--> 1) c= s2 & I c= p1 & I c= p2 & s1 = s2 holds

for k being Nat holds

( Comput (p1,s1,k) = Comput (p2,s2,k) & CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k))) )

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

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & Initialize ((intloc 0) .--> 1) c= s2 & I c= p1 & I c= p2 & s1 = s2 holds

for k being Nat holds

( Comput (p1,s1,k) = Comput (p2,s2,k) & CurInstr (p1,(Comput (p1,s1,k))) = CurInstr (p2,(Comput (p2,s2,k))) )

proof end;

theorem Th6: :: SCM_HALT:8

for s1, s2 being State of SCM+FSA

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

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & Initialize ((intloc 0) .--> 1) c= s2 & I c= p1 & I c= p2 & s1 = s2 holds

( LifeSpan (p1,s1) = LifeSpan (p2,s2) & Result (p1,s1) = Result (p2,s2) )

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

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s1 & Initialize ((intloc 0) .--> 1) c= s2 & I c= p1 & I c= p2 & s1 = s2 holds

( LifeSpan (p1,s1) = LifeSpan (p2,s2) & Result (p1,s1) = Result (p2,s2) )

proof end;

registration

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

( b_{1} is keeping_0 & b_{1} is InitHalting )
end;

cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V34() V63() V73() keeping_0 V167() InitHalting for set ;

existence ex b

( b

proof end;

registration

ex b_{1} being really-closed Program of SCM+FSA st

( b_{1} is keepInt0_1 & b_{1} is InitHalting )
end;

cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V34() V63() V73() really-closed V167() InitHalting keepInt0_1 for set ;

existence ex b

( b

proof end;

theorem Th7: :: SCM_HALT:9

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for I being InitHalting keepInt0_1 Program of SCM+FSA holds (IExec (I,p,s)) . (intloc 0) = 1

for p being Instruction-Sequence of SCM+FSA

for I being InitHalting keepInt0_1 Program of SCM+FSA holds (IExec (I,p,s)) . (intloc 0) = 1

proof end;

theorem Th8: :: SCM_HALT:10

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for I being really-closed Program of SCM+FSA

for J being Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & 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 p being Instruction-Sequence of SCM+FSA

for I being really-closed Program of SCM+FSA

for J being Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & 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;

theorem Th9: :: SCM_HALT:11

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for I being really-closed Program of SCM+FSA st p +* I halts_on s & Directed I c= p & Initialize ((intloc 0) .--> 1) c= s holds

IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I

for p being Instruction-Sequence of SCM+FSA

for I being really-closed Program of SCM+FSA st p +* I halts_on s & Directed I c= p & Initialize ((intloc 0) .--> 1) c= s holds

IC (Comput (p,s,((LifeSpan ((p +* I),s)) + 1))) = card I

proof end;

theorem Th10: :: SCM_HALT:12

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for I being really-closed Program of SCM+FSA st p +* I halts_on s & Directed I c= p & Initialize ((intloc 0) .--> 1) c= s holds

DataPart (Comput (p,s,(LifeSpan ((p +* I),s)))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1)))

for p being Instruction-Sequence of SCM+FSA

for I being really-closed Program of SCM+FSA st p +* I halts_on s & Directed I c= p & Initialize ((intloc 0) .--> 1) c= s holds

DataPart (Comput (p,s,(LifeSpan ((p +* I),s)))) = DataPart (Comput (p,s,((LifeSpan ((p +* I),s)) + 1)))

proof end;

theorem Th11: :: SCM_HALT:13

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= p holds

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

CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) <> halt SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= p holds

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

CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),s,k))) <> halt SCM+FSA

proof end;

theorem Th12: :: SCM_HALT:14

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for I being really-closed Program of SCM+FSA st p +* I halts_on Initialized s holds

for J being Program of SCM+FSA

for k being Nat st k <= LifeSpan ((p +* I),(Initialized s)) holds

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

for p being Instruction-Sequence of SCM+FSA

for I being really-closed Program of SCM+FSA st p +* I halts_on Initialized s holds

for J being Program of SCM+FSA

for k being Nat st k <= LifeSpan ((p +* I),(Initialized s)) holds

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

proof end;

theorem Th13: :: SCM_HALT:15

for p being Instruction-Sequence of SCM+FSA

for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA

for J being really-closed InitHalting Program of SCM+FSA

for s being State of SCM+FSA st 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 ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) & 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),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (p,s)) . (intloc 0) = 1 ) )

for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA

for J being really-closed InitHalting Program of SCM+FSA

for s being State of SCM+FSA st 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 ((Comput ((p +* I),s,(LifeSpan ((p +* I),s)))) +* (Initialize ((intloc 0) .--> 1))) & 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),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))))) & ( J is keeping_0 implies (Result (p,s)) . (intloc 0) = 1 ) )

proof end;

registration

let I be really-closed InitHalting keepInt0_1 Program of SCM+FSA;

let J be really-closed InitHalting Program of SCM+FSA;

coherence

I ";" J is InitHalting

end;
let J be really-closed InitHalting Program of SCM+FSA;

coherence

I ";" J is InitHalting

proof end;

theorem Th14: :: SCM_HALT:16

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for I being really-closed keepInt0_1 Program of SCM+FSA st p +* I halts_on s holds

for J being really-closed Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I ";" J c= p holds

for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k))) + (card I)),SCM+FSA)) = Comput ((p +* (I ";" J)),s,(((LifeSpan ((p +* I),s)) + 1) + k))

for p being Instruction-Sequence of SCM+FSA

for I being really-closed keepInt0_1 Program of SCM+FSA st p +* I halts_on s holds

for J being really-closed Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I ";" J c= p holds

for k being Element of NAT holds (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k)) +* (Start-At (((IC (Comput (((p +* I) +* J),((Result ((p +* I),s)) +* (Initialize ((intloc 0) .--> 1))),k))) + (card I)),SCM+FSA)) = Comput ((p +* (I ";" J)),s,(((LifeSpan ((p +* I),s)) + 1) + k))

proof end;

theorem Th15: :: SCM_HALT:17

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for I being really-closed keepInt0_1 Program of SCM+FSA st not p +* I halts_on Initialized s holds

for J being Program of SCM+FSA

for k being Nat holds Comput ((p +* I),(Initialized s),k) = Comput ((p +* (I ";" J)),(Initialized s),k)

for p being Instruction-Sequence of SCM+FSA

for I being really-closed keepInt0_1 Program of SCM+FSA st not p +* I halts_on Initialized s holds

for J being Program of SCM+FSA

for k being Nat holds Comput ((p +* I),(Initialized s),k) = Comput ((p +* (I ";" J)),(Initialized s),k)

proof end;

theorem Th16: :: SCM_HALT:18

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA

for J being really-closed InitHalting Program of SCM+FSA holds LifeSpan ((p +* (I ";" J)),(Initialized s)) = ((LifeSpan ((p +* I),(Initialized s))) + 1) + (LifeSpan (((p +* I) +* J),((Result ((p +* I),(Initialized s))) +* (Initialize ((intloc 0) .--> 1)))))

for p being Instruction-Sequence of SCM+FSA

for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA

for J being really-closed InitHalting Program of SCM+FSA holds LifeSpan ((p +* (I ";" J)),(Initialized s)) = ((LifeSpan ((p +* I),(Initialized s))) + 1) + (LifeSpan (((p +* I) +* J),((Result ((p +* I),(Initialized s))) +* (Initialize ((intloc 0) .--> 1)))))

proof end;

theorem Th17: :: SCM_HALT:19

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA

for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA

for J being really-closed InitHalting Program of SCM+FSA holds IExec ((I ";" J),p,s) = IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))

for p being Instruction-Sequence of SCM+FSA

for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA

for J being really-closed InitHalting Program of SCM+FSA holds IExec ((I ";" J),p,s) = IncIC ((IExec (J,p,(IExec (I,p,s)))),(card I))

proof end;

registration

let i be sequential Instruction of SCM+FSA;

let J be really-closed parahalting Program of SCM+FSA;

coherence

i ";" J is InitHalting ;

end;
let J be really-closed parahalting Program of SCM+FSA;

coherence

i ";" J is InitHalting ;

registration

let i be keeping_0 sequential Instruction of SCM+FSA;

let J be really-closed InitHalting Program of SCM+FSA;

coherence

i ";" J is InitHalting ;

end;
let J be really-closed InitHalting Program of SCM+FSA;

coherence

i ";" J is InitHalting ;

registration
end;

registration

let j be keeping_0 sequential Instruction of SCM+FSA;

let I be really-closed InitHalting keepInt0_1 Program of SCM+FSA;

coherence

( I ";" j is InitHalting & I ";" j is keepInt0_1 ) ;

end;
let I be really-closed InitHalting keepInt0_1 Program of SCM+FSA;

coherence

( I ";" j is InitHalting & I ";" j is keepInt0_1 ) ;

registration

let i be keeping_0 sequential Instruction of SCM+FSA;

let J be really-closed InitHalting keepInt0_1 Program of SCM+FSA;

coherence

( i ";" J is InitHalting & i ";" J is keepInt0_1 ) ;

end;
let J be really-closed InitHalting keepInt0_1 Program of SCM+FSA;

coherence

( i ";" J is InitHalting & i ";" J is keepInt0_1 ) ;

registration

let j be sequential Instruction of SCM+FSA;

let I be really-closed parahalting Program of SCM+FSA;

coherence

I ";" j is InitHalting ;

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

coherence

I ";" j is InitHalting ;

theorem Th18: :: SCM_HALT:20

for s being State of SCM+FSA

for a being Int-Location

for p being Instruction-Sequence of SCM+FSA

for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA

for J being really-closed InitHalting Program of SCM+FSA holds (IExec ((I ";" J),p,s)) . a = (IExec (J,p,(IExec (I,p,s)))) . a

for a being Int-Location

for p being Instruction-Sequence of SCM+FSA

for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA

for J being really-closed InitHalting Program of SCM+FSA holds (IExec ((I ";" J),p,s)) . a = (IExec (J,p,(IExec (I,p,s)))) . a

proof end;

theorem Th19: :: SCM_HALT:21

for s being State of SCM+FSA

for f being FinSeq-Location

for p being Instruction-Sequence of SCM+FSA

for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA

for J being really-closed InitHalting Program of SCM+FSA holds (IExec ((I ";" J),p,s)) . f = (IExec (J,p,(IExec (I,p,s)))) . f

for f being FinSeq-Location

for p being Instruction-Sequence of SCM+FSA

for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA

for J being really-closed InitHalting Program of SCM+FSA holds (IExec ((I ";" J),p,s)) . f = (IExec (J,p,(IExec (I,p,s)))) . f

proof end;

theorem Th20: :: SCM_HALT:22

for p being Instruction-Sequence of SCM+FSA

for I being InitHalting keepInt0_1 Program of SCM+FSA

for s being State of SCM+FSA holds DataPart (Initialized (IExec (I,p,s))) = DataPart (IExec (I,p,s))

for I being InitHalting keepInt0_1 Program of SCM+FSA

for s being State of SCM+FSA holds DataPart (Initialized (IExec (I,p,s))) = DataPart (IExec (I,p,s))

proof end;

theorem Th21: :: SCM_HALT:23

for s being State of SCM+FSA

for a being Int-Location

for p being Instruction-Sequence of SCM+FSA

for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA

for j being sequential Instruction of SCM+FSA holds (IExec ((I ";" j),p,s)) . a = (Exec (j,(IExec (I,p,s)))) . a

for a being Int-Location

for p being Instruction-Sequence of SCM+FSA

for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA

for j being sequential Instruction of SCM+FSA holds (IExec ((I ";" j),p,s)) . a = (Exec (j,(IExec (I,p,s)))) . a

proof end;

theorem :: SCM_HALT:24

for s being State of SCM+FSA

for f being FinSeq-Location

for p being Instruction-Sequence of SCM+FSA

for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA

for j being sequential Instruction of SCM+FSA holds (IExec ((I ";" j),p,s)) . f = (Exec (j,(IExec (I,p,s)))) . f

for f being FinSeq-Location

for p being Instruction-Sequence of SCM+FSA

for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA

for j being sequential Instruction of SCM+FSA holds (IExec ((I ";" j),p,s)) . f = (Exec (j,(IExec (I,p,s)))) . f

proof end;

definition
end;

:: deftheorem defines is_halting_onInit SCM_HALT:def 3 :

for I being Program of SCM+FSA

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA holds

( I is_halting_onInit s,p iff p +* I halts_on Initialized s );

for I being Program of SCM+FSA

for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA holds

( I is_halting_onInit s,p iff p +* I halts_on Initialized s );

canceled;

::$CD

::$CT

::$CT

theorem Th23: :: SCM_HALT:26

for I being Program of SCM+FSA holds

( I is InitHalting iff for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA holds I is_halting_onInit s,p )

( I is InitHalting iff for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA holds I is_halting_onInit s,p )

proof end;

theorem Th24: :: SCM_HALT:27

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being really-closed Program of SCM+FSA

for a being Int-Location st not I destroys a & Initialize ((intloc 0) .--> 1) c= s & I c= p holds

for k being Nat holds (Comput (p,s,k)) . a = s . a

for s being State of SCM+FSA

for I being really-closed Program of SCM+FSA

for a being Int-Location st not I destroys a & Initialize ((intloc 0) .--> 1) c= s & I c= p holds

for k being Nat holds (Comput (p,s,k)) . a = s . a

proof end;

registration

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

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

cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V34() V63() V73() good V167() InitHalting for set ;

existence ex b

( b

proof end;

registration

coherence

for b_{1} being Program of SCM+FSA st b_{1} is really-closed & b_{1} is good holds

b_{1} is keepInt0_1 ;

end;

cluster non empty Relation-like NAT -defined the InstructionsF of SCM+FSA -valued Function-like V34() V73() really-closed good -> keepInt0_1 for set ;

correctness coherence

for b

b

proof end;

theorem :: SCM_HALT:28

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for i being keeping_0 sequential Instruction of SCM+FSA

for J being really-closed InitHalting Program of SCM+FSA

for a being Int-Location 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 keeping_0 sequential Instruction of SCM+FSA

for J being really-closed InitHalting Program of SCM+FSA

for a being Int-Location holds (IExec ((i ";" J),p,s)) . a = (IExec (J,p,(Exec (i,(Initialized s))))) . a

proof end;

theorem :: SCM_HALT:29

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for i being keeping_0 sequential Instruction of SCM+FSA

for J being really-closed InitHalting Program of SCM+FSA

for f being FinSeq-Location 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 keeping_0 sequential Instruction of SCM+FSA

for J being really-closed InitHalting Program of SCM+FSA

for f being FinSeq-Location holds (IExec ((i ";" J),p,s)) . f = (IExec (J,p,(Exec (i,(Initialized s))))) . f

proof end;

::$CT

theorem Th27: :: SCM_HALT:31

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being Program of SCM+FSA holds

( I is_halting_onInit s,p iff I is_halting_on Initialized s,p ) by MEMSTR_0:44;

for s being State of SCM+FSA

for I being Program of SCM+FSA holds

( I is_halting_onInit s,p iff I is_halting_on Initialized s,p ) by MEMSTR_0:44;

theorem :: SCM_HALT:32

for p being Instruction-Sequence of SCM+FSA

for I being Program of SCM+FSA

for s being State of SCM+FSA holds IExec (I,p,s) = IExec (I,p,(Initialized s))

for I being Program of SCM+FSA

for s being State of SCM+FSA holds IExec (I,p,s) = IExec (I,p,(Initialized s))

proof end;

theorem Th29: :: SCM_HALT:33

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being really-closed MacroInstruction of SCM+FSA

for J being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a = 0 & I is_halting_onInit s,p holds

if=0 (a,I,J) is_halting_onInit s,p

for s being State of SCM+FSA

for I being really-closed MacroInstruction of SCM+FSA

for J being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a = 0 & I is_halting_onInit s,p holds

if=0 (a,I,J) is_halting_onInit s,p

proof end;

theorem Th30: :: SCM_HALT:34

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being really-closed MacroInstruction of SCM+FSA

for J being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a = 0 & I is_halting_onInit s,p holds

IExec ((if=0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

for s being State of SCM+FSA

for I being really-closed MacroInstruction of SCM+FSA

for J being MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a = 0 & I is_halting_onInit s,p holds

IExec ((if=0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

proof end;

theorem Th31: :: SCM_HALT:35

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a <> 0 & J is_halting_onInit s,p holds

if=0 (a,I,J) is_halting_onInit s,p

for s being State of SCM+FSA

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a <> 0 & J is_halting_onInit s,p holds

if=0 (a,I,J) is_halting_onInit s,p

proof end;

theorem Th32: :: SCM_HALT:36

for p being Instruction-Sequence of SCM+FSA

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location

for s being State of SCM+FSA st s . a <> 0 & J is_halting_onInit s,p holds

IExec ((if=0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location

for s being State of SCM+FSA st s . a <> 0 & J is_halting_onInit s,p holds

IExec ((if=0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

proof end;

theorem Th33: :: SCM_HALT:37

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being really-closed InitHalting MacroInstruction of SCM+FSA

for a being read-write Int-Location holds

( if=0 (a,I,J) is InitHalting & ( s . a = 0 implies IExec ((if=0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <> 0 implies IExec ((if=0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )

for s being State of SCM+FSA

for I, J being really-closed InitHalting MacroInstruction of SCM+FSA

for a being read-write Int-Location holds

( if=0 (a,I,J) is InitHalting & ( s . a = 0 implies IExec ((if=0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <> 0 implies IExec ((if=0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )

proof end;

theorem :: SCM_HALT:38

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being really-closed InitHalting MacroInstruction of SCM+FSA

for a being read-write Int-Location holds

( IC (IExec ((if=0 (a,I,J)),p,s)) = ((card I) + (card J)) + 3 & ( s . a = 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (I,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (I,p,s)) . f ) ) ) & ( s . a <> 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (J,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (J,p,s)) . f ) ) ) )

for s being State of SCM+FSA

for I, J being really-closed InitHalting MacroInstruction of SCM+FSA

for a being read-write Int-Location holds

( IC (IExec ((if=0 (a,I,J)),p,s)) = ((card I) + (card J)) + 3 & ( s . a = 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (I,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (I,p,s)) . f ) ) ) & ( s . a <> 0 implies ( ( for d being Int-Location holds (IExec ((if=0 (a,I,J)),p,s)) . d = (IExec (J,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if=0 (a,I,J)),p,s)) . f = (IExec (J,p,s)) . f ) ) ) )

proof end;

theorem Th35: :: SCM_HALT:39

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a > 0 & I is_halting_onInit s,p holds

if>0 (a,I,J) is_halting_onInit s,p

for s being State of SCM+FSA

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a > 0 & I is_halting_onInit s,p holds

if>0 (a,I,J) is_halting_onInit s,p

proof end;

theorem Th36: :: SCM_HALT:40

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a > 0 & I is_halting_onInit s,p holds

IExec ((if>0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

for s being State of SCM+FSA

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a > 0 & I is_halting_onInit s,p holds

IExec ((if>0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

proof end;

theorem Th37: :: SCM_HALT:41

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a <= 0 & J is_halting_onInit s,p holds

if>0 (a,I,J) is_halting_onInit s,p

for s being State of SCM+FSA

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st s . a <= 0 & J is_halting_onInit s,p holds

if>0 (a,I,J) is_halting_onInit s,p

proof end;

theorem Th38: :: SCM_HALT:42

for p being Instruction-Sequence of SCM+FSA

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location

for s being State of SCM+FSA st s . a <= 0 & J is_halting_onInit s,p holds

IExec ((if>0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

for I, J being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location

for s being State of SCM+FSA st s . a <= 0 & J is_halting_onInit s,p holds

IExec ((if>0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))

proof end;

theorem Th39: :: SCM_HALT:43

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being really-closed InitHalting MacroInstruction of SCM+FSA

for a being read-write Int-Location holds

( if>0 (a,I,J) is InitHalting & ( s . a > 0 implies IExec ((if>0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <= 0 implies IExec ((if>0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )

for s being State of SCM+FSA

for I, J being really-closed InitHalting MacroInstruction of SCM+FSA

for a being read-write Int-Location holds

( if>0 (a,I,J) is InitHalting & ( s . a > 0 implies IExec ((if>0 (a,I,J)),p,s) = (IExec (I,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) & ( s . a <= 0 implies IExec ((if>0 (a,I,J)),p,s) = (IExec (J,p,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA)) ) )

proof end;

theorem :: SCM_HALT:44

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I, J being really-closed InitHalting MacroInstruction of SCM+FSA

for a being read-write Int-Location holds

( IC (IExec ((if>0 (a,I,J)),p,s)) = ((card I) + (card J)) + 3 & ( s . a > 0 implies ( ( for d being Int-Location holds (IExec ((if>0 (a,I,J)),p,s)) . d = (IExec (I,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if>0 (a,I,J)),p,s)) . f = (IExec (I,p,s)) . f ) ) ) & ( s . a <= 0 implies ( ( for d being Int-Location holds (IExec ((if>0 (a,I,J)),p,s)) . d = (IExec (J,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if>0 (a,I,J)),p,s)) . f = (IExec (J,p,s)) . f ) ) ) )

for s being State of SCM+FSA

for I, J being really-closed InitHalting MacroInstruction of SCM+FSA

for a being read-write Int-Location holds

( IC (IExec ((if>0 (a,I,J)),p,s)) = ((card I) + (card J)) + 3 & ( s . a > 0 implies ( ( for d being Int-Location holds (IExec ((if>0 (a,I,J)),p,s)) . d = (IExec (I,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if>0 (a,I,J)),p,s)) . f = (IExec (I,p,s)) . f ) ) ) & ( s . a <= 0 implies ( ( for d being Int-Location holds (IExec ((if>0 (a,I,J)),p,s)) . d = (IExec (J,p,s)) . d ) & ( for f being FinSeq-Location holds (IExec ((if>0 (a,I,J)),p,s)) . f = (IExec (J,p,s)) . f ) ) ) )

proof end;

::$CT 4

registration

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

let a be read-write Int-Location;

correctness

coherence

if=0 (a,I,J) is InitHalting ;

by Th33;

correctness

coherence

if>0 (a,I,J) is InitHalting ;

by Th39;

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

correctness

coherence

if=0 (a,I,J) is InitHalting ;

by Th33;

correctness

coherence

if>0 (a,I,J) is InitHalting ;

by Th39;

theorem Th41: :: SCM_HALT:49

for I being Program of SCM+FSA holds

( I is InitHalting iff for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA holds I is_halting_on Initialized s,p )

( I is InitHalting iff for s being State of SCM+FSA

for p being Instruction-Sequence of SCM+FSA holds I is_halting_on Initialized s,p )

proof end;

::$CT

theorem Th42: :: SCM_HALT:51

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being InitHalting Program of SCM+FSA

for a being read-write Int-Location holds (IExec (I,p,s)) . a = (Comput ((p +* I),(Initialize (Initialized s)),(LifeSpan ((p +* I),(Initialize (Initialized s)))))) . a

for s being State of SCM+FSA

for I being InitHalting Program of SCM+FSA

for a being read-write Int-Location holds (IExec (I,p,s)) . a = (Comput ((p +* I),(Initialize (Initialized s)),(LifeSpan ((p +* I),(Initialize (Initialized s)))))) . a

proof end;

theorem Th43: :: SCM_HALT:52

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

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

for a being Int-Location

for k being Element of NAT st not I destroys a holds

(IExec (I,p,s)) . a = (Comput ((p +* I),(Initialize (Initialized s)),k)) . a

for s being State of SCM+FSA

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

for a being Int-Location

for k being Element of NAT st not I destroys a holds

(IExec (I,p,s)) . a = (Comput ((p +* I),(Initialize (Initialized s)),k)) . a

proof end;

set A = NAT ;

set D = Data-Locations ;

theorem Th44: :: SCM_HALT:53

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

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

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

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

for s being State of SCM+FSA

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

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

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

proof end;

theorem :: SCM_HALT:54

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA

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

(Comput ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)),(LifeSpan ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)))))) . a = (s . a) - 1

for s being State of SCM+FSA

for I being really-closed InitHalting keepInt0_1 Program of SCM+FSA

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

(Comput ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)),(LifeSpan ((p +* (I ";" (SubFrom (a,(intloc 0))))),(Initialize (Initialized s)))))) . a = (s . a) - 1

proof end;

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

for s being 0 -started State of SCM+FSA

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

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

for k being Nat holds

( ((StepTimes (a,I,p,s)) . k) . (intloc 0) = 1 & I is_halting_on (StepTimes (a,I,p,s)) . k,p +* (Times (a,I)) )

proof end;

::$CT 7

theorem :: SCM_HALT:62

for p being Instruction-Sequence of SCM+FSA

for s being 0 -started State of SCM+FSA

for I being really-closed good InitHalting 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

for s being 0 -started State of SCM+FSA

for I being really-closed good InitHalting 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

proof end;

registration

let a be read-write Int-Location;

let I be good MacroInstruction of SCM+FSA ;

coherence

Times (a,I) is good ;

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

coherence

Times (a,I) is good ;

::$CT 2

theorem Th47: :: SCM_HALT:65

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

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

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

DataPart (IExec ((Times (a,I)),p,s)) = DataPart s by SCMFSA9A:58;

for s being State of SCM+FSA

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

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

DataPart (IExec ((Times (a,I)),p,s)) = DataPart s by SCMFSA9A:58;

Lm4: for P1, P2 being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 holds

for k being Nat holds

( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) )

proof end;

Lm5: for P1, P2 being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 holds

( LifeSpan (P1,s) = LifeSpan (P2,s) & Result (P1,s) = Result (P2,s) )

proof end;

Lm6: for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being really-closed MacroInstruction of SCM+FSA

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

while>0 (a,I) is_halting_onInit s,P

proof end;

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

for s being State of SCM+FSA

for I being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st I is_halting_onInit s,P & s . a > 0 holds

( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) )

proof end;

Lm8: for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

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

for a being read-write Int-Location st s . a > 0 & while>0 (a,I) is InitHalting holds

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

proof end;

Lm9: for I being really-closed good InitHalting MacroInstruction of SCM+FSA

for a being read-write Int-Location st ( for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA st s . a > 0 holds

(IExec (I,P,s)) . a < s . a ) holds

while>0 (a,I) is InitHalting

proof end;

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

for s being State of SCM+FSA

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

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

(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . a = (s . a) - 1

proof end;

theorem Th48: :: SCM_HALT:66

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

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

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

( (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . a = (s . a) - 1 & ( s . a > 0 implies DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) ) )

for s being State of SCM+FSA

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

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

( (IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)) . a = (s . a) - 1 & ( s . a > 0 implies DataPart (IExec ((Times (a,I)),p,s)) = DataPart (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) ) )

proof end;

theorem :: SCM_HALT:67

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

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

for f being FinSeq-Location

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

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

for s being State of SCM+FSA

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

for f being FinSeq-Location

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

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

proof end;

theorem :: SCM_HALT:68

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

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

for b being Int-Location

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

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

for s being State of SCM+FSA

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

for b being Int-Location

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

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

proof end;

theorem :: SCM_HALT:69

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

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

for f being FinSeq-Location

for a being read-write Int-Location st not I destroys a & s . a > 0 holds

(IExec ((Times (a,I)),p,s)) . f = (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) . f

for s being State of SCM+FSA

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

for f being FinSeq-Location

for a being read-write Int-Location st not I destroys a & s . a > 0 holds

(IExec ((Times (a,I)),p,s)) . f = (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) . f

proof end;

theorem :: SCM_HALT:70

for p being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

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

for b being Int-Location

for a being read-write Int-Location st not I destroys a & s . a > 0 holds

(IExec ((Times (a,I)),p,s)) . b = (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) . b

for s being State of SCM+FSA

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

for b being Int-Location

for a being read-write Int-Location st not I destroys a & s . a > 0 holds

(IExec ((Times (a,I)),p,s)) . b = (IExec ((Times (a,I)),p,(IExec ((I ";" (SubFrom (a,(intloc 0)))),p,s)))) . b

proof end;

definition
end;

:: deftheorem defines good SCM_HALT:def 4 :

for i being Instruction of SCM+FSA holds

( i is good iff not i destroys intloc 0 );

for i being Instruction of SCM+FSA holds

( i is good iff not i destroys intloc 0 );

theorem :: SCM_HALT:71

for P1, P2 being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 holds

for k being Nat holds

( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) by Lm4;

for s being State of SCM+FSA

for I being really-closed InitHalting Program of SCM+FSA st Initialize ((intloc 0) .--> 1) c= s & I c= P1 & I c= P2 holds

for k being Nat holds

( Comput (P1,s,k) = Comput (P2,s,k) & CurInstr (P1,(Comput (P1,s,k))) = CurInstr (P2,(Comput (P2,s,k))) ) by Lm4;

theorem :: SCM_HALT:72

theorem :: SCM_HALT:73

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being really-closed MacroInstruction of SCM+FSA

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

while>0 (a,I) is_halting_onInit s,P by Lm6;

for s being State of SCM+FSA

for I being really-closed MacroInstruction of SCM+FSA

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

while>0 (a,I) is_halting_onInit s,P by Lm6;

theorem :: SCM_HALT:74

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

for I being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st I is_halting_onInit s,P & s . a > 0 holds

( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) ) by Lm7;

for s being State of SCM+FSA

for I being really-closed MacroInstruction of SCM+FSA

for a being read-write Int-Location st I is_halting_onInit s,P & s . a > 0 holds

( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) ) by Lm7;

theorem :: SCM_HALT:75

for P being Instruction-Sequence of SCM+FSA

for s being State of SCM+FSA

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

for a being read-write Int-Location st s . a > 0 & while>0 (a,I) is InitHalting holds

DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s)))) by Lm8;

for s being State of SCM+FSA

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

for a being read-write Int-Location st s . a > 0 & while>0 (a,I) is InitHalting holds

DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(IExec (I,P,s)))) by Lm8;

theorem :: SCM_HALT:76

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

for a being read-write Int-Location st ( for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA st s . a > 0 holds

(IExec (I,P,s)) . a < s . a ) holds

while>0 (a,I) is InitHalting by Lm9;

for a being read-write Int-Location st ( for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA st s . a > 0 holds

(IExec (I,P,s)) . a < s . a ) holds

while>0 (a,I) is InitHalting by Lm9;