:: Conditional branch macro instructions of SCM+FSA, Part II :: by Noriko Asamoto :: :: Received August 27, 1996 :: Copyright (c) 1996-2012 Association of Mizar Users begin 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 Th1: :: SCMFSA8B:1 for P being Instruction-Sequence of SCM+FSA 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 proofend; theorem :: SCMFSA8B:2 canceled; theorem Th3: :: SCMFSA8B:3 for P1, P2 being Instruction-Sequence of SCM+FSA 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 proofend; theorem Th4: :: SCMFSA8B:4 for s1, s2 being State of SCM+FSA for I, J being Program of SCM+FSA st DataPart s1 = DataPart s2 holds Initialize s1 = Initialize s2 by MEMSTR_0:80; theorem Th5: :: SCMFSA8B:5 for P1, P2 being Instruction-Sequence of SCM+FSA 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 ) proofend; theorem Th6: :: SCMFSA8B:6 for P being Instruction-Sequence of SCM+FSA 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 ) proofend; theorem Th7: :: SCMFSA8B:7 for P being Instruction-Sequence of SCM+FSA 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 ) proofend; theorem Th8: :: SCMFSA8B:8 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 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)) ) proofend; theorem Th9: :: SCMFSA8B:9 for P being Instruction-Sequence of SCM+FSA 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 proofend; theorem Th10: :: SCMFSA8B:10 for P being Instruction-Sequence of SCM+FSA 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 proofend; 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)) ) proofend; 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 ) proofend; theorem Th11: :: SCMFSA8B:11 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 proofend; theorem Th12: :: SCMFSA8B:12 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 proofend; theorem Th13: :: SCMFSA8B:13 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 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 ) proofend; theorem Th14: :: SCMFSA8B:14 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)) proofend; theorem Th15: :: SCMFSA8B:15 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 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 ) proofend; theorem Th16: :: SCMFSA8B:16 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)) proofend; theorem Th17: :: SCMFSA8B:17 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)) ) ) proofend; theorem Th18: :: SCMFSA8B:18 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 ) ) ) ) proofend; theorem Th19: :: SCMFSA8B:19 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 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 ) proofend; theorem Th20: :: SCMFSA8B:20 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)) proofend; theorem Th21: :: SCMFSA8B:21 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 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 ) proofend; theorem Th22: :: SCMFSA8B:22 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)) proofend; theorem Th23: :: SCMFSA8B:23 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)) ) ) proofend; theorem Th24: :: SCMFSA8B:24 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 ) ) ) ) proofend; theorem :: SCMFSA8B:25 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 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 ) proofend; theorem Th26: :: SCMFSA8B:26 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)) proofend; theorem :: SCMFSA8B:27 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 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 Th13; theorem Th28: :: SCMFSA8B:28 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)) proofend; theorem :: SCMFSA8B:29 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 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 ) proofend; theorem Th30: :: SCMFSA8B:30 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)) proofend; theorem :: SCMFSA8B:31 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)) ) ) proofend; 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 Th17; cluster if>0 (a,I,J) -> parahalting ; correctness coherence if>0 (a,I,J) is parahalting ; by Th23; 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 :: SCMFSA8B:32 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being Program of SCM+FSA holds DataPart (Result ((P +* I),(Initialized s))) = DataPart (IExec (I,P,s)) by SCMFSA6B:def_1; theorem Th33: :: SCMFSA8B:33 for P being Instruction-Sequence of SCM+FSA for s being State of SCM+FSA for I being Program of SCM+FSA holds Result ((P +* I),(Initialized s)) = IExec (I,P,s) by SCMFSA6B:def_1; theorem Th34: :: SCMFSA8B:34 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)) ) proofend; theorem Th35: :: SCMFSA8B:35 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 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))) ) proofend; theorem :: SCMFSA8B:36 for P being Instruction-Sequence of SCM+FSA 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 ) ) proofend; theorem Th37: :: SCMFSA8B:37 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 & I is_halting_on s1,P1 holds ( I is_closed_on s2,P2 & I is_halting_on s2,P2 ) proofend; theorem Th38: :: SCMFSA8B:38 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)) ) proofend; theorem :: SCMFSA8B:39 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 ) ) ) ) proofend; theorem :: SCMFSA8B:40 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 ) ) ) ) proofend;