let s1, s2 be State of ; :: thesis: for I being shiftable Program of st Initialized (stop I) c= s1 & I is_closed_on s1 & I is_halting_on s1 holds
for n being Element of NAT st Shift I,n c= s2 & card I > 0 & IC s2 = inspos n & DataPart s1 = DataPart s2 holds
for i being Element of NAT st i < LifeSpan s1 holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & CurInstr (Computation s1,i) = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) )
let I be shiftable Program of ; :: thesis: ( Initialized (stop I) c= s1 & I is_closed_on s1 & I is_halting_on s1 implies for n being Element of NAT st Shift I,n c= s2 & card I > 0 & IC s2 = inspos n & DataPart s1 = DataPart s2 holds
for i being Element of NAT st i < LifeSpan s1 holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & CurInstr (Computation s1,i) = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) ) )
set SI = stop I;
set II = Initialized (stop I);
assume that
A1: Initialized (stop I) c= s1 and
A2: I is_closed_on s1 and
A3: I is_halting_on s1 ; :: thesis: for n being Element of NAT st Shift I,n c= s2 & card I > 0 & IC s2 = inspos n & DataPart s1 = DataPart s2 holds
for i being Element of NAT st i < LifeSpan s1 holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & CurInstr (Computation s1,i) = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) )
dom (stop I) misses dom (Start-At (inspos 0 )) by SCMPDS_4:54;
then A4: stop I c= Initialized (stop I) by FUNCT_4:33;
then A5: dom (stop I) c= dom (Initialized (stop I)) by GRFUNC_1:8;
let n be Element of NAT ; :: thesis: ( Shift I,n c= s2 & card I > 0 & IC s2 = inspos n & DataPart s1 = DataPart s2 implies for i being Element of NAT st i < LifeSpan s1 holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & CurInstr (Computation s1,i) = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) ) )
assume that
A6: Shift I,n c= s2 and
A7: card I > 0 and
A8: IC s2 = inspos n and
A9: DataPart s1 = DataPart s2 ; :: thesis: for i being Element of NAT st i < LifeSpan s1 holds
( (IC (Computation s1,i)) + n = IC (Computation s2,i) & CurInstr (Computation s1,i) = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) )
defpred S₁[ Element of NAT ] means ( $1 < LifeSpan s1 implies ( (IC (Computation s1,$1)) + n = IC (Computation s2,$1) & CurInstr (Computation s1,$1) = CurInstr (Computation s2,$1) & DataPart (Computation s1,$1) = DataPart (Computation s2,$1) ) );
A10: s1 = s1 +* (Initialized (stop I)) by A1, FUNCT_4:79;
A11: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A12: S₁[k] ; :: thesis: S₁[k + 1]

now

reconsider m = IC (Computation s1,k) as Element of NAT by ORDINAL1:def 13;
set i = CurInstr (Computation s1,k);
A13: k <= k + 1 by NAT_1:11;
A14: IC (Computation s1,k) = inspos m ;
reconsider l = IC (Computation s1,(k + 1)) as Element of NAT by ORDINAL1:def 13;
A15: Computation s1,(k + 1) = Following (Computation s1,k) by AMI_1:14
.= Exec (CurInstr (Computation s1,k)),(Computation s1,k) ;
assume A16: k + 1 < LifeSpan s1 ; :: thesis: ( (IC (Computation s1,(k + 1))) + n = IC (Computation s2,(k + 1)) & CurInstr (Computation s1,(k + 1)) = CurInstr (Computation s2,(k + 1)) & DataPart (Computation s1,(k + 1)) = DataPart (Computation s2,(k + 1)) )
then A17: IC (Computation s1,(k + 1)) in dom I by A1, A2, A3, Th33;
then A18: l + n in dom (Shift I,n) by VALUED_1:25;
A19: Computation s2,(k + 1) = Following (Computation s2,k) by AMI_1:14
.= Exec (CurInstr (Computation s2,k)),(Computation s2,k) ;
A20: IC (Computation s1,k) in dom (stop I) by A2, A10, SCMPDS_6:def 2;
A21: CurInstr (Computation s1,k) = s1 . (IC (Computation s1,k)) by AMI_1:54
.= (Initialized (stop I)) . (IC (Computation s1,k)) by A1, A5, A20, GRFUNC_1:8
.= (stop I) . (IC (Computation s1,k)) by A4, A20, GRFUNC_1:8 ;
then A22: InsCode (CurInstr (Computation s1,k)) <> 3 by A20, A14, SCMPDS_4:def 12;
A23: IC (Computation s1,(k + 1)) in dom (stop I) by A2, A10, SCMPDS_6:def 2;
A24: CurInstr (Computation s1,k) valid_at m by A20, A21, A14, SCMPDS_4:def 12;
A25: InsCode (CurInstr (Computation s1,k)) <> 1 by A20, A21, A14, SCMPDS_4:def 12;
hence A26: (IC (Computation s1,(k + 1))) + n = IC (Computation s2,(k + 1)) by A12, A16, A13, A15, A19, A14, A22, A24, SCMPDS_4:83, XXREAL_0:2; :: thesis: ( CurInstr (Computation s1,(k + 1)) = CurInstr (Computation s2,(k + 1)) & DataPart (Computation s1,(k + 1)) = DataPart (Computation s2,(k + 1)) )
CurInstr (Computation s1,(k + 1)) = s1 . l by AMI_1:54
.= (Initialized (stop I)) . l by A1, A5, A23, GRFUNC_1:8
.= (stop I) . l by A4, A23, GRFUNC_1:8 ;
hence CurInstr (Computation s1,(k + 1)) = (Shift (stop I),n) . (l + n) by A23, VALUED_1:def 12
.= (Shift I,n) . (IC (Computation s2,(k + 1))) by A26, A17, Th18
.= s2 . (IC (Computation s2,(k + 1))) by A6, A26, A18, GRFUNC_1:8
.= CurInstr (Computation s2,(k + 1)) by AMI_1:54 ;
:: thesis: DataPart (Computation s1,(k + 1)) = DataPart (Computation s2,(k + 1))
thus DataPart (Computation s1,(k + 1)) = DataPart (Computation s2,(k + 1)) by A12, A16, A13, A15, A19, A14, A25, A22, A24, SCMPDS_4:83, XXREAL_0:2; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

let i be Element of NAT ; :: thesis: ( i < LifeSpan s1 implies ( (IC (Computation s1,i)) + n = IC (Computation s2,i) & CurInstr (Computation s1,i) = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) ) )
A27: inspos 0 in dom (stop I) by SCMPDS_4:75;
A28: inspos 0 in dom I by A7, SCMPDS_4:1;
A29: S₁[ 0 ]

proof

assume 0 < LifeSpan s1 ; :: thesis: ( (IC (Computation s1,0 )) + n = IC (Computation s2,0 ) & CurInstr (Computation s1,0 ) = CurInstr (Computation s2,0 ) & DataPart (Computation s1,0 ) = DataPart (Computation s2,0 ) )
A30: inspos (0 + n) in dom (Shift I,n) by A28, VALUED_1:25;
A31: IC SCMPDS in dom (Initialized (stop I)) by SCMPDS_4:7;
then A32: s1 . (IC s1) = s1 . ((Initialized (stop I)) . (IC SCMPDS )) by A1, GRFUNC_1:8
.= s1 . (inspos 0 ) by SCMPDS_4:29
.= (Initialized (stop I)) . (inspos 0 ) by A1, A5, A27, GRFUNC_1:8
.= (stop I) . (inspos 0 ) by A4, A27, GRFUNC_1:8 ;
IC (Computation s1,0 ) = s1 . (IC SCMPDS ) by AMI_1:13
.= (Initialized (stop I)) . (IC SCMPDS ) by A1, A31, GRFUNC_1:8
.= inspos 0 by SCMPDS_4:29 ;
hence (IC (Computation s1,0 )) + n = inspos (0 + n)
.= IC (Computation s2,0 ) by A8, AMI_1:13 ;
:: thesis: ( CurInstr (Computation s1,0 ) = CurInstr (Computation s2,0 ) & DataPart (Computation s1,0 ) = DataPart (Computation s2,0 ) )
thus CurInstr (Computation s1,0 ) = CurInstr s1 by AMI_1:13
.= (Shift (stop I),n) . ((inspos 0 ) + n) by A27, A32, VALUED_1:def 12
.= (Shift (stop I),n) . (inspos (0 + n))
.= (Shift I,n) . (inspos n) by A7, Th19
.= CurInstr s2 by A6, A8, A30, GRFUNC_1:8
.= CurInstr (Computation s2,0 ) by AMI_1:13 ; :: thesis: DataPart (Computation s1,0 ) = DataPart (Computation s2,0 )
thus DataPart (Computation s1,0 ) = DataPart s2 by A9, AMI_1:13
.= DataPart (Computation s2,0 ) by AMI_1:13 ; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A29, A11);
hence ( i < LifeSpan s1 implies ( (IC (Computation s1,i)) + n = IC (Computation s2,i) & CurInstr (Computation s1,i) = CurInstr (Computation s2,i) & DataPart (Computation s1,i) = DataPart (Computation s2,i) ) ) ; :: thesis: verum