set D = Int-Locations \/ FinSeq-Locations ;
set A = NAT ;
let s be State of SCM+FSA ; :: thesis: for I being parahalting good Program of SCM+FSA
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 SCM+FSA ; :: thesis: 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 ; :: thesis: ( 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)) ) )
assume A1:
I does_not_destroy a
; :: thesis: ( 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)) ) )
assume A2:
s . a > 0
; :: thesis: ( (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 )));
A3:
( (Initialize s) . (intloc 0 ) = 1 & (Initialize s) . a > 0 )
by A2, SCMFSA6C:3;
then consider s2 being State of SCM+FSA , k being Element of NAT such that
A4:
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
A5:
(Computation s2,k) . a = ((Initialize s) . a) - 1
and
A6:
(Computation s2,k) . (intloc 0 ) = 1
and
A7:
for b being read-write Int-Location st b <> a holds
(Computation s2,k) . b = (IExec I,(Initialize s)) . b
and
A8:
for f being FinSeq-Location holds (Computation s2,k) . f = (IExec I,(Initialize s)) . f
and
A9:
IC (Computation s2,k) = insloc 0
and
A10:
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 A1, Th122;
A11:
I is_halting_on Initialize s
by SCMFSA7B:25;
hereby :: thesis: DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s))
thus (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 A11, Th92
.=
((Initialize s) . a) - 1
by A1, Th91
.=
(s . a) - 1
by SCMFSA6C:3
;
:: thesis: verum
end;
A13:
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 A14:
Directed (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) is_pseudo-closed_on Initialize s
by A1, A3, Th117;
A15:
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 A1, A3, A13, Th69, Th117;
reconsider J3 = Macro (SubFrom a,(intloc 0 )) as good Program of SCM+FSA by Th99, SCMFSA7B:14;
I ';' (SubFrom a,(intloc 0 )) = I ';' J3
;
then A16:
( I ';' (SubFrom a,(intloc 0 )) is good Program of SCM+FSA & I ';' (SubFrom a,(intloc 0 )) is_halting_on Initialize s & I ';' (SubFrom a,(intloc 0 )) is_closed_on Initialize s )
by SCMFSA7B:24, SCMFSA7B:25;
then A17:
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . (intloc 0 ) = 1
by Th96;
A18:
now let b be
Int-Location ;
:: thesis: (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 A19:
(
b <> a &
b <> intloc 0 )
;
:: thesis: (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 A7, A19
.=
(Exec (SubFrom a,(intloc 0 )),(IExec I,(Initialize s))) . b
by A19, 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
;
:: thesis: verum end; end;
now let f be
FinSeq-Location ;
:: thesis: (Computation s2,k) . f = (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . fthus (Computation s2,k) . f =
(IExec I,(Initialize s)) . f
by A8
.=
(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
;
:: thesis: verum end;
then A20:
DataPart (Computation s2,k) = DataPart (IExec (I ';' (SubFrom a,(intloc 0 ))),s)
by A18, SCMFSA6A:38;
A21:
loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on Initialize s
by A1, A3, Th117;
insloc 0 in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))
by Th54;
then A22:
insloc 0 in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by FUNCT_4:105;
per cases
( (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a = 0 or (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a <> 0 )
;
suppose A23:
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a = 0
;
:: thesis: 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 A24:
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;
A25:
(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 A4, A22, A24, FUNCT_4:14
.=
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) . (insloc 0 )
by A22, SCMFSA6B:7
;
A26:
(Computation s2,k) . a = 0
by A5, A12, A23, SCMFSA6C:3;
A27:
Computation s2,
(k + 1) =
Following (Computation s2,k)
by AMI_1:14
.=
Exec ((Computation s2,k) . (insloc 0 )),
(Computation s2,k)
by A9
;
A28:
(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 &
insloc 0 in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) )
by Th54, SCMFSA_2:48, SCMFSA_2:124;
then A29:
(Computation s2,k) . (insloc 0 ) = a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))
by A25, A28, FUNCT_4:111;
then
InsCode ((Computation s2,k) . (insloc 0 )) = 7
by SCMFSA_2:48;
then
InsCode ((Computation s2,k) . (insloc 0 )) in {0 ,6,7,8}
by ENUMSET1:def 2;
then A30:
DataPart (Computation s2,k) = DataPart (Computation s2,(k + 1))
by A27, Th32;
A31:
IC (Computation s2,(k + 1)) = insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)
by A26, A27, A29, SCMFSA_2:96;
A32:
(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 A33:
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;
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 A34:
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;
A35:
(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 A4, A33, A34, FUNCT_4:14
.=
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))
by A33, SCMFSA6B:7
;
A36:
(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
(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;
then A37:
(Computation s2,(k + 1)) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)) = goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 5))
by A35, A36, FUNCT_4:111;
A38:
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 A26, A27, A29, SCMFSA_2:96
;
then A39:
IC (Computation s2,(k + 2)) =
insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 5)
by A37, SCMFSA_2:95
.=
insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))
by A32, AMI_1:105
;
now let n be
Element of
NAT ;
:: thesis: ( 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 A40:
not
IC (Computation s2,n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
;
:: thesis: k + (1 + 1) <= nthen
k < n
by A10;
then
k + 1
<= n
by INT_1:20;
then
k + 1
< n
by A31, A33, A40, XXREAL_0:1;
then
(k + 1) + 1
<= n
by INT_1:20;
hence
k + (1 + 1) <= n
;
:: thesis: verum end; then A41:
k + 2
= pseudo-LifeSpan (Initialize s),
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A4, A21, A39, SCMFSA8A:def 5;
InsCode ((Computation s2,(k + 1)) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) = 6
by A37, SCMFSA_2:47;
then
InsCode ((Computation s2,(k + 1)) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) in {0 ,6,7,8}
by ENUMSET1:def 2;
then A42:
DataPart (Computation s2,k) = DataPart (Computation s2,(k + 2))
by A30, A38, 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 A15, 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 A1, A3, A4, A13, A20, A41, A42, Th59, Th117
.=
DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s))
by A17, A23, Th123
;
:: thesis: verum end; suppose A43:
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a <> 0
;
:: thesis: DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s))
s . a >= 0 + 1
by A2, INT_1:20;
then A44:
(
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . (intloc 0 ) = 1 &
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a > 0 )
by A12, A16, A43, Th96, XREAL_1:21;
A45:
k < pseudo-LifeSpan (Initialize s),
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A4, A10, A1, A3, Th117, Th2;
then A46:
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 A4, A13, A14, A20, Th58;
A47:
now A48:
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 :: thesis: 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 ;
:: thesis: (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 A49:
a = intloc 0
;
:: thesis: (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 A46, SCMFSA6A:38
.=
1
by A49, SCMFSA6B:35
.=
(Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) . a
by A49, 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 A48, SCMFSA6A:38
;
:: thesis: verum end; suppose
a <> intloc 0
;
:: thesis: (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 A50:
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 A46, SCMFSA6A:38
.=
(Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) . a
by A50, 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 A48, SCMFSA6A:38
;
:: thesis: verum end;
end; let f be
FinSeq-Location ;
:: thesis: (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 A46, 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 A48, SCMFSA6A:38
;
:: thesis: verum end;
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
(
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 )))) &
Directed (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) is_pseudo-closed_on Initialize s )
by A1, A3, Th117, SCMFSA8A:11;
then
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 Th52;
then A51:
(
((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 ))) &
((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 ))) &
(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 ))) &
(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 Th58, FUNCT_4:26;
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 A4, A13, A14, A45, 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 A9, 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 A52:
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 A47, SCMFSA6A:28;
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 A51, A52, 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 A1, A13, A44, Th69, Th117
;
hence
DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s))
by A15, Th17;
:: thesis: verum end;