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 Th21
.= (((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:

assume A5: s . a = s . b ; :: thesis:
A6: I is_closed_on Initialize (Exec (SubFrom a,b),(Initialize s)) by SCMFSA7B:24;
A7: I is_halting_on Initialize (Exec (SubFrom a,b),(Initialize s)) by SCMFSA7B:25;
A8: (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
.= 0 by A5 ;

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 A8, Th21
.= (IExec I,s) . d by A1, A3, A4, A6, 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 A8, Th21
.= (IExec I,s) . f by A1, A3, A4, A6, 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_halting_on Initialize (Exec (SubFrom a,b),(Initialize s)) by SCMFSA7B:25;
A12: J is_closed_on Initialize (Exec (SubFrom a,b),(Initialize s)) by SCMFSA7B:24;
assume s . a <> s . b ; :: thesis:
then A13: (s . a) + (- (s . b)) <> (s . b) + (- (s . b)) ;

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 A10, A13, Th21
.= (IExec J,s) . d by A2, A3, A4, A12, A11, 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 A10, A13, Th21
.= (IExec J,s) . f by A2, A3, A4, A12, A11, Th41 ; :: thesis: