let s be State of SCM+FSA; :: thesis: for p being the Instructions of SCM+FSA -valued ManySortedSet of NAT
for I being InitHalting Program of SCM+FSA st Initialized I c= s & I c= p holds
for k being Element of NAT st k <= LifeSpan (p,s) holds
CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* (Directed I)),k))) <> halt SCM+FSA
let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for I being InitHalting Program of SCM+FSA st Initialized I c= s & I c= p holds
for k being Element of NAT st k <= LifeSpan (p,s) holds
CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* (Directed I)),k))) <> halt SCM+FSA
set A = NAT ;
let I be InitHalting Program of SCM+FSA; :: thesis: ( Initialized I c= s & I c= p implies for k being Element of NAT st k <= LifeSpan (p,s) holds
CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* (Directed I)),k))) <> halt SCM+FSA )
set s2 = s +* (Directed I);
set p2 = p +* (Directed I);
A1: ProgramPart (Initialized I) = I by SCMFSA6A:33;
set m = LifeSpan (p,s);
assume A2: Initialized I c= s ; :: thesis: ( not I c= p or for k being Element of NAT st k <= LifeSpan (p,s) holds
CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* (Directed I)),k))) <> halt SCM+FSA )
assume A3: I c= p ; :: thesis: for k being Element of NAT st k <= LifeSpan (p,s) holds
CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* (Directed I)),k))) <> halt SCM+FSA
then A4: p halts_on s by EXTPRO_1:def 10, A2, A1;
A5: now
set s1 = s +* (I ';' I);
set p1 = p +* (I ';' I);
let k be Element of NAT ; :: thesis: ( k <= LifeSpan (p,s) implies Comput (p,s,k), Comput ((p +* (Directed I)),(s +* (Directed I)),k) equal_outside NAT )
defpred S1[ Nat] means ( $1 <= k implies Comput ((p +* (I ';' I)),(s +* (I ';' I)),$1), Comput ((p +* (Directed I)),(s +* (Directed I)),$1) equal_outside NAT );
assume A6: k <= LifeSpan (p,s) ; :: thesis: Comput (p,s,k), Comput ((p +* (Directed I)),(s +* (Directed I)),k) equal_outside NAT
A7: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
A8: Directed I c= I ';' I by SCMFSA6A:55;
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
A9: dom I c= dom (I ';' I) by SCMFSA6A:56;
assume A10: ( n <= k implies Comput ((p +* (I ';' I)),(s +* (I ';' I)),n), Comput ((p +* (Directed I)),(s +* (Directed I)),n) equal_outside NAT ) ; :: thesis: S1[n + 1]
A11: Comput ((p +* (Directed I)),(s +* (Directed I)),(n + 1)) = Following ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* (Directed I)),n))) by EXTPRO_1:4
.= Exec ((CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* (Directed I)),n)))),(Comput ((p +* (Directed I)),(s +* (Directed I)),n))) ;
A12: Comput ((p +* (I ';' I)),(s +* (I ';' I)),(n + 1)) = Following ((p +* (I ';' I)),(Comput ((p +* (I ';' I)),(s +* (I ';' I)),n))) by EXTPRO_1:4
.= Exec ((CurInstr ((p +* (I ';' I)),(Comput ((p +* (I ';' I)),(s +* (I ';' I)),n)))),(Comput ((p +* (I ';' I)),(s +* (I ';' I)),n))) ;
A13: n <= n + 1 by NAT_1:12;
assume A14: n + 1 <= k ; :: thesis: Comput ((p +* (I ';' I)),(s +* (I ';' I)),(n + 1)), Comput ((p +* (Directed I)),(s +* (Directed I)),(n + 1)) equal_outside NAT
then A15: IC (Comput ((p +* (I ';' I)),(s +* (I ';' I)),n)) = IC (Comput ((p +* (Directed I)),(s +* (Directed I)),n)) by A10, A13, COMPOS_1:24, XXREAL_0:2;
n <= k by A14, A13, XXREAL_0:2;
then n <= LifeSpan (p,s) by A6, XXREAL_0:2;
then IC (Comput (p,s,n)) = IC (Comput ((p +* (I ';' I)),(s +* (I ';' I)),n)) by A2, A4, Th18, COMPOS_1:24, A3;
then A16: IC (Comput ((p +* (I ';' I)),(s +* (I ';' I)),n)) in dom I by A2, Def1, A3;
then A17: IC (Comput ((p +* (Directed I)),(s +* (Directed I)),n)) in dom (Directed I) by A15, FUNCT_4:105;
A18: CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* (Directed I)),n))) = (p +* (Directed I)) . (IC (Comput ((p +* (Directed I)),(s +* (Directed I)),n))) by PBOOLE:158
.= (Directed I) . (IC (Comput ((p +* (Directed I)),(s +* (Directed I)),n))) by A17, FUNCT_4:14 ;
CurInstr ((p +* (I ';' I)),(Comput ((p +* (I ';' I)),(s +* (I ';' I)),n))) = (p +* (I ';' I)) . (IC (Comput ((p +* (I ';' I)),(s +* (I ';' I)),n))) by PBOOLE:158
.= (I ';' I) . (IC (Comput ((p +* (I ';' I)),(s +* (I ';' I)),n))) by A9, A16, FUNCT_4:14
.= (Directed I) . (IC (Comput ((p +* (I ';' I)),(s +* (I ';' I)),n))) by A8, A15, A17, GRFUNC_1:8 ;
hence Comput ((p +* (I ';' I)),(s +* (I ';' I)),(n + 1)), Comput ((p +* (Directed I)),(s +* (Directed I)),(n + 1)) equal_outside NAT by A10, A14, A13, A15, A18, A12, A11, AMISTD_2:def 20, XXREAL_0:2; :: thesis: verum
end;
( Comput ((p +* (I ';' I)),(s +* (I ';' I)),0) = s +* (I ';' I) & Comput ((p +* (Directed I)),(s +* (Directed I)),0) = s +* (Directed I) ) by EXTPRO_1:3;
then Comput ((p +* (Directed I)),(s +* (Directed I)),0), Comput ((p +* (I ';' I)),(s +* (I ';' I)),0) equal_outside NAT by FUNCT_7:107, FUNCT_7:133;
then A19: S1[ 0 ] by FUNCT_7:28;
for n being Element of NAT holds S1[n] from NAT_1:sch 1(A19, A7);
then A20: Comput ((p +* (I ';' I)),(s +* (I ';' I)),k), Comput ((p +* (Directed I)),(s +* (Directed I)),k) equal_outside NAT ;
Comput (p,s,k), Comput ((p +* (I ';' I)),(s +* (I ';' I)),k) equal_outside NAT by A2, A4, A6, Th18, A3;
hence Comput (p,s,k), Comput ((p +* (Directed I)),(s +* (Directed I)),k) equal_outside NAT by A20, FUNCT_7:29; :: thesis: verum
end;
let k be Element of NAT ; :: thesis: ( k <= LifeSpan (p,s) implies CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* (Directed I)),k))) <> halt SCM+FSA )
set lk = IC (Comput (p,s,k));
A21: ( IC (Comput (p,s,k)) in dom I & dom I = dom (Directed I) ) by A2, A3, Def1, FUNCT_4:105;
then A22: (Directed I) . (IC (Comput (p,s,k))) in rng (Directed I) by FUNCT_1:def 5;
assume k <= LifeSpan (p,s) ; :: thesis: CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* (Directed I)),k))) <> halt SCM+FSA
then IC (Comput (p,s,k)) = IC (Comput ((p +* (Directed I)),(s +* (Directed I)),k)) by A5, COMPOS_1:24;
then A23: CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* (Directed I)),k))) = (p +* (Directed I)) . (IC (Comput (p,s,k))) by PBOOLE:158
.= (Directed I) . (IC (Comput (p,s,k))) by A21, FUNCT_4:14 ;
assume CurInstr ((p +* (Directed I)),(Comput ((p +* (Directed I)),(s +* (Directed I)),k))) = halt SCM+FSA ; :: thesis: contradiction
hence contradiction by A23, A22, SCMFSA6A:18; :: thesis: verum