let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I, J being really-closed parahalting MacroInstruction 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 ) ) ) )
let s be State of SCM+FSA; :: thesis: for I, J being really-closed parahalting MacroInstruction 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 ) ) ) )
let I, J be really-closed parahalting MacroInstruction of SCM+FSA ; :: thesis: 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 ) ) ) )
let a, b be read-write Int-Location; :: thesis: ( not I refers a & not J refers a implies ( 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 ) ) ) ) )
assume that
A1: not I refers a and
A2: not J refers a ; :: thesis: ( 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 ) ) ) )
reconsider JJ = if>0 (a,I,J) as parahalting Program of SCM+FSA ;
reconsider II = Macro (SubFrom (a,b)) as keeping_0 parahalting Program of SCM+FSA ;
set i = SubFrom (a,b);
set s1 = Exec ((SubFrom (a,b)),(Initialized s));

A3: now :: thesis: for c being read-write Int-Location st a <> c holds
(Exec ((SubFrom (a,b)),(Initialized s))) . c = s . c

let c be read-write Int-Location; :: thesis: ( a <> c implies (Exec ((SubFrom (a,b)),(Initialized s))) . c = s . c )
assume a <> c ; :: thesis: (Exec ((SubFrom (a,b)),(Initialized s))) . c = s . c
hence (Exec ((SubFrom (a,b)),(Initialized s))) . c = (Initialized s) . c by SCMFSA_2:65
.= s . c by SCMFSA_M:37 ;
:: thesis: verum

end;

IExec ((if>0 (a,b,I,J)),P,s) = IncIC ((IExec (JJ,P,(IExec (II,P,s)))),(card II)) by SCMFSA6B:20;
hence IC (IExec ((if>0 (a,b,I,J)),P,s)) = (IC (IExec (JJ,P,(IExec (II,P,s))))) + (card II) by FUNCT_4:113
.= (((card I) + (card J)) + 3) + (card II) by Th18
.= (((card I) + (card J)) + 3) + 2 by COMPOS_1:56
.= ((card I) + (card J)) + 5 ;
:: thesis: ( ( 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 ) ) ) )

A4: now :: thesis: for f being FinSeq-Location holds (Exec ((SubFrom (a,b)),(Initialized s))) . f = s . f

let f be FinSeq-Location ; :: thesis: (Exec ((SubFrom (a,b)),(Initialized s))) . f = s . f
thus (Exec ((SubFrom (a,b)),(Initialized s))) . f = (Initialized s) . f by SCMFSA_2:65
.= s . f by SCMFSA_M:37 ; :: thesis: verum

end;

hereby :: thesis: ( 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 ) ) )

A5: (Exec ((SubFrom (a,b)),(Initialized s))) . a = ((Initialized s) . a) - ((Initialized s) . b) by SCMFSA_2:65
.= (s . a) - ((Initialized s) . b) by SCMFSA_M:37
.= (s . a) - (s . b) by SCMFSA_M:37 ;
assume s . a > s . b ; :: thesis: ( ( 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 ) )
then A6: (Exec ((SubFrom (a,b)),(Initialized s))) . a > 0 by A5, XREAL_1:50;
A7: I is_halting_on Initialized s,P by SCMFSA7B:19;

hereby :: thesis: for f being FinSeq-Location holds (IExec ((if>0 (a,b,I,J)),P,s)) . f = (IExec (I,P,s)) . f

let d be Int-Location; :: thesis: ( a <> d implies (IExec ((if>0 (a,b,I,J)),P,s)) . d = (IExec (I,P,s)) . d )
assume A8: a <> d ; :: thesis: (IExec ((if>0 (a,b,I,J)),P,s)) . d = (IExec (I,P,s)) . d
thus (IExec ((if>0 (a,b,I,J)),P,s)) . d = (IExec (JJ,P,(Exec ((SubFrom (a,b)),(Initialized s))))) . d by Th3
.= (IExec (I,P,(Exec ((SubFrom (a,b)),(Initialized s))))) . d by A6, Th18
.= (IExec (I,P,s)) . d by A1, A3, A4, A7, A8, Th25 ; :: thesis: verum

end;

let f be FinSeq-Location ; :: thesis: (IExec ((if>0 (a,b,I,J)),P,s)) . f = (IExec (I,P,s)) . f
thus (IExec ((if>0 (a,b,I,J)),P,s)) . f = (IExec (JJ,P,(Exec ((SubFrom (a,b)),(Initialized s))))) . f by Th4
.= (IExec (I,P,(Exec ((SubFrom (a,b)),(Initialized s))))) . f by A6, Th18
.= (IExec (I,P,s)) . f by A1, A3, A4, A7, Th25 ; :: thesis: verum

end;

A9: (Exec ((SubFrom (a,b)),(Initialized s))) . a = ((Initialized s) . a) - ((Initialized s) . b) by SCMFSA_2:65
.= (s . a) - ((Initialized s) . b) by SCMFSA_M:37
.= (s . a) - (s . b) by SCMFSA_M:37 ;
A10: J is_halting_on Initialized s,P by SCMFSA7B:19;
assume s . a <= s . b ; :: thesis: ( ( 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 ) )
then A11: (Exec ((SubFrom (a,b)),(Initialized s))) . a <= 0 by A9, XREAL_1:47;

hereby :: thesis: for f being FinSeq-Location holds (IExec ((if>0 (a,b,I,J)),P,s)) . f = (IExec (J,P,s)) . f

let d be Int-Location; :: thesis: ( a <> d implies (IExec ((if>0 (a,b,I,J)),P,s)) . d = (IExec (J,P,s)) . d )
assume A12: a <> d ; :: thesis: (IExec ((if>0 (a,b,I,J)),P,s)) . d = (IExec (J,P,s)) . d
thus (IExec ((if>0 (a,b,I,J)),P,s)) . d = (IExec (JJ,P,(Exec ((SubFrom (a,b)),(Initialized s))))) . d by Th3
.= (IExec (J,P,(Exec ((SubFrom (a,b)),(Initialized s))))) . d by A11, Th18
.= (IExec (J,P,s)) . d by A2, A3, A4, A10, A12, Th25 ; :: thesis: verum

end;

let f be FinSeq-Location ; :: thesis: (IExec ((if>0 (a,b,I,J)),P,s)) . f = (IExec (J,P,s)) . f
thus (IExec ((if>0 (a,b,I,J)),P,s)) . f = (IExec (JJ,P,(Exec ((SubFrom (a,b)),(Initialized s))))) . f by Th4
.= (IExec (J,P,(Exec ((SubFrom (a,b)),(Initialized s))))) . f by A11, Th18
.= (IExec (J,P,s)) . f by A2, A3, A4, A10, Th25 ; :: thesis: verum