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 refersrefer a & not J refersrefer a holds
( IC (IExec (if>0 a,b,I,J),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),s) . d = (IExec I,s) . d ) & ( for f being FinSeq-Location holds (IExec (if>0 a,b,I,J),s) . f = (IExec I,s) . f ) ) ) & ( s . a <= s . b implies ( ( for d being Int-Location st a <> d holds
(IExec (if>0 a,b,I,J),s) . d = (IExec J,s) . d ) & ( for f being FinSeq-Location holds (IExec (if>0 a,b,I,J),s) . f = (IExec J,s) . f ) ) ) )
let I, J be parahalting Program of SCM+FSA ; :: thesis: for a, b being read-write Int-Location st not I refersrefer a & not J refersrefer a holds
( IC (IExec (if>0 a,b,I,J),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),s) . d = (IExec I,s) . d ) & ( for f being FinSeq-Location holds (IExec (if>0 a,b,I,J),s) . f = (IExec I,s) . f ) ) ) & ( s . a <= s . b implies ( ( for d being Int-Location st a <> d holds
(IExec (if>0 a,b,I,J),s) . d = (IExec J,s) . d ) & ( for f being FinSeq-Location holds (IExec (if>0 a,b,I,J),s) . f = (IExec J,s) . f ) ) ) )
let a, b be read-write Int-Location ; :: thesis: ( not I refersrefer a & not J refersrefer a implies ( IC (IExec (if>0 a,b,I,J),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),s) . d = (IExec I,s) . d ) & ( for f being FinSeq-Location holds (IExec (if>0 a,b,I,J),s) . f = (IExec I,s) . f ) ) ) & ( s . a <= s . b implies ( ( for d being Int-Location st a <> d holds
(IExec (if>0 a,b,I,J),s) . d = (IExec J,s) . d ) & ( for f being FinSeq-Location holds (IExec (if>0 a,b,I,J),s) . f = (IExec J,s) . f ) ) ) ) )
assume that
A1: not I refersrefer a and
A2: not J refersrefer a ; :: thesis: ( IC (IExec (if>0 a,b,I,J),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),s) . d = (IExec I,s) . d ) & ( for f being FinSeq-Location holds (IExec (if>0 a,b,I,J),s) . f = (IExec I,s) . f ) ) ) & ( s . a <= s . b implies ( ( for d being Int-Location st a <> d holds
(IExec (if>0 a,b,I,J),s) . d = (IExec J,s) . d ) & ( for f being FinSeq-Location holds (IExec (if>0 a,b,I,J),s) . f = (IExec J,s) . f ) ) ) )
set s2 = s;
reconsider JJ = if>0 a,I,J as parahalting Program of SCM+FSA ;
reconsider II = Macro (SubFrom a,b) as parahalting keeping_0 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:91
.= s . c by SCMFSA6C:3 ;
:: thesis: verum

end;

IExec (if>0 a,b,I,J),s = IExec (II ';' JJ),s by SCMFSA6A:def 6
.= (IExec JJ,(IExec II,s)) +* (Start-At ((IC (IExec JJ,(IExec II,s))) + (card II)),SCM+FSA ) by SCMFSA6B:44 ;
hence IC (IExec (if>0 a,b,I,J),s) = (IC (IExec JJ,(IExec II,s))) + (card II) by FUNCT_4:121
.= (((card I) + (card J)) + 3) + (card II) by Th27
.= (((card I) + (card J)) + 3) + 2 by SCMFSA7B:6
.= ((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),s) . d = (IExec I,s) . d ) & ( for f being FinSeq-Location holds (IExec (if>0 a,b,I,J),s) . f = (IExec I,s) . f ) ) ) & ( s . a <= s . b implies ( ( for d being Int-Location st a <> d holds
(IExec (if>0 a,b,I,J),s) . d = (IExec J,s) . d ) & ( for f being FinSeq-Location holds (IExec (if>0 a,b,I,J),s) . f = (IExec J,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:91
.= 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),s) . d = (IExec J,s) . d ) & ( for f being FinSeq-Location holds (IExec (if>0 a,b,I,J),s) . f = (IExec J,s) . f ) ) )

A5: (Exec (SubFrom a,b),(Initialized s)) . a = ((Initialized s) . a) - ((Initialized s) . b) by SCMFSA_2:91
.= (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),s) . d = (IExec I,s) . d ) & ( for f being FinSeq-Location holds (IExec (if>0 a,b,I,J),s) . f = (IExec I,s) . f ) )
then A6: (Exec (SubFrom a,b),(Initialized s)) . a > 0 by A5, XREAL_1:52;
A7: I is_halting_on Initialized (Exec (SubFrom a,b),(Initialized s)) by SCMFSA7B:25;
A8: I is_closed_on Initialized (Exec (SubFrom a,b),(Initialized s)) by SCMFSA7B:24;

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

let d be Int-Location ; :: thesis: ( a <> d implies (IExec (if>0 a,b,I,J),s) . d = (IExec I,s) . d )
assume A9: a <> d ; :: thesis: (IExec (if>0 a,b,I,J),s) . d = (IExec I,s) . d
thus (IExec (if>0 a,b,I,J),s) . d = (IExec JJ,(Exec (SubFrom a,b),(Initialized s))) . d by Th12
.= (IExec I,(Exec (SubFrom a,b),(Initialized s))) . d by A6, Th27
.= (IExec I,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),s) . f = (IExec I,s) . f
thus (IExec (if>0 a,b,I,J),s) . f = (IExec JJ,(Exec (SubFrom a,b),(Initialized s))) . f by Th13
.= (IExec I,(Exec (SubFrom a,b),(Initialized s))) . f by A6, Th27
.= (IExec I,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:91
.= (s . a) - ((Initialized s) . b) by SCMFSA6C:3
.= (s . a) - (s . b) by SCMFSA6C:3 ;
A11: J is_closed_on Initialized (Exec (SubFrom a,b),(Initialized s)) by SCMFSA7B:24;
A12: J is_halting_on Initialized (Exec (SubFrom a,b),(Initialized s)) by SCMFSA7B:25;
assume s . a <= s . b ; :: thesis: ( ( for d being Int-Location st a <> d holds
(IExec (if>0 a,b,I,J),s) . d = (IExec J,s) . d ) & ( for f being FinSeq-Location holds (IExec (if>0 a,b,I,J),s) . f = (IExec J,s) . f ) )
then A13: (Exec (SubFrom a,b),(Initialized s)) . a <= 0 by A10, XREAL_1:49;

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

let d be Int-Location ; :: thesis: ( a <> d implies (IExec (if>0 a,b,I,J),s) . d = (IExec J,s) . d )
assume A14: a <> d ; :: thesis: (IExec (if>0 a,b,I,J),s) . d = (IExec J,s) . d
thus (IExec (if>0 a,b,I,J),s) . d = (IExec JJ,(Exec (SubFrom a,b),(Initialized s))) . d by Th12
.= (IExec J,(Exec (SubFrom a,b),(Initialized s))) . d by A13, Th27
.= (IExec J,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),s) . f = (IExec J,s) . f
thus (IExec (if>0 a,b,I,J),s) . f = (IExec JJ,(Exec (SubFrom a,b),(Initialized s))) . f by Th13
.= (IExec J,(Exec (SubFrom a,b),(Initialized s))) . f by A13, Th27
.= (IExec J,s) . f by A2, A3, A4, A11, A12, Th41 ; :: thesis: verum