let s be State of SCM+FSA ; 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 ; 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)) ) )
assume A1:
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)) ) )
reconsider J3 = Macro (SubFrom a,(intloc 0 )) as good Program of SCM+FSA by SCMFSA7B:14, SCMFSA8C:99;
set I1 = I ';' (SubFrom a,(intloc 0 ));
set ss = IExec (I ';' (SubFrom a,(intloc 0 ))),s;
I ';' (SubFrom a,(intloc 0 )) is_closed_onInit s
by Th35;
then A2:
I ';' (SubFrom a,(intloc 0 )) is_closed_on Initialize s
by Th40;
I ';' (SubFrom a,(intloc 0 )) is_halting_onInit s
by Th36;
then A3:
( I ';' (SubFrom a,(intloc 0 )) = I ';' J3 & I ';' (SubFrom a,(intloc 0 )) is_halting_on Initialize s )
by Th41;
then A4:
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . (intloc 0 ) = 1
by A2, SCMFSA8C:96;
set P = if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )));
set s0 = Initialize s;
assume A5:
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 A6:
(Initialize s) . a > 0
by SCMFSA6C:3;
then consider s2 being State of SCM+FSA , k being Element of NAT such that
A7:
s2 = (Initialize s) +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))
and
k = (LifeSpan ((Initialize s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1
and
A8:
(Comput (ProgramPart s2),s2,k) . a = ((Initialize s) . a) - 1
and
A9:
(Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1
and
A10:
for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,(Initialize s)) . b
and
A11:
for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,(Initialize s)) . f
and
A12:
IC (Comput (ProgramPart s2),s2,k) = 0
and
A13:
for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
by A1, Th77;
A14: s2 =
(Initialize (Initialize s)) +* ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA ))
by A7, SCMFSA8A:13
.=
(Initialize s) +* ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA ))
by SCMFSA8C:15
;
A15:
now let f be
FinSeq-Location ;
(Comput (ProgramPart s2),s2,k) . f = (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . fthus (Comput (ProgramPart s2),s2,k) . f =
(IExec I,(Initialize s)) . f
by A11
.=
(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
;
verum end;
thus A16: (IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a =
(Exec (SubFrom a,(intloc 0 )),(IExec I,s)) . a
by Th33
.=
((IExec I,s) . a) - ((IExec I,s) . (intloc 0 ))
by SCMFSA_2:91
.=
((IExec I,s) . a) - 1
by Th17
.=
((Initialize s) . a) - 1
by A1, Th63
.=
(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 ;
(Comput (ProgramPart s2),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 A17:
(
b <> a &
b <> intloc 0 )
;
(Comput (ProgramPart s2),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 (Comput (ProgramPart s2),s2,k) . b =
(IExec I,(Initialize s)) . bb
by A10, A17
.=
(Exec (SubFrom a,(intloc 0 )),(IExec I,(Initialize s))) . b
by A17, 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
;
verum end; end;
then A18:
DataPart (Comput (ProgramPart s2),s2,k) = DataPart (IExec (I ';' (SubFrom a,(intloc 0 ))),s)
by A15, SCMFSA6A:38;
set s21 = (Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ));
set ss0 = Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s);
set s31 = (Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ));
0 in dom (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))
by SCMFSA8C:54;
then A19:
0 in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
by FUNCT_4:105;
A20:
(Initialize s) . (intloc 0 ) = 1
by SCMFSA6C:3;
then A21:
loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on Initialize s
by A1, A6, Th73;
A22:
Directed (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) = loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))
by SCMFSA6A:63;
then A23:
Directed (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) is_pseudo-closed_on Initialize s
by A1, A20, A6, Th73;
A24:
DataPart (IExec (Times a,I),(Initialize s)) = DataPart (IExec ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )),(Initialize s))
by A1, A20, A6, A22, Th73, SCMFSA8C:69;
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
;
DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s))
loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) c= (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA )
by SCMFSA8A:9;
then A26:
dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) c= dom ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA ))
by GRFUNC_1:8;
A27:
(if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . ((card (I ';' (SubFrom a,(intloc 0 )))) + 3) = goto ((card (I ';' (SubFrom a,(intloc 0 )))) + 5)
by SCMFSA8C:65;
then A28:
(if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . ((card (I ';' (SubFrom a,(intloc 0 )))) + 3) <> halt SCM+FSA
by SCMFSA_2:47, SCMFSA_2:124;
A29:
(card (I ';' (SubFrom a,(intloc 0 )))) + (3 + 2) =
((card (I ';' (SubFrom a,(intloc 0 )))) + 1) + 4
.=
((card (Goto 2)) + (card (I ';' (SubFrom a,(intloc 0 ))))) + 4
by SCMFSA8A:29
.=
card (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))
by SCMFSA8B:14
.=
card (dom (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
by CARD_1:104
.=
card (dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))
by FUNCT_4:105
.=
card (loop (if=0 a,(Goto 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 2),(I ';' (SubFrom a,(intloc 0 )))))
by XREAL_1:8;
then A30:
(card (I ';' (SubFrom a,(intloc 0 )))) + 3
in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
by SCMFSA6A:15;
(Comput (ProgramPart s2),s2,(k + 1)) . ((card (I ';' (SubFrom a,(intloc 0 )))) + 3) =
s2 . ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)
by AMI_1:54
.=
((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA )) . ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)
by A14, A30, A26, FUNCT_4:14
.=
(loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) . ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)
by A30, SCMFSA6B:7
;
then A31:
(Comput (ProgramPart s2),s2,(k + 1)) . ((card (I ';' (SubFrom a,(intloc 0 )))) + 3) = goto ((card (I ';' (SubFrom a,(intloc 0 )))) + 5)
by A27, A28, FUNCT_4:111;
loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) c= (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA )
by SCMFSA8A:9;
then A32:
dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) c= dom ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA ))
by GRFUNC_1:8;
A33:
(Comput (ProgramPart s2),s2,k) . 0 =
s2 . 0
by AMI_1:54
.=
((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA )) . 0
by A14, A19, A32, FUNCT_4:14
.=
(loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) . 0
by A19, SCMFSA6B:7
;
Y:
(ProgramPart (Comput (ProgramPart s2),s2,k)) /. (IC (Comput (ProgramPart s2),s2,k)) = (Comput (ProgramPart s2),s2,k) . (IC (Comput (ProgramPart s2),s2,k))
by AMI_1:150;
T:
ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,k)
by AMI_1:144;
A34:
Comput (ProgramPart s2),
s2,
(k + 1) =
Following (ProgramPart s2),
(Comput (ProgramPart s2),s2,k)
by AMI_1:14
.=
Exec ((Comput (ProgramPart s2),s2,k) . 0 ),
(Comput (ProgramPart s2),s2,k)
by A12, Y, T
;
A35:
(if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . 0 = a =0_goto ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)
by SCMFSA8C:55;
then
(if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . 0 <> halt SCM+FSA
by SCMFSA_2:48, SCMFSA_2:124;
then A36:
(Comput (ProgramPart s2),s2,k) . 0 = a =0_goto ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)
by A33, A35, FUNCT_4:111;
then
InsCode ((Comput (ProgramPart s2),s2,k) . 0 ) = 7
by SCMFSA_2:48;
then
InsCode ((Comput (ProgramPart s2),s2,k) . 0 ) in {0 ,6,7,8}
by ENUMSET1:def 2;
then A37:
DataPart (Comput (ProgramPart s2),s2,k) = DataPart (Comput (ProgramPart s2),s2,(k + 1))
by A34, SCMFSA8C:32;
A38:
(Comput (ProgramPart s2),s2,k) . a = 0
by A8, A16, A25, SCMFSA6C:3;
then A39:
IC (Comput (ProgramPart s2),s2,(k + 1)) = (card (I ';' (SubFrom a,(intloc 0 )))) + 3
by A34, A36, SCMFSA_2:96;
A40:
now let n be
Element of
NAT ;
( not IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) implies k + (1 + 1) <= n )assume A41:
not
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
;
k + (1 + 1) <= nthen
k < n
by A13;
then
k + 1
<= n
by INT_1:20;
then
k + 1
< n
by A39, A30, A41, XXREAL_0:1;
then
(k + 1) + 1
<= n
by INT_1:20;
hence
k + (1 + 1) <= n
;
verum end; Y:
(ProgramPart (Comput (ProgramPart s2),s2,(k + 1))) /. (IC (Comput (ProgramPart s2),s2,(k + 1))) = (Comput (ProgramPart s2),s2,(k + 1)) . (IC (Comput (ProgramPart s2),s2,(k + 1)))
by AMI_1:150;
T:
ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,(k + 1))
by AMI_1:144;
A42:
Comput (ProgramPart s2),
s2,
(k + (1 + 1)) =
Comput (ProgramPart s2),
s2,
((k + 1) + 1)
.=
Following (ProgramPart s2),
(Comput (ProgramPart s2),s2,(k + 1))
by AMI_1:14
.=
Exec ((Comput (ProgramPart s2),s2,(k + 1)) . ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)),
(Comput (ProgramPart s2),s2,(k + 1))
by A38, A34, A36, SCMFSA_2:96, Y, T
;
then IC (Comput (ProgramPart s2),s2,(k + 2)) =
(card (I ';' (SubFrom a,(intloc 0 )))) + 5
by A31, SCMFSA_2:95
.=
card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))
by A29, AMI_1:105
;
then A43:
k + 2
= pseudo-LifeSpan (Initialize s),
(loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
by A14, A21, A40, SCMFSA8A:def 5;
InsCode ((Comput (ProgramPart s2),s2,(k + 1)) . ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)) = 6
by A31, SCMFSA_2:47;
then
InsCode ((Comput (ProgramPart s2),s2,(k + 1)) . ((card (I ';' (SubFrom a,(intloc 0 )))) + 3)) in {0 ,6,7,8}
by ENUMSET1:def 2;
then A44:
DataPart (Comput (ProgramPart s2),s2,k) = DataPart (Comput (ProgramPart s2),s2,(k + 2))
by A37, A42, 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 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )),s)
by A24, SCMFSA8C:17
.=
DataPart ((Result (s +* (Initialized ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA ))))) +* (s | NAT ))
by SCMFSA6B:def 1
.=
DataPart ((Result ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) +* (s | NAT ))
by SCMFSA8A:13
.=
DataPart (Result ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))))
by SCMFSA8C:35
.=
DataPart (IExec (I ';' (SubFrom a,(intloc 0 ))),s)
by A1, A20, A6, A14, A22, A18, A43, A44, Th73, SCMFSA8C:59
.=
DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s))
by A4, A25, Th78
;
verum end; suppose A45:
(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 A5, INT_1:20;
then A46:
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a > 0
by A16, A45, XREAL_1:21;
A47:
(
((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ) c= (Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) &
((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ) c= (Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) )
by FUNCT_4:26;
A48:
k < pseudo-LifeSpan (Initialize s),
(loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
by A1, A20, A6, A13, A14, Th73, SCMFSA8C:2;
then A49:
DataPart (Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) = DataPart (IExec (I ';' (SubFrom a,(intloc 0 ))),s)
by A14, A22, A23, A18, SCMFSA8C:58;
A50:
now A51:
DataPart (Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) = DataPart ((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))
by SCMFSA8A:11;
hereby for f being FinSeq-Location holds (Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) . f = ((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) . f
let a be
Int-Location ;
(Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) . b1 = ((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) . b1per cases
( a = intloc 0 or a <> intloc 0 )
;
suppose A52:
a = intloc 0
;
(Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) . b1 = ((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) . b1thus (Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) . a =
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a
by A49, SCMFSA6A:38
.=
1
by A52, Th17
.=
(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 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) . a
by A51, SCMFSA6A:38
;
verum end; suppose
a <> intloc 0
;
(Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) . b1 = ((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) . b1then A53:
a is
read-write Int-Location
by SF_MASTR:def 5;
thus (Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) . a =
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a
by A49, SCMFSA6A:38
.=
(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 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) . a
by A51, SCMFSA6A:38
;
verum end;
end; let f be
FinSeq-Location ;
(Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) . f = ((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) . fthus (Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) . f =
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . f
by A49, 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 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) . f
by A51, SCMFSA6A:38
;
verum end; IC (Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),k) =
IC (Comput (ProgramPart s2),s2,k)
by A14, A22, A23, A48, SCMFSA8C:58
.=
IC (((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA ))) +* (Start-At 0 ,SCM+FSA ))
by A12, AMI_1:111
.=
IC ((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))
by FUNCT_4:15
;
then A54:
Comput (ProgramPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))),
((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))),
k,
(Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) equal_outside NAT
by A50, SCMFSA6A:28;
A55:
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . (intloc 0 ) = 1
by A3, A2, SCMFSA8C:96;
(
Directed (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) = loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) &
DataPart (Initialize s) = DataPart ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))) )
by SCMFSA6A:63, SCMFSA8A:11;
then
Directed (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) is_pseudo-closed_on (Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))
by A1, A20, A6, Th73, SCMFSA8C:52;
then A56:
(
(loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA ) is_closed_on (Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) &
(loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA ) is_halting_on (Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )) )
by SCMFSA8C:58;
DataPart (IExec ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )),(Initialize s)) =
DataPart (IExec ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )),s)
by SCMFSA8C:17
.=
DataPart ((Result (s +* (Initialized ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA ))))) +* (s | NAT ))
by SCMFSA6B:def 1
.=
DataPart ((Result ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) +* (s | NAT ))
by SCMFSA8A:13
.=
DataPart (Result ((Initialize s) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))))
by SCMFSA8C:35
.=
DataPart (Result ((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA ))))
by A47, A56, A54, SCMFSA6A:39, SCMFSA8C:103
.=
DataPart ((Result ((Initialize (IExec (I ';' (SubFrom a,(intloc 0 ))),s)) +* (((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ';' (Stop SCM+FSA )) +* (Start-At 0 ,SCM+FSA )))) +* ((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 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 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, A22, A55, A46, Th73, SCMFSA8C:69
;
hence
DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s))
by A24, SCMFSA8C:17;
verum end;