let s be State of SCM+FSA ; :: thesis:
let I, J be parahalting Program of SCM+FSA ; :: thesis:
let a, b be read-write Int-Location ; :: thesis:
assume that
A1: I does_not_refer a and
A2: J does_not_refer a ; :: thesis:
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),(Initialize s);

A3: now

let c be read-write Int-Location ; :: thesis:
assume a <> c ; :: thesis:
hence (Exec (SubFrom a,b),(Initialize s)) . c = (Initialize s) . c by SCMFSA_2:91
.= s . c by SCMFSA6C:3 ;
:: thesis:

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 AMI_1:111
.= (((card I) + (card J)) + 3) + (card II) by Th27
.= (((card I) + (card J)) + 3) + 2 by SCMFSA7B:6
.= ((card I) + (card J)) + 5 ;
:: thesis:

A4: now

let f be FinSeq-Location ; :: thesis:
thus (Exec (SubFrom a,b),(Initialize s)) . f = (Initialize s) . f by SCMFSA_2:91
.= s . f by SCMFSA6C:3 ; :: thesis:

end;

hereby :: thesis:

A5: (Exec (SubFrom a,b),(Initialize s)) . a = ((Initialize s) . a) - ((Initialize s) . b) by SCMFSA_2:91
.= (s . a) - ((Initialize s) . b) by SCMFSA6C:3
.= (s . a) - (s . b) by SCMFSA6C:3 ;
assume s . a > s . b ; :: thesis:
then A6: (Exec (SubFrom a,b),(Initialize s)) . a > 0 by A5, XREAL_1:52;
A7: I is_halting_on Initialize (Exec (SubFrom a,b),(Initialize s)) by SCMFSA7B:25;
A8: I is_closed_on Initialize (Exec (SubFrom a,b),(Initialize s)) by SCMFSA7B:24;

hereby :: thesis:

let d be Int-Location ; :: thesis:
assume A9: a <> d ; :: thesis:
thus (IExec (if>0 a,b,I,J),s) . d = (IExec JJ,(Exec (SubFrom a,b),(Initialize s))) . d by Th12
.= (IExec I,(Exec (SubFrom a,b),(Initialize s))) . d by A6, Th27
.= (IExec I,s) . d by A1, A3, A4, A8, A7, A9, Th41 ; :: thesis:

end;

let f be FinSeq-Location ; :: thesis:
thus (IExec (if>0 a,b,I,J),s) . f = (IExec JJ,(Exec (SubFrom a,b),(Initialize s))) . f by Th13
.= (IExec I,(Exec (SubFrom a,b),(Initialize s))) . f by A6, Th27
.= (IExec I,s) . f by A1, A3, A4, A8, A7, Th41 ; :: thesis:

end;

A10: (Exec (SubFrom a,b),(Initialize s)) . a = ((Initialize s) . a) - ((Initialize s) . b) by SCMFSA_2:91
.= (s . a) - ((Initialize s) . b) by SCMFSA6C:3
.= (s . a) - (s . b) by SCMFSA6C:3 ;
A11: J is_closed_on Initialize (Exec (SubFrom a,b),(Initialize s)) by SCMFSA7B:24;
A12: J is_halting_on Initialize (Exec (SubFrom a,b),(Initialize s)) by SCMFSA7B:25;
assume s . a <= s . b ; :: thesis:
then A13: (Exec (SubFrom a,b),(Initialize s)) . a <= 0 by A10, XREAL_1:49;

hereby :: thesis:

let d be Int-Location ; :: thesis:
assume A14: a <> d ; :: thesis:
thus (IExec (if>0 a,b,I,J),s) . d = (IExec JJ,(Exec (SubFrom a,b),(Initialize s))) . d by Th12
.= (IExec J,(Exec (SubFrom a,b),(Initialize s))) . d by A13, Th27
.= (IExec J,s) . d by A2, A3, A4, A11, A12, A14, Th41 ; :: thesis:

end;

let f be FinSeq-Location ; :: thesis:
thus (IExec (if>0 a,b,I,J),s) . f = (IExec JJ,(Exec (SubFrom a,b),(Initialize s))) . f by Th13
.= (IExec J,(Exec (SubFrom a,b),(Initialize s))) . f by A13, Th27
.= (IExec J,s) . f by A2, A3, A4, A11, A12, Th41 ; :: thesis: