let R be good Ring; :: thesis: ( not R is trivial implies for p being autonomic FinPartState of (SCM R) st DataPart p <> {} holds
IC (SCM R) in dom p )
assume A1:
not R is trivial
; :: thesis: for p being autonomic FinPartState of (SCM R) st DataPart p <> {} holds
IC (SCM R) in dom p
let p be autonomic FinPartState of (SCM R); :: thesis: ( DataPart p <> {} implies IC (SCM R) in dom p )
assume
DataPart p <> {}
; :: thesis: IC (SCM R) in dom p
then A2:
dom (DataPart p) <> {}
;
assume A3:
not IC (SCM R) in dom p
; :: thesis: contradiction
not p is autonomic
proof
consider d1 being
Element of
dom (DataPart p);
A4:
d1 in dom (DataPart p)
by A2;
dom (DataPart p) c= the
carrier of
(SCM R)
by AMI_1:80;
then reconsider d1 =
d1 as
Element of
(SCM R) by A4;
Data-Locations (SCM R) = SCM-Data-Loc
by SCMRING2:31;
then
dom (DataPart p) c= SCM-Data-Loc
by RELAT_1:87;
then reconsider d1 =
d1 as
Data-Location of
R by A4, SCMRING2:1;
consider d2 being
Element of
SCM-Data-Loc \ (dom p);
not
SCM-Data-Loc c= dom p
;
then A5:
SCM-Data-Loc \ (dom p) <> {}
by XBOOLE_1:37;
then
d2 in SCM-Data-Loc
by XBOOLE_0:def 5;
then reconsider d2 =
d2 as
Data-Location of
R by SCMRING2:1;
consider il being
Element of
NAT \ (dom p);
not
NAT c= dom p
;
then A6:
NAT \ (dom p) <> {}
by XBOOLE_1:37;
then
il is
Element of
NAT
by XBOOLE_0:def 5;
then reconsider il =
il as
Instruction-Location of
SCM R by AMI_1:def 4;
consider e being
Element of
R such that A7:
e <> 0. R
by A1, STRUCT_0:def 19;
set p1 =
p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At il));
set p2 =
p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At il));
consider s1 being
State of
(SCM R) such that A8:
p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At il)) c= s1
by CARD_3:97;
consider s2 being
State of
(SCM R) such that A9:
p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At il)) c= s2
by CARD_3:97;
take
s1
;
:: according to AMI_1:def 25 :: thesis: ex b1 being Element of product the Object-Kind of (SCM R) st
( p c= s1 & p c= b1 & not for b2 being Element of NAT holds (Computation s1,b2) | (dom p) = (Computation b1,b2) | (dom p) )
take
s2
;
:: thesis: ( p c= s1 & p c= s2 & not for b1 being Element of NAT holds (Computation s1,b1) | (dom p) = (Computation s2,b1) | (dom p) )
A10:
not
d2 in dom p
by A5, XBOOLE_0:def 5;
A11:
not
il in dom p
by A6, XBOOLE_0:def 5;
dom p misses dom (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At il))
then
p c= p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At il))
by FUNCT_4:33;
hence
p c= s1
by A8, XBOOLE_1:1;
:: thesis: ( p c= s2 & not for b1 being Element of NAT holds (Computation s1,b1) | (dom p) = (Computation s2,b1) | (dom p) )
dom p misses dom (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At il))
then
p c= p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At il))
by FUNCT_4:33;
hence
p c= s2
by A9, XBOOLE_1:1;
:: thesis: not for b1 being Element of NAT holds (Computation s1,b1) | (dom p) = (Computation s2,b1) | (dom p)
take
1
;
:: thesis: not (Computation s1,1) | (dom p) = (Computation s2,1) | (dom p)
DataPart p c= p
by RELAT_1:88;
then A12:
dom (DataPart p) c= dom p
by RELAT_1:25;
dom (Computation s1,1) = the
carrier of
(SCM R)
by AMI_1:79;
then A13:
dom ((Computation s1,1) | (dom p)) = dom p
by AMI_1:80, RELAT_1:91;
A14:
dom (Start-At il) = {(IC (SCM R))}
by FUNCOP_1:19;
then A15:
IC (SCM R) in dom (Start-At il)
by TARSKI:def 1;
A16:
dom (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At il)) = (dom ((il .--> (d1 := d2)) +* (d2 .--> (0. R)))) \/ (dom (Start-At il))
by FUNCT_4:def 1;
then A17:
IC (SCM R) in dom (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At il))
by A15, XBOOLE_0:def 3;
A18:
dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At il))) = (dom p) \/ (dom (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At il)))
by FUNCT_4:def 1;
then
IC (SCM R) in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At il)))
by A17, XBOOLE_0:def 3;
then A19:
IC s1 =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At il))) . (IC (SCM R))
by A8, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At il)) . (IC (SCM R))
by A17, FUNCT_4:14
.=
(Start-At il) . (IC (SCM R))
by A15, FUNCT_4:14
.=
il
by FUNCOP_1:87
;
dom (il .--> (d1 := d2)) = {il}
by FUNCOP_1:19;
then A20:
il in dom (il .--> (d1 := d2))
by TARSKI:def 1;
A21:
dom (d2 .--> (0. R)) = {d2}
by FUNCOP_1:19;
A22:
il <> d2
by Th20;
then A23:
not
il in dom (d2 .--> (0. R))
by A21, TARSKI:def 1;
A24:
dom ((il .--> (d1 := d2)) +* (d2 .--> (0. R))) = (dom (il .--> (d1 := d2))) \/ (dom (d2 .--> (0. R)))
by FUNCT_4:def 1;
then A25:
il in dom ((il .--> (d1 := d2)) +* (d2 .--> (0. R)))
by A20, XBOOLE_0:def 3;
A26:
il <> IC (SCM R)
by AMI_1:48;
then A27:
not
il in dom (Start-At il)
by A14, TARSKI:def 1;
A28:
il in dom (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At il))
by A16, A25, XBOOLE_0:def 3;
then
il in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At il)))
by A18, XBOOLE_0:def 3;
then A29:
s1 . il =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At il))) . il
by A8, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At il)) . il
by A28, FUNCT_4:14
.=
((il .--> (d1 := d2)) +* (d2 .--> (0. R))) . il
by A27, FUNCT_4:12
.=
(il .--> (d1 := d2)) . il
by A23, FUNCT_4:12
.=
d1 := d2
by FUNCOP_1:87
;
A30:
d2 in dom (d2 .--> (0. R))
by A21, TARSKI:def 1;
then A31:
d2 in dom ((il .--> (d1 := d2)) +* (d2 .--> (0. R)))
by A24, XBOOLE_0:def 3;
A32:
d2 <> IC (SCM R)
by SCMRING3:3;
then A33:
not
d2 in dom (Start-At il)
by A14, TARSKI:def 1;
A34:
d2 in dom (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At il))
by A16, A31, XBOOLE_0:def 3;
then
d2 in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At il)))
by A18, XBOOLE_0:def 3;
then A35:
s1 . d2 =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At il))) . d2
by A8, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> (0. R))) +* (Start-At il)) . d2
by A34, FUNCT_4:14
.=
((il .--> (d1 := d2)) +* (d2 .--> (0. R))) . d2
by A33, FUNCT_4:12
.=
(d2 .--> (0. R)) . d2
by A30, FUNCT_4:14
.=
0. R
by FUNCOP_1:87
;
(Computation s1,(0 + 1)) . d1 =
(Following (Computation s1,0 )) . d1
by AMI_1:14
.=
(Following s1) . d1
by AMI_1:13
.=
0. R
by A19, A29, A35, SCMRING2:13
;
then A36:
((Computation s1,1) | (dom p)) . d1 = 0. R
by A4, A12, A13, FUNCT_1:70;
dom (Computation s2,1) = the
carrier of
(SCM R)
by AMI_1:79;
then A37:
dom ((Computation s2,1) | (dom p)) = dom p
by AMI_1:80, RELAT_1:91;
A38:
dom (Start-At il) = {(IC (SCM R))}
by FUNCOP_1:19;
then A39:
IC (SCM R) in dom (Start-At il)
by TARSKI:def 1;
A40:
dom (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At il)) = (dom ((il .--> (d1 := d2)) +* (d2 .--> e))) \/ (dom (Start-At il))
by FUNCT_4:def 1;
then A41:
IC (SCM R) in dom (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At il))
by A39, XBOOLE_0:def 3;
A42:
dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At il))) = (dom p) \/ (dom (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At il)))
by FUNCT_4:def 1;
then
IC (SCM R) in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At il)))
by A41, XBOOLE_0:def 3;
then A43:
IC s2 =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At il))) . (IC (SCM R))
by A9, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At il)) . (IC (SCM R))
by A41, FUNCT_4:14
.=
(Start-At il) . (IC (SCM R))
by A39, FUNCT_4:14
.=
il
by FUNCOP_1:87
;
dom (il .--> (d1 := d2)) = {il}
by FUNCOP_1:19;
then A44:
il in dom (il .--> (d1 := d2))
by TARSKI:def 1;
A45:
dom (d2 .--> e) = {d2}
by FUNCOP_1:19;
then A46:
not
il in dom (d2 .--> e)
by A22, TARSKI:def 1;
A47:
dom ((il .--> (d1 := d2)) +* (d2 .--> e)) = (dom (il .--> (d1 := d2))) \/ (dom (d2 .--> e))
by FUNCT_4:def 1;
then A48:
il in dom ((il .--> (d1 := d2)) +* (d2 .--> e))
by A44, XBOOLE_0:def 3;
A49:
not
il in dom (Start-At il)
by A26, A38, TARSKI:def 1;
A50:
il in dom (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At il))
by A40, A48, XBOOLE_0:def 3;
then
il in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At il)))
by A42, XBOOLE_0:def 3;
then A51:
s2 . il =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At il))) . il
by A9, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At il)) . il
by A50, FUNCT_4:14
.=
((il .--> (d1 := d2)) +* (d2 .--> e)) . il
by A49, FUNCT_4:12
.=
(il .--> (d1 := d2)) . il
by A46, FUNCT_4:12
.=
d1 := d2
by FUNCOP_1:87
;
A52:
d2 in dom (d2 .--> e)
by A45, TARSKI:def 1;
then A53:
d2 in dom ((il .--> (d1 := d2)) +* (d2 .--> e))
by A47, XBOOLE_0:def 3;
A54:
not
d2 in dom (Start-At il)
by A32, A38, TARSKI:def 1;
A55:
d2 in dom (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At il))
by A40, A53, XBOOLE_0:def 3;
then
d2 in dom (p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At il)))
by A42, XBOOLE_0:def 3;
then A56:
s2 . d2 =
(p +* (((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At il))) . d2
by A9, GRFUNC_1:8
.=
(((il .--> (d1 := d2)) +* (d2 .--> e)) +* (Start-At il)) . d2
by A55, FUNCT_4:14
.=
((il .--> (d1 := d2)) +* (d2 .--> e)) . d2
by A54, FUNCT_4:12
.=
(d2 .--> e) . d2
by A52, FUNCT_4:14
.=
e
by FUNCOP_1:87
;
(Computation s2,(0 + 1)) . d1 =
(Following (Computation s2,0 )) . d1
by AMI_1:14
.=
(Following s2) . d1
by AMI_1:13
.=
e
by A43, A51, A56, SCMRING2:13
;
hence
(Computation s1,1) | (dom p) <> (Computation s2,1) | (dom p)
by A4, A7, A12, A36, A37, FUNCT_1:70;
:: thesis: verum
end;
hence
contradiction
; :: thesis: verum