let s be State of SCM+FSA ; :: thesis: for I being good InitHalting 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 good InitHalting 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 )));
A4:
( (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
A5:
s2 = (Initialize s) +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))
and
k = (LifeSpan ((Initialize s) +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1
and
A6:
(Computation s2,k) . a = ((Initialize s) . a) - 1
and
A7:
(Computation s2,k) . (intloc 0 ) = 1
and
A8:
for b being read-write Int-Location st b <> a holds
(Computation s2,k) . b = (IExec I,(Initialize s)) . b
and
A9:
for f being FinSeq-Location holds (Computation s2,k) . f = (IExec I,(Initialize s)) . f
and
A10:
IC (Computation s2,k) = insloc 0
and
A11:
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, Th77;
A12: s2 =
(Initialize (Initialize s)) +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))
by A5, SCMFSA8A:13
.=
(Initialize s) +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))
by SCMFSA8C:15
;
A14:
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 A15:
Directed (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) is_pseudo-closed_on Initialize s
by A1, A4, Th73;
A16:
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, A4, A14, Th73, SCMFSA8C:69;
reconsider J3 = Macro (SubFrom a,(intloc 0 )) as good Program of SCM+FSA by SCMFSA7B:14, SCMFSA8C:99;
A17:
I ';' (SubFrom a,(intloc 0 )) = I ';' J3
;
( I ';' (SubFrom a,(intloc 0 )) is_halting_onInit s & I ';' (SubFrom a,(intloc 0 )) is_closed_onInit s )
by Th35, Th36;
then A18:
( I ';' (SubFrom a,(intloc 0 )) is_halting_on Initialize s & I ';' (SubFrom a,(intloc 0 )) is_closed_on Initialize s )
by Th40, Th41;
then A19:
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . (intloc 0 ) = 1
by A17, SCMFSA8C:96;
A20:
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 A21:
(
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 A8, A21
.=
(Exec (SubFrom a,(intloc 0 )),(IExec I,(Initialize s))) . b
by A21, SCMFSA_2:91
.=
(IExec (I ';' (SubFrom a,(intloc 0 ))),(Initialize s)) . b
by Th33
.=
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . b
by SCMFSA8C:17
;
:: 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 A9
.=
(Exec (SubFrom a,(intloc 0 )),(IExec I,(Initialize s))) . f
by SCMFSA_2:91
.=
(IExec (I ';' (SubFrom a,(intloc 0 ))),(Initialize s)) . f
by Th34
.=
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . f
by SCMFSA8C:17
;
:: thesis: verum end;
then A22:
DataPart (Computation s2,k) = DataPart (IExec (I ';' (SubFrom a,(intloc 0 ))),s)
by A20, SCMFSA6A:38;
A23:
loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on Initialize s
by A1, A4, Th73;
insloc 0 in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))
by SCMFSA8C:54;
then A24:
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 A25:
(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 A26:
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;
A27:
(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 A12, A24, A26, FUNCT_4:14
.=
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) . (insloc 0 )
by A24, SCMFSA6B:7
;
A28:
(Computation s2,k) . a = 0
by A6, A13, A25, SCMFSA6C:3;
A29:
Computation s2,
(k + 1) =
Following (Computation s2,k)
by AMI_1:14
.=
Exec ((Computation s2,k) . (insloc 0 )),
(Computation s2,k)
by A10
;
A30:
(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 SCMFSA8C:55;
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 SCMFSA8C:54, SCMFSA_2:48, SCMFSA_2:124;
then A31:
(Computation s2,k) . (insloc 0 ) = a =0_goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))
by A27, A30, 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 A32:
DataPart (Computation s2,k) = DataPart (Computation s2,(k + 1))
by A29, SCMFSA8C:32;
A33:
IC (Computation s2,(k + 1)) = insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)
by A28, A29, A31, SCMFSA_2:96;
A34:
(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 A35:
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 A36:
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;
A37:
(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 A12, A35, A36, FUNCT_4:14
.=
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))
by A35, SCMFSA6B:7
;
A38:
(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 SCMFSA8C:65;
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 A39:
(Computation s2,(k + 1)) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)) = goto (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 5))
by A37, A38, FUNCT_4:111;
A40:
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 A28, A29, A31, SCMFSA_2:96
;
then A41:
IC (Computation s2,(k + 2)) =
insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 5)
by A39, SCMFSA_2:95
.=
insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))
by A34, 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 A42:
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 A11;
then
k + 1
<= n
by INT_1:20;
then
k + 1
< n
by A33, A35, A42, XXREAL_0:1;
then
(k + 1) + 1
<= n
by INT_1:20;
hence
k + (1 + 1) <= n
;
:: thesis: verum end; then A43:
k + 2
= pseudo-LifeSpan (Initialize s),
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A12, A23, A41, SCMFSA8A:def 5;
InsCode ((Computation s2,(k + 1)) . (insloc ((card (I ';' (SubFrom a,(intloc 0 )))) + 3))) = 6
by A39, 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 A44:
DataPart (Computation s2,k) = DataPart (Computation s2,(k + 2))
by A32, A40, SCMFSA8C:32;
thus DataPart (IExec (Times a,I),s) =
DataPart (IExec (Times a,I),(Initialize s))
by SCMFSA8C:17
.=
DataPart (IExec ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )),s)
by A16, SCMFSA8C:17
.=
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 SCMFSA8C:35
.=
DataPart (IExec (I ';' (SubFrom a,(intloc 0 ))),s)
by A1, A4, A12, A14, A22, A43, A44, Th73, SCMFSA8C:59
.=
DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s))
by A19, A25, Th78
;
:: thesis: verum end; suppose A45:
(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 A46:
(
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . (intloc 0 ) = 1 &
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a > 0 )
by A13, A17, A18, A45, SCMFSA8C:96, XREAL_1:21;
A47:
k < pseudo-LifeSpan (Initialize s),
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A11, A12, A1, A4, Th73, SCMFSA8C:2;
then A48:
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 A12, A14, A15, A22, SCMFSA8C:58;
A49:
now A50:
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 A51:
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 A48, SCMFSA6A:38
.=
1
by A51, Th17
.=
(Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) . a
by A51, 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 A50, 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 A52:
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 A48, SCMFSA6A:38
.=
(Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) . a
by A52, 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 A50, 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 A48, 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 A50, 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, A4, Th73, 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 SCMFSA8C:52;
then A53:
(
((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 FUNCT_4:26, SCMFSA8C:58;
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 A12, A14, A15, A47, SCMFSA8C:58
.=
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 A10, 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 A54:
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 A49, 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 SCMFSA8C:17
.=
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 SCMFSA8C:35
.=
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 A53, A54, SCMFSA6A:39, SCMFSA8C:103
.=
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 SCMFSA8C:35
.=
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, A14, A46, Th73, SCMFSA8C:69
;
hence
DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s))
by A16, SCMFSA8C:17;
:: thesis: verum end;