let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N
for l being Element of NAT
for P being NAT -defined the Instructions of b₁ -valued Function st l .--> (halt S) c= P holds
for p being b₂ -started PartState of S holds p +* P is halting
let S be non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N; :: thesis: for l being Element of NAT
for P being NAT -defined the Instructions of S -valued Function st l .--> (halt S) c= P holds
for p being b₁ -started PartState of S holds p +* P is halting
let l be Element of NAT ; :: thesis: for P being NAT -defined the Instructions of S -valued Function st l .--> (halt S) c= P holds
for p being l -started PartState of S holds p +* P is halting
let P be NAT -defined the Instructions of S -valued Function; :: thesis: ( l .--> (halt S) c= P implies for p being l -started PartState of S holds p +* P is halting )
assume A1: l .--> (halt S) c= P ; :: thesis: for p being l -started PartState of S holds p +* P is halting
let p be l -started PartState of S; :: thesis: p +* P is halting
set h = halt S;
set I = p +* P;
let s be State of S; :: according to EXTPRO_1:def 10 :: thesis: ( p +* P c= s implies ProgramPart s halts_on s )
assume A3: p +* P c= s ; :: thesis: ProgramPart s halts_on s
B3: Start-At (l,S) c= p by COMPOS_1:151;
B4: P c= p +* P by FUNCT_4:26;
take 0 ; :: according to EXTPRO_1:def 7 :: thesis: ( IC (Comput ((ProgramPart s),s,0)) in dom (ProgramPart s) & CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,0))) = halt S )
IC (Comput ((ProgramPart s),s,0)) in NAT ;
hence IC (Comput ((ProgramPart s),s,0)) in dom (ProgramPart s) by COMPOS_1:34; :: thesis: CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,0))) = halt S
dom (Start-At (l,S)) misses dom P by COMPOS_1:130;
then Start-At (l,S) c= p +* P by B3, FUNCT_4:125;
then B1: Start-At (l,S) c= s by A3, XBOOLE_1:1;
l .--> (halt S) c= p +* P by A1, B4, XBOOLE_1:1;
then l .--> (halt S) c= s by A3, XBOOLE_1:1;
then B4: l .--> (halt S) c= ProgramPart s by RELAT_1:210;
B7: dom (l .--> (halt S)) = {l} by FUNCOP_1:19;
IC S in dom (Start-At (l,S)) by COMPOS_1:52;
then B5: IC s = IC (Start-At (l,S)) by B1, GRFUNC_1:8
.= l by COMPOS_1:64 ;
B3: IC s in dom (l .--> (halt S)) by B7, B5, TARSKI:def 1;
B2: dom (l .--> (halt S)) c= dom (ProgramPart s) by B4, RELAT_1:25;
thus CurInstr ((ProgramPart s),(Comput ((ProgramPart s),s,0))) = CurInstr ((ProgramPart s),s) by Th3
.= (ProgramPart s) . (IC s) by B2, B3, PARTFUN1:def 8
.= (l .--> (halt S)) . (IC s) by B3, B4, GRFUNC_1:8
.= CurInstr ((l .--> (halt S)),s) by B3, PARTFUN1:def 8
.= halt S by B1, COMPOS_1:6 ; :: thesis: verum