let I be Program of SCM+FSA; :: thesis: for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for s being State of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) & P +* (I ';' (Stop SCM+FSA)) halts_on s +* (Initialize (I ';' (Stop SCM+FSA))) & LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 & I ';' (Stop SCM+FSA) is_closed_on s,P & I ';' (Stop SCM+FSA) is_halting_on s,P )
let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA st I is_closed_on s,P & I is_halting_on s,P holds
( IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) & P +* (I ';' (Stop SCM+FSA)) halts_on s +* (Initialize (I ';' (Stop SCM+FSA))) & LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 & I ';' (Stop SCM+FSA) is_closed_on s,P & I ';' (Stop SCM+FSA) is_halting_on s,P )
let s be State of SCM+FSA; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies ( IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) & P +* (I ';' (Stop SCM+FSA)) halts_on s +* (Initialize (I ';' (Stop SCM+FSA))) & LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 & I ';' (Stop SCM+FSA) is_closed_on s,P & I ';' (Stop SCM+FSA) is_halting_on s,P ) )
assume A1: I is_closed_on s,P ; :: thesis: ( not I is_halting_on s,P or ( IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) & P +* (I ';' (Stop SCM+FSA)) halts_on s +* (Initialize (I ';' (Stop SCM+FSA))) & LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 & I ';' (Stop SCM+FSA) is_closed_on s,P & I ';' (Stop SCM+FSA) is_halting_on s,P ) )
card (Stop SCM+FSA) = 1 by COMPOS_1:46;
then card (I ';' (Stop SCM+FSA)) = (card I) + 1 by SCMFSA6A:61;
then card I < card (I ';' (Stop SCM+FSA)) by NAT_1:13;
then A2: card I in dom (I ';' (Stop SCM+FSA)) by AFINSQ_1:70;
A3: 0 in dom (Stop SCM+FSA) by COMPOS_1:45;
0 + (card I) in { (m + (card I)) where m is Element of NAT : m in dom (Stop SCM+FSA) } by A3;
then A4: 0 + (card I) in dom (Reloc ((Stop SCM+FSA),(card I))) by COMPOS_1:117;
set s2 = s +* (Initialize (I ';' (Stop SCM+FSA)));
set s1 = s +* (Initialize I);
A5: 0 in dom (Stop SCM+FSA) by COMPOS_1:45;
A6: (Stop SCM+FSA) . 0 = halt SCM+FSA by AFINSQ_1:38;
assume A7: I is_halting_on s,P ; :: thesis: ( IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) & P +* (I ';' (Stop SCM+FSA)) halts_on s +* (Initialize (I ';' (Stop SCM+FSA))) & LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 & I ';' (Stop SCM+FSA) is_closed_on s,P & I ';' (Stop SCM+FSA) is_halting_on s,P )
then A8: IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) = IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) by A1, Th42;
A9: (P +* (I ';' (Stop SCM+FSA))) . (card I) = (I ';' (Stop SCM+FSA)) . (card I) by A2, FUNCT_4:14
.= (I ';' (Stop SCM+FSA)) . (card I)
.= (Reloc ((Stop SCM+FSA),(card I))) . (0 + (card I)) by A4, FUNCT_4:14
.= IncAddr ((halt SCM+FSA),(card I)) by A6, A5, COMPOS_1:122
.= halt SCM+FSA by COMPOS_1:93 ;
DataPart (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) by A1, A7, Th42;
hence ( IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) = card I & DataPart (Comput ((P +* I),(s +* (Initialize I)),(LifeSpan ((P +* I),(s +* (Initialize I)))))) = DataPart (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1))) ) by A1, A7, A8, Th36; :: thesis: ( P +* (I ';' (Stop SCM+FSA)) halts_on s +* (Initialize (I ';' (Stop SCM+FSA))) & LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 & I ';' (Stop SCM+FSA) is_closed_on s,P & I ';' (Stop SCM+FSA) is_halting_on s,P )
dom (P +* (I ';' (Stop SCM+FSA))) = NAT by PARTFUN1:def 4;
then A10: (P +* (I ';' (Stop SCM+FSA))) /. (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1)))) = (P +* (I ';' (Stop SCM+FSA))) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1)))) by PARTFUN1:def 8;
A11: CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),((LifeSpan ((P +* I),(s +* (Initialize I)))) + 1)))) = (P +* (I ';' (Stop SCM+FSA))) . (card I) by A1, A7, A8, Th36, A10
.= halt SCM+FSA by A9 ;
hence A12: P +* (I ';' (Stop SCM+FSA)) halts_on s +* (Initialize (I ';' (Stop SCM+FSA))) by EXTPRO_1:30; :: thesis: ( LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 & I ';' (Stop SCM+FSA) is_closed_on s,P & I ';' (Stop SCM+FSA) is_halting_on s,P )
A13: now
let k be Element of NAT ; :: thesis: ( k <= LifeSpan ((P +* I),(s +* (Initialize I))) implies IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),k)) in dom (I ';' (Stop SCM+FSA)) )
assume A14: k <= LifeSpan ((P +* I),(s +* (Initialize I))) ; :: thesis: IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),k)) in dom (I ';' (Stop SCM+FSA))
then IC (Comput ((P +* I),(s +* (Initialize I)),k)) = IC (Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k)) by A1, A7, Th35, COMPOS_1:24;
then A15: IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),k)) = IC (Comput ((P +* I),(s +* (Initialize I)),k)) by A1, A7, A14, Th42;
A16: ProgramPart I = I by RELAT_1:209;
A17: IC (Comput ((P +* I),(s +* (Initialize I)),k)) in dom I by A1, SCMFSA7B:def 7, A16;
dom I c= dom (I ';' (Stop SCM+FSA)) by SCMFSA6A:56;
hence IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),k)) in dom (I ';' (Stop SCM+FSA)) by A15, A17; :: thesis: verum
end;
defpred S1[ Nat] means ( ( LifeSpan ((P +* I),(s +* (Initialize I))) < $1 implies IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),$1)) = card I ) & IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),$1)) in dom (I ';' (Stop SCM+FSA)) );
card (Stop SCM+FSA) = 1 by COMPOS_1:46;
then card (I ';' (Stop SCM+FSA)) = (card I) + 1 by SCMFSA6A:61;
then A18: (card I) + 0 < card (I ';' (Stop SCM+FSA)) by XREAL_1:8;
then A19: card I in dom (I ';' (Stop SCM+FSA)) by AFINSQ_1:70;
A20: now
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[b1 + 1] )
assume A21: S1[k] ; :: thesis: S1[b1 + 1]
per cases ( k < LifeSpan ((P +* I),(s +* (Initialize I))) or k = LifeSpan ((P +* I),(s +* (Initialize I))) or k > LifeSpan ((P +* I),(s +* (Initialize I))) ) by XXREAL_0:1;
suppose k < LifeSpan ((P +* I),(s +* (Initialize I))) ; :: thesis: S1[b1 + 1]
then k + 1 <= LifeSpan ((P +* I),(s +* (Initialize I))) by NAT_1:13;
hence S1[k + 1] by A13; :: thesis: verum
end;
suppose k = LifeSpan ((P +* I),(s +* (Initialize I))) ; :: thesis: S1[b1 + 1]
hence S1[k + 1] by A1, A7, A8, A19, Th36; :: thesis: verum
end;
suppose A22: k > LifeSpan ((P +* I),(s +* (Initialize I))) ; :: thesis: S1[b1 + 1]
A23: now
assume k + 1 > LifeSpan ((P +* I),(s +* (Initialize I))) ; :: thesis: IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(k + 1))) = card I
dom (P +* (I ';' (Stop SCM+FSA))) = NAT by PARTFUN1:def 4;
then A24: (P +* (I ';' (Stop SCM+FSA))) /. (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),k))) = (P +* (I ';' (Stop SCM+FSA))) . (IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),k))) by PARTFUN1:def 8;
A25: CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),k))) = halt SCM+FSA by A9, A21, A22, A24;
thus IC (Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),(k + 1))) = IC (Following ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),k)))) by EXTPRO_1:4
.= card I by A21, A22, A25, EXTPRO_1:def 3 ; :: thesis: verum
end;
k + 1 > k + 0 by XREAL_1:8;
hence S1[k + 1] by A18, A22, A23, AFINSQ_1:70, XXREAL_0:2; :: thesis: verum
end;
end;
end;
now
let k be Element of NAT ; :: thesis: ( k < (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 implies CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),k))) <> halt SCM+FSA )
assume k < (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 ; :: thesis: CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),k))) <> halt SCM+FSA
then A26: k <= LifeSpan ((P +* I),(s +* (Initialize I))) by NAT_1:13;
then CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize (Directed I))),k))) <> halt SCM+FSA by A1, A7, Th35;
hence CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),k))) <> halt SCM+FSA by A1, A7, A26, Th42; :: thesis: verum
end;
then for k being Element of NAT st CurInstr ((P +* (I ';' (Stop SCM+FSA))),(Comput ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA)))),k))) = halt SCM+FSA holds
(LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 <= k ;
hence LifeSpan ((P +* (I ';' (Stop SCM+FSA))),(s +* (Initialize (I ';' (Stop SCM+FSA))))) = (LifeSpan ((P +* I),(s +* (Initialize I)))) + 1 by A11, A12, EXTPRO_1:def 14; :: thesis: ( I ';' (Stop SCM+FSA) is_closed_on s,P & I ';' (Stop SCM+FSA) is_halting_on s,P )
A27: S1[ 0 ] by A13, NAT_1:2;
A28: ProgramPart (I ';' (Stop SCM+FSA)) = I ';' (Stop SCM+FSA) by RELAT_1:209;
for k being Element of NAT holds S1[k] from NAT_1:sch 1(A27, A20);
 hence I ';' (Stop SCM+FSA) is_closed_on s,P by SCMFSA7B:def 7, A28; :: thesis: I ';' (Stop SCM+FSA) is_halting_on s,P
thus I ';' (Stop SCM+FSA) is_halting_on s,P by A12, SCMFSA7B:def 8, A28; :: thesis: verum