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 . (intloc 0 ) = 1 & s . a > 0 holds
loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s
set A = NAT ;
let I be parahalting good Program of SCM+FSA ; :: thesis: for a being read-write Int-Location st I does_not_destroy a & s . (intloc 0 ) = 1 & s . a > 0 holds
loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s
let a be read-write Int-Location ; :: thesis: ( I does_not_destroy a & s . (intloc 0 ) = 1 & s . a > 0 implies loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s )
set P = if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )));
reconsider I1 = I ';' (SubFrom a,(intloc 0 )) as parahalting Program of SCM+FSA ;
set i = a =0_goto (insloc ((card I1) + 3));
defpred S1[ Element of NAT ] means for s being State of SCM+FSA st s . (intloc 0 ) = 1 & s . a = $1 & s . a > 0 holds
( (Computation (s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . a = (s . a) - 1 & (Computation (s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (s +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . (intloc 0 ) = 1 & ex k being Element of NAT st
( IC (Computation (s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),k) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < k holds
IC (Computation (s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) ) );
assume A1:
I does_not_destroy a
; :: thesis: ( not s . (intloc 0 ) = 1 or not s . a > 0 or loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s )
A2:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A3:
S1[
k]
;
:: thesis: S1[k + 1]
let ss be
State of
SCM+FSA ;
:: thesis: ( ss . (intloc 0 ) = 1 & ss . a = k + 1 & ss . a > 0 implies ( (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . a = (ss . a) - 1 & (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . (intloc 0 ) = 1 & ex k being Element of NAT st
( IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),k) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < k holds
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) ) ) )
assume A4:
ss . (intloc 0 ) = 1
;
:: thesis: ( not ss . a = k + 1 or not ss . a > 0 or ( (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . a = (ss . a) - 1 & (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . (intloc 0 ) = 1 & ex k being Element of NAT st
( IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),k) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < k holds
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) ) ) )
set s2 =
ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )));
set s1 =
ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )));
assume A5:
ss . a = k + 1
;
:: thesis: ( not ss . a > 0 or ( (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . a = (ss . a) - 1 & (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . (intloc 0 ) = 1 & ex k being Element of NAT st
( IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),k) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < k holds
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) ) ) )
set s3 =
Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),
((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1);
assume A6:
ss . a > 0
;
:: thesis: ( (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . a = (ss . a) - 1 & (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . (intloc 0 ) = 1 & ex k being Element of NAT st
( IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),k) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < k holds
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) ) )
A7:
Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),
((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) =
Following (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),(LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))))
by AMI_1:14
.=
Exec (CurInstr (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),(LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))))),
(Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),(LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))))
;
A8:
I1 is_halting_on ss
by SCMFSA7B:25;
A9:
I1 is_closed_on ss
by SCMFSA7B:24;
then A10:
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_closed_on ss
by A6, A8, SCMFSA8B:18;
A11:
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_halting_on ss
by A6, A9, A8, SCMFSA8B:18;
A12:
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_closed_on ss
by A6, A9, A8, SCMFSA8B:18;
then A13:
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) =
(Exec (goto (insloc 0 )),(Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),(LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))))) . (IC SCM+FSA )
by A11, A7, Lm2
.=
insloc 0
by SCMFSA_2:95
;
A14:
Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),
((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) = Exec (goto (insloc 0 )),
(Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),(LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))))
by A12, A11, A7, Lm2;
A15:
now A16:
I1 is_halting_on Initialize ss
by SCMFSA7B:25;
I1 is_closed_on Initialize ss
by SCMFSA7B:24;
then
IExec (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))),
ss = (IExec I1,ss) +* (Start-At (insloc (((card (Goto (insloc 2))) + (card I1)) + 3)))
by A6, A16, SCMFSA8B:19;
then A17:
(IExec (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))),ss) . a = (IExec I1,ss) . a
by SCMFSA_3:11;
A18:
card (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) =
((card (Goto (insloc 2))) + (card I1)) + 4
by SCMFSA8B:14
.=
((card I1) + 1) + 4
by SCMFSA8A:29
.=
((card I1) + 3) + 2
;
A19:
card (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) =
card (dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))
by CARD_1:104
.=
card (dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by FUNCT_4:105
.=
card (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))
by CARD_1:104
;
hereby :: thesis: ( intloc 0 in dom ss & (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . a = (ss . a) - 1 & (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . (intloc 0 ) = 1 )
thus
insloc 0 in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A19, A18, SCMFSA6A:15;
:: thesis: insloc ((card I1) + 3) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
((card I1) + 3) + (1 + 1) = (((card I1) + 3) + 1) + 1
;
then
((card I1) + 3) + 1
< card (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))
by A18, NAT_1:13;
then
(card I1) + 3
< card (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A19, NAT_1:13;
hence
insloc ((card I1) + 3) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by SCMFSA6A:15;
:: thesis: verum
end; A20:
dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) misses dom (Start-At (insloc 0 ))
by SF_MASTR:64;
thus
intloc 0 in dom ss
by SCMFSA_2:66;
:: thesis: ( (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . a = (ss . a) - 1 & (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . (intloc 0 ) = 1 )then A21:
ss +* ((intloc 0 ) .--> 1) = ss
by A4, FUNCT_7:111;
A22:
I1 is_closed_on Initialize ss
by SCMFSA7B:24;
A23:
I1 is_halting_on Initialize ss
by SCMFSA7B:25;
A24:
(Initialize ss) . a > 0
by A6, SCMFSA6C:3;
then A25:
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_halting_on Initialize ss
by A22, A23, SCMFSA8B:18;
A26:
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_closed_on Initialize ss
by A24, A22, A23, SCMFSA8B:18;
consider Is being
State of
SCM+FSA such that A27:
Is = (Initialize ss) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))
;
Initialize ss = (ss +* ((intloc 0 ) .--> 1)) +* (Start-At (insloc 0 ))
by SCMFSA6C:def 3;
then A28:
(Initialize ss) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))) =
(ss +* (Start-At (insloc 0 ))) +* ((Start-At (insloc 0 )) +* (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A21, A20, FUNCT_4:36
.=
((ss +* (Start-At (insloc 0 ))) +* (Start-At (insloc 0 ))) +* (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))
by FUNCT_4:15
.=
(ss +* ((Start-At (insloc 0 )) +* (Start-At (insloc 0 )))) +* (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))
by FUNCT_4:15
.=
ss +* ((Start-At (insloc 0 )) +* (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by FUNCT_4:15
.=
ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))
by A20, FUNCT_4:36
;
A29:
now let b be
Int-Location ;
:: thesis: (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . b = (Computation Is,(LifeSpan Is)) . b
(Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . b = (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),(LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))))) . b
by A14, SCMFSA_2:95;
hence
(Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . b = (Computation Is,(LifeSpan Is)) . b
by A11, A10, A28, A27, Th109, SCMFSA6A:30;
:: thesis: verum end; then (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . a =
(Computation Is,(LifeSpan Is)) . a
.=
(IExec (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))),ss) . a
by A27, A25, Th87
;
hence (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . a =
(Computation ((Initialize ss) +* (I1 +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize ss) +* (I1 +* (Start-At (insloc 0 )))))) . a
by A16, A17, Th87
.=
(ss . a) - 1
by A1, Th98
;
:: thesis: (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . (intloc 0 ) = 1A30:
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is
good
by Th115;
(Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . (intloc 0 ) =
(Computation Is,(LifeSpan Is)) . (intloc 0 )
by A29
.=
1
by A27, A25, A26, A30, Th96
;
hence
(Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . (intloc 0 ) = 1
;
:: thesis: verum end;
hence
(
(Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . a = (ss . a) - 1 &
(Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) . (intloc 0 ) = 1 )
;
:: thesis: ex k being Element of NAT st
( IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),k) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < k holds
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )
A31:
now
InsCode (a =0_goto (insloc ((card I1) + 3))) = 7
by SCMFSA_2:48;
then A32:
(Macro (a =0_goto (insloc ((card I1) + 3)))) . (insloc 0 ) <> halt SCM+FSA
by SCMFSA6B:33, SCMFSA_2:124;
A33:
insloc 0 in dom (Macro (a =0_goto (insloc ((card I1) + 3))))
by SCMFSA6B:32;
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) =
((((a =0_goto (insloc ((card I1) + 3))) ';' I1) ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))) ';' (Goto (insloc 2))) ';' (Stop SCM+FSA )
by SCMFSA8B:def 1
.=
(((a =0_goto (insloc ((card I1) + 3))) ';' (I1 ';' (Goto (insloc ((card (Goto (insloc 2))) + 1))))) ';' (Goto (insloc 2))) ';' (Stop SCM+FSA )
by SCMFSA6A:71
.=
((a =0_goto (insloc ((card I1) + 3))) ';' ((I1 ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))) ';' (Goto (insloc 2)))) ';' (Stop SCM+FSA )
by SCMFSA6A:71
.=
(a =0_goto (insloc ((card I1) + 3))) ';' (((I1 ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))) ';' (Goto (insloc 2))) ';' (Stop SCM+FSA ))
by SCMFSA6A:71
.=
(Macro (a =0_goto (insloc ((card I1) + 3)))) ';' (((I1 ';' (Goto (insloc ((card (Goto (insloc 2))) + 1)))) ';' (Goto (insloc 2))) ';' (Stop SCM+FSA ))
;
hence (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc 0 ) =
(Macro (a =0_goto (insloc ((card I1) + 3)))) . (insloc 0 )
by A33, A32, SCMFSA6A:54
.=
a =0_goto (insloc ((card I1) + 3))
by SCMFSA6B:33
;
:: thesis: ( (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 )))) & (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card I1) + 3)) = goto (insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))) & (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card I1) + 3)) <> halt SCM+FSA & insloc ((card I1) + 3) in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) )hence
(if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc 0 ) <> halt SCM+FSA
by SCMFSA_2:48, SCMFSA_2:124;
:: thesis: ( insloc 0 in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) & (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card I1) + 3)) = goto (insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))) & (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card I1) + 3)) <> halt SCM+FSA & insloc ((card I1) + 3) in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) )A34:
card (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) =
((card (Goto (insloc 2))) + (card I1)) + 4
by SCMFSA8B:14
.=
((card I1) + 1) + 4
by SCMFSA8A:29
.=
((card I1) + 3) + 2
;
hence
insloc 0 in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))
by SCMFSA6A:15;
:: thesis: ( (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card I1) + 3)) = goto (insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))) & (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card I1) + 3)) <> halt SCM+FSA & insloc ((card I1) + 3) in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) ) card (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) =
card (dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))
by CARD_1:104
.=
card (dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by FUNCT_4:105
.=
card (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))
by CARD_1:104
;
then
card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) = (card I1) + (3 + 2)
by A34, AMI_1:105;
hence
(if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card I1) + 3)) = goto (insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))))
by Th116;
:: thesis: ( (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card I1) + 3)) <> halt SCM+FSA & insloc ((card I1) + 3) in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) )hence
(if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) . (insloc ((card I1) + 3)) <> halt SCM+FSA
by SCMFSA_2:47, SCMFSA_2:124;
:: thesis: insloc ((card I1) + 3) in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) end;
hereby :: thesis: verum
per cases
( k = 0 or k > 0 )
;
suppose A35:
k = 0
;
:: thesis: ex m being Element of NAT st
( IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),m) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < m holds
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )take m =
(((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) + 1) + 1;
:: thesis: ( IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),m) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < m holds
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )A36:
CurInstr (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) =
(ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))) . (insloc 0 )
by A13, AMI_1:54
.=
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) . (insloc 0 )
by A15, Th26
.=
a =0_goto (insloc ((card I1) + 3))
by A31, FUNCT_4:111
;
A37:
Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),
(((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) + 1) =
Following (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1))
by AMI_1:14
.=
Exec (a =0_goto (insloc ((card I1) + 3))),
(Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1))
by A36
;
then
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),(((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) + 1)) = insloc ((card I1) + 3)
by A5, A15, A35, SCMFSA_2:96;
then A38:
CurInstr (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),(((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) + 1)) =
(ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))) . (insloc ((card I1) + 3))
by AMI_1:54
.=
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) . (insloc ((card I1) + 3))
by A15, Th26
.=
goto (insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))))
by A31, FUNCT_4:111
;
Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),
m =
Following (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),(((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) + 1))
by AMI_1:14
.=
Exec (goto (insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))))),
(Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),(((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) + 1))
by A38
;
hence
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),m) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))
by SCMFSA_2:95;
:: thesis: for n being Element of NAT st n < m holds
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))hereby :: thesis: verum
let n be
Element of
NAT ;
:: thesis: ( n < m implies IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),b1) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) )assume
n < m
;
:: thesis: IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),b1) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))then
n <= ((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) + 1
by NAT_1:13;
then A39:
(
n <= (LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1 or
n = ((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) + 1 )
by NAT_1:8;
per cases
( n <= LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))) or n = (LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1 or n = ((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) + 1 )
by A39, NAT_1:8;
suppose A40:
n <= LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))
;
:: thesis: IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),b1) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))A41:
I1 is_halting_on ss
by SCMFSA7B:25;
A42:
I1 is_closed_on ss
by SCMFSA7B:24;
then A43:
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_closed_on ss
by A6, A41, SCMFSA8B:18;
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_halting_on ss
by A6, A42, A41, SCMFSA8B:18;
then
Computation (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))),
n,
Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),
n equal_outside NAT
by A40, A43, Th109;
then A44:
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) = IC (Computation (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))),n)
by SCMFSA8A:6;
IC (Computation (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))),n) in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))
by A43, SCMFSA7B:def 7;
hence
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A44, FUNCT_4:105;
:: thesis: verum end; suppose
n = (LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1
;
:: thesis: IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),b1) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))end; suppose
n = ((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) + 1
;
:: thesis: IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),b1) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))hence
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A5, A15, A35, A37, SCMFSA_2:96;
:: thesis: verum end;
end; end; suppose A45:
k > 0
;
:: thesis: ex m being Element of NAT st
( IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),m) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < m holds
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )consider Is3 being
State of
SCM+FSA such that A46:
Is3 = Initialize (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1))
;
A47:
dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) misses dom (Start-At (insloc 0 ))
by SF_MASTR:64;
then (Initialize (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1))) +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))) =
(Initialize (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1))) +* ((Start-At (insloc 0 )) +* (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))
by FUNCT_4:36
.=
((Initialize (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1))) +* (Start-At (insloc 0 ))) +* (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by FUNCT_4:15
;
then A48:
(Initialize (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1))) +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))) = ((Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) +* ((IC SCM+FSA ) .--> (insloc 0 ))) +* (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A13, A15, Th14;
ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))) =
ss +* ((Start-At (insloc 0 )) +* (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))
by A47, FUNCT_4:36
.=
(ss +* (Start-At (insloc 0 ))) +* (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by FUNCT_4:15
;
then
ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) c= Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),
((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)
by AMI_1:99, FUNCT_4:26;
then A49:
loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) c= Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),
((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)
by AMI_1:105;
A50:
Is3 . (intloc 0 ) = 1
by A46, SCMFSA6C:3;
Is3 . a = k
by A5, A15, A46, SCMFSA6C:3;
then consider m0 being
Element of
NAT such that A51:
IC (Computation (Is3 +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),m0) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))
and A52:
for
n being
Element of
NAT st
n < m0 holds
IC (Computation (Is3 +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A3, A45, A50;
take m =
((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) + m0;
:: thesis: ( IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),m) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < m holds
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )
IC SCM+FSA in dom (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1))
by AMI_1:94;
then A53:
(Initialize (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1))) +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 ))) =
(Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)) +* (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A13, A48, FUNCT_7:111
.=
Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),
((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)
by A49, FUNCT_4:79
;
hence
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),m) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))
by A46, A51, AMI_1:51;
:: thesis: for n being Element of NAT st n < m holds
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))hereby :: thesis: verum
let n be
Element of
NAT ;
:: thesis: ( n < m implies IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),b1) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) )assume A54:
n < m
;
:: thesis: IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),b1) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))A55:
I1 is_halting_on ss
by SCMFSA7B:25;
A56:
I1 is_closed_on ss
by SCMFSA7B:24;
then A57:
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_closed_on ss
by A6, A55, SCMFSA8B:18;
A58:
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_halting_on ss
by A6, A56, A55, SCMFSA8B:18;
per cases
( n <= LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))) or (LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1 <= n )
by NAT_1:13;
suppose
n <= LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))
;
:: thesis: IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),b1) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))then
Computation (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))),
n,
Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),
n equal_outside NAT
by A57, A58, Th109;
then A59:
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) = IC (Computation (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))),n)
by SCMFSA8A:6;
IC (Computation (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))),n) in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))
by A57, SCMFSA7B:def 7;
hence
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A59, FUNCT_4:105;
:: thesis: verum end; suppose A60:
(LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1
<= n
;
:: thesis: IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),b1) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))consider mm being
Element of
NAT such that A61:
mm = n -' ((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)
;
n - ((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) >= 0
by A60, XREAL_1:50;
then A62:
mm = n - ((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)
by A61, XREAL_0:def 2;
mm + ((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) = n
by A60, A61, XREAL_1:237;
then A63:
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) = IC (Computation (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)),mm)
by AMI_1:51;
m0 = m - ((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)
;
then
mm < m0
by A54, A62, XREAL_1:11;
hence
IC (Computation (ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A46, A52, A53, A63;
:: thesis: verum end;
end; end;
end;
assume A64:
s . (intloc 0 ) = 1
; :: thesis: ( not s . a > 0 or loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s )
assume A65:
s . a > 0
; :: thesis: loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s
then reconsider sa = s . a as Element of NAT by INT_1:16;
A66:
S1[ 0 ]
;
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A66, A2);
then
S1[sa]
;
then
ex k being Element of NAT st
( IC (Computation (s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),k) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) & ( for n being Element of NAT st n < k holds
IC (Computation (s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )
by A64, A65;
hence
loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s
by SCMFSA8A:def 3; :: thesis: verum