set A = NAT ;
set D = Data-Locations ;
set SA0 = Start-At (0,SCM+FSA);
Lm1:
for I, J being Program of SCM+FSA holds Reloc (J,(card I)) c= I ";" J
by FUNCT_4:25;
theorem Th7:
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA for
s1 being
0 -started State of
SCM+FSA for
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA st
I is_closed_on s1,
P1 &
I c= P1 holds
for
n being
Nat st
IC s2 = n &
DataPart s1 = DataPart s2 &
Reloc (
I,
n)
c= P2 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)) )
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 Th13:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location st
s . a = 0 &
I is_closed_on Initialized s,
P &
I is_halting_on Initialized s,
P holds
IExec (
(if=0 (a,I,J)),
P,
s)
= (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
theorem Th15:
for
P being
Instruction-Sequence of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location for
s being
State of
SCM+FSA st
s . a <> 0 &
J is_closed_on Initialized s,
P &
J is_halting_on Initialized s,
P holds
IExec (
(if=0 (a,I,J)),
P,
s)
= (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
theorem Th16:
for
P being
Instruction-Sequence of
SCM+FSA 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)),
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)) ) )
theorem Th17:
for
P being
Instruction-Sequence of
SCM+FSA 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)),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 ) ) ) )
theorem Th19:
for
P being
Instruction-Sequence of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location for
s being
State of
SCM+FSA st
s . a > 0 &
I is_closed_on Initialized s,
P &
I is_halting_on Initialized s,
P holds
IExec (
(if>0 (a,I,J)),
P,
s)
= (IExec (I,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
theorem Th21:
for
P being
Instruction-Sequence of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location for
s being
State of
SCM+FSA st
s . a <= 0 &
J is_closed_on Initialized s,
P &
J is_halting_on Initialized s,
P holds
IExec (
(if>0 (a,I,J)),
P,
s)
= (IExec (J,P,s)) +* (Start-At ((((card I) + (card J)) + 3),SCM+FSA))
theorem Th22:
for
P being
Instruction-Sequence of
SCM+FSA 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)),
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)) ) )
theorem Th23:
for
P being
Instruction-Sequence of
SCM+FSA 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)),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 ) ) ) )
theorem Th25:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location st
s . a < 0 &
I is_closed_on Initialized s,
P &
I is_halting_on Initialized s,
P holds
IExec (
(if<0 (a,I,J)),
P,
s)
= (IExec (I,P,s)) +* (Start-At (((((card I) + (card J)) + (card J)) + 7),SCM+FSA))
theorem Th27:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location st
s . a = 0 &
J is_closed_on Initialized s,
P &
J is_halting_on Initialized s,
P holds
IExec (
(if<0 (a,I,J)),
P,
s)
= (IExec (J,P,s)) +* (Start-At (((((card I) + (card J)) + (card J)) + 7),SCM+FSA))
theorem Th29:
for
P being
Instruction-Sequence of
SCM+FSA for
s being
State of
SCM+FSA for
I,
J being
Program of
SCM+FSA for
a being
read-write Int-Location st
s . a > 0 &
J is_closed_on Initialized s,
P &
J is_halting_on Initialized s,
P holds
IExec (
(if<0 (a,I,J)),
P,
s)
= (IExec (J,P,s)) +* (Start-At (((((card I) + (card J)) + (card J)) + 7),SCM+FSA))
theorem
for
P being
Instruction-Sequence of
SCM+FSA 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)),
P,
s)
= (IExec (I,P,s)) +* (Start-At (((((card I) + (card J)) + (card J)) + 7),SCM+FSA)) ) & (
s . a >= 0 implies
IExec (
(if<0 (a,I,J)),
P,
s)
= (IExec (J,P,s)) +* (Start-At (((((card I) + (card J)) + (card J)) + 7),SCM+FSA)) ) )
theorem Th34:
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA for
a being
Int-Location st not
I refers 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,
P1 holds
for
k being
Nat holds
( ( for
b being
Int-Location st
a <> b holds
(Comput ((P1 +* I),(Initialize s1),k)) . b = (Comput ((P2 +* I),(Initialize s2),k)) . b ) & ( for
f being
FinSeq-Location holds
(Comput ((P1 +* I),(Initialize s1),k)) . f = (Comput ((P2 +* I),(Initialize s2),k)) . f ) &
IC (Comput ((P1 +* I),(Initialize s1),k)) = IC (Comput ((P2 +* I),(Initialize s2),k)) &
CurInstr (
(P1 +* I),
(Comput ((P1 +* I),(Initialize s1),k)))
= CurInstr (
(P2 +* I),
(Comput ((P2 +* I),(Initialize s2),k))) )
theorem Th37:
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA for
I being
Program of
SCM+FSA for
a being
Int-Location st ( for
d being
read-write Int-Location st
a <> d holds
s1 . d = s2 . d ) & ( for
f being
FinSeq-Location holds
s1 . f = s2 . f ) & not
I refers a &
I is_closed_on Initialized s1,
P1 &
I is_halting_on Initialized s1,
P1 holds
( ( for
d being
Int-Location st
a <> d holds
(IExec (I,P1,s1)) . d = (IExec (I,P2,s2)) . d ) & ( for
f being
FinSeq-Location holds
(IExec (I,P1,s1)) . f = (IExec (I,P2,s2)) . f ) &
IC (IExec (I,P1,s1)) = IC (IExec (I,P2,s2)) )
theorem
for
P being
Instruction-Sequence of
SCM+FSA 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 not
I refers a & not
J refers a holds
(
IC (IExec ((if=0 (a,b,I,J)),P,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)),P,s)) . d = (IExec (I,P,s)) . d ) & ( for
f being
FinSeq-Location holds
(IExec ((if=0 (a,b,I,J)),P,s)) . f = (IExec (I,P,s)) . f ) ) ) & (
s . a <> s . b implies ( ( for
d being
Int-Location st
a <> d holds
(IExec ((if=0 (a,b,I,J)),P,s)) . d = (IExec (J,P,s)) . d ) & ( for
f being
FinSeq-Location holds
(IExec ((if=0 (a,b,I,J)),P,s)) . f = (IExec (J,P,s)) . f ) ) ) )
theorem
for
P being
Instruction-Sequence of
SCM+FSA 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 not
I refers a & not
J refers a holds
(
IC (IExec ((if>0 (a,b,I,J)),P,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)),P,s)) . d = (IExec (I,P,s)) . d ) & ( for
f being
FinSeq-Location holds
(IExec ((if>0 (a,b,I,J)),P,s)) . f = (IExec (I,P,s)) . f ) ) ) & (
s . a <= s . b implies ( ( for
d being
Int-Location st
a <> d holds
(IExec ((if>0 (a,b,I,J)),P,s)) . d = (IExec (J,P,s)) . d ) & ( for
f being
FinSeq-Location holds
(IExec ((if>0 (a,b,I,J)),P,s)) . f = (IExec (J,P,s)) . f ) ) ) )