let P be Instruction-Sequence of SCM+FSA; :: thesis: 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 ) ) ) )
let s be State of SCM+FSA; :: thesis: 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 ) ) ) )
let I, J be parahalting Program 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

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 SCMFSA6C:3 ;
:: 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 Th27
.= (((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

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 SCMFSA6C:3 ; :: 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 SCMFSA6C:3
.= (s . a) - (s . b) by SCMFSA6C:3 ;
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;
A8: I is_closed_on Initialized s,P by SCMFSA7B:18;

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 A9: 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 Th12
.= (IExec (I,P,(Exec ((SubFrom (a,b)),(Initialized s))))) . d by A6, Th27
.= (IExec (I,P,s)) . d by A1, A3, A4, A8, A7, A9, Th41 ; :: 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 Th13
.= (IExec (I,P,(Exec ((SubFrom (a,b)),(Initialized s))))) . f by A6, Th27
.= (IExec (I,P,s)) . f by A1, A3, A4, A8, A7, Th41 ; :: thesis: verum

end;

A10: (Exec ((SubFrom (a,b)),(Initialized s))) . a = ((Initialized s) . a) - ((Initialized s) . b) by SCMFSA_2:65
.= (s . a) - ((Initialized s) . b) by SCMFSA6C:3
.= (s . a) - (s . b) by SCMFSA6C:3 ;
A11: J is_closed_on Initialized s,P by SCMFSA7B:18;
A12: 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 A13: (Exec ((SubFrom (a,b)),(Initialized s))) . a <= 0 by A10, 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 A14: 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 Th12
.= (IExec (J,P,(Exec ((SubFrom (a,b)),(Initialized s))))) . d by A13, Th27
.= (IExec (J,P,s)) . d by A2, A3, A4, A11, A12, A14, Th41 ; :: 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 Th13
.= (IExec (J,P,(Exec ((SubFrom (a,b)),(Initialized s))))) . f by A13, Th27
.= (IExec (J,P,s)) . f by A2, A3, A4, A11, A12, Th41 ; :: thesis: verum