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: ( NPP (p +* P) c= s implies for P being the Instructions of S -valued ManySortedSet of NAT st ProgramPart (p +* P) c= P holds
P halts_on s )
assume A2: NPP (p +* P) c= s ; :: thesis: for P being the Instructions of S -valued ManySortedSet of NAT st ProgramPart (p +* P) c= P holds
P halts_on s
let Q be the Instructions of S -valued ManySortedSet of NAT ; :: thesis: ( ProgramPart (p +* P) c= Q implies Q halts_on s )
assume A3: ProgramPart (p +* P) c= Q ; :: thesis: Q halts_on s
A4: P c= p +* P by FUNCT_4:26;
take 0 ; :: according to EXTPRO_1:def 7 :: thesis: ( IC (Comput (Q,s,0)) in dom Q & CurInstr (Q,(Comput (Q,s,0))) = halt S )
dom Q = NAT by PARTFUN1:def 4;
hence IC (Comput (Q,s,0)) in dom Q ; :: thesis: CurInstr (Q,(Comput (Q,s,0))) = halt S
Start-At (l,S) c= p +* P by COMPOS_1:151;
then Start-At (l,S) c= NPP (p +* P) by COMPOS_1:204;
then A5: Start-At (l,S) c= s by A2, XBOOLE_1:1;
l .--> (halt S) c= p +* P by A1, A4, XBOOLE_1:1;
then l .--> (halt S) c= ProgramPart (p +* P) by RELAT_1:210;
then A6: l .--> (halt S) c= Q by A3, XBOOLE_1:1;
A7: dom (l .--> (halt S)) = {l} by FUNCOP_1:19;
IC in dom (Start-At (l,S)) by COMPOS_1:52;
then A8: IC s = IC (Start-At (l,S)) by A5, GRFUNC_1:8
.= l by COMPOS_1:64 ;
A9: IC s in dom (l .--> (halt S)) by A7, A8, TARSKI:def 1;
A10: dom (l .--> (halt S)) c= dom Q by A6, RELAT_1:25;
thus CurInstr (Q,(Comput (Q,s,0))) = CurInstr (Q,s) by Th3
.= Q . (IC s) by A10, A9, PARTFUN1:def 8
.= (l .--> (halt S)) . (IC s) by A9, A6, GRFUNC_1:8
.= CurInstr ((l .--> (halt S)),s) by A9, PARTFUN1:def 8
.= halt S by A5, COMPOS_1:6 ; :: thesis: verum