let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for i being parahalting Instruction of SCMPDS holds Exec (i,s) = IExec ((Load i),P,s)

let s be 0 -started State of SCMPDS; :: thesis: for i being parahalting Instruction of SCMPDS holds Exec (i,s) = IExec ((Load i),P,s)
let i be parahalting Instruction of SCMPDS; :: thesis: Exec (i,s) = IExec ((Load i),P,s)
set Li = Load i;
set Mi = Macro i;
set PI = P +* ();
set IC1 = IC (Comput ((P +* ()),s,1));
A1: Initialize s = s by MEMSTR_0:44;
Macro i c= P +* () by FUNCT_4:25;
then A2: P +* () halts_on s by SCMPDS_4:def 7;
A3: 1 in dom () by COMPOS_1:57;
A4: 0 in dom () by COMPOS_1:57;
A5: (Macro i) . 1 = halt SCMPDS by COMPOS_1:59;
A6: (Macro i) . 0 = i by COMPOS_1:58;
A7: Macro i c= P +* () by FUNCT_4:25;
then A8: IC (Comput ((P +* ()),s,1)) in dom () by SCMPDS_4:def 6;
A9: (P +* ()) /. (IC s) = (P +* ()) . (IC s) by PBOOLE:143;
A10: Comput ((P +* ()),s,(0 + 1)) = Following ((P +* ()),(Comput ((P +* ()),s,0))) by EXTPRO_1:3
.= Following ((P +* ()),s)
.= Exec (((P +* ()) . 0),s) by
.= Exec (i,s) by ;
per cases ( IC (Comput ((P +* ()),s,1)) = 0 or IC (Comput ((P +* ()),s,1)) = 1 ) by ;
suppose A11: IC (Comput ((P +* ()),s,1)) = 0 ; :: thesis: Exec (i,s) = IExec ((Load i),P,s)
set Ni = InsCode i;
(IC s) + 1 = 0 + 1 by ;
then A12: InsCode i in {0,1,4,5,6,14} by ;
A13: CurInstr ((P +* ()),(Comput ((P +* ()),s,1))) = (P +* ()) . 0 by
.= i by ;
A14: InsCode i <> 1 by Th10;
hereby :: thesis: verum
per cases ;
suppose i = halt SCMPDS ; :: thesis: Exec (i,s) = IExec ((Load i),P,s)
hence Exec (i,s) = IExec ((Load i),P,s) by ; :: thesis: verum
end;
suppose A15: i <> halt SCMPDS ; :: thesis: Exec (i,s) = IExec ((Load i),P,s)
A16: now :: thesis: for b being Int_position holds s . b = (Exec (i,s)) . b
let b be Int_position; :: thesis: s . b1 = (Exec (i,s)) . b1
per cases ( InsCode i = 0 or InsCode i = 14 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 ) by ;
suppose InsCode i = 0 ; :: thesis: s . b1 = (Exec (i,s)) . b1
hence s . b = (Exec (i,s)) . b by SCMPDS_2:86; :: thesis: verum
end;
suppose InsCode i = 14 ; :: thesis: s . b1 = (Exec (i,s)) . b1
end;
suppose InsCode i = 4 ; :: thesis: s . b1 = (Exec (i,s)) . b1
then ex a being Int_position ex k1, k2 being Integer st i = (a,k1) <>0_goto k2 by SCMPDS_2:30;
hence s . b = (Exec (i,s)) . b by SCMPDS_2:55; :: thesis: verum
end;
suppose InsCode i = 5 ; :: thesis: s . b1 = (Exec (i,s)) . b1
then ex a being Int_position ex k1, k2 being Integer st i = (a,k1) <=0_goto k2 by SCMPDS_2:31;
hence s . b = (Exec (i,s)) . b by SCMPDS_2:56; :: thesis: verum
end;
suppose InsCode i = 6 ; :: thesis: s . b1 = (Exec (i,s)) . b1
then ex a being Int_position ex k1, k2 being Integer st i = (a,k1) >=0_goto k2 by SCMPDS_2:32;
hence s . b = (Exec (i,s)) . b by SCMPDS_2:57; :: thesis: verum
end;
end;
end;
A17: Following ((P +* ()),s) = Following ((P +* ()),(Comput ((P +* ()),s,0)))
.= Exec (i,s) by ;
A18: IC s = IC (Exec (i,s)) by ;
then A19: s = Exec (i,s) by ;
now :: thesis: for n being Nat holds CurInstr ((P +* ()),(Comput ((P +* ()),s,n))) <> halt SCMPDS
let n be Nat; :: thesis: CurInstr ((P +* ()),(Comput ((P +* ()),s,n))) <> halt SCMPDS
Comput ((P +* ()),s,n) = s by
.= Following ((P +* ()),(Comput ((P +* ()),s,0))) by
.= Comput ((P +* ()),s,(0 + 1)) by EXTPRO_1:3 ;
hence CurInstr ((P +* ()),(Comput ((P +* ()),s,n))) <> halt SCMPDS by ; :: thesis: verum
end;
then not P +* () halts_on s ;
hence Exec (i,s) = IExec ((Load i),P,s) by ; :: thesis: verum
end;
end;
end;
end;
suppose A20: IC (Comput ((P +* ()),s,1)) = 1 ; :: thesis: Exec (i,s) = IExec ((Load i),P,s)
CurInstr ((P +* ()),(Comput ((P +* ()),s,1))) = (P +* ()) . 1 by
.= halt SCMPDS by ;
hence Exec (i,s) = IExec ((Load i),P,s) by ; :: thesis: verum
end;
end;