let s be State of ; for I being parahalting good Program of
for a being read-write Int-Location st I does_not_destroy a & s . a > 0 holds
( (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a = (s . a) - 1 & DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s)) )
let I be parahalting good Program of ; for a being read-write Int-Location st I does_not_destroy a & s . a > 0 holds
( (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a = (s . a) - 1 & DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s)) )
let a be read-write Int-Location ; ( I does_not_destroy a & s . a > 0 implies ( (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a = (s . a) - 1 & DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s)) ) )
set I1 = I ';' (SubFrom a,(intloc 0 ));
set ss = IExec (I ';' (SubFrom a,(intloc 0 ))),s;
set s0 = Initialize s;
set ss0 = Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s);
set P = if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )));
set s21 = (Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )));
set s31 = (Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )));
A1:
I is_halting_on Initialize s
by SCMFSA7B:25;
A2:
I ';' (SubFrom a,(intloc 0 )) is_halting_on Initialize s
by SCMFSA7B:25;
reconsider J3 = Macro (SubFrom a,(intloc 0 )) as good Program of by Th99, SCMFSA7B:14;
set D = Int-Locations \/ FinSeq-Locations ;
set A = NAT ;
assume A3:
I does_not_destroy a
; ( not s . a > 0 or ( (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a = (s . a) - 1 & DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s)) ) )
insloc 0 in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))
by Th54;
then A4:
insloc 0 in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by FUNCT_4:105;
A5:
I ';' (SubFrom a,(intloc 0 )) is_closed_on Initialize s
by SCMFSA7B:24;
A6:
I ';' (SubFrom a,(intloc 0 )) = I ';' J3
;
then A7:
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . (intloc 0 ) = 1
by A2, A5, Th96;
assume A8:
s . a > 0
; ( (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a = (s . a) - 1 & DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s)) )
then A9:
(Initialize s) . a > 0
by SCMFSA6C:3;
A10:
(Initialize s) . (intloc 0 ) = 1
by SCMFSA6C:3;
then A11:
loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on Initialize s
by A3, A9, Th117;
A12:
Directed (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) = loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))
by SCMFSA6A:63;
then A13:
Directed (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) is_pseudo-closed_on Initialize s
by A3, A10, A9, Th117;
consider s2 being State of , k being Element of NAT such that
A14:
s2 = (Initialize s) +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))
and
k = (LifeSpan ((Initialize s) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1
and
A15:
(Computation s2,k) . a = ((Initialize s) . a) - 1
and
A16:
(Computation s2,k) . (intloc 0 ) = 1
and
A17:
for b being read-write Int-Location st b <> a holds
(Computation s2,k) . b = (IExec I,(Initialize s)) . b
and
A18:
for f being FinSeq-Location holds (Computation s2,k) . f = (IExec I,(Initialize s)) . f
and
A19:
IC (Computation s2,k) = insloc 0
and
A20:
for n being Element of NAT st n <= k holds
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A3, A10, A9, Th122;
A21:
now let f be
FinSeq-Location ;
(Computation s2,k) . f = (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . fthus (Computation s2,k) . f =
(IExec I,(Initialize s)) . f
by A18
.=
(Exec (SubFrom a,(intloc 0 )),(IExec I,(Initialize s))) . f
by SCMFSA_2:91
.=
(IExec (I ';' (SubFrom a,(intloc 0 ))),(Initialize s)) . f
by SCMFSA6C:8
.=
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . f
by Th17
;
verum end;
thus A22: (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a =
(Exec (SubFrom a,(intloc 0 )),(IExec I,s)) . a
by SCMFSA6C:7
.=
((IExec I,s) . a) - ((IExec I,s) . (intloc 0 ))
by SCMFSA_2:91
.=
((IExec I,s) . a) - 1
by A1, Th92
.=
((Initialize s) . a) - 1
by A3, Th91
.=
(s . a) - 1
by SCMFSA6C:3
; DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s))
now let b be
Int-Location ;
(Computation s2,k) . b1 = (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . b1per cases
( b = intloc 0 or b = a or ( b <> a & b <> intloc 0 ) )
;
suppose A23:
(
b <> a &
b <> intloc 0 )
;
(Computation s2,k) . b1 = (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . b1then reconsider bb =
b as
read-write Int-Location by SF_MASTR:def 5;
thus (Computation s2,k) . b =
(IExec I,(Initialize s)) . bb
by A17, A23
.=
(Exec (SubFrom a,(intloc 0 )),(IExec I,(Initialize s))) . b
by A23, SCMFSA_2:91
.=
(IExec (I ';' (SubFrom a,(intloc 0 ))),(Initialize s)) . b
by SCMFSA6C:7
.=
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . b
by Th17
;
verum end; end;
then A24:
DataPart (Computation s2,k) = DataPart (IExec (I ';' (SubFrom a,(intloc 0 ))),s)
by A21, SCMFSA6A:38;
A25:
DataPart (IExec (Times a,I),(Initialize s)) = DataPart (IExec ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )),(Initialize s))
by A3, A10, A9, A12, Th69, Th117;
per cases
( (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a = 0 or (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a <> 0 )
;
suppose A26:
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a = 0
;
DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s))
loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) c= (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))
by SCMFSA8A:9;
then A27:
dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) c= dom ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))
by GRFUNC_1:8;
A28:
(if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)) = goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 5))
by Th65;
then A29:
(if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)) <> halt SCM+FSA
by SCMFSA_2:47, SCMFSA_2:124;
A30:
(card (I ';' (SubFrom a,(intloc 0 )))) + (3 + 2) =
((card (I ';' (SubFrom a,(intloc 0 )))) + 1) + 4
.=
((card (Goto (insloc 2))) + (card (I ';' (SubFrom a,(intloc 0 ))))) + 4
by SCMFSA8A:29
.=
card (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))
by SCMFSA8B:14
.=
card (dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by CARD_1:104
.=
card (dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))
by FUNCT_4:105
.=
card (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by CARD_1:104
;
then
((card (I ';' (SubFrom a,(intloc 0 )))) + 3) + 0 < card (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by XREAL_1:8;
then A31:
insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by SCMFSA6A:15;
(Computation s2,(k + 1)) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)) =
s2 . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))
by AMI_1:54
.=
((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))
by A14, A31, A27, FUNCT_4:14
.=
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))
by A31, SCMFSA6B:7
;
then A32:
(Computation s2,(k + 1)) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)) = goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 5))
by A28, A29, FUNCT_4:111;
then
InsCode ((Computation s2,(k + 1)) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) = 6
by SCMFSA_2:47;
then A33:
InsCode ((Computation s2,(k + 1)) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) in {0 ,6,7,8}
by ENUMSET1:def 2;
A34:
Computation s2,
(k + 1) =
Following (Computation s2,k)
by AMI_1:14
.=
Exec ((Computation s2,k) . (insloc 0 )),
(Computation s2,k)
by A19
;
loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) c= (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))
by SCMFSA8A:9;
then A35:
dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) c= dom ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))
by GRFUNC_1:8;
A36:
(Computation s2,k) . (insloc 0 ) =
s2 . (insloc 0 )
by AMI_1:54
.=
((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))) . (insloc 0 )
by A14, A4, A35, FUNCT_4:14
.=
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) . (insloc 0 )
by A4, SCMFSA6B:7
;
A37:
(if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc 0 ) = a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))
by Th55;
then
(if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc 0 ) <> halt SCM+FSA
by SCMFSA_2:48, SCMFSA_2:124;
then A38:
(Computation s2,k) . (insloc 0 ) = a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))
by A36, A37, FUNCT_4:111;
A39:
(Computation s2,k) . a = 0
by A15, A22, A26, SCMFSA6C:3;
then A40:
IC (Computation s2,(k + 1)) = insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)
by A34, A38, SCMFSA_2:96;
A41:
now let n be
Element of
NAT ;
( not IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) implies k + (1 + 1) <= n )assume A42:
not
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
;
k + (1 + 1) <= nthen
k < n
by A20;
then
k + 1
<= n
by INT_1:20;
then
k + 1
< n
by A40, A31, A42, XXREAL_0:1;
then
(k + 1) + 1
<= n
by INT_1:20;
hence
k + (1 + 1) <= n
;
verum end; A43:
Computation s2,
(k + (1 + 1)) =
Computation s2,
((k + 1) + 1)
.=
Following (Computation s2,(k + 1))
by AMI_1:14
.=
Exec ((Computation s2,(k + 1)) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))),
(Computation s2,(k + 1))
by A39, A34, A38, SCMFSA_2:96
;
then IC (Computation s2,(k + 2)) =
insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 5)
by A32, SCMFSA_2:95
.=
insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))
by A30, AMI_1:105
;
then A44:
k + 2
= pseudo-LifeSpan (Initialize s),
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A14, A11, A41, SCMFSA8A:def 5;
InsCode ((Computation s2,k) . (insloc 0 )) = 7
by A38, SCMFSA_2:48;
then
InsCode ((Computation s2,k) . (insloc 0 )) in {0 ,6,7,8}
by ENUMSET1:def 2;
then
DataPart (Computation s2,k) = DataPart (Computation s2,(k + 1))
by A34, Th32;
then A45:
DataPart (Computation s2,k) = DataPart (Computation s2,(k + 2))
by A43, A33, Th32;
thus DataPart (IExec (Times a,I),s) =
DataPart (IExec (Times a,I),(Initialize s))
by Th17
.=
DataPart (IExec ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )),s)
by A25, Th17
.=
DataPart ((Result (s +* (Initialized ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA ))))) +* (s | NAT ))
by SCMFSA6B:def 1
.=
DataPart ((Result ((Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) +* (s | NAT ))
by SCMFSA8A:13
.=
DataPart (Result ((Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))))
by Th35
.=
DataPart (IExec (I ';' (SubFrom a,(intloc 0 ))),s)
by A3, A10, A9, A14, A12, A24, A44, A45, Th59, Th117
.=
DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s))
by A7, A26, Th123
;
verum end; suppose A46:
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a <> 0
;
DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s))
s . a >= 0 + 1
by A8, INT_1:20;
then A47:
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a > 0
by A22, A46, XREAL_1:21;
A48:
DataPart (Initialize s) = DataPart ((Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))
by SCMFSA8A:11;
A49:
k < pseudo-LifeSpan (Initialize s),
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A3, A10, A9, A14, A20, Th2, Th117;
then A50:
DataPart (Computation ((Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) = DataPart (IExec (I ';' (SubFrom a,(intloc 0 ))),s)
by A14, A12, A13, A24, Th58;
A51:
now A52:
DataPart (Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) = DataPart ((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))
by SCMFSA8A:11;
hereby for f being FinSeq-Location holds (Computation ((Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) . f = ((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . f
let a be
Int-Location ;
(Computation ((Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) . b1 = ((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . b1per cases
( a = intloc 0 or a <> intloc 0 )
;
suppose A53:
a = intloc 0
;
(Computation ((Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) . b1 = ((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . b1thus (Computation ((Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) . a =
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a
by A50, SCMFSA6A:38
.=
1
by A53, SCMFSA6B:35
.=
(Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) . a
by A53, SCMFSA6C:3
.=
((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . a
by A52, SCMFSA6A:38
;
verum end; suppose
a <> intloc 0
;
(Computation ((Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) . b1 = ((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . b1then A54:
a is
read-write Int-Location
by SF_MASTR:def 5;
thus (Computation ((Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) . a =
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a
by A50, SCMFSA6A:38
.=
(Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) . a
by A54, SCMFSA6C:3
.=
((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . a
by A52, SCMFSA6A:38
;
verum end;
end; let f be
FinSeq-Location ;
(Computation ((Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) . f = ((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . fthus (Computation ((Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) . f =
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . f
by A50, SCMFSA6A:38
.=
(Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) . f
by SCMFSA6C:3
.=
((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))) . f
by A52, SCMFSA6A:38
;
verum end; IC (Computation ((Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),k) =
IC (Computation s2,k)
by A14, A12, A13, A49, Th58
.=
IC (((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA ))) +* (Start-At (insloc 0 )))
by A19, AMI_1:111
.=
IC ((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))
by FUNCT_4:15
;
then A55:
Computation ((Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))),
k,
(Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))) equal_outside NAT
by A51, SCMFSA6A:28;
A56:
((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )) c= (Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))
by FUNCT_4:26;
Directed (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) = loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))
by SCMFSA6A:63;
then A57:
Directed (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) is_pseudo-closed_on (Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))
by A3, A10, A9, A48, Th52, Th117;
then A58:
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA ) is_closed_on (Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))
by Th58;
A59:
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA ) is_halting_on (Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))
by A57, Th58;
A60:
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . (intloc 0 ) = 1
by A6, A2, A5, Th96;
A61:
((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )) c= (Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))
by FUNCT_4:26;
DataPart (IExec ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )),(Initialize s)) =
DataPart (IExec ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )),s)
by Th17
.=
DataPart ((Result (s +* (Initialized ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA ))))) +* (s | NAT ))
by SCMFSA6B:def 1
.=
DataPart ((Result ((Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) +* (s | NAT ))
by SCMFSA8A:13
.=
DataPart (Result ((Initialize s) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))))
by Th35
.=
DataPart (Result ((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 )))))
by A56, A61, A58, A59, A55, Th103, SCMFSA6A:39
.=
DataPart ((Result ((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At (insloc 0 ))))) +* ((IExec (I ';' (SubFrom a,(intloc 0 ))),s) | NAT ))
by Th35
.=
DataPart ((Result ((IExec (I ';' (SubFrom a,(intloc 0 ))),s) +* (Initialized ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA ))))) +* ((IExec (I ';' (SubFrom a,(intloc 0 ))),s) | NAT ))
by SCMFSA8A:13
.=
DataPart (IExec ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )),(IExec (I ';' (SubFrom a,(intloc 0 ))),s))
by SCMFSA6B:def 1
.=
DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s))
by A3, A12, A60, A47, Th69, Th117
;
hence
DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s))
by A25, Th17;
verum end;