begin
set A = NAT ;
set D = Int-Locations \/ FinSeq-Locations ;
Lm1:
for I, J being Program of 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:
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 ;
func if<0 a,
I,
J -> Program of
equals
if=0 a,
J,
(if>0 a,J,I);
coherence
if=0 a,J,(if>0 a,J,I) is Program of
;
end;
:: deftheorem defines if<0 SCMFSA8B:def 3 :
Lm2:
for a being Int-Location
for I, J being Program of holds
( insloc 0 in dom (if=0 a,I,J) & insloc 1 in dom (if=0 a,I,J) & insloc 0 in dom (if>0 a,I,J) & insloc 1 in dom (if>0 a,I,J) )
Lm3:
for a being Int-Location
for I, J being Program of holds
( (if=0 a,I,J) . (insloc 0 ) = a =0_goto (insloc ((card J) + 3)) & (if=0 a,I,J) . (insloc 1) = goto (insloc 2) & (if>0 a,I,J) . (insloc 0 ) = a >0_goto (insloc ((card J) + 3)) & (if>0 a,I,J) . (insloc 1) = goto (insloc 2) )
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
for
s being
State of
for
I,
J being
parahalting Program of
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 (insloc (((card I) + (card J)) + 3))) ) & (
s . a <> 0 implies
IExec (if=0 a,I,J),
s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) )
theorem Th21:
for
s being
State of
for
I,
J being
parahalting Program of
for
a being
read-write Int-Location holds
(
IC (IExec (if=0 a,I,J),s) = insloc (((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
for
I,
J being
parahalting Program of
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 (insloc (((card I) + (card J)) + 3))) ) & (
s . a <= 0 implies
IExec (if>0 a,I,J),
s = (IExec J,s) +* (Start-At (insloc (((card I) + (card J)) + 3))) ) )
theorem Th27:
for
s being
State of
for
I,
J being
parahalting Program of
for
a being
read-write Int-Location holds
(
IC (IExec (if>0 a,I,J),s) = insloc (((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
for
I,
J being
parahalting Program of
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 (insloc ((((card I) + (card J)) + (card J)) + 7))) ) & (
s . a >= 0 implies
IExec (if<0 a,I,J),
s = (IExec J,s) +* (Start-At (insloc ((((card I) + (card J)) + (card J)) + 7))) ) )
definition
let a,
b be
Int-Location ;
let I,
J be
Program of ;
func if=0 a,
b,
I,
J -> Program of
equals
(SubFrom a,b) ';' (if=0 a,I,J);
coherence
(SubFrom a,b) ';' (if=0 a,I,J) is Program of
;
func if>0 a,
b,
I,
J -> Program of
equals
(SubFrom a,b) ';' (if>0 a,I,J);
coherence
(SubFrom a,b) ';' (if>0 a,I,J) is Program of
;
end;
:: deftheorem defines if=0 SCMFSA8B:def 4 :
:: deftheorem defines if>0 SCMFSA8B:def 5 :
registration
let I,
J be
parahalting Program of ;
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:
theorem Th39:
theorem Th40:
theorem Th41:
theorem
for
s being
State of
for
I,
J being
parahalting Program of
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) = insloc (((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
for
I,
J being
parahalting Program of
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) = insloc (((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 ) ) ) )