:: Conditional branch macro instructions of SCM+FSA, Part II
:: by Noriko Asamoto
::
:: Received August 27, 1996
:: Copyright (c) 1996-2011 Association of Mizar Users


begin

set A = NAT ;

set D = Data-Locations SCM+FSA;

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:26;

theorem :: SCMFSA8B:1
canceled;

theorem :: SCMFSA8B:2
canceled;

theorem Th3: :: SCMFSA8B:3
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being Program of SCM+FSA
for s being State of SCM+FSA st I is_closed_on s,P holds
0 in dom I
proof end;

theorem :: SCMFSA8B:4
canceled;

theorem :: SCMFSA8B:5
for s being State of SCM+FSA
for I being Program of SCM+FSA holds DataPart (Initialized s) = DataPart (s +* (Initialize ((intloc 0) .--> 1))) ;

theorem Th6: :: SCMFSA8B:6
for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_closed_on s1,P1 holds
I is_closed_on s2,P2
proof end;

theorem Th7: :: SCMFSA8B:7
for s1, s2 being State of SCM+FSA
for I, J being Program of SCM+FSA st DataPart s1 = DataPart s2 holds
NPP (Initialize s1) = NPP (Initialize s2)
proof end;

theorem Th8: :: SCMFSA8B:8
for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st DataPart s1 = DataPart s2 & I is_closed_on s1,P1 & I is_halting_on s1,P1 holds
( I is_closed_on s2,P2 & I is_halting_on s2,P2 )
proof end;

theorem Th9: :: SCMFSA8B:9
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I, J being Program of SCM+FSA holds
( I is_closed_on Initialized s,P iff I is_closed_on s +* (Initialize ((intloc 0) .--> 1)),P +* J )
proof end;

theorem Th10: :: SCMFSA8B:10
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for l being Element of NAT holds
( I is_closed_on s,P iff I is_closed_on s +* (Start-At (0,SCM+FSA)),P +* I )
proof end;

theorem Th11: :: SCMFSA8B:11
for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s1, s2 being State of SCM+FSA
for I being Program of SCM+FSA st Start-At (0,SCM+FSA) c= s1 & I is_closed_on s1,P1 & I c= P1 holds
for n being Element of NAT st IC s2 = n & DataPart s1 = DataPart s2 & Reloc (I,n) c= P2 holds
for i being Element of 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;

LmX: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s1, s2 being State of SCM+FSA
for J being parahalting Program of SCM+FSA st NPP s1 = NPP s2 holds
NPP (IExec (J,P,s1)) = NPP (IExec (J,P,s2))
proof end;

theorem Th12: :: SCMFSA8B:12
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for i being parahalting keeping_0 Instruction of SCM+FSA
for J being parahalting 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 Th13: :: SCMFSA8B:13
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for i being parahalting keeping_0 Instruction of SCM+FSA
for J being parahalting 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;

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 :: SCMFSA8B:def 1
((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA);
coherence
((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA) is Program of SCM+FSA
;
func if>0 (a,I,J) -> Program of SCM+FSA equals :: SCMFSA8B:def 2
((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA);
coherence
((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA) is Program of SCM+FSA
;
end;

:: deftheorem defines if=0 SCMFSA8B:def 1 :
for a being Int-Location
for I, J being Program of SCM+FSA holds if=0 (a,I,J) = ((((a =0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA);

:: deftheorem defines if>0 SCMFSA8B:def 2 :
for a being Int-Location
for I, J being Program of SCM+FSA holds if>0 (a,I,J) = ((((a >0_goto ((card J) + 3)) ';' J) ';' (Goto ((card I) + 1))) ';' I) ';' (Stop SCM+FSA);

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 :: SCMFSA8B:def 3
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 :
for a being Int-Location
for I, J being Program of SCM+FSA holds if<0 (a,I,J) = if=0 (a,J,(if>0 (a,J,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)) )
proof end;

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 )
proof end;

theorem Th14: :: SCMFSA8B:14
for I, J being Program of SCM+FSA
for a being Int-Location holds card (if=0 (a,I,J)) = ((card I) + (card J)) + 4
proof end;

theorem Th15: :: SCMFSA8B:15
for I, J being Program of SCM+FSA
for a being Int-Location holds card (if>0 (a,I,J)) = ((card I) + (card J)) + 4
proof end;

theorem Th16: :: SCMFSA8B:16
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 s,P & I is_halting_on s,P holds
( if=0 (a,I,J) is_closed_on s,P & if=0 (a,I,J) is_halting_on s,P )
proof end;

theorem Th17: :: SCMFSA8B:17
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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))
proof end;

theorem Th18: :: SCMFSA8B:18
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 s,P & J is_halting_on s,P holds
( if=0 (a,I,J) is_closed_on s,P & if=0 (a,I,J) is_halting_on s,P )
proof end;

theorem Th19: :: SCMFSA8B:19
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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))
proof end;

theorem Th20: :: SCMFSA8B:20
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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)) ) )
proof end;

theorem Th21: :: SCMFSA8B:21
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 ) ) ) )
proof end;

theorem Th22: :: SCMFSA8B:22
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 s,P & I is_halting_on s,P holds
( if>0 (a,I,J) is_closed_on s,P & if>0 (a,I,J) is_halting_on s,P )
proof end;

theorem Th23: :: SCMFSA8B:23
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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))
proof end;

theorem Th24: :: SCMFSA8B:24
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 s,P & J is_halting_on s,P holds
( if>0 (a,I,J) is_closed_on s,P & if>0 (a,I,J) is_halting_on s,P )
proof end;

theorem Th25: :: SCMFSA8B:25
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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))
proof end;

theorem Th26: :: SCMFSA8B:26
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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)) ) )
proof end;

theorem Th27: :: SCMFSA8B:27
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 ) ) ) )
proof end;

theorem :: SCMFSA8B:28
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 s,P & I is_halting_on s,P holds
( if<0 (a,I,J) is_closed_on s,P & if<0 (a,I,J) is_halting_on s,P )
proof end;

theorem Th29: :: SCMFSA8B:29
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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))
proof end;

theorem :: SCMFSA8B:30
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 s,P & J is_halting_on s,P holds
( if<0 (a,I,J) is_closed_on s,P & if<0 (a,I,J) is_halting_on s,P ) by Th16;

theorem Th31: :: SCMFSA8B:31
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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))
proof end;

theorem :: SCMFSA8B:32
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 s,P & J is_halting_on s,P holds
( if<0 (a,I,J) is_closed_on s,P & if<0 (a,I,J) is_halting_on s,P )
proof end;

theorem Th33: :: SCMFSA8B:33
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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))
proof end;

theorem :: SCMFSA8B:34
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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)) ) )
proof end;

registration
let I, J be parahalting Program of SCM+FSA;
let a be read-write Int-Location ;
cluster if=0 (a,I,J) -> parahalting ;
correctness
coherence
if=0 (a,I,J) is parahalting
;
by Th20;
cluster if>0 (a,I,J) -> parahalting ;
correctness
coherence
if>0 (a,I,J) is parahalting
;
by Th26;
end;

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 :: SCMFSA8B:def 4
(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 :: SCMFSA8B:def 5
(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 :
for a, b being Int-Location
for I, J being Program of SCM+FSA holds if=0 (a,b,I,J) = (SubFrom (a,b)) ';' (if=0 (a,I,J));

:: deftheorem defines if>0 SCMFSA8B:def 5 :
for a, b being Int-Location
for I, J being Program of SCM+FSA holds if>0 (a,b,I,J) = (SubFrom (a,b)) ';' (if>0 (a,I,J));

registration
let a be Int-Location ;
let I, J be Program of SCM+FSA;
cluster if=0 (a,I,J) -> non halt-free ;
coherence
not if=0 (a,I,J) is halt-free
;
cluster if>0 (a,I,J) -> non halt-free ;
coherence
not if>0 (a,I,J) is halt-free
;
cluster if<0 (a,I,J) -> non halt-free ;
coherence
not if<0 (a,I,J) is halt-free
;
end;

registration
let a, b be Int-Location ;
let I, J be Program of SCM+FSA;
cluster if=0 (a,b,I,J) -> non halt-free ;
coherence
not if=0 (a,b,I,J) is halt-free
;
cluster if>0 (a,b,I,J) -> non halt-free ;
coherence
not if>0 (a,b,I,J) is halt-free
;
end;

notation
let a, b be Int-Location ;
let I, J be Program of SCM+FSA;
synonym if<0 (b,a,I,J) for if>0 (a,b,I,J);
end;

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: :: SCMFSA8B:35
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA holds DataPart (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) = DataPart (IExec (I,P,s))
proof end;

theorem Th36: :: SCMFSA8B:36
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I being Program of SCM+FSA
for a being Int-Location holds NPP (Result ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))))) = NPP (IExec (I,P,s))
proof end;

theorem Th37: :: SCMFSA8B:37
for s1, s2 being State of SCM+FSA
for i being Instruction of SCM+FSA
for a being Int-Location st ( for b being Int-Location st a <> b holds
s1 . b = s2 . b ) & ( for f being FinSeq-Location holds s1 . f = s2 . f ) & not i refers a & IC s1 = IC s2 holds
( ( for b being Int-Location st a <> b holds
(Exec (i,s1)) . b = (Exec (i,s2)) . b ) & ( for f being FinSeq-Location holds (Exec (i,s1)) . f = (Exec (i,s2)) . f ) & IC (Exec (i,s1)) = IC (Exec (i,s2)) )
proof end;

theorem Th38: :: SCMFSA8B:38
for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 Element of 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))) )
proof end;

theorem :: SCMFSA8B:39
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA
for I, J being Program of SCM+FSA
for l being Element of NAT holds
( I is_closed_on s,P & I is_halting_on s,P iff ( I is_closed_on s +* (Start-At (l,SCM+FSA)),P +* I & I is_halting_on s +* (Start-At (l,SCM+FSA)),P +* I ) )
proof end;

theorem Th40: :: SCMFSA8B:40
for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 & I is_halting_on s1,P1 holds
( I is_closed_on s2,P2 & I is_halting_on s2,P2 )
proof end;

theorem Th41: :: SCMFSA8B:41
for P1, P2 being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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)) )
proof end;

theorem :: SCMFSA8B:42
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 ) ) ) )
proof end;

theorem :: SCMFSA8B:43
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
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 ) ) ) )
proof end;

theorem :: SCMFSA8B:44
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s1, s2 being State of SCM+FSA
for J being parahalting Program of SCM+FSA st NPP s1 = NPP s2 holds
NPP (IExec (J,P,s1)) = NPP (IExec (J,P,s2)) by LmX;

theorem :: SCMFSA8B:45
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s1, s2 being State of SCM+FSA
for J being Program of SCM+FSA st NPP s1 = NPP s2 & J is_halting_on Initialized s1,P holds
NPP (IExec (J,P,s1)) = NPP (IExec (J,P,s2))
proof end;