let s be State of SCM+FSA; :: thesis: for P being Instruction-Sequence of SCM+FSA
for I being really-closed Program of SCM+FSA st I is_halting_on Initialized s,P holds
for k being Nat st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA )
let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed Program of SCM+FSA st I is_halting_on Initialized s,P holds
for k being Nat st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA )
let I be really-closed Program of SCM+FSA; :: thesis: ( I is_halting_on Initialized s,P implies for k being Nat st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA ) )
set s1 = s +* (Initialize ((intloc 0) .--> 1));
set s2 = s +* (Initialize ((intloc 0) .--> 1));
A1: dom (P +* (Directed I)) = NAT by PARTFUN1:def 2;
A2: dom (P +* I) = NAT by PARTFUN1:def 2;
A3: Directed I c= P +* (Directed I) by FUNCT_4:25;
defpred S1[ Nat] means ( $1 <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) implies ( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),$1) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),$1) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),$1))) <> halt SCM+FSA ) );
A4: s +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized s) by MEMSTR_0:44;
IC (s +* (Initialize ((intloc 0) .--> 1))) = 0 by A4, MEMSTR_0:47;
then A5: IC (s +* (Initialize ((intloc 0) .--> 1))) in dom I by AFINSQ_1:65;
A6: I c= P +* I by FUNCT_4:25;
A7: now :: thesis: for k being Nat st Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) holds
not CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = halt SCM+FSA
let k be Nat; :: thesis: ( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) implies not CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = halt SCM+FSA )
dom (Directed I) = dom I by FUNCT_4:99;
then A8: IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) in dom (Directed I) by A5, A6, AMISTD_1:21;
A9: (P +* (Directed I)) /. (IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A1, PARTFUN1:def 6;
assume Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) ; :: thesis: not CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = halt SCM+FSA
then CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = (P +* (Directed I)) . (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A9
.= (Directed I) . (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A8, A3, GRFUNC_1:2 ;
then A10: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) in rng (Directed I) by A8, FUNCT_1:def 3;
assume CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) = halt SCM+FSA ; :: thesis: contradiction
hence contradiction by A10, SCMFSA6A:1; :: thesis: verum
end;
assume A11: I is_halting_on Initialized s,P ; :: thesis: for k being Nat st k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA )
now :: thesis: for k being Nat st ( k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) implies Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) ) & k + 1 <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) holds
( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) <> halt SCM+FSA )
A12: P +* I halts_on s +* (Initialize ((intloc 0) .--> 1)) by A11, A4, SCMFSA7B:def 7;
A13: dom I c= dom (Directed I) by FUNCT_4:99;
let k be Nat; :: thesis: ( ( k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) implies Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) ) & k + 1 <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) implies ( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) <> halt SCM+FSA ) )
assume A14: ( k <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) implies Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k) ) ; :: thesis: ( k + 1 <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) implies ( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) <> halt SCM+FSA ) )
A15: Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) = Following ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k)))),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) ;
A16: IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)) in dom I by A5, A6, AMISTD_1:21;
A17: I c= P +* I by FUNCT_4:25;
A18: CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) = (P +* I) . (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A2, PARTFUN1:def 6
.= I . (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A16, A17, GRFUNC_1:2 ;
A19: k + 0 < k + 1 by XREAL_1:6;
assume A20: k + 1 <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) ; :: thesis: ( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) <> halt SCM+FSA )
then k < LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) by A19, XXREAL_0:2;
then I . (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) <> halt SCM+FSA by A18, A12, EXTPRO_1:def 15;
then A21: CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) = (Directed I) . (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A18, FUNCT_4:105
.= (P +* (Directed I)) . (IC (Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A3, A16, A13, GRFUNC_1:2
.= (P +* (Directed I)) . (IC (Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A14, A20, A19, XXREAL_0:2
.= CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),k))) by A1, PARTFUN1:def 6 ;
Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) = Following ((P +* I),(Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) by EXTPRO_1:3
.= Exec ((CurInstr ((P +* I),(Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k)))),(Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),k))) ;
hence Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)) by A14, A20, A19, A21, A15, XXREAL_0:2; :: thesis: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) <> halt SCM+FSA
hence CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),(k + 1)))) <> halt SCM+FSA by A7; :: thesis: verum
end;
then A22: for k being Nat st S1[k] holds
S1[k + 1] ;
now :: thesis: ( 0 <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) implies ( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),0) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),0) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),0))) <> halt SCM+FSA ) )
assume 0 <= LifeSpan ((P +* I),(s +* (Initialize ((intloc 0) .--> 1)))) ; :: thesis: ( Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),0) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),0) & CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),0))) <> halt SCM+FSA )
thus Comput ((P +* I),(s +* (Initialize ((intloc 0) .--> 1))),0) = Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),0) ; :: thesis: CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),0))) <> halt SCM+FSA
hence CurInstr ((P +* (Directed I)),(Comput ((P +* (Directed I)),(s +* (Initialize ((intloc 0) .--> 1))),0))) <> halt SCM+FSA by A7; :: thesis: verum
end;
then A23: S1[ 0 ] ;
thus for k being Nat holds S1[k] from NAT_1:sch 2(A23, A22); :: thesis: verum