let s be State of SCM+FSA ; :: thesis: for I being good InitHalting Program of SCM+FSA
for a being read-write Int-Location st I does_not_destroy a & s . (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 good InitHalting 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 InitHalting 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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (s +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (s . a) - 1 & (Computation (s +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (s +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 & ex k being Element of NAT st
( IC (Computation (s +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 & ex k being Element of NAT st
( IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 & ex k being Element of NAT st
( IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 & ex k being Element of NAT st
( IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) ) ) )
assume A9:
ss . a > 0
;
:: thesis: ( (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 & ex k being Element of NAT st
( IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) ) )
set s1 =
ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))));
set s2 =
ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))));
set s3 =
Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),
((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 PRE_CIRC:21
.=
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 PRE_CIRC:21
;
:: 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 SCMFSA8C:116;
:: 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_onInit ss &
I1 is_halting_onInit ss )
by Th35, Th36;
hence A14:
(
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_closed_onInit ss &
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_halting_onInit ss )
by A9, Th45;
:: thesis: ( Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) = Exec (goto (insloc 0 )),(Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))) & IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) = insloc 0 ) Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),
((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) =
Following (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))))
by AMI_1:14
.=
Exec (CurInstr (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))))),
(Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))))
;
hence
Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),
((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) = Exec (goto (insloc 0 )),
(Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))))
by A14, Th71;
:: thesis: IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) = insloc 0 hence
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) = insloc 0
by SCMFSA_2:95;
:: thesis: verum
A15:
now A16:
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 PRE_CIRC:21
.=
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 PRE_CIRC:21
;
:: 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) +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) = ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) & (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 )
thus
insloc 0 in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A16, 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 A16, NAT_1:13;
then
(card I1) + 3
< card (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A16, 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; thus A17:
(Initialize ss) +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) = ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by SCMFSA8A:8;
:: thesis: ( (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 )A18:
Initialize (Initialize ss) = Initialize ss
by SCMFSA8C:15;
consider Is being
State of
SCM+FSA such that A19:
Is = (Initialize ss) +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
;
A20:
Is = (Initialize ss) +* ((if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At (insloc 0 )))
by A18, A19, SCMFSA8A:13;
A21:
I1 is_halting_onInit ss
by Th36;
then A22:
I1 is_halting_on Initialize ss
by Th41;
A23:
now A24:
now let b be
Int-Location ;
:: thesis: (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . b = (Computation Is,(LifeSpan Is)) . b
(
Computation (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))),
(LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),
Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),
(LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) equal_outside NAT &
(Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . b = (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))) . b )
by A13, Th68, SCMFSA_2:95;
hence
(Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . b = (Computation Is,(LifeSpan Is)) . b
by A17, A19, SCMFSA6A:30;
:: thesis: verum end; A25:
(Initialize ss) . a > 0
by A9, SCMFSA6C:3;
(
I1 is_closed_onInit ss &
I1 is_halting_onInit ss )
by Th35, Th36;
then
(
I1 is_closed_on Initialize ss &
I1 is_halting_on Initialize ss )
by Th40, Th41;
then A26:
(
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 A25, SCMFSA8B:18;
thus (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 A20, A26, SCMFSA8C:87
;
:: thesis: (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1A27:
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is
good
by SCMFSA8C:115;
thus (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) =
(Computation Is,(LifeSpan Is)) . (intloc 0 )
by A24
.=
1
by A20, A26, A27, SCMFSA8C:96
;
:: thesis: verum
(
ss . a <> 0 &
I1 is_closed_onInit ss )
by A9, Th35;
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 A21, Th46;
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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a =
(Computation ((Initialize ss) +* (I1 +* (Start-At (insloc 0 )))),(LifeSpan ((Initialize ss) +* (I1 +* (Start-At (insloc 0 )))))) . a
by A22, A23, SCMFSA8C:87
.=
(ss . a) - 1
by A1, Th64
;
:: thesis: (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1thus
(Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1
by A23;
:: thesis: verum
hence
(
(Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 &
(Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 )
;
:: thesis: ex k being Element of NAT st
( IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 A28:
k = 0
;
:: thesis: ex m being Element of NAT st
( IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )take m =
(((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1) + 1;
:: thesis: ( IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )A29:
ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) = ss +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))
by A7, SCMFSA8C:18;
A30:
now thus CurInstr (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) =
(ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) . (insloc 0 )
by A13, AMI_1:54
.=
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) . (insloc 0 )
by A15, A29, SCMFSA8C:26
.=
a =0_goto (insloc ((card I1) + 3))
by A10, FUNCT_4:111
;
:: thesis: verum end; A31:
now thus Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),
(((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1) =
Following (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1))
by AMI_1:14
.=
Exec (a =0_goto (insloc ((card I1) + 3))),
(Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1))
by A30
;
:: thesis: verum end; then A32:
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1)) = insloc ((card I1) + 3)
by A8, A15, A28, SCMFSA_2:96;
A33:
now thus CurInstr (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1)) =
(ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) . (insloc ((card I1) + 3))
by A32, AMI_1:54
.=
(loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) . (insloc ((card I1) + 3))
by A15, A29, SCMFSA8C:26
.=
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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),
m =
Following (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1))
by A33
;
hence
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),b1) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) )assume
n < m
;
:: thesis: IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),b1) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))then
n <= ((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1
by NAT_1:13;
then A34:
(
n <= (LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 or
n = ((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1 )
by NAT_1:8;
per cases
( n <= LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) or n = (LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 or n = ((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1 )
by A34, NAT_1:8;
suppose A35:
n <= LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))
;
:: thesis: IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),b1) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
(
I1 is_closed_onInit ss &
I1 is_halting_onInit ss )
by Th35, Th36;
then A36:
(
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_closed_onInit ss &
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_halting_onInit ss )
by A9, Th45;
then
Computation (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))),
n,
Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),
n equal_outside NAT
by A35, Th68;
then A37:
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) = IC (Computation (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))),n)
by SCMFSA8A:6;
IC (Computation (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))),n) in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))
by A36, Def4;
hence
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A37, FUNCT_4:105;
:: thesis: verum suppose
n = (LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1
;
:: thesis: IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),b1) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))end; suppose
n = ((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1
;
:: thesis: IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),b1) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))hence
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A8, A15, A28, A31, SCMFSA_2:96;
:: thesis: verum end;
end; end; suppose A38:
k > 0
;
:: thesis: ex m being Element of NAT st
( IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 A39:
Is3 = Initialize (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1))
;
A40:
Is3 . (intloc 0 ) = 1
by A39, SCMFSA6C:3;
(
Is3 . a = k &
Is3 . a > 0 )
by A8, A15, A38, A39, SCMFSA6C:3;
then consider m0 being
Element of
NAT such that A41:
IC (Computation (Is3 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),m0) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))
and A42:
for
n being
Element of
NAT st
n < m0 holds
IC (Computation (Is3 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A6, A40;
take m =
((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + m0;
:: thesis: ( IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )A43:
now thus
loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) c= ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))
by Th67;
:: thesis: (Initialize (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1))) +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) = Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)
ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) c= Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),
((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)
by Th67, AMI_1:99;
then A44:
loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) c= Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),
((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)
by AMI_1:105;
thus (Initialize (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1))) +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) =
(Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))
by SCMFSA8A:8
.=
(Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))))
by FUNCT_4:15
.=
((Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) +* (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))
by FUNCT_4:15
.=
((Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) +* (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by Th19
.=
(((Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) +* ((intloc 0 ) .--> 1)) +* (Start-At (insloc 0 ))) +* (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by FUNCT_4:15
.=
(Initialize (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1))) +* (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by SCMFSA6C:def 3
.=
(Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) +* (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A13, A15, SCMFSA8C:14
.=
Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),
((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)
by A44, FUNCT_4:79
;
:: thesis: verum end; hence
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),m) = insloc (card (ProgramPart (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))))
by A39, A41, AMI_1:51;
:: thesis: for n being Element of NAT st n < m holds
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),b1) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) )assume A45:
n < m
;
:: thesis: IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),b1) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
(
I1 is_closed_onInit ss &
I1 is_halting_onInit ss )
by Th35, Th36;
then A46:
(
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_closed_onInit ss &
if=0 a,
(Goto (insloc 2)),
(I ';' (SubFrom a,(intloc 0 ))) is_halting_onInit ss )
by A9, Th45;
per cases
( n <= LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) or (LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 <= n )
by NAT_1:13;
suppose
n <= LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))
;
:: thesis: IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),b1) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))then
Computation (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))),
n,
Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),
n equal_outside NAT
by A46, Th68;
then A47:
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) = IC (Computation (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))),n)
by SCMFSA8A:6;
IC (Computation (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))),n) in dom (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))
by A46, Def4;
hence
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1
<= n
;
:: thesis: IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)
;
mm + ((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) = n
by A48, A49, XREAL_1:237;
then A50:
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) = IC (Computation (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)),mm)
by AMI_1:51;
n - ((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) >= 0
by A48, XREAL_1:50;
then
(
mm = n - ((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) &
m0 = m - ((LifeSpan (ss +* (Initialized (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) )
by A49, XREAL_0:def 2;
then
mm < m0
by A45, XREAL_1:11;
hence
IC (Computation (ss +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))
by A39, A42, A43, 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 A51:
ex k being Element of NAT st
( IC (Computation (s +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 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 +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) ) )
by A2, A3;
s +* (Initialized (loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))))) = s +* ((loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At (insloc 0 )))
by A2, SCMFSA8C:18;
hence
loop (if=0 a,(Goto (insloc 2)),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s
by A51, SCMFSA8A:def 3; :: thesis: verum