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 . (intloc 0 ) = 1 & s . a > 0 holds
loop (if=0 a,(Goto 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 not I destroysdestroy a & s . (intloc 0 ) = 1 & s . a > 0 holds
loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s
let a be read-write Int-Location ; :: thesis: ( not I destroysdestroy a & s . (intloc 0 ) = 1 & s . a > 0 implies loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s )
set P = if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )));
reconsider I1 = I ';' (SubFrom a,(intloc 0 )) as InitHalting Program of SCM+FSA ;
set i = a =0_goto ((card I1) + 3);
defpred S1[ Nat] means for s being State of SCM+FSA st s . (intloc 0 ) = 1 & s . a = $1 & s . a > 0 holds
( (Comput (ProgramPart (s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((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 = (s . a) - 1 & (Comput (ProgramPart (s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((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 ) = 1 & ex k being Element of NAT st
( IC (Comput (ProgramPart (s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),k) = card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) & ( for n being Element of NAT st n < k holds
IC (Comput (ProgramPart (s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) ) );
assume A1: not I destroysdestroy a ; :: thesis: ( not s . (intloc 0 ) = 1 or not s . a > 0 or loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s )
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
A3: now
InsCode (a =0_goto ((card I1) + 3)) = 7 by SCMFSA_2:48;
then A4: ( 0 in dom (Macro (a =0_goto ((card I1) + 3))) & (Macro (a =0_goto ((card I1) + 3))) . 0 <> halt SCM+FSA ) by SCMFSA6B:32, SCMFSA6B:33, SCMFSA_2:124;
if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) = ((((a =0_goto ((card I1) + 3)) ';' I1) ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2)) ';' (Stop SCM+FSA ) by SCMFSA8B:def 1
.= (((a =0_goto ((card I1) + 3)) ';' (I1 ';' (Goto ((card (Goto 2)) + 1)))) ';' (Goto 2)) ';' (Stop SCM+FSA ) by SCMFSA6A:71
.= ((a =0_goto ((card I1) + 3)) ';' ((I1 ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2))) ';' (Stop SCM+FSA ) by SCMFSA6A:71
.= (a =0_goto ((card I1) + 3)) ';' (((I1 ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2)) ';' (Stop SCM+FSA )) by SCMFSA6A:71
.= (Macro (a =0_goto ((card I1) + 3))) ';' (((I1 ';' (Goto ((card (Goto 2)) + 1))) ';' (Goto 2)) ';' (Stop SCM+FSA )) ;
hence (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . 0 = (Macro (a =0_goto ((card I1) + 3))) . 0 by A4, SCMFSA6A:54
.= a =0_goto ((card I1) + 3) by SCMFSA6B:33 ;
:: thesis: ( (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . 0 <> halt SCM+FSA & 0 in dom (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) & (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . ((card I1) + 3) = goto (card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) & (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . ((card I1) + 3) <> halt SCM+FSA & (card I1) + 3 in dom (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) )
hence (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . 0 <> halt SCM+FSA by SCMFSA_2:48, SCMFSA_2:124; :: thesis: ( 0 in dom (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) & (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . ((card I1) + 3) = goto (card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) & (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . ((card I1) + 3) <> halt SCM+FSA & (card I1) + 3 in dom (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) )
A5: 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 ;
hence 0 in dom (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) by AFINSQ_1:70; :: thesis: ( (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . ((card I1) + 3) = goto (card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) & (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . ((card I1) + 3) <> halt SCM+FSA & (card I1) + 3 in dom (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) )
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 ;
then card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) = (card I1) + (3 + 2) by A5, RELAT_1:209;
hence (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . ((card I1) + 3) = goto (card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) by SCMFSA8C:116; :: thesis: ( (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . ((card I1) + 3) <> halt SCM+FSA & (card I1) + 3 in dom (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) )
hence (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) . ((card I1) + 3) <> halt SCM+FSA by SCMFSA_2:47, SCMFSA_2:124; :: thesis: (card I1) + 3 in dom (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))
hereby :: thesis: verum
((card I1) + 3) + 0 < card (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) by A5, XREAL_1:8;
hence (card I1) + 3 in dom (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) by AFINSQ_1:70; :: thesis: verum
end;
end;
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 ( (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 & ex k being Element of NAT st
( IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),k) = card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) & ( for n being Element of NAT st n < k holds
IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) ) ) )
assume A7: ss . (intloc 0 ) = 1 ; :: thesis: ( not ss . a = k + 1 or not ss . a > 0 or ( (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 & ex k being Element of NAT st
( IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),k) = card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) & ( for n being Element of NAT st n < k holds
IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) ) ) )
set s2 = ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))));
set s1 = ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))));
assume A8: ss . a = k + 1 ; :: thesis: ( not ss . a > 0 or ( (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 & ex k being Element of NAT st
( IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),k) = card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) & ( for n being Element of NAT st n < k holds
IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) ) ) )
T: ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) = ProgramPart (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))) by AMI_1:123;
A9: Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) = Following (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))))),(Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))))),(Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))) by T ;
set s3 = Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1);
assume A10: ss . a > 0 ; :: thesis: ( (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 & ex k being Element of NAT st
( IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),k) = card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) & ( for n being Element of NAT st n < k holds
IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) ) )
A11: ( I1 is_closed_onInit ss & I1 is_halting_onInit ss ) by Th35, Th36;
then A12: if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_halting_onInit ss by A10, Th45;
if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_closed_onInit ss by A10, A11, Th45;
then A13: Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) = Exec (goto 0 ),(Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))) by A12, A9, Th71;
A14: if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_closed_onInit ss by A10, A11, Th45;
A15: now
A16: I1 is_halting_onInit ss by Th36;
then A17: I1 is_halting_on Initialized ss by Th41;
I1 is_closed_onInit ss by Th35;
then IExec (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))),ss = (IExec I1,ss) +* (Start-At (((card (Goto 2)) + (card I1)) + 3),SCM+FSA ) by A10, A16, Th46;
then A18: (IExec (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))),ss) . a = (IExec I1,ss) . a by SCMFSA_3:11;
A19: 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 ;
A20: 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 ;
hereby :: thesis: ( (Initialized ss) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) = ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) & (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 )
thus 0 in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by A20, A19, AFINSQ_1:70; :: thesis: (card I1) + 3 in dom (loop (if=0 a,(Goto 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 2),(I ';' (SubFrom a,(intloc 0 )))) by A19, NAT_1:13;
then (card I1) + 3 < card (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by A20, NAT_1:13;
hence (card I1) + 3 in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by AFINSQ_1:70; :: thesis: verum
end;
consider Is being State of SCM+FSA such that
A21: Is = (Initialized ss) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ;
Initialized (Initialized ss) = Initialized ss by SCMFSA8C:15;
then A22: Is = (Initialized ss) +* ((if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )) by A21, SCMFSA8A:13;
I1 is_closed_onInit ss by Th35;
then A23: I1 is_closed_on Initialized ss by Th40;
I1 is_halting_onInit ss by Th36;
then A24: I1 is_halting_on Initialized ss by Th41;
A25: (Initialized ss) . a > 0 by A10, SCMFSA6C:3;
then A26: if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_halting_on Initialized ss by A23, A24, SCMFSA8B:18;
thus A27: (Initialized ss) +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) = ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by SCMFSA8A:8; :: thesis: ( (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 )
A28: now
let b be Int-Location ; :: thesis: (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . b = (Comput (ProgramPart Is),Is,(LifeSpan (ProgramPart Is),Is)) . b
(Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . b = (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))) . b by A13, SCMFSA_2:95;
hence (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . b = (Comput (ProgramPart Is),Is,(LifeSpan (ProgramPart Is),Is)) . b by A12, A14, A27, A21, Th68, SCMFSA10:92; :: thesis: verum
end;
then (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (Comput (ProgramPart Is),Is,(LifeSpan (ProgramPart Is),Is)) . a
.= (IExec (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))),ss) . a by A22, A26, SCMFSA8C:87 ;
hence (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (Comput (ProgramPart ((Initialized ss) +* (I1 +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* (I1 +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart ((Initialized ss) +* (I1 +* (Start-At 0 ,SCM+FSA )))),((Initialized ss) +* (I1 +* (Start-At 0 ,SCM+FSA ))))) . a by A17, A18, SCMFSA8C:87
.= (ss . a) - 1 by A1, Th64 ;
:: thesis: (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1
A29: if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is good by SCMFSA8C:115;
A30: if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_closed_on Initialized ss by A25, A23, A24, SCMFSA8B:18;
(Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = (Comput (ProgramPart Is),Is,(LifeSpan (ProgramPart Is),Is)) . (intloc 0 ) by A28
.= 1 by A22, A26, A30, A29, SCMFSA8C:96 ;
hence (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 ; :: thesis: verum
end;
hence ( (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . a = (ss . a) - 1 & (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (intloc 0 ) = 1 ) ; :: thesis: ex k being Element of NAT st
( IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),k) = card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) & ( for n being Element of NAT st n < k holds
IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
A31: IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) = 0 by A13, SCMFSA_2:95;
hereby :: thesis: verum
per cases ( k = 0 or k > 0 ) ;
suppose A32: k = 0 ; :: thesis: ex m being Element of NAT st
( IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),m) = card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) & ( for n being Element of NAT st n < m holds
IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
take m = (((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1) + 1; :: thesis: ( IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),m) = card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) & ( for n being Element of NAT st n < m holds
IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
A33: ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) = ss +* ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA )) by A7, SCMFSA8C:18;
Y: (ProgramPart (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1))) /. (IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1))) = (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) . (IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1))) by COMPOS_1:38;
A34: CurInstr (ProgramPart (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1))),(Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) = (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) . 0 by A31, Y, AMI_1:54
.= (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) . 0 by A15, A33, SCMFSA8C:26
.= a =0_goto ((card I1) + 3) by A3, FUNCT_4:111 ;
Y: (ProgramPart (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1))) /. (IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1))) = (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1)) . (IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1))) by COMPOS_1:38;
T: ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) = ProgramPart (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) by AMI_1:123;
A35: Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1) = Following (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) by AMI_1:14
.= Exec (a =0_goto ((card I1) + 3)),(Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) by A34, T ;
then IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1)) = (card I1) + 3 by A8, A15, A32, SCMFSA_2:96;
then A36: CurInstr (ProgramPart (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1))),(Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1)) = (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) . ((card I1) + 3) by Y, AMI_1:54
.= (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) . ((card I1) + 3) by A15, A33, SCMFSA8C:26
.= goto (card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) by A3, FUNCT_4:111 ;
T: ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) = ProgramPart (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1)) by AMI_1:123;
Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),m = Following (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1)) by AMI_1:14
.= Exec (goto (card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1)) by A36, T ;
hence IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),m) = card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) by SCMFSA_2:95; :: thesis: for n being Element of NAT st n < m holds
IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
hereby :: thesis: verum
let n be Element of NAT ; :: thesis: ( n < m implies IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),b1) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) )
assume n < m ; :: thesis: IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),b1) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
then n <= ((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1 by NAT_1:13;
then A37: ( n <= (LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 or n = ((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1 ) by NAT_1:8;
per cases ( n <= LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) or n = (LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 or n = ((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1 ) by A37, NAT_1:8;
suppose A38: n <= LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) ; :: thesis: IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),b1) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
A39: ( I1 is_closed_onInit ss & I1 is_halting_onInit ss ) by Th35, Th36;
then A40: if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_closed_onInit ss by A10, Th45;
if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_halting_onInit ss by A10, A39, Th45;
then Comput (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))),n, Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n equal_outside NAT by A38, A40, Th68;
then A41: IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) = IC (Comput (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))),n) by SCMFSA8A:6;
IC (Comput (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (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 A40, Def4;
hence IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by A41, FUNCT_4:105; :: thesis: verum
end;
suppose n = (LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 ; :: thesis: IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),b1) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
hence IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by A13, A15, SCMFSA_2:95; :: thesis: verum
end;
suppose n = ((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + 1 ; :: thesis: IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),b1) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
hence IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by A8, A15, A32, A35, SCMFSA_2:96; :: thesis: verum
end;
end;
end;
end;
suppose A42: k > 0 ; :: thesis: ex m being Element of NAT st
( IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),m) = card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) & ( for n being Element of NAT st n < m holds
IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
consider Is3 being State of SCM+FSA such that
A43: Is3 = Initialized (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) ;
ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) c= Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) by Th67, AMI_1:99;
then A44: loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) c= Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) by RELAT_1:209;
( Is3 . (intloc 0 ) = 1 & Is3 . a = k ) by A8, A15, A43, SCMFSA6C:3;
then consider m0 being Element of NAT such that
A45: IC (Comput (ProgramPart (Is3 +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(Is3 +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),m0) = card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) and
A46: for n being Element of NAT st n < m0 holds
IC (Comput (ProgramPart (Is3 +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(Is3 +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by A6, A42;
take m = ((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) + m0; :: thesis: ( IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),m) = card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) & ( for n being Element of NAT st n < m holds
IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) )
T: ProgramPart (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) = ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) by AMI_1:123;
A47: (Initialized (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1))) +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) = (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) by SCMFSA8A:8
.= (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) +* ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA ))) by FUNCT_4:15
.= ((Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) +* (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA )) by FUNCT_4:15
.= ((Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) +* (((intloc 0 ) .--> 1) +* (Start-At 0 ,SCM+FSA ))) +* (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by Th19
.= (((Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) +* ((intloc 0 ) .--> 1)) +* (Start-At 0 ,SCM+FSA )) +* (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by FUNCT_4:15
.= (Initialized (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1))) +* (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by SCMFSA6A:def 4
.= (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) +* (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by A31, A15, SCMFSA8C:14
.= Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) by A44, FUNCT_4:79 ;
hence IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),m) = card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) by A43, A45, T, AMI_1:51; :: thesis: for n being Element of NAT st n < m holds
IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
hereby :: thesis: verum
let n be Element of NAT ; :: thesis: ( n < m implies IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),b1) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) )
assume A48: n < m ; :: thesis: IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),b1) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
A49: ( I1 is_closed_onInit ss & I1 is_halting_onInit ss ) by Th35, Th36;
then A50: if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_closed_onInit ss by A10, Th45;
A51: if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) is_halting_onInit ss by A10, A49, Th45;
per cases ( n <= LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) or (LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 <= n ) by NAT_1:13;
suppose n <= LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) ; :: thesis: IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),b1) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
then Comput (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))),n, Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n equal_outside NAT by A50, A51, Th68;
then A52: IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) = IC (Comput (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))),n) by SCMFSA8A:6;
IC (Comput (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (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 A50, Def4;
hence IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by A52, FUNCT_4:105; :: thesis: verum
end;
suppose A53: (LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1 <= n ; :: thesis: IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),b1) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))
consider mm being Element of NAT such that
A54: mm = n -' ((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) ;
n - ((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) >= 0 by A53, XREAL_1:50;
then A55: mm = n - ((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) by A54, XREAL_0:def 2;
T: ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) = ProgramPart (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)) by AMI_1:123;
mm + ((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) = n by A53, A54, XREAL_1:237;
then A56: IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) = IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1)),mm) by AMI_1:51;
m0 = m - ((LifeSpan (ProgramPart (ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),(ss +* (Initialized (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))) + 1) ;
then mm < m0 by A48, A55, XREAL_1:11;
hence IC (Comput (ProgramPart (ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(ss +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) by A43, A46, A47, A56, T; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
assume A57: s . (intloc 0 ) = 1 ; :: thesis: ( not s . a > 0 or loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s )
assume A58: s . a > 0 ; :: thesis: loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s
then reconsider sa = s . a as Element of NAT by INT_1:16;
A59: S1[ 0 ] ;
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A59, A2);
 then S1[sa] ;
then A60: ex k being Element of NAT st
( IC (Comput (ProgramPart (s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),k) = card (ProgramPart (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) & ( for n being Element of NAT st n < k holds
IC (Comput (ProgramPart (s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))))),(s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))))),n) in dom (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) ) ) by A57, A58;
s +* (Initialized (loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))))) = s +* ((loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))))) +* (Start-At 0 ,SCM+FSA )) by A57, SCMFSA8C:18;
hence loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) is_pseudo-closed_on s by A60, SCMFSA8A:def 3; :: thesis: verum