let p be non NAT -defined autonomic FinPartState of ; :: according to AMISTD_5:def 4 :: thesis: for b1 being set holds
( not NPP p c= b1 or for b2 being set holds
( not ProgramPart p c= b2 or for b3 being Element of NAT holds IC (Comput (b2,b1,b3)) in proj1 (ProgramPart p) ) )
let s be State of SCM; :: thesis: ( not NPP p c= s or for b1 being set holds
( not ProgramPart p c= b1 or for b2 being Element of NAT holds IC (Comput (b1,s,b2)) in proj1 (ProgramPart p) ) )
assume A1: NPP p c= s ; :: thesis: for b1 being set holds
( not ProgramPart p c= b1 or for b2 being Element of NAT holds IC (Comput (b1,s,b2)) in proj1 (ProgramPart p) )
let P be the Instructions of SCM -valued ManySortedSet of NAT ; :: thesis: ( not ProgramPart p c= P or for b1 being Element of NAT holds IC (Comput (P,s,b1)) in proj1 (ProgramPart p) )
assume A2: ProgramPart p c= P ; :: thesis: for b1 being Element of NAT holds IC (Comput (P,s,b1)) in proj1 (ProgramPart p)
let i be Element of NAT ; :: thesis: IC (Comput (P,s,i)) in proj1 (ProgramPart p)
set Csi = Comput (P,s,i);
set loc = IC (Comput (P,s,i));
set loc1 = (IC (Comput (P,s,i))) + 1;
A3: ( IC (Comput (P,s,i)) in dom (ProgramPart p) iff IC (Comput (P,s,i)) in (dom p) /\ NAT ) by RELAT_1:90;
assume not IC (Comput (P,s,i)) in dom (ProgramPart p) ; :: thesis: contradiction
then A4: not IC (Comput (P,s,i)) in dom p by A3, XBOOLE_0:def 4;
set I = (dl. 0) := (dl. 0);
set p1 = p +* ((IC (Comput (P,s,i))) .--> ((dl. 0) := (dl. 0)));
set p2 = p +* ((IC (Comput (P,s,i))) .--> (halt SCM));
reconsider P1 = P +* ((IC (Comput (P,s,i))) .--> ((dl. 0) := (dl. 0))) as the Instructions of SCM -valued ManySortedSet of NAT ;
reconsider P2 = P +* ((IC (Comput (P,s,i))) .--> (halt SCM)) as the Instructions of SCM -valued ManySortedSet of NAT ;
A6: dom ((IC (Comput (P,s,i))) .--> (halt SCM)) = {(IC (Comput (P,s,i)))} by FUNCOP_1:19;
then A7: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> (halt SCM)) by TARSKI:def 1;
A12: dom ((IC (Comput (P,s,i))) .--> ((dl. 0) := (dl. 0))) = {(IC (Comput (P,s,i)))} by FUNCOP_1:19;
then A13: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> ((dl. 0) := (dl. 0))) by TARSKI:def 1;
Y6: dom p misses dom ((IC (Comput (P,s,i))) .--> (halt SCM)) by A4, A6, ZFMISC_1:56;
Y5: dom p misses dom ((IC (Comput (P,s,i))) .--> ((dl. 0) := (dl. 0))) by A4, A12, ZFMISC_1:56;
ProgramPart (p +* ((IC (Comput (P,s,i))) .--> ((dl. 0) := (dl. 0)))) = (ProgramPart p) +* (ProgramPart ((IC (Comput (P,s,i))) .--> ((dl. 0) := (dl. 0)))) by FUNCT_4:75
.= (ProgramPart p) +* ((IC (Comput (P,s,i))) .--> ((dl. 0) := (dl. 0))) by RELAT_1:209 ;
then P3: ProgramPart (p +* ((IC (Comput (P,s,i))) .--> ((dl. 0) := (dl. 0)))) c= P1 by A2, FUNCT_4:131;
ProgramPart (p +* ((IC (Comput (P,s,i))) .--> (halt SCM))) = (ProgramPart p) +* (ProgramPart ((IC (Comput (P,s,i))) .--> (halt SCM))) by FUNCT_4:75
.= (ProgramPart p) +* ((IC (Comput (P,s,i))) .--> (halt SCM)) by RELAT_1:209 ;
then P4: ProgramPart (p +* ((IC (Comput (P,s,i))) .--> (halt SCM))) c= P2 by A2, FUNCT_4:131;
set Cs2i = Comput (P2,s,i);
set Cs1i = Comput (P1,s,i);
not p is autonomic
proof
((IC (Comput (P,s,i))) .--> (halt SCM)) . (IC (Comput (P,s,i))) = halt SCM by FUNCOP_1:87;
then A18: P2 . (IC (Comput (P,s,i))) = halt SCM by A7, FUNCT_4:14;
((IC (Comput (P,s,i))) .--> ((dl. 0) := (dl. 0))) . (IC (Comput (P,s,i))) = (dl. 0) := (dl. 0) by FUNCOP_1:87;
then A19: P1 . (IC (Comput (P,s,i))) = (dl. 0) := (dl. 0) by A13, FUNCT_4:14;
take P1 ; :: according to EXTPRO_1:def 9 :: thesis: ex b1 being set st
( ProgramPart p c= P1 & ProgramPart p c= b1 & ex b2, b3 being set st
( NPP p c= b2 & NPP p c= b3 & not for b4 being Element of NAT holds (Comput (P1,b2,b4)) | (proj1 (NPP p)) = (Comput (b1,b3,b4)) | (proj1 (NPP p)) ) )
take P2 ; :: thesis: ( ProgramPart p c= P1 & ProgramPart p c= P2 & ex b1, b2 being set st
( NPP p c= b1 & NPP p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (proj1 (NPP p)) = (Comput (P2,b2,b3)) | (proj1 (NPP p)) ) )
ProgramPart p c= ProgramPart (p +* ((IC (Comput (P,s,i))) .--> ((dl. 0) := (dl. 0)))) by Y5, FUNCT_4:33, RELAT_1:105;
hence A25: ProgramPart p c= P1 by P3, XBOOLE_1:1; :: thesis: ( ProgramPart p c= P2 & ex b1, b2 being set st
( NPP p c= b1 & NPP p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (proj1 (NPP p)) = (Comput (P2,b2,b3)) | (proj1 (NPP p)) ) )
ProgramPart p c= ProgramPart (p +* ((IC (Comput (P,s,i))) .--> (halt SCM))) by Y6, FUNCT_4:33, RELAT_1:105;
hence A27: ProgramPart p c= P2 by P4, XBOOLE_1:1; :: thesis: ex b1, b2 being set st
( NPP p c= b1 & NPP p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (proj1 (NPP p)) = (Comput (P2,b2,b3)) | (proj1 (NPP p)) )
take s ; :: thesis: ex b1 being set st
( NPP p c= s & NPP p c= b1 & not for b2 being Element of NAT holds (Comput (P1,s,b2)) | (proj1 (NPP p)) = (Comput (P2,b1,b2)) | (proj1 (NPP p)) )
take s ; :: thesis: ( NPP p c= s & NPP p c= s & not for b1 being Element of NAT holds (Comput (P1,s,b1)) | (proj1 (NPP p)) = (Comput (P2,s,b1)) | (proj1 (NPP p)) )
thus NPP p c= s by A1; :: thesis: ( NPP p c= s & not for b1 being Element of NAT holds (Comput (P1,s,b1)) | (proj1 (NPP p)) = (Comput (P2,s,b1)) | (proj1 (NPP p)) )
A28: (Comput (P1,s,i)) | (dom (NPP p)) = (Comput (P,s,i)) | (dom (NPP p)) by A25, A2, A1, EXTPRO_1:def 9;
thus NPP p c= s by A1; :: thesis: not for b1 being Element of NAT holds (Comput (P1,s,b1)) | (proj1 (NPP p)) = (Comput (P2,s,b1)) | (proj1 (NPP p))
A29: (Comput (P1,s,i)) | (dom (NPP p)) = (Comput (P2,s,i)) | (dom (NPP p)) by A25, A27, A1, EXTPRO_1:def 9;
take k = i + 1; :: thesis: not (Comput (P1,s,k)) | (proj1 (NPP p)) = (Comput (P2,s,k)) | (proj1 (NPP p))
set Cs1k = Comput (P1,s,k);
A33: IC in dom p by AMISTD_5:6;
IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom (NPP p))) by A33, COMPOS_1:179, FUNCT_1:72;
then IC (Comput (P1,s,i)) = IC (Comput (P,s,i)) by A28, A33, COMPOS_1:179, FUNCT_1:72;
then XX: CurInstr (P1,(Comput (P1,s,i))) = P1 . (IC (Comput (P,s,i))) by PBOOLE:158
.= (dl. 0) := (dl. 0) by A19 ;
A31: Comput (P1,s,k) = Following (P1,(Comput (P1,s,i))) by EXTPRO_1:4
.= Exec ((CurInstr (P1,(Comput (P1,s,i)))),(Comput (P1,s,i)))
.= Exec (((dl. 0) := (dl. 0)),(Comput (P1,s,i))) by XX ;
A32: IC (Exec (((dl. 0) := (dl. 0)),(Comput (P1,s,i)))) = succ (IC (Comput (P1,s,i))) by AMI_3:8;
A33: IC in dom p by AMISTD_5:6;
A34: IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom (NPP p))) by A33, COMPOS_1:179, FUNCT_1:72;
then IC (Comput (P1,s,i)) = IC (Comput (P,s,i)) by A28, A33, COMPOS_1:179, FUNCT_1:72;
then A35: IC (Comput (P1,s,k)) = succ (IC (Comput (P,s,i))) by A31, A32
.= (IC (Comput (P,s,i))) + 1 by NAT_1:39 ;
set Cs2k = Comput (P2,s,k);
A36: Comput (P2,s,k) = Following (P2,(Comput (P2,s,i))) by EXTPRO_1:4
.= Exec ((CurInstr (P2,(Comput (P2,s,i)))),(Comput (P2,s,i))) ;
A37: P2 /. (IC (Comput (P2,s,i))) = P2 . (IC (Comput (P2,s,i))) by PBOOLE:158;
IC (Comput (P2,s,i)) = IC (Comput (P,s,i)) by A28, A34, A29, A33, COMPOS_1:179, FUNCT_1:72;
then A38: IC (Comput (P2,s,k)) = IC (Comput (P,s,i)) by A36, A18, A37, EXTPRO_1:def 3;
( IC ((Comput (P1,s,k)) | (dom (NPP p))) = IC (Comput (P1,s,k)) & IC ((Comput (P2,s,k)) | (dom (NPP p))) = IC (Comput (P2,s,k)) ) by A33, COMPOS_1:179, FUNCT_1:72;
hence not (Comput (P1,s,k)) | (proj1 (NPP p)) = (Comput (P2,s,k)) | (proj1 (NPP p)) by A35, A38; :: thesis: verum
end;
hence contradiction ; :: thesis: verum