let P be Instruction-Sequence of SCM+FSA; 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; 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 ; 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; ( 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
; ( 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));
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 Th12
.=
(((card I) + (card J)) + 3) + 2
by COMPOS_1:56
.=
((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 ) ) ) )
hereby ( 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 A5:
s . a = s . b
;
( ( 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 ) )A6:
I is_halting_on Initialized s,
P
by SCMFSA7B:19;
A7:
(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
.=
0
by A5
;
hereby 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;
( a <> d implies (IExec ((if=0 (a,b,I,J)),P,s)) . d = (IExec (I,P,s)) . d )assume A8:
a <> d
;
(IExec ((if=0 (a,b,I,J)),P,s)) . d = (IExec (I,P,s)) . dthus (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 A7, Th12
.=
(IExec (I,P,s)) . d
by A1, A3, A4, A6, A8, Th25
;
verum
end; let f be
FinSeq-Location ;
(IExec ((if=0 (a,b,I,J)),P,s)) . f = (IExec (I,P,s)) . fthus (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 A7, Th12
.=
(IExec (I,P,s)) . f
by A1, A3, A4, A6, Th25
;
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
; ( ( 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:
(s . a) + (- (s . b)) <> (s . b) + (- (s . b))
;
hereby 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;
( a <> d implies (IExec ((if=0 (a,b,I,J)),P,s)) . d = (IExec (J,P,s)) . d )assume A12:
a <> d
;
(IExec ((if=0 (a,b,I,J)),P,s)) . d = (IExec (J,P,s)) . dthus (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 A9, A11, Th12
.=
(IExec (J,P,s)) . d
by A2, A3, A4, A10, A12, Th25
;
verum
end;
let f be FinSeq-Location ; (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 A9, A11, Th12
.=
(IExec (J,P,s)) . f
by A2, A3, A4, A10, Th25
; verum