let s be State of ; :: thesis:
let I be shiftable No-StopCode Program of ; :: thesis:
let J be shiftable Program of ; :: thesis:
let a be Int_position ; :: thesis:
let k1 be Integer; :: thesis:
set b = DataLoc (s . a),k1;
assume A1: s . (DataLoc (s . a),k1) = 0 ; :: thesis:
set i = a,k1 <>0_goto ((card I) + 2);
set G = Goto ((card J) + 1);
set I2 = (I ';' (Goto ((card J) + 1))) ';' J;
set IF = if=0 a,k1,I,J;
set IsIF = Initialized (stop (if=0 a,k1,I,J));
set pI2 = stop ((I ';' (Goto ((card J) + 1))) ';' J);
set II2 = Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J));
set s2 = s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)));
set s3 = s +* (Initialized (stop (if=0 a,k1,I,J)));
set s4 = Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),1;
A2: IC (s +* (Initialized (stop (if=0 a,k1,I,J)))) = inspos 0 by FUNCT_4:26, SCMPDS_5:18;
A3: not DataLoc (s . a),k1 in dom (Initialized (stop (if=0 a,k1,I,J))) by SCMPDS_4:31;
A4: if=0 a,k1,I,J = ((a,k1 <>0_goto ((card I) + 2)) ';' (I ';' (Goto ((card J) + 1)))) ';' J by SCMPDS_4:50
.= (a,k1 <>0_goto ((card I) + 2)) ';' ((I ';' (Goto ((card J) + 1))) ';' J) by SCMPDS_4:50 ;
then A5: Shift (stop ((I ';' (Goto ((card J) + 1))) ';' J)),1 c= Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),1 by Lm5;
A6: Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),(0 + 1) = Following (Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),0 ) by AMI_1:14
.= Following (s +* (Initialized (stop (if=0 a,k1,I,J)))) by AMI_1:13
.= Exec (a,k1 <>0_goto ((card I) + 2)),(s +* (Initialized (stop (if=0 a,k1,I,J)))) by A4, Th22 ;
not a in dom (Initialized (stop (if=0 a,k1,I,J))) by SCMPDS_4:31;
then (s +* (Initialized (stop (if=0 a,k1,I,J)))) . (DataLoc ((s +* (Initialized (stop (if=0 a,k1,I,J)))) . a),k1) = (s +* (Initialized (stop (if=0 a,k1,I,J)))) . (DataLoc (s . a),k1) by FUNCT_4:12
.= 0 by A1, A3, FUNCT_4:12 ;
then A7: IC (Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),1) = Next (IC (s +* (Initialized (stop (if=0 a,k1,I,J))))) by A6, SCMPDS_2:67
.= inspos (0 + 1) by A2 ;
A8: DataPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = DataPart (s +* (Initialized (stop (if=0 a,k1,I,J)))) by SCMPDS_4:24, SCMPDS_4:36;

now

let a be Int_position ; :: thesis:
thus (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) . a = (s +* (Initialized (stop (if=0 a,k1,I,J)))) . a by A8, SCMPDS_4:23
.= (Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),1) . a by A6, SCMPDS_2:67 ; :: thesis:

end;

now

let l be Element of NAT ; :: thesis:
assume A18: l < (LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) + 1 ; :: thesis:

per cases ;

suppose l = 0 ; :: thesis:

then CurInstr (Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),l) = CurInstr (s +* (Initialized (stop (if=0 a,k1,I,J)))) by AMI_1:13;
hence CurInstr (Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),l) <> halt SCMPDS by A17, Th29; :: thesis:

end;

suppose l <> 0 ; :: thesis:

then consider n being Nat such that
A19: l = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A20: n < LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) by A18, A19, XREAL_1:8;
assume A21: CurInstr (Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),l) = halt SCMPDS ; :: thesis:
CurInstr (Computation (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),n) = CurInstr (Computation (Computation (s +* (Initialized (stop (if=0 a,k1,I,J)))),1),n) by A14, A5, A7, A9, Th45
.= halt SCMPDS by A19, A21, AMI_1:51 ;
hence contradiction by A13, A20, AMI_1:def 46; :: thesis:

end;

A24: now

let x be set ; :: thesis:
A25: IExec ((I ';' (Goto ((card J) + 1))) ';' J),s = (Result (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) +* (s | NAT ) by SCMPDS_4:def 8;
A26: IExec (if=0 a,k1,I,J),s = (Result (s +* (Initialized (stop (if=0 a,k1,I,J))))) +* (s | NAT ) by SCMPDS_4:def 8;
A27: dom (Start-At (inspos (((card I) + (card J)) + 2))) = {(IC SCMPDS )} by FUNCOP_1:19;
assume A28: x in dom (IExec (if=0 a,k1,I,J),s) ; :: thesis:

per cases by A28, SCMPDS_4:20;

suppose A29: x is Int_position ; :: thesis:

then x <> IC SCMPDS by SCMPDS_2:52;
then A30: not x in dom (Start-At (inspos (((card I) + (card J)) + 2))) by A27, TARSKI:def 1;

A31: now

assume x in dom (s | NAT ) ; :: thesis:
then reconsider l = x as Instruction-Location of SCMPDS by A10, AMI_1:def 4;
l = x ;
hence contradiction by A29, SCMPDS_2:53; :: thesis:

end;

hence (IExec (if=0 a,k1,I,J),s) . x = (Result (s +* (Initialized (stop (if=0 a,k1,I,J))))) . x by A26, FUNCT_4:12
.= (Result (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))) . x by A23, A29, SCMPDS_4:23
.= (IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) . x by A25, A31, FUNCT_4:12
.= ((IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) +* (Start-At (inspos (((card I) + (card J)) + 2)))) . x by A30, FUNCT_4:12 ;
:: thesis:

end;

suppose A32: x = IC SCMPDS ; :: thesis:

A33: now

assume x in dom (s | NAT ) ; :: thesis:
then reconsider l = x as Instruction-Location of SCMPDS by A10, AMI_1:def 4;
l = x ;
hence contradiction by A32, AMI_1:48; :: thesis:

end;

end;

suppose x is Instruction-Location of SCMPDS ; :: thesis:

hence (IExec (if=0 a,k1,I,J),s) . x = ((IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) +* (Start-At (inspos (((card I) + (card J)) + 2)))) . x by Th26; :: thesis:

end;

dom (IExec (if=0 a,k1,I,J),s) = the carrier of SCMPDS by AMI_1:79
.= dom ((IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) +* (Start-At (inspos (((card I) + (card J)) + 2)))) by AMI_1:79 ;
hence IExec (if=0 a,k1,I,J),s = (IExec ((I ';' (Goto ((card J) + 1))) ';' J),s) +* (Start-At (inspos (((card I) + (card J)) + 2))) by A24, FUNCT_1:9
.= ((IExec I,s) +* (Start-At (inspos (((card I) + (card J)) + 1)))) +* (Start-At (inspos (((card I) + (card J)) + 2))) by A11, A12, Th47
.= (IExec I,s) +* (Start-At (inspos (((card I) + (card J)) + 2))) by Th14 ;
:: thesis: