begin
set A = NAT ;
set D = Int-Locations \/ FinSeq-Locations ;
Lm1:
for I, J being Program of SCM+FSA holds ProgramPart (Relocated J,(card I)) c= I ';' J
theorem
theorem
theorem Th3:
theorem
canceled;
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
for
s1,
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I +* (Start-At 0 ,SCM+FSA ) c= s1 &
I is_closed_on s1 holds
for
n being
Element of
NAT st
ProgramPart (Relocated I,n) c= s2 &
IC s2 = n &
DataPart s1 = DataPart s2 holds
for
i being
Element of
NAT holds
(
(IC (Comput (ProgramPart s1),s1,i)) + n = IC (Comput (ProgramPart s2),s2,i) &
IncAddr (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,i)),(Comput (ProgramPart s1),s1,i)),
n = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,i)),
(Comput (ProgramPart s2),s2,i) &
DataPart (Comput (ProgramPart s1),s1,i) = DataPart (Comput (ProgramPart s2),s2,i) )
theorem Th12:
theorem Th13:
:: deftheorem defines if=0 SCMFSA8B:def 1 :
:: deftheorem defines if>0 SCMFSA8B:def 2 :
definition
let a be
Int-Location ;
let I,
J be
Program of
SCM+FSA ;
func if<0 a,
I,
J -> Program of
SCM+FSA equals
if=0 a,
J,
(if>0 a,J,I);
coherence
if=0 a,J,(if>0 a,J,I) is Program of SCM+FSA
;
end;
:: deftheorem defines if<0 SCMFSA8B:def 3 :
Lm2:
for a being Int-Location
for I, J being Program of SCM+FSA holds
( 0 in dom (if=0 a,I,J) & 1 in dom (if=0 a,I,J) & 0 in dom (if>0 a,I,J) & 1 in dom (if>0 a,I,J) )
Lm3:
for a being Int-Location
for I, J being Program of SCM+FSA holds
( (if=0 a,I,J) . 0 = a =0_goto ((card J) + 3) & (if=0 a,I,J) . 1 = goto 2 & (if>0 a,I,J) . 0 = a >0_goto ((card J) + 3) & (if>0 a,I,J) . 1 = goto 2 )
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
for
s being
State of
SCM+FSA for
I,
J being
parahalting Program of
SCM+FSA for
a being
read-write Int-Location holds
(
if=0 a,
I,
J is
parahalting & (
s . a = 0 implies
IExec (if=0 a,I,J),
s = (IExec I,s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA ) ) & (
s . a <> 0 implies
IExec (if=0 a,I,J),
s = (IExec J,s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA ) ) )
theorem Th21:
for
s being
State of
SCM+FSA for
I,
J being
parahalting Program of
SCM+FSA for
a being
read-write Int-Location holds
(
IC (IExec (if=0 a,I,J),s) = ((card I) + (card J)) + 3 & (
s . a = 0 implies ( ( for
d being
Int-Location holds
(IExec (if=0 a,I,J),s) . d = (IExec I,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if=0 a,I,J),s) . f = (IExec I,s) . f ) ) ) & (
s . a <> 0 implies ( ( for
d being
Int-Location holds
(IExec (if=0 a,I,J),s) . d = (IExec J,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if=0 a,I,J),s) . f = (IExec J,s) . f ) ) ) )
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
for
s being
State of
SCM+FSA for
I,
J being
parahalting Program of
SCM+FSA for
a being
read-write Int-Location holds
(
if>0 a,
I,
J is
parahalting & (
s . a > 0 implies
IExec (if>0 a,I,J),
s = (IExec I,s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA ) ) & (
s . a <= 0 implies
IExec (if>0 a,I,J),
s = (IExec J,s) +* (Start-At (((card I) + (card J)) + 3),SCM+FSA ) ) )
theorem Th27:
for
s being
State of
SCM+FSA for
I,
J being
parahalting Program of
SCM+FSA for
a being
read-write Int-Location holds
(
IC (IExec (if>0 a,I,J),s) = ((card I) + (card J)) + 3 & (
s . a > 0 implies ( ( for
d being
Int-Location holds
(IExec (if>0 a,I,J),s) . d = (IExec I,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if>0 a,I,J),s) . f = (IExec I,s) . f ) ) ) & (
s . a <= 0 implies ( ( for
d being
Int-Location holds
(IExec (if>0 a,I,J),s) . d = (IExec J,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if>0 a,I,J),s) . f = (IExec J,s) . f ) ) ) )
theorem
theorem Th29:
theorem
theorem Th31:
theorem
theorem Th33:
theorem
for
s being
State of
SCM+FSA for
I,
J being
parahalting Program of
SCM+FSA for
a being
read-write Int-Location holds
(
if<0 a,
I,
J is
parahalting & (
s . a < 0 implies
IExec (if<0 a,I,J),
s = (IExec I,s) +* (Start-At ((((card I) + (card J)) + (card J)) + 7),SCM+FSA ) ) & (
s . a >= 0 implies
IExec (if<0 a,I,J),
s = (IExec J,s) +* (Start-At ((((card I) + (card J)) + (card J)) + 7),SCM+FSA ) ) )
definition
let a,
b be
Int-Location ;
let I,
J be
Program of
SCM+FSA ;
func if=0 a,
b,
I,
J -> Program of
SCM+FSA equals
(SubFrom a,b) ';' (if=0 a,I,J);
coherence
(SubFrom a,b) ';' (if=0 a,I,J) is Program of SCM+FSA
;
func if>0 a,
b,
I,
J -> Program of
SCM+FSA equals
(SubFrom a,b) ';' (if>0 a,I,J);
coherence
(SubFrom a,b) ';' (if>0 a,I,J) is Program of SCM+FSA
;
end;
:: deftheorem defines if=0 SCMFSA8B:def 4 :
:: deftheorem defines if>0 SCMFSA8B:def 5 :
registration
let I,
J be
parahalting Program of
SCM+FSA ;
let a,
b be
read-write Int-Location ;
cluster if=0 a,
b,
I,
J -> parahalting ;
correctness
coherence
if=0 a,b,I,J is parahalting ;
;
cluster if>0 a,
b,
I,
J -> parahalting ;
correctness
coherence
if>0 a,b,I,J is parahalting ;
;
end;
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
for
s1,
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA for
a being
Int-Location st
I does_not_refer a & ( for
b being
Int-Location st
a <> b holds
s1 . b = s2 . b ) & ( for
f being
FinSeq-Location holds
s1 . f = s2 . f ) &
I is_closed_on s1 holds
for
k being
Element of
NAT holds
( ( for
b being
Int-Location st
a <> b holds
(Comput (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),k) . b = (Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),k) . b ) & ( for
f being
FinSeq-Location holds
(Comput (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),k) . f = (Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),k) . f ) &
IC (Comput (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),k) = IC (Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),k) &
CurInstr (ProgramPart (Comput (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),k)),
(Comput (ProgramPart (s1 +* (I +* (Start-At 0 ,SCM+FSA )))),(s1 +* (I +* (Start-At 0 ,SCM+FSA ))),k) = CurInstr (ProgramPart (Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),k)),
(Comput (ProgramPart (s2 +* (I +* (Start-At 0 ,SCM+FSA )))),(s2 +* (I +* (Start-At 0 ,SCM+FSA ))),k) )
theorem Th39:
theorem Th40:
theorem Th41:
theorem
for
s being
State of
SCM+FSA for
I,
J being
parahalting Program of
SCM+FSA for
a,
b being
read-write Int-Location st
I does_not_refer a &
J does_not_refer a holds
(
IC (IExec (if=0 a,b,I,J),s) = ((card I) + (card J)) + 5 & (
s . a = s . b implies ( ( for
d being
Int-Location st
a <> d holds
(IExec (if=0 a,b,I,J),s) . d = (IExec I,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if=0 a,b,I,J),s) . f = (IExec I,s) . f ) ) ) & (
s . a <> s . b implies ( ( for
d being
Int-Location st
a <> d holds
(IExec (if=0 a,b,I,J),s) . d = (IExec J,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if=0 a,b,I,J),s) . f = (IExec J,s) . f ) ) ) )
theorem
for
s being
State of
SCM+FSA for
I,
J being
parahalting Program of
SCM+FSA for
a,
b being
read-write Int-Location st
I does_not_refer a &
J does_not_refer a holds
(
IC (IExec (if>0 a,b,I,J),s) = ((card I) + (card J)) + 5 & (
s . a > s . b implies ( ( for
d being
Int-Location st
a <> d holds
(IExec (if>0 a,b,I,J),s) . d = (IExec I,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if>0 a,b,I,J),s) . f = (IExec I,s) . f ) ) ) & (
s . a <= s . b implies ( ( for
d being
Int-Location st
a <> d holds
(IExec (if>0 a,b,I,J),s) . d = (IExec J,s) . d ) & ( for
f being
FinSeq-Location holds
(IExec (if>0 a,b,I,J),s) . f = (IExec J,s) . f ) ) ) )