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 +* (Macro i);
set IC1 = IC (Comput ((P +* (Macro i)),s,1));
I: Initialize s = s by MEMSTR_0:44;
Macro i c= P +* (Macro i) by FUNCT_4:25;
then A2: P +* (Macro i) halts_on s by SCMPDS_4:def 7;
A3: 1 in dom (Macro i) by COMPOS_1:57;
A4: 0 in dom (Macro i) by COMPOS_1:57;
A22: (Macro i) . 1 = halt SCMPDS by COMPOS_1:59;
A23: (Macro i) . 0 = i by COMPOS_1:58;
A24: Macro i c= P +* (Macro i) by FUNCT_4:25;
then A25: IC (Comput ((P +* (Macro i)),s,1)) in dom (Macro i) by SCMPDS_4:def 6;
A26: (P +* (Macro i)) /. (IC s) = (P +* (Macro i)) . (IC s) by PBOOLE:143;
A27: Comput ((P +* (Macro i)),s,(0 + 1)) = Following ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,0))) by EXTPRO_1:3
.= Following ((P +* (Macro i)),s) by EXTPRO_1:2
.= Exec (((P +* (Macro i)) . 0),s) by A26, MEMSTR_0:47, I
.= Exec (i,s) by A4, A23, A24, GRFUNC_1:2 ;

per cases ( IC (Comput ((P +* (Macro i)),s,1)) = 0 or IC (Comput ((P +* (Macro i)),s,1)) = 1 ) by A25, COMPOS_1:60;

suppose A28: IC (Comput ((P +* (Macro i)),s,1)) = 0 ; :: thesis: Exec (i,s) = IExec ((Load i),P,s)

set Ni = InsCode i;
succ (IC s) = succ 0 by MEMSTR_0:47, I
.= 1 ;
then A29: InsCode i in {0,1,4,5,6} by A27, A28, SCMPDS_4:1;
A30: CurInstr ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,1))) = (P +* (Macro i)) . 0 by A28, PBOOLE:143
.= i by A4, A23, A24, GRFUNC_1:2 ;
A31: InsCode i <> 1 by Th26;

hereby :: thesis: verum

per cases ( i = halt SCMPDS or i <> halt SCMPDS ) ;

suppose i = halt SCMPDS ; :: thesis: Exec (i,s) = IExec ((Load i),P,s)

hence Exec (i,s) = IExec ((Load i),P,s) by A2, A27, A30, EXTPRO_1:def 9; :: thesis: verum

end;

suppose A32: i <> halt SCMPDS ; :: thesis: Exec (i,s) = IExec ((Load i),P,s)

A34: now

let b be Int_position ; :: thesis: s . b₁ = (Exec (i,s)) . b₁

per cases ( InsCode i = 0 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 ) by A29, A31, ENUMSET1:def 3;

suppose InsCode i = 0 ; :: thesis: s . b₁ = (Exec (i,s)) . b₁

then ex k1 being Integer st i = goto k1 by SCMPDS_2:26;
hence s . b = (Exec (i,s)) . b by SCMPDS_2:54; :: thesis: verum

end;

suppose InsCode i = 4 ; :: thesis: s . b₁ = (Exec (i,s)) . b₁

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 . b₁ = (Exec (i,s)) . b₁

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 . b₁ = (Exec (i,s)) . b₁

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;

A35: Following ((P +* (Macro i)),s) = Following ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,0))) by EXTPRO_1:2
.= Exec (i,s) by A27, EXTPRO_1:3 ;
A36: IC s = IC (Exec (i,s)) by A27, A28, MEMSTR_0:47, I;
then A37: s = Exec (i,s) by A34, SCMPDS_2:44;

now

let n be Element of NAT ; :: thesis: CurInstr ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,n))) <> halt SCMPDS
Comput ((P +* (Macro i)),s,n) = s by A36, A34, A35, EXTPRO_1:27, SCMPDS_2:44
.= Following ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,0))) by A37, A35, EXTPRO_1:2
.= Comput ((P +* (Macro i)),s,(0 + 1)) by EXTPRO_1:3 ;
hence CurInstr ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,n))) <> halt SCMPDS by A30, A32; :: thesis: verum

end;

then not P +* (Macro i) halts_on s by EXTPRO_1:29;
hence Exec (i,s) = IExec ((Load i),P,s) by A24, SCMPDS_4:def 7; :: thesis: verum

end;

end;

end;

end;

suppose A38: IC (Comput ((P +* (Macro i)),s,1)) = 1 ; :: thesis: Exec (i,s) = IExec ((Load i),P,s)

CurInstr ((P +* (Macro i)),(Comput ((P +* (Macro i)),s,1))) = (P +* (Macro i)) . 1 by A38, PBOOLE:143
.= halt SCMPDS by A3, A22, A24, GRFUNC_1:2 ;
hence Exec (i,s) = IExec ((Load i),P,s) by A2, A27, EXTPRO_1:def 9; :: thesis: verum

end;

end;