thus SCM is IC-good :: thesis: SCM is Exec-preserving
proof
let I be Instruction of SCM ; :: according to AMISTD_2:def 18 :: thesis: I is IC-good
per cases ( I = [0 ,{} ] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo a,b or ex a, b being Data-Location st I = SubFrom a,b or ex a, b being Data-Location st I = MultBy a,b or ex a, b being Data-Location st I = Divide a,b or ex k being natural number st I = SCM-goto k or ex a being Data-Location ex k being natural number st I = a =0_goto k or ex a being Data-Location ex k being natural number st I = a >0_goto k ) by AMI_3:69;
suppose A1: ex k being natural number st I = SCM-goto k ; :: thesis: I is IC-good
let k be natural number ; :: according to AMISTD_2:def 17 :: thesis: for b1, b2 being set holds
( not b2 = b1 +* ((IC SCM ) .--> ((IC b1) + k,SCM )) or (IC (Exec I,b1)) + k,SCM = IC (Exec (IncAddr I,k),b2) )
let s1, s2 be State of SCM ; :: thesis: ( not s2 = s1 +* ((IC SCM ) .--> ((IC s1) + k,SCM )) or (IC (Exec I,s1)) + k,SCM = IC (Exec (IncAddr I,k),s2) )
assume s2 = s1 +* ((IC SCM ) .--> ((IC s1) + k,SCM )) ; :: thesis: (IC (Exec I,s1)) + k,SCM = IC (Exec (IncAddr I,k),s2)
consider k1 being natural number such that
A2: I = SCM-goto k1 by A1;
k1 in NAT by ORDINAL1:def 13;
then reconsider i1 = k1 as Element of NAT ;
IC (Exec I,s1) = k1 by A2, AMI_3:13;
hence (IC (Exec I,s1)) + k,SCM = IC (Exec (SCM-goto (il. SCM ,((locnum i1,SCM ) + k))),s2) by AMI_3:13
.= IC (Exec (IncAddr I,k),s2) by A2, Th57 ;
:: thesis: verum
end;
suppose ex a being Data-Location ex k being natural number st I = a =0_goto k ; :: thesis: I is IC-good
then consider a being Data-Location , k1 being natural number such that
A3: I = a =0_goto k1 ;
k1 in NAT by ORDINAL1:def 13;
then reconsider i1 = k1 as Element of NAT ;
let k be natural number ; :: according to AMISTD_2:def 17 :: thesis: for b1, b2 being set holds
( not b2 = b1 +* ((IC SCM ) .--> ((IC b1) + k,SCM )) or (IC (Exec I,b1)) + k,SCM = IC (Exec (IncAddr I,k),b2) )
let s1, s2 be State of SCM ; :: thesis: ( not s2 = s1 +* ((IC SCM ) .--> ((IC s1) + k,SCM )) or (IC (Exec I,s1)) + k,SCM = IC (Exec (IncAddr I,k),s2) )
assume A4: s2 = s1 +* ((IC SCM ) .--> ((IC s1) + k,SCM )) ; :: thesis: (IC (Exec I,s1)) + k,SCM = IC (Exec (IncAddr I,k),s2)
( a <> IC SCM & dom ((IC SCM ) .--> ((IC s1) + k,SCM )) = {(IC SCM )} ) by AMI_5:20, FUNCOP_1:19;
then not a in dom ((IC SCM ) .--> ((IC s1) + k,SCM )) by TARSKI:def 1;
then A5: s1 . a = s2 . a by A4, FUNCT_4:12;
now
per cases ( s1 . a = 0 or s1 . a <> 0 ) ;
suppose A6: s1 . a = 0 ; :: thesis: (IC (Exec I,s1)) + k,SCM = IC (Exec (IncAddr I,k),s2)
then IC (Exec I,s1) = k1 by A3, AMI_3:14;
hence (IC (Exec I,s1)) + k,SCM = IC (Exec (a =0_goto (il. SCM ,((locnum i1,SCM ) + k))),s2) by A5, A6, AMI_3:14
.= IC (Exec (IncAddr I,k),s2) by A3, Th58 ;
:: thesis: verum
end;
suppose A7: s1 . a <> 0 ; :: thesis: (IC (Exec I,s1)) + k,SCM = IC (Exec (IncAddr I,k),s2)
dom ((IC SCM ) .--> ((IC s1) + k,SCM )) = {(IC SCM )} by FUNCOP_1:19;
then IC SCM in dom ((IC SCM ) .--> ((IC s1) + k,SCM )) by TARSKI:def 1;
then A8: IC s2 = ((IC SCM ) .--> ((IC s1) + k,SCM )) . (IC SCM ) by A4, FUNCT_4:14
.= il. SCM ,((locnum (IC s1),SCM ) + k) by FUNCOP_1:87 ;
A9: IC (Exec I,s1) = succ (IC s1) by A3, A7, AMI_3:14
.= NextLoc (IC s1),SCM by Th56
.= il. SCM ,((locnum (IC s1),SCM ) + 1) ;
IC (Exec I,s2) = succ (IC s2) by A3, A5, A7, AMI_3:14
.= NextLoc (IC s2),SCM by Th56
.= il. SCM ,(((locnum (IC s1),SCM ) + k) + 1) by A8, AMISTD_1:def 13
.= il. SCM ,(((locnum (IC s1),SCM ) + 1) + k) ;
hence (IC (Exec I,s1)) + k,SCM = (Exec I,s2) . (IC SCM ) by A9, AMISTD_1:def 13
.= succ (IC s2) by A3, A5, A7, AMI_3:14
.= IC (Exec (a =0_goto (il. SCM ,((locnum i1,SCM ) + k))),s2) by A5, A7, AMI_3:14
.= IC (Exec (IncAddr I,k),s2) by A3, Th58 ;
:: thesis: verum
end;
end;
end;
hence (IC (Exec I,s1)) + k,SCM = IC (Exec (IncAddr I,k),s2) ; :: thesis: verum
end;
suppose ex a being Data-Location ex k being natural number st I = a >0_goto k ; :: thesis: I is IC-good
then consider a being Data-Location , k1 being natural number such that
A10: I = a >0_goto k1 ;
k1 in NAT by ORDINAL1:def 13;
then reconsider i1 = k1 as Element of NAT ;
let k be natural number ; :: according to AMISTD_2:def 17 :: thesis: for b1, b2 being set holds
( not b2 = b1 +* ((IC SCM ) .--> ((IC b1) + k,SCM )) or (IC (Exec I,b1)) + k,SCM = IC (Exec (IncAddr I,k),b2) )
let s1, s2 be State of SCM ; :: thesis: ( not s2 = s1 +* ((IC SCM ) .--> ((IC s1) + k,SCM )) or (IC (Exec I,s1)) + k,SCM = IC (Exec (IncAddr I,k),s2) )
assume A11: s2 = s1 +* ((IC SCM ) .--> ((IC s1) + k,SCM )) ; :: thesis: (IC (Exec I,s1)) + k,SCM = IC (Exec (IncAddr I,k),s2)
( a <> IC SCM & dom ((IC SCM ) .--> ((IC s1) + k,SCM )) = {(IC SCM )} ) by AMI_5:20, FUNCOP_1:19;
then not a in dom ((IC SCM ) .--> ((IC s1) + k,SCM )) by TARSKI:def 1;
then A12: s1 . a = s2 . a by A11, FUNCT_4:12;
now
per cases ( s1 . a > 0 or s1 . a <= 0 ) ;
suppose A13: s1 . a > 0 ; :: thesis: (IC (Exec I,s1)) + k,SCM = IC (Exec (IncAddr I,k),s2)
then IC (Exec I,s1) = k1 by A10, AMI_3:15;
hence (IC (Exec I,s1)) + k,SCM = IC (Exec (a >0_goto (il. SCM ,((locnum i1,SCM ) + k))),s2) by A12, A13, AMI_3:15
.= IC (Exec (IncAddr I,k),s2) by A10, Th59 ;
:: thesis: verum
end;
suppose A14: s1 . a <= 0 ; :: thesis: (IC (Exec I,s1)) + k,SCM = IC (Exec (IncAddr I,k),s2)
dom ((IC SCM ) .--> ((IC s1) + k,SCM )) = {(IC SCM )} by FUNCOP_1:19;
then IC SCM in dom ((IC SCM ) .--> ((IC s1) + k,SCM )) by TARSKI:def 1;
then A15: IC s2 = ((IC SCM ) .--> ((IC s1) + k,SCM )) . (IC SCM ) by A11, FUNCT_4:14
.= il. SCM ,((locnum (IC s1),SCM ) + k) by FUNCOP_1:87 ;
A16: IC (Exec I,s1) = succ (IC s1) by A10, A14, AMI_3:15
.= NextLoc (IC s1),SCM by Th56
.= il. SCM ,((locnum (IC s1),SCM ) + 1) ;
IC (Exec I,s2) = succ (IC s2) by A10, A12, A14, AMI_3:15
.= NextLoc (IC s2),SCM by Th56
.= il. SCM ,(((locnum (IC s1),SCM ) + k) + 1) by A15, AMISTD_1:def 13
.= il. SCM ,(((locnum (IC s1),SCM ) + 1) + k) ;
hence (IC (Exec I,s1)) + k,SCM = (Exec I,s2) . (IC SCM ) by A16, AMISTD_1:def 13
.= succ (IC s2) by A10, A12, A14, AMI_3:15
.= IC (Exec (a >0_goto (il. SCM ,((locnum i1,SCM ) + k))),s2) by A12, A14, AMI_3:15
.= IC (Exec (IncAddr I,k),s2) by A10, Th59 ;
:: thesis: verum
end;
end;
end;
hence (IC (Exec I,s1)) + k,SCM = IC (Exec (IncAddr I,k),s2) ; :: thesis: verum
end;
end;
end;
let I be Instruction of SCM ; :: according to AMISTD_2:def 20 :: thesis: I is Exec-preserving
let s1, s2 be State of SCM ; :: according to AMISTD_2:def 19 :: thesis: ( not s1,s2 equal_outside NAT or Exec I,s1, Exec I,s2 equal_outside NAT )
assume A18: s1,s2 equal_outside NAT ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT
A19: IC s1 = IC s2 by A18, AMI_1:121;
A20: dom (Exec I,s1) = the carrier of SCM by PARTFUN1:def 4;
then A21: dom (Exec I,s1) = dom (Exec I,s2) by PARTFUN1:def 4;
per cases ( I = [0 ,{} ] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo a,b or ex a, b being Data-Location st I = SubFrom a,b or ex a, b being Data-Location st I = MultBy a,b or ex a, b being Data-Location st I = Divide a,b or ex k being natural number st I = SCM-goto k or ex a being Data-Location ex k being natural number st I = a =0_goto k or ex a being Data-Location ex k being natural number st I = a >0_goto k ) by AMI_3:69;
suppose I = [0 ,{} ] ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT
hence Exec I,s1, Exec I,s2 equal_outside NAT by A18, AMISTD_2:def 19, AMI_3:71; :: thesis: verum
end;
suppose ex a, b being Data-Location st I = a := b ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT
then consider a, b being Data-Location such that
A22: I = a := b ;
for x being set st x in (dom (Exec I,s1)) \ NAT holds
(Exec I,s1) . x = (Exec I,s2) . x
proof
let x be set ; :: thesis: ( x in (dom (Exec I,s1)) \ NAT implies (Exec I,s1) . x = (Exec I,s2) . x )
assume A23: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A24: not x in NAT by XBOOLE_0:def 5;
per cases ( x = IC SCM or x = a or ( x is Data-Location & x <> a ) ) by A20, A23, A24, Th3;
suppose A25: x = IC SCM ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = succ (IC s1) by A22, AMI_3:8
.= (Exec I,s2) . x by A19, A22, A25, AMI_3:8 ;
:: thesis: verum
end;
suppose A26: x = a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = s1 . b by A22, AMI_3:8
.= s2 . b by A18, Th5
.= (Exec I,s2) . x by A22, A26, AMI_3:8 ;
:: thesis: verum
end;
suppose that A27: x is Data-Location and
A28: x <> a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
thus (Exec I,s1) . x = s1 . x by A22, A27, A28, AMI_3:8
.= s2 . x by A18, A27, Th5
.= (Exec I,s2) . x by A22, A27, A28, AMI_3:8 ; :: thesis: verum
end;
end;
end;
hence (Exec I,s1) | ((dom (Exec I,s1)) \ NAT ) = (Exec I,s2) | ((dom (Exec I,s2)) \ NAT ) by A21, FUNCT_1:165; :: according to FUNCT_7:def 2 :: thesis: verum
end;
suppose ex a, b being Data-Location st I = AddTo a,b ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT
then consider a, b being Data-Location such that
A29: I = AddTo a,b ;
for x being set st x in (dom (Exec I,s1)) \ NAT holds
(Exec I,s1) . x = (Exec I,s2) . x
proof
let x be set ; :: thesis: ( x in (dom (Exec I,s1)) \ NAT implies (Exec I,s1) . x = (Exec I,s2) . x )
assume A30: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A31: not x in NAT by XBOOLE_0:def 5;
per cases ( x = IC SCM or x = a or ( x is Data-Location & x <> a ) ) by A20, A30, A31, Th3;
suppose A32: x = IC SCM ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = succ (IC s1) by A29, AMI_3:9
.= (Exec I,s2) . x by A19, A29, A32, AMI_3:9 ;
:: thesis: verum
end;
suppose A33: x = a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = (s1 . a) + (s1 . b) by A29, AMI_3:9
.= (s1 . a) + (s2 . b) by A18, Th5
.= (s2 . a) + (s2 . b) by A18, Th5
.= (Exec I,s2) . x by A29, A33, AMI_3:9 ;
:: thesis: verum
end;
suppose that A34: x is Data-Location and
A35: x <> a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
thus (Exec I,s1) . x = s1 . x by A29, A34, A35, AMI_3:9
.= s2 . x by A18, A34, Th5
.= (Exec I,s2) . x by A29, A34, A35, AMI_3:9 ; :: thesis: verum
end;
end;
end;
hence (Exec I,s1) | ((dom (Exec I,s1)) \ NAT ) = (Exec I,s2) | ((dom (Exec I,s2)) \ NAT ) by A21, FUNCT_1:165; :: according to FUNCT_7:def 2 :: thesis: verum
end;
suppose ex a, b being Data-Location st I = SubFrom a,b ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT
then consider a, b being Data-Location such that
A36: I = SubFrom a,b ;
for x being set st x in (dom (Exec I,s1)) \ NAT holds
(Exec I,s1) . x = (Exec I,s2) . x
proof
let x be set ; :: thesis: ( x in (dom (Exec I,s1)) \ NAT implies (Exec I,s1) . x = (Exec I,s2) . x )
assume A37: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A38: not x in NAT by XBOOLE_0:def 5;
per cases ( x = IC SCM or x = a or ( x is Data-Location & x <> a ) ) by A20, A37, A38, Th3;
suppose A39: x = IC SCM ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = succ (IC s1) by A36, AMI_3:10
.= (Exec I,s2) . x by A19, A36, A39, AMI_3:10 ;
:: thesis: verum
end;
suppose A40: x = a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = (s1 . a) - (s1 . b) by A36, AMI_3:10
.= (s1 . a) - (s2 . b) by A18, Th5
.= (s2 . a) - (s2 . b) by A18, Th5
.= (Exec I,s2) . x by A36, A40, AMI_3:10 ;
:: thesis: verum
end;
suppose that A41: x is Data-Location and
A42: x <> a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
thus (Exec I,s1) . x = s1 . x by A36, A41, A42, AMI_3:10
.= s2 . x by A18, A41, Th5
.= (Exec I,s2) . x by A36, A41, A42, AMI_3:10 ; :: thesis: verum
end;
end;
end;
hence (Exec I,s1) | ((dom (Exec I,s1)) \ NAT ) = (Exec I,s2) | ((dom (Exec I,s2)) \ NAT ) by A21, FUNCT_1:165; :: according to FUNCT_7:def 2 :: thesis: verum
end;
suppose ex a, b being Data-Location st I = MultBy a,b ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT
then consider a, b being Data-Location such that
A43: I = MultBy a,b ;
for x being set st x in (dom (Exec I,s1)) \ NAT holds
(Exec I,s1) . x = (Exec I,s2) . x
proof
let x be set ; :: thesis: ( x in (dom (Exec I,s1)) \ NAT implies (Exec I,s1) . x = (Exec I,s2) . x )
assume A44: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A45: not x in NAT by XBOOLE_0:def 5;
per cases ( x = IC SCM or x = a or ( x is Data-Location & x <> a ) ) by A20, A44, A45, Th3;
suppose A46: x = IC SCM ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = succ (IC s1) by A43, AMI_3:11
.= (Exec I,s2) . x by A19, A43, A46, AMI_3:11 ;
:: thesis: verum
end;
suppose A47: x = a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = (s1 . a) * (s1 . b) by A43, AMI_3:11
.= (s1 . a) * (s2 . b) by A18, Th5
.= (s2 . a) * (s2 . b) by A18, Th5
.= (Exec I,s2) . x by A43, A47, AMI_3:11 ;
:: thesis: verum
end;
suppose that A48: x is Data-Location and
A49: x <> a ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
thus (Exec I,s1) . x = s1 . x by A43, A48, A49, AMI_3:11
.= s2 . x by A18, A48, Th5
.= (Exec I,s2) . x by A43, A48, A49, AMI_3:11 ; :: thesis: verum
end;
end;
end;
hence (Exec I,s1) | ((dom (Exec I,s1)) \ NAT ) = (Exec I,s2) | ((dom (Exec I,s2)) \ NAT ) by A21, FUNCT_1:165; :: according to FUNCT_7:def 2 :: thesis: verum
end;
suppose ex a, b being Data-Location st I = Divide a,b ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT
then consider a, b being Data-Location such that
A50: I = Divide a,b ;
for x being set st x in (dom (Exec I,s1)) \ NAT holds
(Exec I,s1) . x = (Exec I,s2) . x
proof
let x be set ; :: thesis: ( x in (dom (Exec I,s1)) \ NAT implies (Exec I,s1) . x = (Exec I,s2) . x )
assume A51: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A52: not x in NAT by XBOOLE_0:def 5;
per cases ( x = IC SCM or x is Data-Location ) by A20, A51, A52, Th3;
suppose A53: x = IC SCM ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = succ (IC s1) by A50, AMI_3:12
.= (Exec I,s2) . x by A19, A50, A53, AMI_3:12 ;
:: thesis: verum
end;
suppose A54: x is Data-Location ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
A55: ( s1 . a = s2 . a & s1 . b = s2 . b ) by A18, Th5;
now
let c be Data-Location ; :: thesis: (Exec I,s1) . b1 = (Exec I,s2) . b1
per cases ( c = b or ( c = a & c <> b ) or ( c <> a & c <> b ) ) ;
suppose A56: c = b ; :: thesis: (Exec I,s1) . b1 = (Exec I,s2) . b1
hence (Exec I,s1) . c = (s2 . a) mod (s2 . b) by A50, A55, AMI_3:12
.= (Exec I,s2) . c by A50, A56, AMI_3:12 ;
:: thesis: verum
end;
suppose A57: ( c = a & c <> b ) ; :: thesis: (Exec I,s1) . b1 = (Exec I,s2) . b1
hence (Exec I,s1) . c = (s2 . a) div (s2 . b) by A50, A55, AMI_3:12
.= (Exec I,s2) . c by A50, A57, AMI_3:12 ;
:: thesis: verum
end;
suppose A58: ( c <> a & c <> b ) ; :: thesis: (Exec I,s1) . b1 = (Exec I,s2) . b1
hence (Exec I,s1) . c = s1 . c by A50, AMI_3:12
.= s2 . c by A18, Th5
.= (Exec I,s2) . c by A50, A58, AMI_3:12 ;
:: thesis: verum
end;
end;
end;
hence (Exec I,s1) . x = (Exec I,s2) . x by A54; :: thesis: verum
end;
end;
end;
hence (Exec I,s1) | ((dom (Exec I,s1)) \ NAT ) = (Exec I,s2) | ((dom (Exec I,s2)) \ NAT ) by A21, FUNCT_1:165; :: according to FUNCT_7:def 2 :: thesis: verum
end;
suppose ex k being natural number st I = SCM-goto k ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT
then consider k1 being natural number such that
A59: I = SCM-goto k1 ;
for x being set st x in (dom (Exec I,s1)) \ NAT holds
(Exec I,s1) . x = (Exec I,s2) . x
proof
let x be set ; :: thesis: ( x in (dom (Exec I,s1)) \ NAT implies (Exec I,s1) . x = (Exec I,s2) . x )
assume A60: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A61: not x in NAT by XBOOLE_0:def 5;
per cases ( x = IC SCM or x is Data-Location ) by A20, A60, A61, Th3;
suppose A62: x = IC SCM ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = k1 by A59, AMI_3:13
.= (Exec I,s2) . x by A59, A62, AMI_3:13 ;
:: thesis: verum
end;
suppose A63: x is Data-Location ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = s1 . x by A59, AMI_3:13
.= s2 . x by A18, A63, Th5
.= (Exec I,s2) . x by A59, A63, AMI_3:13 ;
:: thesis: verum
end;
end;
end;
hence (Exec I,s1) | ((dom (Exec I,s1)) \ NAT ) = (Exec I,s2) | ((dom (Exec I,s2)) \ NAT ) by A21, FUNCT_1:165; :: according to FUNCT_7:def 2 :: thesis: verum
end;
suppose ex a being Data-Location ex k being natural number st I = a =0_goto k ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT
then consider a being Data-Location , k1 being natural number such that
A64: I = a =0_goto k1 ;
for x being set st x in (dom (Exec I,s1)) \ NAT holds
(Exec I,s1) . x = (Exec I,s2) . x
proof
let x be set ; :: thesis: ( x in (dom (Exec I,s1)) \ NAT implies (Exec I,s1) . x = (Exec I,s2) . x )
assume A65: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A66: not x in NAT by XBOOLE_0:def 5;
A67: s1 . a = s2 . a by A18, Th5;
per cases ( ( x = IC SCM & s1 . a = 0 ) or ( x = IC SCM & s1 . a <> 0 ) or x is Data-Location ) by A20, A65, A66, Th3;
suppose A68: ( x = IC SCM & s1 . a = 0 ) ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
thus (Exec I,s1) . x = k1 by A64, A68, AMI_3:14
.= (Exec I,s2) . x by A64, A67, A68, AMI_3:14 ; :: thesis: verum
end;
suppose A69: ( x = IC SCM & s1 . a <> 0 ) ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
thus (Exec I,s1) . x = succ (IC s1) by A64, A69, AMI_3:14
.= (Exec I,s2) . x by A19, A64, A67, A69, AMI_3:14 ; :: thesis: verum
end;
suppose A70: x is Data-Location ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = s1 . x by A64, AMI_3:14
.= s2 . x by A18, A70, Th5
.= (Exec I,s2) . x by A64, A70, AMI_3:14 ;
:: thesis: verum
end;
end;
end;
hence (Exec I,s1) | ((dom (Exec I,s1)) \ NAT ) = (Exec I,s2) | ((dom (Exec I,s2)) \ NAT ) by A21, FUNCT_1:165; :: according to FUNCT_7:def 2 :: thesis: verum
end;
suppose ex a being Data-Location ex k being natural number st I = a >0_goto k ; :: thesis: Exec I,s1, Exec I,s2 equal_outside NAT
then consider a being Data-Location , k being natural number such that
A71: I = a >0_goto k ;
for x being set st x in (dom (Exec I,s1)) \ NAT holds
(Exec I,s1) . x = (Exec I,s2) . x
proof
let x be set ; :: thesis: ( x in (dom (Exec I,s1)) \ NAT implies (Exec I,s1) . x = (Exec I,s2) . x )
assume A72: x in (dom (Exec I,s1)) \ NAT ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
then A73: not x in NAT by XBOOLE_0:def 5;
A74: s1 . a = s2 . a by A18, Th5;
per cases ( ( x = IC SCM & s1 . a > 0 ) or ( x = IC SCM & s1 . a <= 0 ) or x is Data-Location ) by A20, A72, A73, Th3;
suppose A75: ( x = IC SCM & s1 . a > 0 ) ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
thus (Exec I,s1) . x = k by A71, A75, AMI_3:15
.= (Exec I,s2) . x by A71, A74, A75, AMI_3:15 ; :: thesis: verum
end;
suppose A76: ( x = IC SCM & s1 . a <= 0 ) ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
thus (Exec I,s1) . x = succ (IC s1) by A71, A76, AMI_3:15
.= (Exec I,s2) . x by A19, A71, A74, A76, AMI_3:15 ; :: thesis: verum
end;
suppose A77: x is Data-Location ; :: thesis: (Exec I,s1) . x = (Exec I,s2) . x
hence (Exec I,s1) . x = s1 . x by A71, AMI_3:15
.= s2 . x by A18, A77, Th5
.= (Exec I,s2) . x by A71, A77, AMI_3:15 ;
:: thesis: verum
end;
end;
end;
hence (Exec I,s1) | ((dom (Exec I,s1)) \ NAT ) = (Exec I,s2) | ((dom (Exec I,s2)) \ NAT ) by A21, FUNCT_1:165; :: according to FUNCT_7:def 2 :: thesis: verum
end;
end;