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 not I destroysdestroy a & s . a > 0 holds
ex s2 being State of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) & k = (LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 & (Comput (ProgramPart s2),s2,k) . a = (s . a) - 1 & (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
let I be good InitHalting Program of SCM+FSA ; :: thesis: for a being read-write Int-Location st not I destroysdestroy a & s . a > 0 holds
ex s2 being State of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) & k = (LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 & (Comput (ProgramPart s2),s2,k) . a = (s . a) - 1 & (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
let a be read-write Int-Location ; :: thesis: ( not I destroysdestroy a & s . a > 0 implies ex s2 being State of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) & k = (LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 & (Comput (ProgramPart s2),s2,k) . a = (s . a) - 1 & (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) ) )
assume A1: not I destroysdestroy a ; :: thesis: ( not s . a > 0 or ex s2 being State of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) & k = (LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 & (Comput (ProgramPart s2),s2,k) . a = (s . a) - 1 & (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) ) )
reconsider I1 = I ';' (SubFrom a,(intloc 0 )) as InitHalting Program of SCM+FSA ;
set P = if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )));
assume A2: s . a > 0 ; :: thesis: ex s2 being State of SCM+FSA ex k being Element of NAT st
( s2 = s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) & k = (LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 & (Comput (ProgramPart s2),s2,k) . a = (s . a) - 1 & (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
set Is = (Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))));
take s2 = s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))); :: thesis: ex k being Element of NAT st
( s2 = s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) & k = (LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 & (Comput (ProgramPart s2),s2,k) . a = (s . a) - 1 & (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
set s1 = s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))));
take k = (LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1; :: thesis: ( s2 = s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) & k = (LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 & (Comput (ProgramPart s2),s2,k) . a = (s . a) - 1 & (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
thus ( s2 = s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) & k = (LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 ) ; :: thesis: ( (Comput (ProgramPart s2),s2,k) . a = (s . a) - 1 & (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
Initialized (Initialized s) = Initialized s by SCMFSA8C:15;
then A3: (Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) = (Initialized s) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )) by SCMFSA8A:13;
A4: if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is good by SCMFSA8C:115;
A5: I1 is_halting_onInit s by Th36;
then A6: I1 is_halting_on Initialized s by Th41;
I1 is_closed_onInit s by Th35;
then A7: IExec (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))),s = (IExec I1,s) +* (Start-At (((card (Goto 2)) + (card I1)) + 3),SCM+FSA ) by A2, A5, Th46;
then A8: (IExec (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))),s) . a = (IExec I1,s) . a by SCMFSA_3:11;
( I1 is_closed_onInit s & I1 is_halting_onInit s ) by Th35, Th36;
then A9: ( if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_closed_onInit s & if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_halting_onInit s ) by A2, Th45;
T: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))) by AMI_1:123;
Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) = Following (ProgramPart s2),(Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))))),(Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))))),(Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))) by T ;
then A10: Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) = Exec (goto 0 ),(Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))) by A9, Th71;
A11: ( I1 is_closed_onInit s & I1 is_halting_onInit s ) by Th35, Th36;
then if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_closed_onInit s by A2, Th45;
then A12: if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_closed_on Initialized s by Th40;
if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_halting_onInit s by A2, A11, Th45;
then A13: if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_halting_on Initialized s by Th41;
A14: (Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) = s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by SCMFSA8A:8;
A15: now
let b be Int-Location ; :: thesis: (Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . b = (Comput (ProgramPart ((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))),(LifeSpan (ProgramPart ((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))) . b
(Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . b = (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))) . b by A10, SCMFSA_2:95;
hence (Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . b = (Comput (ProgramPart ((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))),(LifeSpan (ProgramPart ((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))) . b by A9, A14, Th68, SCMFSA10:92; :: thesis: verum
end;
then (Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (Comput (ProgramPart ((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))),(LifeSpan (ProgramPart ((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))) . a
.= (IExec (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))),s) . a by A3, A13, SCMFSA8C:87 ;
hence (Comput (ProgramPart s2),s2,k) . a = (Comput (ProgramPart ((Initialized s) +* (I1 +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I1 +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart ((Initialized s) +* (I1 +* (Start-At 0 ,SCM+FSA )))),((Initialized s) +* (I1 +* (Start-At 0 ,SCM+FSA ))))) . a by A6, A8, SCMFSA8C:87
.= (s . a) - 1 by A1, Th64 ;
:: thesis: ( (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 & ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
(Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = (Comput (ProgramPart ((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))),(LifeSpan (ProgramPart ((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))) . (intloc 0 ) by A15
.= 1 by A3, A13, A12, A4, SCMFSA8C:96 ;
hence (Comput (ProgramPart s2),s2,k) . (intloc 0 ) = 1 ; :: thesis: ( ( for b being read-write Int-Location st b <> a holds
(Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b ) & ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
hereby :: thesis: ( ( for f being FinSeq-Location holds (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f ) & IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
let b be read-write Int-Location ; :: thesis: ( b <> a implies (Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b )
assume A16: b <> a ; :: thesis: (Comput (ProgramPart s2),s2,k) . b = (IExec I,s) . b
thus (Comput (ProgramPart s2),s2,k) . b = (Comput (ProgramPart ((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))),(LifeSpan (ProgramPart ((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))) . b by A15
.= (IExec (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))),s) . b by A3, A13, SCMFSA8C:87
.= (IExec I1,s) . b by A7, SCMFSA_3:11
.= (Exec (SubFrom a,(intloc 0 )),(IExec I,s)) . b by Th33
.= (IExec I,s) . b by A16, SCMFSA_2:91 ; :: thesis: verum
end;
hereby :: thesis: ( IC (Comput (ProgramPart s2),s2,k) = 0 & ( for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
let f be FinSeq-Location ; :: thesis: (Comput (ProgramPart s2),s2,k) . f = (IExec I,s) . f
(Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . f = (Comput (ProgramPart s2),s2,(LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))) . f by A10, SCMFSA_2:95;
hence (Comput (ProgramPart s2),s2,k) . f = (Comput (ProgramPart ((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))),(LifeSpan (ProgramPart ((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((Initialized s) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))) . f by A9, A14, Th68, SCMFSA10:93
.= (IExec (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))),s) . f by A3, A13, SCMFSA8C:87
.= (IExec I1,s) . f by A7, SCMFSA_3:12
.= (Exec (SubFrom a,(intloc 0 )),(IExec I,s)) . f by Th34
.= (IExec I,s) . f by SCMFSA_2:91 ;
:: thesis: verum
end;
thus IC (Comput (ProgramPart s2),s2,k) = 0 by A10, SCMFSA_2:95; :: thesis: for n being Element of NAT st n <= k holds
IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
A17: IC (Comput (ProgramPart s2),s2,((LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) = 0 by A10, SCMFSA_2:95;
hereby :: thesis: verum
let n be Element of NAT ; :: thesis: ( n <= k implies IC (Comput (ProgramPart s2),s2,b1) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) )
assume A18: n <= k ; :: thesis: IC (Comput (ProgramPart s2),s2,b1) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
per cases ( n <= LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) or n = (LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 ) by A18, NAT_1:8;
suppose A19: n <= LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) ; :: thesis: IC (Comput (ProgramPart s2),s2,b1) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
A20: ( I1 is_closed_onInit s & I1 is_halting_onInit s ) by Th35, Th36;
then A21: if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_closed_onInit s by A2, Th45;
if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_halting_onInit s by A2, A20, Th45;
then Comput (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))),n, Comput (ProgramPart s2),s2,n equal_outside NAT by A19, A21, Th68;
then A22: IC (Comput (ProgramPart s2),s2,n) = IC (Comput (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))),n) by SCMFSA8A:6;
IC (Comput (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))),n) in dom (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) by A21, Def4;
hence IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by A22, FUNCT_4:105; :: thesis: verum
end;
suppose A23: n = (LifeSpan (ProgramPart (s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(s +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 ; :: thesis: IC (Comput (ProgramPart s2),s2,b1) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
A24: card (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) = ((card (Goto 2)) + (card I1)) + 4 by SCMFSA8B:14
.= ((card I1) + 1) + 4 by SCMFSA8A:29
.= ((card I1) + 3) + 2 ;
card (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) = card (dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) by CARD_1:104
.= card (dom (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by FUNCT_4:105
.= card (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) by CARD_1:104 ;
hence IC (Comput (ProgramPart s2),s2,n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by A17, A23, A24, AFINSQ_1:70; :: thesis: verum
end;
end;
end;