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 . (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 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 )
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 )
assume A2:
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 A3:
s . a > 0
; :: thesis: 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 ))))) ) ) );
A4:
S1[ 0 ]
;
A5:
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 A6:
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 A7:
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 ))))) ) ) ) )
assume A8:
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 ))))) ) ) ) )
assume A9:
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 ))))) ) ) )
set s1 =
ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )));
set s2 =
ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 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);
A10:
now A11:
now thus 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
;
:: thesis: card (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) = ((card I1) + 3) + 2thus 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
;
:: thesis: verum end;
(
InsCode (a =0_goto (insloc ((card I1) + 3))) = 7 &
InsCode (halt SCM+FSA ) = 0 )
by SCMFSA_2:48, SCMFSA_2:124;
then
(
insloc 0 in dom (Macro (a =0_goto (insloc ((card I1) + 3)))) &
(Macro (a =0_goto (insloc ((card I1) + 3)))) . (insloc 0 ) <> halt SCM+FSA )
by SCMFSA6B:32, SCMFSA6B:33;
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 A12, 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 )))) )thus
insloc 0 in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))
by A11, 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 (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) = (card I1) + (3 + 2)
by A11, 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 ))))
A13:
now
(
I1 is_closed_on ss &
I1 is_halting_on ss )
by SCMFSA7B:24, SCMFSA7B:25;
hence A14:
(
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_closed_on ss &
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_halting_on ss )
by A9, SCMFSA8B:18;
:: 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) = 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 (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)) = insloc 0 )A15:
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 ))))))
;
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) = 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 A14, Lm3;
:: thesis: 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)) = insloc 0 thus 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 A14, A15, Lm3
.=
insloc 0
by SCMFSA_2:95
;
:: thesis: verum
A16:
now A17:
now thus 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
;
:: thesis: card (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) = ((card I1) + 3) + 2thus 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
;
:: thesis: verum end; hereby :: thesis: ( (Initialize ss) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))) = 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 ))))) + 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 A17, 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 A17, NAT_1:13;
then
(card I1) + 3
< card (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A17, 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; hereby :: 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 )
intloc 0 in dom ss
by SCMFSA_2:66;
then A19:
ss +* ((intloc 0 ) .--> 1) = ss
by A7, FUNCT_7:111;
A20:
dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) misses dom (Start-At (insloc 0 ))
by SF_MASTR:64;
Initialize ss = (ss +* ((intloc 0 ) .--> 1)) +* (Start-At (insloc 0 ))
by SCMFSA6C:def 3;
hence (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 A19, 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
;
:: thesis: verum
end; consider Is being
State of
SCM+FSA such that A21:
Is = (Initialize ss) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))
;
A22:
I1 is_halting_on Initialize ss
by SCMFSA7B:25;
A23:
now A24:
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 +* ((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 ))))) equal_outside NAT &
(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 A13, Th109, 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 A18, A21, SCMFSA6A:30;
:: thesis: verum end;
(
(Initialize ss) . a > 0 &
I1 is_closed_on Initialize ss &
I1 is_halting_on Initialize ss )
by A9, SCMFSA6C:3, SCMFSA7B:24, SCMFSA7B:25;
then A25:
(
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_halting_on Initialize ss &
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_closed_on Initialize ss )
by SCMFSA8B:18;
thus (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
by A24
.=
(IExec (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))),ss) . a
by A21, A25, Th87
;
:: 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 ) = 1A26:
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is
good
by Th115;
thus (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 A24
.=
1
by A21, A25, A26, Th96
;
:: thesis: verum
(
ss . a <> 0 &
I1 is_closed_on Initialize ss )
by A9, 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 A22, SCMFSA8B:19;
then
(IExec (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))),ss) . a = (IExec I1,ss) . a
by SCMFSA_3:11;
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 A22, A23, 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 ) = 1thus
(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
by A23;
:: thesis: verum
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 ))))) ) )
hereby :: thesis: verum
per cases
( k = 0 or k > 0 )
;
suppose A27:
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 ))))) ) )A28:
now thus 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 A16, Th26
.=
a =0_goto (insloc ((card I1) + 3))
by A10, FUNCT_4:111
;
:: thesis: verum end; A29:
now thus 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 A28
;
:: thesis: verum end; then A30:
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 A8, A16, A27, SCMFSA_2:96;
A31:
now thus 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 A30, AMI_1:54
.=
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) . (insloc ((card I1) + 3))
by A16, Th26
.=
goto (insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))))
by A10, FUNCT_4:111
;
:: thesis: verum end; 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 A31
;
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 A32:
(
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 A32, NAT_1:8;
suppose A33:
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 )))))
(
I1 is_closed_on ss &
I1 is_halting_on ss )
by SCMFSA7B:24, SCMFSA7B:25;
then A34:
(
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_closed_on ss &
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_halting_on ss )
by A9, 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 A33, Th109;
then A35:
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 A34, 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 A35, FUNCT_4:105;
:: thesis: verum 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 A8, A16, A27, A29, SCMFSA_2:96;
:: thesis: verum end;
end; end; suppose A36:
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 A37:
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))
;
A38:
Is3 . (intloc 0 ) = 1
by A37, SCMFSA6C:3;
(
Is3 . a = k &
Is3 . a > 0 )
by A8, A16, A36, A37, SCMFSA6C:3;
then consider m0 being
Element of
NAT such that A39:
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 A40:
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 A6, A38;
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 ))))) ) )A41:
now thus
(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 ) = 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))
;
:: thesis: (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)A42:
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;
A43:
dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) misses dom (Start-At (insloc 0 ))
by SF_MASTR:64;
now thus 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 A43, FUNCT_4:36
.=
(ss +* (Start-At (insloc 0 ))) +* (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by FUNCT_4:15
;
:: thesis: verum end; 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 A44:
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;
now thus (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 A43, 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
;
:: thesis: verum end; 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 ))) = ((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, A16, Th14;
hence (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, A42, 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 A44, FUNCT_4:79
;
:: thesis: verum end; 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 A37, A39, 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 A45:
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 )))))
(
I1 is_closed_on ss &
I1 is_halting_on ss )
by SCMFSA7B:24, SCMFSA7B:25;
then A46:
(
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_closed_on ss &
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_halting_on ss )
by A9, 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 A46, Th109;
then A47:
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 A46, 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 A47, FUNCT_4:105;
:: thesis: verum end; suppose A48:
(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 A49:
mm = n -' ((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1)
;
mm + ((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) = n
by A48, A49, XREAL_1:237;
then A50:
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;
n - ((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) >= 0
by A48, XREAL_1:50;
then
(
mm = n - ((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) &
m0 = m - ((LifeSpan (ss +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 ))))) + 1) )
by A49, XREAL_0:def 2;
then
mm < m0
by A45, 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 A37, A40, A41, A50;
:: thesis: verum end;
end; end;
end;
reconsider sa = s . a as Element of NAT by A3, INT_1:16;
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A4, A5);
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 A2, A3;
hence
loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s
by SCMFSA8A:def 3; :: thesis: verum