:: AMI_5 semantic presentation
begin
theorem Th1: :: AMI_5:1
for dl being Data-Location ex i being Element of NAT st dl = dl. i
proof
let dl be Data-Location; ::_thesis: ex i being Element of NAT st dl = dl. i
dl in Data-Locations by AMI_2:def_16, AMI_3:27;
then consider x, y being set such that
A1: x in {1} and
A2: y in NAT and
A3: dl = [x,y] by AMI_3:27, ZFMISC_1:84;
reconsider k = y as Element of NAT by A2;
take k ; ::_thesis: dl = dl. k
thus dl = dl. k by A1, A3, TARSKI:def_1; ::_thesis: verum
end;
theorem Th2: :: AMI_5:2
for dl being Data-Location holds dl <> IC
proof
let dl be Data-Location; ::_thesis: dl <> IC
ex i being Element of NAT st dl = dl. i by Th1;
hence dl <> IC by AMI_3:13; ::_thesis: verum
end;
theorem :: AMI_5:3
for il being Element of NAT
for dl being Data-Location holds il <> dl
proof
let il be Element of NAT ; ::_thesis: for dl being Data-Location holds il <> dl
let dl be Data-Location; ::_thesis: il <> dl
ex j being Element of NAT st dl = dl. j by Th1;
hence il <> dl ; ::_thesis: verum
end;
theorem :: AMI_5:4
for s being State of SCM
for d being Data-Location holds d in dom s
proof
let s be State of SCM; ::_thesis: for d being Data-Location holds d in dom s
let d be Data-Location; ::_thesis: d in dom s
A1: dom s = the carrier of SCM by PARTFUN1:def_2;
thus d in dom s by A1; ::_thesis: verum
end;
registration
cluster NonZero SCM -> infinite ;
coherence
not Data-Locations is finite by AMI_3:27;
end;
Lm1: for b being Element of Data-Locations holds b is Data-Location
proof
let b be Element of Data-Locations ; ::_thesis: b is Data-Location
b in Data-Locations ;
then reconsider b = b as Object of SCM ;
b is Data-Location by AMI_2:def_16, AMI_3:27;
hence b is Data-Location ; ::_thesis: verum
end;
theorem :: AMI_5:5
for l being Instruction of SCM holds InsCode l <= 8
proof
let l be Instruction of SCM; ::_thesis: InsCode l <= 8
( l in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } or l in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : I in {1,2,3,4,5} } ) by AMI_3:27, XBOOLE_0:def_3;
then A1: ( l in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } or l in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } or l in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : I in {1,2,3,4,5} } ) by XBOOLE_0:def_3;
percases ( l in {[SCM-Halt,{},{}]} or l in { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } or l in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } or l in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : I in {1,2,3,4,5} } ) by A1, XBOOLE_0:def_3;
suppose l in {[SCM-Halt,{},{}]} ; ::_thesis: InsCode l <= 8
then l = [SCM-Halt,{},{}] by TARSKI:def_1;
then l `1_3 = 0 by RECDEF_2:def_1;
hence InsCode l <= 8 ; ::_thesis: verum
end;
suppose l in { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ; ::_thesis: InsCode l <= 8
then ex J being Element of Segm 9 ex a being Element of NAT st
( l = [J,<*a*>,{}] & J = 6 ) ;
then l `1_3 = 6 by RECDEF_2:def_1;
hence InsCode l <= 8 ; ::_thesis: verum
end;
suppose l in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } ; ::_thesis: InsCode l <= 8
then ex K being Element of Segm 9 ex a1 being Element of NAT ex b1 being Element of Data-Locations st
( l = [K,<*a1*>,<*b1*>] & K in {7,8} ) ;
then l `1_3 in {7,8} by RECDEF_2:def_1;
then ( l `1_3 = 7 or l `1_3 = 8 ) by TARSKI:def_2;
hence InsCode l <= 8 ; ::_thesis: verum
end;
suppose l in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : I in {1,2,3,4,5} } ; ::_thesis: InsCode l <= 8
then ex I being Element of Segm 9 ex b, c being Element of Data-Locations st
( l = [I,{},<*b,c*>] & I in {1,2,3,4,5} ) ;
then l `1_3 in {1,2,3,4,5} by RECDEF_2:def_1;
then ( l `1_3 = 1 or l `1_3 = 2 or l `1_3 = 3 or l `1_3 = 4 or l `1_3 = 5 ) by ENUMSET1:def_3;
hence InsCode l <= 8 ; ::_thesis: verum
end;
end;
end;
theorem :: AMI_5:6
canceled;
theorem :: AMI_5:7
for ins being Instruction of SCM st InsCode ins = 0 holds
ins = halt SCM
proof
let ins be Instruction of SCM; ::_thesis: ( InsCode ins = 0 implies ins = halt SCM )
assume A1: InsCode ins = 0 ; ::_thesis: ins = halt SCM
A2: now__::_thesis:_not_ins_in__{__[J,<*a*>,{}]_where_J_is_Element_of_Segm_9,_a_is_Element_of_NAT_:_J_=_6__}_
assume ins in { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ; ::_thesis: contradiction
then ex J being Element of Segm 9 ex a being Element of NAT st
( ins = [J,<*a*>,{}] & J = 6 ) ;
hence contradiction by A1, RECDEF_2:def_1; ::_thesis: verum
end;
now__::_thesis:_not_ins_in__{__[I,{},<*b,c*>]_where_I_is_Element_of_Segm_9,_b,_c_is_Element_of_Data-Locations_:_I_in_{1,2,3,4,5}__}_
assume ins in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : I in {1,2,3,4,5} } ; ::_thesis: contradiction
then ex I being Element of Segm 9 ex b, c being Element of Data-Locations st
( ins = [I,{},<*b,c*>] & I in {1,2,3,4,5} ) ;
hence contradiction by A1, RECDEF_2:def_1; ::_thesis: verum
end;
then A3: ins in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } by AMI_3:27, XBOOLE_0:def_3;
now__::_thesis:_not_ins_in__{__[K,<*a1*>,<*b1*>]_where_K_is_Element_of_Segm_9,_a1_is_Element_of_NAT_,_b1_is_Element_of_Data-Locations_:_K_in_{7,8}__}_
assume ins in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } ; ::_thesis: contradiction
then ex K being Element of Segm 9 ex a1 being Element of NAT ex b1 being Element of Data-Locations st
( ins = [K,<*a1*>,<*b1*>] & K in {7,8} ) ;
hence contradiction by A1, RECDEF_2:def_1; ::_thesis: verum
end;
then ins in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } by A3, XBOOLE_0:def_3;
then ins in {[SCM-Halt,{},{}]} by A2, XBOOLE_0:def_3;
hence ins = halt SCM by AMI_3:26, TARSKI:def_1; ::_thesis: verum
end;
theorem :: AMI_5:8
for ins being Instruction of SCM st InsCode ins = 1 holds
ex da, db being Data-Location st ins = da := db
proof
let ins be Instruction of SCM; ::_thesis: ( InsCode ins = 1 implies ex da, db being Data-Location st ins = da := db )
assume A1: InsCode ins = 1 ; ::_thesis: ex da, db being Data-Location st ins = da := db
A2: now__::_thesis:_not_ins_in__{__[J,<*a*>,{}]_where_J_is_Element_of_Segm_9,_a_is_Element_of_NAT_:_J_=_6__}_
assume ins in { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ; ::_thesis: contradiction
then ex J being Element of Segm 9 ex a being Element of NAT st
( ins = [J,<*a*>,{}] & J = 6 ) ;
hence contradiction by A1, RECDEF_2:def_1; ::_thesis: verum
end;
A3: now__::_thesis:_not_ins_in__{__[K,<*a1*>,<*b1*>]_where_K_is_Element_of_Segm_9,_a1_is_Element_of_NAT_,_b1_is_Element_of_Data-Locations_:_K_in_{7,8}__}_
assume ins in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } ; ::_thesis: contradiction
then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of Data-Locations such that
A4: ins = [K,<*a1*>,<*b1*>] and
A5: K in {7,8} ;
InsCode ins = K by A4, RECDEF_2:def_1;
hence contradiction by A1, A5, TARSKI:def_2; ::_thesis: verum
end;
InsCode (halt SCM) = 0 by COMPOS_1:70;
then not ins in {[SCM-Halt,{},{}]} by A1, AMI_3:26, TARSKI:def_1;
then not ins in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } by A2, XBOOLE_0:def_3;
then not ins in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } by A3, XBOOLE_0:def_3;
then ins in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : I in {1,2,3,4,5} } by AMI_3:27, XBOOLE_0:def_3;
then consider I being Element of Segm 9, b, c being Element of Data-Locations such that
A6: ins = [I,{},<*b,c*>] and
I in {1,2,3,4,5} ;
reconsider da = b, db = c as Data-Location by Lm1;
take da ; ::_thesis: ex db being Data-Location st ins = da := db
take db ; ::_thesis: ins = da := db
thus ins = da := db by A1, A6, RECDEF_2:def_1; ::_thesis: verum
end;
theorem :: AMI_5:9
for ins being Instruction of SCM st InsCode ins = 2 holds
ex da, db being Data-Location st ins = AddTo (da,db)
proof
let ins be Instruction of SCM; ::_thesis: ( InsCode ins = 2 implies ex da, db being Data-Location st ins = AddTo (da,db) )
assume A1: InsCode ins = 2 ; ::_thesis: ex da, db being Data-Location st ins = AddTo (da,db)
A2: now__::_thesis:_not_ins_in__{__[J,<*a*>,{}]_where_J_is_Element_of_Segm_9,_a_is_Element_of_NAT_:_J_=_6__}_
assume ins in { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ; ::_thesis: contradiction
then ex J being Element of Segm 9 ex a being Element of NAT st
( ins = [J,<*a*>,{}] & J = 6 ) ;
hence contradiction by A1, RECDEF_2:def_1; ::_thesis: verum
end;
A3: now__::_thesis:_not_ins_in__{__[K,<*a1*>,<*b1*>]_where_K_is_Element_of_Segm_9,_a1_is_Element_of_NAT_,_b1_is_Element_of_Data-Locations_:_K_in_{7,8}__}_
assume ins in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } ; ::_thesis: contradiction
then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of Data-Locations such that
A4: ins = [K,<*a1*>,<*b1*>] and
A5: K in {7,8} ;
InsCode ins = K by A4, RECDEF_2:def_1;
hence contradiction by A1, A5, TARSKI:def_2; ::_thesis: verum
end;
InsCode (halt SCM) = 0 by COMPOS_1:70;
then not ins in {[SCM-Halt,{},{}]} by A1, AMI_3:26, TARSKI:def_1;
then not ins in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } by A2, XBOOLE_0:def_3;
then not ins in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } by A3, XBOOLE_0:def_3;
then ins in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : I in {1,2,3,4,5} } by AMI_3:27, XBOOLE_0:def_3;
then consider I being Element of Segm 9, b, c being Element of Data-Locations such that
A6: ins = [I,{},<*b,c*>] and
I in {1,2,3,4,5} ;
reconsider da = b, db = c as Data-Location by Lm1;
take da ; ::_thesis: ex db being Data-Location st ins = AddTo (da,db)
take db ; ::_thesis: ins = AddTo (da,db)
thus ins = AddTo (da,db) by A1, A6, RECDEF_2:def_1; ::_thesis: verum
end;
theorem :: AMI_5:10
for ins being Instruction of SCM st InsCode ins = 3 holds
ex da, db being Data-Location st ins = SubFrom (da,db)
proof
let ins be Instruction of SCM; ::_thesis: ( InsCode ins = 3 implies ex da, db being Data-Location st ins = SubFrom (da,db) )
assume A1: InsCode ins = 3 ; ::_thesis: ex da, db being Data-Location st ins = SubFrom (da,db)
A2: now__::_thesis:_not_ins_in__{__[J,<*a*>,{}]_where_J_is_Element_of_Segm_9,_a_is_Element_of_NAT_:_J_=_6__}_
assume ins in { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ; ::_thesis: contradiction
then ex J being Element of Segm 9 ex a being Element of NAT st
( ins = [J,<*a*>,{}] & J = 6 ) ;
hence contradiction by A1, RECDEF_2:def_1; ::_thesis: verum
end;
A3: now__::_thesis:_not_ins_in__{__[K,<*a1*>,<*b1*>]_where_K_is_Element_of_Segm_9,_a1_is_Element_of_NAT_,_b1_is_Element_of_Data-Locations_:_K_in_{7,8}__}_
assume ins in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } ; ::_thesis: contradiction
then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of Data-Locations such that
A4: ins = [K,<*a1*>,<*b1*>] and
A5: K in {7,8} ;
InsCode ins = K by A4, RECDEF_2:def_1;
hence contradiction by A1, A5, TARSKI:def_2; ::_thesis: verum
end;
InsCode (halt SCM) = 0 by COMPOS_1:70;
then not ins in {[SCM-Halt,{},{}]} by A1, AMI_3:26, TARSKI:def_1;
then not ins in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } by A2, XBOOLE_0:def_3;
then not ins in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } by A3, XBOOLE_0:def_3;
then ins in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : I in {1,2,3,4,5} } by AMI_3:27, XBOOLE_0:def_3;
then consider I being Element of Segm 9, b, c being Element of Data-Locations such that
A6: ins = [I,{},<*b,c*>] and
I in {1,2,3,4,5} ;
reconsider da = b, db = c as Data-Location by Lm1;
take da ; ::_thesis: ex db being Data-Location st ins = SubFrom (da,db)
take db ; ::_thesis: ins = SubFrom (da,db)
thus ins = SubFrom (da,db) by A1, A6, RECDEF_2:def_1; ::_thesis: verum
end;
theorem :: AMI_5:11
for ins being Instruction of SCM st InsCode ins = 4 holds
ex da, db being Data-Location st ins = MultBy (da,db)
proof
let ins be Instruction of SCM; ::_thesis: ( InsCode ins = 4 implies ex da, db being Data-Location st ins = MultBy (da,db) )
assume A1: InsCode ins = 4 ; ::_thesis: ex da, db being Data-Location st ins = MultBy (da,db)
A2: now__::_thesis:_not_ins_in__{__[J,<*a*>,{}]_where_J_is_Element_of_Segm_9,_a_is_Element_of_NAT_:_J_=_6__}_
assume ins in { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ; ::_thesis: contradiction
then ex J being Element of Segm 9 ex a being Element of NAT st
( ins = [J,<*a*>,{}] & J = 6 ) ;
hence contradiction by A1, RECDEF_2:def_1; ::_thesis: verum
end;
A3: now__::_thesis:_not_ins_in__{__[K,<*a1*>,<*b1*>]_where_K_is_Element_of_Segm_9,_a1_is_Element_of_NAT_,_b1_is_Element_of_Data-Locations_:_K_in_{7,8}__}_
assume ins in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } ; ::_thesis: contradiction
then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of Data-Locations such that
A4: ins = [K,<*a1*>,<*b1*>] and
A5: K in {7,8} ;
InsCode ins = K by A4, RECDEF_2:def_1;
hence contradiction by A1, A5, TARSKI:def_2; ::_thesis: verum
end;
InsCode (halt SCM) = 0 by COMPOS_1:70;
then not ins in {[SCM-Halt,{},{}]} by A1, AMI_3:26, TARSKI:def_1;
then not ins in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } by A2, XBOOLE_0:def_3;
then not ins in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } by A3, XBOOLE_0:def_3;
then ins in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : I in {1,2,3,4,5} } by AMI_3:27, XBOOLE_0:def_3;
then consider I being Element of Segm 9, b, c being Element of Data-Locations such that
A6: ins = [I,{},<*b,c*>] and
I in {1,2,3,4,5} ;
reconsider da = b, db = c as Data-Location by Lm1;
take da ; ::_thesis: ex db being Data-Location st ins = MultBy (da,db)
take db ; ::_thesis: ins = MultBy (da,db)
thus ins = MultBy (da,db) by A1, A6, RECDEF_2:def_1; ::_thesis: verum
end;
theorem :: AMI_5:12
for ins being Instruction of SCM st InsCode ins = 5 holds
ex da, db being Data-Location st ins = Divide (da,db)
proof
let ins be Instruction of SCM; ::_thesis: ( InsCode ins = 5 implies ex da, db being Data-Location st ins = Divide (da,db) )
assume A1: InsCode ins = 5 ; ::_thesis: ex da, db being Data-Location st ins = Divide (da,db)
A2: now__::_thesis:_not_ins_in__{__[J,<*a*>,{}]_where_J_is_Element_of_Segm_9,_a_is_Element_of_NAT_:_J_=_6__}_
assume ins in { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ; ::_thesis: contradiction
then ex J being Element of Segm 9 ex a being Element of NAT st
( ins = [J,<*a*>,{}] & J = 6 ) ;
hence contradiction by A1, RECDEF_2:def_1; ::_thesis: verum
end;
A3: now__::_thesis:_not_ins_in__{__[K,<*a1*>,<*b1*>]_where_K_is_Element_of_Segm_9,_a1_is_Element_of_NAT_,_b1_is_Element_of_Data-Locations_:_K_in_{7,8}__}_
assume ins in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } ; ::_thesis: contradiction
then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of Data-Locations such that
A4: ins = [K,<*a1*>,<*b1*>] and
A5: K in {7,8} ;
InsCode ins = K by A4, RECDEF_2:def_1;
hence contradiction by A1, A5, TARSKI:def_2; ::_thesis: verum
end;
InsCode (halt SCM) = 0 by COMPOS_1:70;
then not ins in {[SCM-Halt,{},{}]} by A1, AMI_3:26, TARSKI:def_1;
then not ins in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } by A2, XBOOLE_0:def_3;
then not ins in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } by A3, XBOOLE_0:def_3;
then ins in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : I in {1,2,3,4,5} } by AMI_3:27, XBOOLE_0:def_3;
then consider I being Element of Segm 9, b, c being Element of Data-Locations such that
A6: ins = [I,{},<*b,c*>] and
I in {1,2,3,4,5} ;
reconsider da = b, db = c as Data-Location by Lm1;
take da ; ::_thesis: ex db being Data-Location st ins = Divide (da,db)
take db ; ::_thesis: ins = Divide (da,db)
thus ins = Divide (da,db) by A1, A6, RECDEF_2:def_1; ::_thesis: verum
end;
theorem :: AMI_5:13
for ins being Instruction of SCM st InsCode ins = 6 holds
ex loc being Element of NAT st ins = SCM-goto loc
proof
let ins be Instruction of SCM; ::_thesis: ( InsCode ins = 6 implies ex loc being Element of NAT st ins = SCM-goto loc )
assume A1: InsCode ins = 6 ; ::_thesis: ex loc being Element of NAT st ins = SCM-goto loc
now__::_thesis:_not_ins_in__{__[I,{},<*b,c*>]_where_I_is_Element_of_Segm_9,_b,_c_is_Element_of_Data-Locations_:_I_in_{1,2,3,4,5}__}_
assume ins in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : I in {1,2,3,4,5} } ; ::_thesis: contradiction
then consider I being Element of Segm 9, b, c being Element of Data-Locations such that
A2: ins = [I,{},<*b,c*>] and
A3: I in {1,2,3,4,5} ;
InsCode ins = I by A2, RECDEF_2:def_1;
hence contradiction by A1, A3, ENUMSET1:def_3; ::_thesis: verum
end;
then A4: ins in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } by AMI_3:27, XBOOLE_0:def_3;
now__::_thesis:_not_ins_in__{__[K,<*a1*>,<*b1*>]_where_K_is_Element_of_Segm_9,_a1_is_Element_of_NAT_,_b1_is_Element_of_Data-Locations_:_K_in_{7,8}__}_
assume ins in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } ; ::_thesis: contradiction
then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of Data-Locations such that
A5: ins = [K,<*a1*>,<*b1*>] and
A6: K in {7,8} ;
InsCode ins = K by A5, RECDEF_2:def_1;
hence contradiction by A1, A6, TARSKI:def_2; ::_thesis: verum
end;
then A7: ins in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } by A4, XBOOLE_0:def_3;
InsCode (halt SCM) = 0 by COMPOS_1:70;
then not ins in {[SCM-Halt,{},{}]} by A1, AMI_3:26, TARSKI:def_1;
then ins in { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } by A7, XBOOLE_0:def_3;
then consider J being Element of Segm 9, a being Element of NAT such that
A8: ( ins = [J,<*a*>,{}] & J = 6 ) ;
reconsider loc = a as Element of NAT ;
take loc ; ::_thesis: ins = SCM-goto loc
thus ins = SCM-goto loc by A8; ::_thesis: verum
end;
theorem :: AMI_5:14
for ins being Instruction of SCM st InsCode ins = 7 holds
ex loc being Element of NAT ex da being Data-Location st ins = da =0_goto loc
proof
let ins be Instruction of SCM; ::_thesis: ( InsCode ins = 7 implies ex loc being Element of NAT ex da being Data-Location st ins = da =0_goto loc )
assume A1: InsCode ins = 7 ; ::_thesis: ex loc being Element of NAT ex da being Data-Location st ins = da =0_goto loc
A2: now__::_thesis:_not_ins_in__{__[J,<*a*>,{}]_where_J_is_Element_of_Segm_9,_a_is_Element_of_NAT_:_J_=_6__}_
assume ins in { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ; ::_thesis: contradiction
then ex J being Element of Segm 9 ex a being Element of NAT st
( ins = [J,<*a*>,{}] & J = 6 ) ;
hence contradiction by A1, RECDEF_2:def_1; ::_thesis: verum
end;
now__::_thesis:_not_ins_in__{__[I,{},<*b,c*>]_where_I_is_Element_of_Segm_9,_b,_c_is_Element_of_Data-Locations_:_I_in_{1,2,3,4,5}__}_
assume ins in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : I in {1,2,3,4,5} } ; ::_thesis: contradiction
then consider I being Element of Segm 9, b, c being Element of Data-Locations such that
A3: ins = [I,{},<*b,c*>] and
A4: I in {1,2,3,4,5} ;
InsCode ins = I by A3, RECDEF_2:def_1;
hence contradiction by A1, A4, ENUMSET1:def_3; ::_thesis: verum
end;
then A5: ins in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } by AMI_3:27, XBOOLE_0:def_3;
InsCode (halt SCM) = 0 by COMPOS_1:70;
then not ins in {[SCM-Halt,{},{}]} by A1, AMI_3:26, TARSKI:def_1;
then not ins in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } by A2, XBOOLE_0:def_3;
then ins in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } by A5, XBOOLE_0:def_3;
then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of Data-Locations such that
A6: ins = [K,<*a1*>,<*b1*>] and
K in {7,8} ;
reconsider da = b1 as Data-Location by Lm1;
reconsider loc = a1 as Element of NAT ;
take loc ; ::_thesis: ex da being Data-Location st ins = da =0_goto loc
take da ; ::_thesis: ins = da =0_goto loc
thus ins = da =0_goto loc by A1, A6, RECDEF_2:def_1; ::_thesis: verum
end;
theorem :: AMI_5:15
for ins being Instruction of SCM st InsCode ins = 8 holds
ex loc being Element of NAT ex da being Data-Location st ins = da >0_goto loc
proof
let ins be Instruction of SCM; ::_thesis: ( InsCode ins = 8 implies ex loc being Element of NAT ex da being Data-Location st ins = da >0_goto loc )
assume A1: InsCode ins = 8 ; ::_thesis: ex loc being Element of NAT ex da being Data-Location st ins = da >0_goto loc
A2: now__::_thesis:_not_ins_in__{__[J,<*a*>,{}]_where_J_is_Element_of_Segm_9,_a_is_Element_of_NAT_:_J_=_6__}_
assume ins in { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ; ::_thesis: contradiction
then ex J being Element of Segm 9 ex a being Element of NAT st
( ins = [J,<*a*>,{}] & J = 6 ) ;
hence contradiction by A1, RECDEF_2:def_1; ::_thesis: verum
end;
now__::_thesis:_not_ins_in__{__[I,{},<*b,c*>]_where_I_is_Element_of_Segm_9,_b,_c_is_Element_of_Data-Locations_:_I_in_{1,2,3,4,5}__}_
assume ins in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of Data-Locations : I in {1,2,3,4,5} } ; ::_thesis: contradiction
then consider I being Element of Segm 9, b, c being Element of Data-Locations such that
A3: ins = [I,{},<*b,c*>] and
A4: I in {1,2,3,4,5} ;
InsCode ins = I by A3, RECDEF_2:def_1;
hence contradiction by A1, A4, ENUMSET1:def_3; ::_thesis: verum
end;
then A5: ins in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } by AMI_3:27, XBOOLE_0:def_3;
InsCode (halt SCM) = 0 by COMPOS_1:70;
then not ins in {[SCM-Halt,{},{}]} by A1, AMI_3:26, TARSKI:def_1;
then not ins in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Element of NAT : J = 6 } by A2, XBOOLE_0:def_3;
then ins in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of Data-Locations : K in {7,8} } by A5, XBOOLE_0:def_3;
then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of Data-Locations such that
A6: ins = [K,<*a1*>,<*b1*>] and
K in {7,8} ;
reconsider da = b1 as Data-Location by Lm1;
reconsider loc = a1 as Element of NAT ;
take loc ; ::_thesis: ex da being Data-Location st ins = da >0_goto loc
take da ; ::_thesis: ins = da >0_goto loc
thus ins = da >0_goto loc by A1, A6, RECDEF_2:def_1; ::_thesis: verum
end;
begin
theorem :: AMI_5:16
for s being State of SCM
for iloc being Element of NAT
for a being Data-Location holds s . a = (s +* (Start-At (iloc,SCM))) . a
proof
let s be State of SCM; ::_thesis: for iloc being Element of NAT
for a being Data-Location holds s . a = (s +* (Start-At (iloc,SCM))) . a
let iloc be Element of NAT ; ::_thesis: for a being Data-Location holds s . a = (s +* (Start-At (iloc,SCM))) . a
let a be Data-Location; ::_thesis: s . a = (s +* (Start-At (iloc,SCM))) . a
a in the carrier of SCM ;
then a in dom s by PARTFUN1:def_2;
then A1: ( dom (Start-At (iloc,SCM)) = {(IC )} & a in (dom s) \/ (dom (Start-At (iloc,SCM))) ) by FUNCOP_1:13, XBOOLE_0:def_3;
a <> IC by Th2;
then not a in {(IC )} by TARSKI:def_1;
hence s . a = (s +* (Start-At (iloc,SCM))) . a by A1, FUNCT_4:def_1; ::_thesis: verum
end;
begin
registration
cluster SCM -> IC-recognized ;
coherence
SCM is IC-recognized
proof
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being b1 -autonomic FinPartState of SCM st DataPart p <> {} holds
IC in dom p
proof
let q be NAT -defined the InstructionsF of SCM -valued finite non halt-free Function; ::_thesis: for p being q -autonomic FinPartState of SCM st DataPart p <> {} holds
IC in dom p
let p be q -autonomic FinPartState of SCM; ::_thesis: ( DataPart p <> {} implies IC in dom p )
assume DataPart p <> {} ; ::_thesis: IC in dom p
then A1: dom (DataPart p) <> {} ;
assume A2: not IC in dom p ; ::_thesis: contradiction
then dom p misses {(IC )} by ZFMISC_1:50;
then A3: (dom p) /\ {(IC )} = {} by XBOOLE_0:def_7;
not p is q -autonomic
proof
set il = the Element of NAT \ (dom q);
set d2 = the Element of (Data-Locations ) \ (dom p);
set d1 = the Element of dom (DataPart p);
A4: the Element of dom (DataPart p) in dom (DataPart p) by A1;
DataPart p c= p by MEMSTR_0:12;
then A5: dom (DataPart p) c= dom p by RELAT_1:11;
dom (DataPart p) c= the carrier of SCM by RELAT_1:def_18;
then reconsider d1 = the Element of dom (DataPart p) as Element of SCM by A4;
not Data-Locations c= dom p ;
then A6: (Data-Locations ) \ (dom p) <> {} by XBOOLE_1:37;
then the Element of (Data-Locations ) \ (dom p) in Data-Locations by XBOOLE_0:def_5;
then reconsider d2 = the Element of (Data-Locations ) \ (dom p) as Data-Location by AMI_2:def_16, AMI_3:27;
A7: not d2 in dom p by A6, XBOOLE_0:def_5;
then A8: dom p misses {d2} by ZFMISC_1:50;
not NAT c= dom q ;
then A9: NAT \ (dom q) <> {} by XBOOLE_1:37;
then reconsider il = the Element of NAT \ (dom q) as Element of NAT by XBOOLE_0:def_5;
A10: not il in dom q by A9, XBOOLE_0:def_5;
dom (DataPart p) c= Data-Locations by RELAT_1:58;
then reconsider d1 = d1 as Data-Location by A4, AMI_2:def_16, AMI_3:27;
set p2 = p +* ((d2 .--> 1) +* (Start-At (il,SCM)));
set p1 = p +* ((d2 .--> 0) +* (Start-At (il,SCM)));
set q2 = q +* (il .--> (d1 := d2));
set q1 = q +* (il .--> (d1 := d2));
consider s1 being State of SCM such that
A11: p +* ((d2 .--> 0) +* (Start-At (il,SCM))) c= s1 by PBOOLE:141;
consider S1 being Instruction-Sequence of SCM such that
A12: q +* (il .--> (d1 := d2)) c= S1 by PBOOLE:145;
A13: dom p misses {d2} by A7, ZFMISC_1:50;
A14: dom ((d2 .--> 1) +* (Start-At (il,SCM))) = (dom (d2 .--> 1)) \/ (dom (Start-At (il,SCM))) by FUNCT_4:def_1;
consider s2 being State of SCM such that
A15: p +* ((d2 .--> 1) +* (Start-At (il,SCM))) c= s2 by PBOOLE:141;
consider S2 being Instruction-Sequence of SCM such that
A16: q +* (il .--> (d1 := d2)) c= S2 by PBOOLE:145;
A17: dom p c= the carrier of SCM by RELAT_1:def_18;
dom (Comput (S2,s2,1)) = the carrier of SCM by PARTFUN1:def_2;
then A18: dom ((Comput (S2,s2,1)) | (dom p)) = dom p by A17, RELAT_1:62;
A19: dom (Comput (S1,s1,1)) = the carrier of SCM by PARTFUN1:def_2;
A20: dom ((Comput (S1,s1,1)) | (dom p)) = dom p by A17, A19, RELAT_1:62;
A21: dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM)))) = (dom p) \/ (dom ((d2 .--> 1) +* (Start-At (il,SCM)))) by FUNCT_4:def_1;
A22: dom (q +* (il .--> (d1 := d2))) = (dom q) \/ (dom (il .--> (d1 := d2))) by FUNCT_4:def_1;
A23: dom (Start-At (il,SCM)) = {(IC )} by FUNCOP_1:13;
then A24: IC in dom (Start-At (il,SCM)) by TARSKI:def_1;
then A25: IC in dom ((d2 .--> 1) +* (Start-At (il,SCM))) by A14, XBOOLE_0:def_3;
then IC in dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM)))) by A21, XBOOLE_0:def_3;
then A26: IC s2 = (p +* ((d2 .--> 1) +* (Start-At (il,SCM)))) . (IC ) by A15, GRFUNC_1:2
.= ((d2 .--> 1) +* (Start-At (il,SCM))) . (IC ) by A25, FUNCT_4:13
.= (Start-At (il,SCM)) . (IC ) by A24, FUNCT_4:13
.= il by FUNCOP_1:72 ;
d2 <> IC by Th2;
then A27: not d2 in dom (Start-At (il,SCM)) by A23, TARSKI:def_1;
dom (d2 .--> 1) = {d2} by FUNCOP_1:13;
then d2 in dom (d2 .--> 1) by TARSKI:def_1;
then A28: d2 in dom ((d2 .--> 1) +* (Start-At (il,SCM))) by A14, XBOOLE_0:def_3;
then d2 in dom (p +* ((d2 .--> 1) +* (Start-At (il,SCM)))) by A21, XBOOLE_0:def_3;
then A29: s2 . d2 = (p +* ((d2 .--> 1) +* (Start-At (il,SCM)))) . d2 by A15, GRFUNC_1:2
.= ((d2 .--> 1) +* (Start-At (il,SCM))) . d2 by A28, FUNCT_4:13
.= (d2 .--> 1) . d2 by A27, FUNCT_4:11
.= 1 by FUNCOP_1:72 ;
A30: dom (il .--> (d1 := d2)) = {il} by FUNCOP_1:13;
then A31: il in dom (il .--> (d1 := d2)) by TARSKI:def_1;
then il in dom (q +* (il .--> (d1 := d2))) by A22, XBOOLE_0:def_3;
then A32: S2 . il = (q +* (il .--> (d1 := d2))) . il by A16, GRFUNC_1:2
.= (il .--> (d1 := d2)) . il by A31, FUNCT_4:13
.= d1 := d2 by FUNCOP_1:72 ;
A33: S2 /. (IC s2) = S2 . (IC s2) by PBOOLE:143;
A34: (Comput (S2,s2,(0 + 1))) . d1 = (Following (S2,(Comput (S2,s2,0)))) . d1 by EXTPRO_1:3
.= (Following (S2,s2)) . d1
.= 1 by A26, A32, A29, A33, AMI_3:2 ;
dom p misses {(IC )} by A2, ZFMISC_1:50;
then A35: (dom p) /\ {(IC )} = {} by XBOOLE_0:def_7;
take P = S1; :: according to EXTPRO_1:def_10 ::_thesis: ex b1 being set st
( q c= P & q c= b1 & ex b2, b3 being set st
( p c= b2 & p c= b3 & not for b4 being Element of NAT holds (Comput (P,b2,b4)) | (proj1 p) = (Comput (b1,b3,b4)) | (proj1 p) ) )
take Q = S2; ::_thesis: ( q c= P & q c= Q & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P,b1,b3)) | (proj1 p) = (Comput (Q,b2,b3)) | (proj1 p) ) )
dom ((d2 .--> 0) +* (Start-At (il,SCM))) = (dom (d2 .--> 0)) \/ (dom (Start-At (il,SCM))) by FUNCT_4:def_1
.= (dom (d2 .--> 0)) \/ {(IC )} by FUNCOP_1:13
.= {d2} \/ {(IC )} by FUNCOP_1:13 ;
then (dom p) /\ (dom ((d2 .--> 0) +* (Start-At (il,SCM)))) = ((dom p) /\ {d2}) \/ {} by A35, XBOOLE_1:23
.= {} by A8, XBOOLE_0:def_7 ;
then dom p misses dom ((d2 .--> 0) +* (Start-At (il,SCM))) by XBOOLE_0:def_7;
then p c= p +* ((d2 .--> 0) +* (Start-At (il,SCM))) by FUNCT_4:32;
then A36: p c= s1 by A11, XBOOLE_1:1;
dom q misses dom (il .--> (d1 := d2)) by A30, A10, ZFMISC_1:50;
then q c= q +* (il .--> (d1 := d2)) by FUNCT_4:32;
hence q c= P by A12, XBOOLE_1:1; ::_thesis: ( q c= Q & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P,b1,b3)) | (proj1 p) = (Comput (Q,b2,b3)) | (proj1 p) ) )
A37: dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM)))) = (dom p) \/ (dom ((d2 .--> 0) +* (Start-At (il,SCM)))) by FUNCT_4:def_1;
dom ((d2 .--> 1) +* (Start-At (il,SCM))) = (dom (d2 .--> 1)) \/ (dom (Start-At (il,SCM))) by FUNCT_4:def_1
.= (dom (d2 .--> 1)) \/ {(IC )} by FUNCOP_1:13
.= {d2} \/ {(IC )} by FUNCOP_1:13 ;
then (dom p) /\ (dom ((d2 .--> 1) +* (Start-At (il,SCM)))) = ((dom p) /\ {d2}) \/ {} by A3, XBOOLE_1:23
.= {} by A13, XBOOLE_0:def_7 ;
then dom p misses dom ((d2 .--> 1) +* (Start-At (il,SCM))) by XBOOLE_0:def_7;
then p c= p +* ((d2 .--> 1) +* (Start-At (il,SCM))) by FUNCT_4:32;
then A38: p c= s2 by A15, XBOOLE_1:1;
dom q misses dom (il .--> (d1 := d2)) by A30, A10, ZFMISC_1:50;
then q c= q +* (il .--> (d1 := d2)) by FUNCT_4:32;
hence q c= Q by A16, XBOOLE_1:1; ::_thesis: ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P,b1,b3)) | (proj1 p) = (Comput (Q,b2,b3)) | (proj1 p) )
take s1 ; ::_thesis: ex b1 being set st
( p c= s1 & p c= b1 & not for b2 being Element of NAT holds (Comput (P,s1,b2)) | (proj1 p) = (Comput (Q,b1,b2)) | (proj1 p) )
take s2 ; ::_thesis: ( p c= s1 & p c= s2 & not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 p) = (Comput (Q,s2,b1)) | (proj1 p) )
thus p c= s1 by A36; ::_thesis: ( p c= s2 & not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 p) = (Comput (Q,s2,b1)) | (proj1 p) )
thus p c= s2 by A38; ::_thesis: not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 p) = (Comput (Q,s2,b1)) | (proj1 p)
take 1 ; ::_thesis: not (Comput (P,s1,1)) | (proj1 p) = (Comput (Q,s2,1)) | (proj1 p)
A39: dom ((d2 .--> 0) +* (Start-At (il,SCM))) = (dom (d2 .--> 0)) \/ (dom (Start-At (il,SCM))) by FUNCT_4:def_1;
A40: dom (Start-At (il,SCM)) = {(IC )} by FUNCOP_1:13;
then A41: IC in dom (Start-At (il,SCM)) by TARSKI:def_1;
then A42: IC in dom ((d2 .--> 0) +* (Start-At (il,SCM))) by A39, XBOOLE_0:def_3;
then IC in dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM)))) by A37, XBOOLE_0:def_3;
then A43: IC s1 = (p +* ((d2 .--> 0) +* (Start-At (il,SCM)))) . (IC ) by A11, GRFUNC_1:2
.= ((d2 .--> 0) +* (Start-At (il,SCM))) . (IC ) by A42, FUNCT_4:13
.= (Start-At (il,SCM)) . (IC ) by A41, FUNCT_4:13
.= il by FUNCOP_1:72 ;
d2 <> IC by Th2;
then A44: not d2 in dom (Start-At (il,SCM)) by A40, TARSKI:def_1;
dom (d2 .--> 0) = {d2} by FUNCOP_1:13;
then d2 in dom (d2 .--> 0) by TARSKI:def_1;
then A45: d2 in dom ((d2 .--> 0) +* (Start-At (il,SCM))) by A39, XBOOLE_0:def_3;
then d2 in dom (p +* ((d2 .--> 0) +* (Start-At (il,SCM)))) by A37, XBOOLE_0:def_3;
then A46: s1 . d2 = (p +* ((d2 .--> 0) +* (Start-At (il,SCM)))) . d2 by A11, GRFUNC_1:2
.= ((d2 .--> 0) +* (Start-At (il,SCM))) . d2 by A45, FUNCT_4:13
.= (d2 .--> 0) . d2 by A44, FUNCT_4:11
.= 0 by FUNCOP_1:72 ;
dom (il .--> (d1 := d2)) = {il} by FUNCOP_1:13;
then A47: il in dom (il .--> (d1 := d2)) by TARSKI:def_1;
dom (q +* (il .--> (d1 := d2))) = (dom q) \/ (dom (il .--> (d1 := d2))) by FUNCT_4:def_1;
then il in dom (q +* (il .--> (d1 := d2))) by A47, XBOOLE_0:def_3;
then A48: S1 . il = (q +* (il .--> (d1 := d2))) . il by A12, GRFUNC_1:2
.= (il .--> (d1 := d2)) . il by A47, FUNCT_4:13
.= d1 := d2 by FUNCOP_1:72 ;
A49: S1 /. (IC s1) = S1 . (IC s1) by PBOOLE:143;
(Comput (S1,s1,(0 + 1))) . d1 = (Following (S1,(Comput (S1,s1,0)))) . d1 by EXTPRO_1:3
.= 0 by A43, A48, A46, A49, AMI_3:2 ;
then ((Comput (P,s1,1)) | (dom p)) . d1 = 0 by A4, A5, A20, FUNCT_1:47;
hence (Comput (P,s1,1)) | (dom p) <> (Comput (Q,s2,1)) | (dom p) by A18, A34, A4, A5, FUNCT_1:47; ::_thesis: verum
end;
hence contradiction ; ::_thesis: verum
end;
hence SCM is IC-recognized by AMISTD_5:3; ::_thesis: verum
end;
end;
registration
cluster SCM -> CurIns-recognized ;
coherence
SCM is CurIns-recognized
proof
let q be NAT -defined the InstructionsF of SCM -valued finite non halt-free Function; :: according to AMISTD_5:def_4 ::_thesis: for b1 being set
for b2 being set holds
( not b1 c= b2 or for b3 being set holds
( not q c= b3 or for b4 being Element of NAT holds IC (Comput (b3,b2,b4)) in proj1 q ) )
let p be non empty q -autonomic FinPartState of SCM; ::_thesis: for b1 being set holds
( not p c= b1 or for b2 being set holds
( not q c= b2 or for b3 being Element of NAT holds IC (Comput (b2,b1,b3)) in proj1 q ) )
let s be State of SCM; ::_thesis: ( not p c= s or for b1 being set holds
( not q c= b1 or for b2 being Element of NAT holds IC (Comput (b1,s,b2)) in proj1 q ) )
assume A1: p c= s ; ::_thesis: for b1 being set holds
( not q c= b1 or for b2 being Element of NAT holds IC (Comput (b1,s,b2)) in proj1 q )
let P be Instruction-Sequence of SCM; ::_thesis: ( not q c= P or for b1 being Element of NAT holds IC (Comput (P,s,b1)) in proj1 q )
assume A2: q c= P ; ::_thesis: for b1 being Element of NAT holds IC (Comput (P,s,b1)) in proj1 q
let i be Element of NAT ; ::_thesis: IC (Comput (P,s,i)) in proj1 q
set Csi = Comput (P,s,i);
set loc = IC (Comput (P,s,i));
set loc1 = (IC (Comput (P,s,i))) + 1;
assume A3: not IC (Comput (P,s,i)) in dom q ; ::_thesis: contradiction
set I = (dl. 0) := (dl. 0);
set q1 = q +* ((IC (Comput (P,s,i))) .--> ((dl. 0) := (dl. 0)));
set q2 = q +* ((IC (Comput (P,s,i))) .--> (halt SCM));
reconsider P1 = P +* ((IC (Comput (P,s,i))) .--> ((dl. 0) := (dl. 0))) as Instruction-Sequence of SCM ;
reconsider P2 = P +* ((IC (Comput (P,s,i))) .--> (halt SCM)) as Instruction-Sequence of SCM ;
A4: dom ((IC (Comput (P,s,i))) .--> (halt SCM)) = {(IC (Comput (P,s,i)))} by FUNCOP_1:13;
then A5: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> (halt SCM)) by TARSKI:def_1;
A6: dom ((IC (Comput (P,s,i))) .--> ((dl. 0) := (dl. 0))) = {(IC (Comput (P,s,i)))} by FUNCOP_1:13;
then A7: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> ((dl. 0) := (dl. 0))) by TARSKI:def_1;
A8: dom q misses dom ((IC (Comput (P,s,i))) .--> (halt SCM)) by A3, A4, ZFMISC_1:50;
A9: dom q misses dom ((IC (Comput (P,s,i))) .--> ((dl. 0) := (dl. 0))) by A3, A6, ZFMISC_1:50;
A10: q +* ((IC (Comput (P,s,i))) .--> ((dl. 0) := (dl. 0))) c= P1 by A2, FUNCT_4:123;
A11: q +* ((IC (Comput (P,s,i))) .--> (halt SCM)) c= P2 by A2, FUNCT_4:123;
set Cs2i = Comput (P2,s,i);
set Cs1i = Comput (P1,s,i);
not p is q -autonomic
proof
((IC (Comput (P,s,i))) .--> (halt SCM)) . (IC (Comput (P,s,i))) = halt SCM by FUNCOP_1:72;
then A12: P2 . (IC (Comput (P,s,i))) = halt SCM by A5, FUNCT_4:13;
A13: ((IC (Comput (P,s,i))) .--> ((dl. 0) := (dl. 0))) . (IC (Comput (P,s,i))) = (dl. 0) := (dl. 0) by FUNCOP_1:72;
take P1 ; :: according to EXTPRO_1:def_10 ::_thesis: ex b1 being set st
( q c= P1 & q c= b1 & ex b2, b3 being set st
( p c= b2 & p c= b3 & not for b4 being Element of NAT holds (Comput (P1,b2,b4)) | (proj1 p) = (Comput (b1,b3,b4)) | (proj1 p) ) )
take P2 ; ::_thesis: ( q c= P1 & q c= P2 & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (proj1 p) = (Comput (P2,b2,b3)) | (proj1 p) ) )
q c= q +* ((IC (Comput (P,s,i))) .--> ((dl. 0) := (dl. 0))) by A9, FUNCT_4:32;
hence A14: q c= P1 by A10, XBOOLE_1:1; ::_thesis: ( q c= P2 & ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (proj1 p) = (Comput (P2,b2,b3)) | (proj1 p) ) )
q c= q +* ((IC (Comput (P,s,i))) .--> (halt SCM)) by A8, FUNCT_4:32;
hence A15: q c= P2 by A11, XBOOLE_1:1; ::_thesis: ex b1, b2 being set st
( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (proj1 p) = (Comput (P2,b2,b3)) | (proj1 p) )
take s ; ::_thesis: ex b1 being set st
( p c= s & p c= b1 & not for b2 being Element of NAT holds (Comput (P1,s,b2)) | (proj1 p) = (Comput (P2,b1,b2)) | (proj1 p) )
take s ; ::_thesis: ( p c= s & p c= s & not for b1 being Element of NAT holds (Comput (P1,s,b1)) | (proj1 p) = (Comput (P2,s,b1)) | (proj1 p) )
thus p c= s by A1; ::_thesis: ( p c= s & not for b1 being Element of NAT holds (Comput (P1,s,b1)) | (proj1 p) = (Comput (P2,s,b1)) | (proj1 p) )
A16: (Comput (P1,s,i)) | (dom p) = (Comput (P,s,i)) | (dom p) by A14, A2, A1, EXTPRO_1:def_10;
thus p c= s by A1; ::_thesis: not for b1 being Element of NAT holds (Comput (P1,s,b1)) | (proj1 p) = (Comput (P2,s,b1)) | (proj1 p)
A17: (Comput (P1,s,i)) | (dom p) = (Comput (P2,s,i)) | (dom p) by A14, A15, A1, EXTPRO_1:def_10;
take k = i + 1; ::_thesis: not (Comput (P1,s,k)) | (proj1 p) = (Comput (P2,s,k)) | (proj1 p)
set Cs1k = Comput (P1,s,k);
A18: IC in dom p by AMISTD_5:6;
IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom p)) by A18, FUNCT_1:49;
then IC (Comput (P1,s,i)) = IC (Comput (P,s,i)) by A16, A18, FUNCT_1:49;
then A19: CurInstr (P1,(Comput (P1,s,i))) = P1 . (IC (Comput (P,s,i))) by PBOOLE:143
.= (dl. 0) := (dl. 0) by A13, A7, FUNCT_4:13 ;
A20: Comput (P1,s,k) = Following (P1,(Comput (P1,s,i))) by EXTPRO_1:3
.= Exec (((dl. 0) := (dl. 0)),(Comput (P1,s,i))) by A19 ;
A21: IC (Exec (((dl. 0) := (dl. 0)),(Comput (P1,s,i)))) = succ (IC (Comput (P1,s,i))) by AMI_3:2;
A22: IC in dom p by AMISTD_5:6;
A23: IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom p)) by A22, FUNCT_1:49;
then A24: IC (Comput (P1,s,k)) = succ (IC (Comput (P,s,i))) by A20, A21, A16, A22, FUNCT_1:49
.= (IC (Comput (P,s,i))) + 1 by NAT_1:38 ;
set Cs2k = Comput (P2,s,k);
A25: Comput (P2,s,k) = Following (P2,(Comput (P2,s,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s,i)))),(Comput (P2,s,i))) ;
A26: P2 /. (IC (Comput (P2,s,i))) = P2 . (IC (Comput (P2,s,i))) by PBOOLE:143;
IC (Comput (P2,s,i)) = IC (Comput (P,s,i)) by A16, A23, A17, A22, FUNCT_1:49;
then A27: IC (Comput (P2,s,k)) = IC (Comput (P,s,i)) by A25, A12, A26, EXTPRO_1:def_3;
( IC ((Comput (P1,s,k)) | (dom p)) = IC (Comput (P1,s,k)) & IC ((Comput (P2,s,k)) | (dom p)) = IC (Comput (P2,s,k)) ) by A22, FUNCT_1:49;
hence not (Comput (P1,s,k)) | (proj1 p) = (Comput (P2,s,k)) | (proj1 p) by A24, A27; ::_thesis: verum
end;
hence contradiction ; ::_thesis: verum
end;
end;
theorem :: AMI_5:17
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db
proof
let q be NAT -defined the InstructionsF of SCM -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db
let p be non empty q -autonomic FinPartState of SCM; ::_thesis: for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db
let s1, s2 be State of SCM; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db
let P1, P2 be Instruction-Sequence of SCM; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db
let i be Element of NAT ; ::_thesis: for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db
let da, db be Data-Location; ::_thesis: for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da := db & da in dom p holds
(Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db
let I be Instruction of SCM; ::_thesis: ( I = CurInstr (P1,(Comput (P1,s1,i))) & I = da := db & da in dom p implies (Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db )
assume A3: I = CurInstr (P1,(Comput (P1,s1,i))) ; ::_thesis: ( not I = da := db or not da in dom p or (Comput (P1,s1,i)) . db = (Comput (P2,s2,i)) . db )
set Cs2i1 = Comput (P2,s2,(i + 1));
set Cs2i = Comput (P2,s2,i);
A4: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
assume that
A5: I = da := db and
A6: ( da in dom p & (Comput (P1,s1,i)) . db <> (Comput (P2,s2,i)) . db ) ; ::_thesis: contradiction
I = CurInstr (P2,(Comput (P2,s2,i))) by A3, A2, A1, AMISTD_5:7;
then A7: (Comput (P2,s2,(i + 1))) . da = (Comput (P2,s2,i)) . db by A4, A5, AMI_3:2;
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs1i = Comput (P1,s1,i);
A8: ( da in dom p implies ( ((Comput (P1,s1,(i + 1))) | (dom p)) . da = (Comput (P1,s1,(i + 1))) . da & ((Comput (P2,s2,(i + 1))) | (dom p)) . da = (Comput (P2,s2,(i + 1))) . da ) ) by FUNCT_1:49;
Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
then (Comput (P1,s1,(i + 1))) . da = (Comput (P1,s1,i)) . db by A3, A5, AMI_3:2;
hence contradiction by A8, A6, A7, A2, A1, EXTPRO_1:def_10; ::_thesis: verum
end;
theorem :: AMI_5:18
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db)
proof
let q be NAT -defined the InstructionsF of SCM -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db)
let p be non empty q -autonomic FinPartState of SCM; ::_thesis: for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db)
let s1, s2 be State of SCM; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db)
let P1, P2 be Instruction-Sequence of SCM; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db)
let i be Element of NAT ; ::_thesis: for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db)
let da, db be Data-Location; ::_thesis: for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = AddTo (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db)
let I be Instruction of SCM; ::_thesis: ( I = CurInstr (P1,(Comput (P1,s1,i))) & I = AddTo (da,db) & da in dom p implies ((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) )
assume A3: I = CurInstr (P1,(Comput (P1,s1,i))) ; ::_thesis: ( not I = AddTo (da,db) or not da in dom p or ((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) )
set Cs2i1 = Comput (P2,s2,(i + 1));
set Cs2i = Comput (P2,s2,i);
A4: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
assume that
A5: I = AddTo (da,db) and
A6: ( da in dom p & ((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) <> ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) ) ; ::_thesis: contradiction
I = CurInstr (P2,(Comput (P2,s2,i))) by A3, A2, A1, AMISTD_5:7;
then A7: (Comput (P2,s2,(i + 1))) . da = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) by A4, A5, AMI_3:3;
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs1i = Comput (P1,s1,i);
A8: ( da in dom p implies ( ((Comput (P1,s1,(i + 1))) | (dom p)) . da = (Comput (P1,s1,(i + 1))) . da & ((Comput (P2,s2,(i + 1))) | (dom p)) . da = (Comput (P2,s2,(i + 1))) . da ) ) by FUNCT_1:49;
Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
then (Comput (P1,s1,(i + 1))) . da = ((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) by A3, A5, AMI_3:3;
hence contradiction by A8, A6, A7, A2, A1, EXTPRO_1:def_10; ::_thesis: verum
end;
theorem :: AMI_5:19
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)
proof
let q be NAT -defined the InstructionsF of SCM -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)
let p be non empty q -autonomic FinPartState of SCM; ::_thesis: for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)
let s1, s2 be State of SCM; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)
let P1, P2 be Instruction-Sequence of SCM; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)
let i be Element of NAT ; ::_thesis: for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)
let da, db be Data-Location; ::_thesis: for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = SubFrom (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db)
let I be Instruction of SCM; ::_thesis: ( I = CurInstr (P1,(Comput (P1,s1,i))) & I = SubFrom (da,db) & da in dom p implies ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) )
assume A3: I = CurInstr (P1,(Comput (P1,s1,i))) ; ::_thesis: ( not I = SubFrom (da,db) or not da in dom p or ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) )
set Cs2i1 = Comput (P2,s2,(i + 1));
set Cs2i = Comput (P2,s2,i);
A4: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
assume that
A5: I = SubFrom (da,db) and
A6: ( da in dom p & ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) <> ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) ) ; ::_thesis: contradiction
I = CurInstr (P2,(Comput (P2,s2,i))) by A3, A2, A1, AMISTD_5:7;
then A7: (Comput (P2,s2,(i + 1))) . da = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) by A4, A5, AMI_3:4;
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs1i = Comput (P1,s1,i);
A8: ( da in dom p implies ( ((Comput (P1,s1,(i + 1))) | (dom p)) . da = (Comput (P1,s1,(i + 1))) . da & ((Comput (P2,s2,(i + 1))) | (dom p)) . da = (Comput (P2,s2,(i + 1))) . da ) ) by FUNCT_1:49;
Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
then (Comput (P1,s1,(i + 1))) . da = ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) by A3, A5, AMI_3:4;
hence contradiction by A8, A6, A7, A2, A1, EXTPRO_1:def_10; ::_thesis: verum
end;
theorem :: AMI_5:20
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db)
proof
let q be NAT -defined the InstructionsF of SCM -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db)
let p be non empty q -autonomic FinPartState of SCM; ::_thesis: for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db)
let s1, s2 be State of SCM; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db)
let P1, P2 be Instruction-Sequence of SCM; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db)
let i be Element of NAT ; ::_thesis: for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db)
let da, db be Data-Location; ::_thesis: for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = MultBy (da,db) & da in dom p holds
((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db)
let I be Instruction of SCM; ::_thesis: ( I = CurInstr (P1,(Comput (P1,s1,i))) & I = MultBy (da,db) & da in dom p implies ((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) )
assume A3: I = CurInstr (P1,(Comput (P1,s1,i))) ; ::_thesis: ( not I = MultBy (da,db) or not da in dom p or ((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) )
set Cs2i1 = Comput (P2,s2,(i + 1));
set Cs2i = Comput (P2,s2,i);
A4: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
assume that
A5: I = MultBy (da,db) and
A6: ( da in dom p & ((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) <> ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) ) ; ::_thesis: contradiction
I = CurInstr (P2,(Comput (P2,s2,i))) by A3, A2, A1, AMISTD_5:7;
then A7: (Comput (P2,s2,(i + 1))) . da = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) by A4, A5, AMI_3:5;
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs1i = Comput (P1,s1,i);
A8: ( da in dom p implies ( ((Comput (P1,s1,(i + 1))) | (dom p)) . da = (Comput (P1,s1,(i + 1))) . da & ((Comput (P2,s2,(i + 1))) | (dom p)) . da = (Comput (P2,s2,(i + 1))) . da ) ) by FUNCT_1:49;
Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
then (Comput (P1,s1,(i + 1))) . da = ((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) by A3, A5, AMI_3:5;
hence contradiction by A8, A6, A7, A2, A1, EXTPRO_1:def_10; ::_thesis: verum
end;
theorem :: AMI_5:21
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & da in dom p & da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db)
proof
let q be NAT -defined the InstructionsF of SCM -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & da in dom p & da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db)
let p be non empty q -autonomic FinPartState of SCM; ::_thesis: for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & da in dom p & da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db)
let s1, s2 be State of SCM; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & da in dom p & da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & da in dom p & da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db)
let P1, P2 be Instruction-Sequence of SCM; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & da in dom p & da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & da in dom p & da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db)
let i be Element of NAT ; ::_thesis: for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & da in dom p & da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db)
let da, db be Data-Location; ::_thesis: for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & da in dom p & da <> db holds
((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db)
let I be Instruction of SCM; ::_thesis: ( I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & da in dom p & da <> db implies ((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) )
assume A3: I = CurInstr (P1,(Comput (P1,s1,i))) ; ::_thesis: ( not I = Divide (da,db) or not da in dom p or not da <> db or ((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) )
set Cs2i1 = Comput (P2,s2,(i + 1));
set Cs2i = Comput (P2,s2,i);
A4: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
assume that
A5: I = Divide (da,db) and
A6: da in dom p and
A7: da <> db and
A8: ((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) <> ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) ; ::_thesis: contradiction
I = CurInstr (P2,(Comput (P2,s2,i))) by A3, A2, A1, AMISTD_5:7;
then A9: (Comput (P2,s2,(i + 1))) . da = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) by A4, A5, A7, AMI_3:6;
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs1i = Comput (P1,s1,i);
A10: ( da in dom p implies ( ((Comput (P1,s1,(i + 1))) | (dom p)) . da = (Comput (P1,s1,(i + 1))) . da & ((Comput (P2,s2,(i + 1))) | (dom p)) . da = (Comput (P2,s2,(i + 1))) . da ) ) by FUNCT_1:49;
Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
then (Comput (P1,s1,(i + 1))) . da = ((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) by A3, A5, A7, AMI_3:6;
hence contradiction by A10, A8, A9, A2, A6, A1, EXTPRO_1:def_10; ::_thesis: verum
end;
theorem :: AMI_5:22
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
proof
let q be NAT -defined the InstructionsF of SCM -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
let p be non empty q -autonomic FinPartState of SCM; ::_thesis: for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
let s1, s2 be State of SCM; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
let P1, P2 be Instruction-Sequence of SCM; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
let i be Element of NAT ; ::_thesis: for da, db being Data-Location
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
let da, db be Data-Location; ::_thesis: for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & db in dom p holds
((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db)
let I be Instruction of SCM; ::_thesis: ( I = CurInstr (P1,(Comput (P1,s1,i))) & I = Divide (da,db) & db in dom p implies ((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) )
assume A3: I = CurInstr (P1,(Comput (P1,s1,i))) ; ::_thesis: ( not I = Divide (da,db) or not db in dom p or ((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) )
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs1i = Comput (P1,s1,i);
set Cs2i1 = Comput (P2,s2,(i + 1));
set Cs2i = Comput (P2,s2,i);
A4: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
assume that
A5: I = Divide (da,db) and
A6: db in dom p and
A7: ((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) <> ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) ; ::_thesis: contradiction
A8: ( ((Comput (P1,s1,(i + 1))) | (dom p)) . db = (Comput (P1,s1,(i + 1))) . db & ((Comput (P2,s2,(i + 1))) | (dom p)) . db = (Comput (P2,s2,(i + 1))) . db ) by A6, FUNCT_1:49;
I = CurInstr (P2,(Comput (P2,s2,i))) by A3, A2, A1, AMISTD_5:7;
then A9: (Comput (P2,s2,(i + 1))) . db = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A4, A5, AMI_3:6;
Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
then (Comput (P1,s1,(i + 1))) . db = ((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) by A3, A5, AMI_3:6;
hence contradiction by A7, A8, A9, A2, A1, EXTPRO_1:def_10; ::_thesis: verum
end;
theorem :: AMI_5:23
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Data-Location
for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )
proof
let q be NAT -defined the InstructionsF of SCM -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Data-Location
for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )
let p be non empty q -autonomic FinPartState of SCM; ::_thesis: for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Data-Location
for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )
let s1, s2 be State of SCM; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Data-Location
for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 ) )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Data-Location
for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )
let P1, P2 be Instruction-Sequence of SCM; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da being Data-Location
for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 ) )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da being Data-Location
for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )
let i be Element of NAT ; ::_thesis: for da being Data-Location
for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )
let da be Data-Location; ::_thesis: for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )
let loc be Element of NAT ; ::_thesis: for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )
let I be Instruction of SCM; ::_thesis: ( I = CurInstr (P1,(Comput (P1,s1,i))) & I = da =0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) implies ( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 ) )
assume A3: I = CurInstr (P1,(Comput (P1,s1,i))) ; ::_thesis: ( not I = da =0_goto loc or not loc <> succ (IC (Comput (P1,s1,i))) or ( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 ) )
set Cs2i1 = Comput (P2,s2,(i + 1));
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs2i = Comput (P2,s2,i);
set Cs1i = Comput (P1,s1,i);
A4: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
A5: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
IC in dom p by AMISTD_5:6;
then A6: ( ((Comput (P1,s1,(i + 1))) | (dom p)) . (IC ) = IC (Comput (P1,s1,(i + 1))) & ((Comput (P2,s2,(i + 1))) | (dom p)) . (IC ) = IC (Comput (P2,s2,(i + 1))) ) by FUNCT_1:49;
assume that
A7: I = da =0_goto loc and
A8: loc <> succ (IC (Comput (P1,s1,i))) ; ::_thesis: ( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 )
A9: I = CurInstr (P2,(Comput (P2,s2,i))) by A3, A2, A1, AMISTD_5:7;
A10: now__::_thesis:_(_(Comput_(P2,s2,i))_._da_=_0_implies_not_(Comput_(P1,s1,i))_._da_<>_0_)
assume ( (Comput (P2,s2,i)) . da = 0 & (Comput (P1,s1,i)) . da <> 0 ) ; ::_thesis: contradiction
then ( (Comput (P2,s2,(i + 1))) . (IC ) = loc & (Comput (P1,s1,(i + 1))) . (IC ) = succ (IC (Comput (P1,s1,i))) ) by A3, A9, A4, A5, A7, AMI_3:8;
hence contradiction by A6, A8, A2, A1, EXTPRO_1:def_10; ::_thesis: verum
end;
A11: (Comput (P1,s1,(i + 1))) | (dom p) = (Comput (P2,s2,(i + 1))) | (dom p) by A2, A1, EXTPRO_1:def_10;
now__::_thesis:_(_(Comput_(P1,s1,i))_._da_=_0_implies_not_(Comput_(P2,s2,i))_._da_<>_0_)
assume ( (Comput (P1,s1,i)) . da = 0 & (Comput (P2,s2,i)) . da <> 0 ) ; ::_thesis: contradiction
then ( (Comput (P1,s1,(i + 1))) . (IC ) = loc & (Comput (P2,s2,(i + 1))) . (IC ) = succ (IC (Comput (P2,s2,i))) ) by A3, A9, A4, A5, A7, AMI_3:8;
hence contradiction by A6, A11, A8, A2, A1, AMISTD_5:7; ::_thesis: verum
end;
hence ( (Comput (P1,s1,i)) . da = 0 iff (Comput (P2,s2,i)) . da = 0 ) by A10; ::_thesis: verum
end;
theorem :: AMI_5:24
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Data-Location
for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )
proof
let q be NAT -defined the InstructionsF of SCM -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Data-Location
for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )
let p be non empty q -autonomic FinPartState of SCM; ::_thesis: for s1, s2 being State of SCM st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Data-Location
for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )
let s1, s2 be State of SCM; ::_thesis: ( p c= s1 & p c= s2 implies for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Data-Location
for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 ) )
assume A1: ( p c= s1 & p c= s2 ) ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM st q c= P1 & q c= P2 holds
for i being Element of NAT
for da being Data-Location
for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )
let P1, P2 be Instruction-Sequence of SCM; ::_thesis: ( q c= P1 & q c= P2 implies for i being Element of NAT
for da being Data-Location
for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 ) )
assume A2: ( q c= P1 & q c= P2 ) ; ::_thesis: for i being Element of NAT
for da being Data-Location
for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )
let i be Element of NAT ; ::_thesis: for da being Data-Location
for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )
let da be Data-Location; ::_thesis: for loc being Element of NAT
for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )
let loc be Element of NAT ; ::_thesis: for I being Instruction of SCM st I = CurInstr (P1,(Comput (P1,s1,i))) & I = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) holds
( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )
let I be Instruction of SCM; ::_thesis: ( I = CurInstr (P1,(Comput (P1,s1,i))) & I = da >0_goto loc & loc <> succ (IC (Comput (P1,s1,i))) implies ( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 ) )
assume A3: I = CurInstr (P1,(Comput (P1,s1,i))) ; ::_thesis: ( not I = da >0_goto loc or not loc <> succ (IC (Comput (P1,s1,i))) or ( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 ) )
set Cs2i1 = Comput (P2,s2,(i + 1));
set Cs1i1 = Comput (P1,s1,(i + 1));
A4: (Comput (P1,s1,(i + 1))) | (dom p) = (Comput (P2,s2,(i + 1))) | (dom p) by A2, A1, EXTPRO_1:def_10;
set Cs2i = Comput (P2,s2,i);
set Cs1i = Comput (P1,s1,i);
A5: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
IC in dom p by AMISTD_5:6;
then A6: ( ((Comput (P1,s1,(i + 1))) | (dom p)) . (IC ) = IC (Comput (P1,s1,(i + 1))) & ((Comput (P2,s2,(i + 1))) | (dom p)) . (IC ) = IC (Comput (P2,s2,(i + 1))) ) by FUNCT_1:49;
A7: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
assume that
A8: I = da >0_goto loc and
A9: loc <> succ (IC (Comput (P1,s1,i))) ; ::_thesis: ( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 )
A10: I = CurInstr (P2,(Comput (P2,s2,i))) by A3, A2, A1, AMISTD_5:7;
A11: now__::_thesis:_(_(Comput_(P2,s2,i))_._da_>_0_implies_not_(Comput_(P1,s1,i))_._da_<=_0_)
assume that
A12: (Comput (P2,s2,i)) . da > 0 and
A13: (Comput (P1,s1,i)) . da <= 0 ; ::_thesis: contradiction
(Comput (P2,s2,(i + 1))) . (IC ) = loc by A10, A7, A8, A12, AMI_3:9;
hence contradiction by A3, A5, A6, A4, A8, A9, A13, AMI_3:9; ::_thesis: verum
end;
A14: IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) by A2, A1, AMISTD_5:7;
now__::_thesis:_(_(Comput_(P1,s1,i))_._da_>_0_implies_not_(Comput_(P2,s2,i))_._da_<=_0_)
assume that
A15: (Comput (P1,s1,i)) . da > 0 and
A16: (Comput (P2,s2,i)) . da <= 0 ; ::_thesis: contradiction
(Comput (P1,s1,(i + 1))) . (IC ) = loc by A3, A5, A8, A15, AMI_3:9;
hence contradiction by A14, A10, A7, A6, A4, A8, A9, A16, AMI_3:9; ::_thesis: verum
end;
hence ( (Comput (P1,s1,i)) . da > 0 iff (Comput (P2,s2,i)) . da > 0 ) by A11; ::_thesis: verum
end;
theorem :: AMI_5:25
for s1, s2 being State of SCM st IC s1 = IC s2 & ( for a being Data-Location holds s1 . a = s2 . a ) holds
s1 = s2
proof
let s1, s2 be State of SCM; ::_thesis: ( IC s1 = IC s2 & ( for a being Data-Location holds s1 . a = s2 . a ) implies s1 = s2 )
assume A1: IC s1 = IC s2 ; ::_thesis: ( ex a being Data-Location st not s1 . a = s2 . a or s1 = s2 )
( IC in dom s1 & IC in dom s2 ) by MEMSTR_0:2;
then A2: ( s1 = (DataPart s1) +* (Start-At ((IC s1),SCM)) & s2 = (DataPart s2) +* (Start-At ((IC s2),SCM)) ) by MEMSTR_0:26;
assume A3: for a being Data-Location holds s1 . a = s2 . a ; ::_thesis: s1 = s2
DataPart s1 = DataPart s2
proof
A4: dom (DataPart s1) = Data-Locations by MEMSTR_0:9;
hence dom (DataPart s1) = dom (DataPart s2) by MEMSTR_0:9; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds
( not b1 in proj1 (DataPart s1) or (DataPart s1) . b1 = (DataPart s2) . b1 )
let x be set ; ::_thesis: ( not x in proj1 (DataPart s1) or (DataPart s1) . x = (DataPart s2) . x )
assume A5: x in dom (DataPart s1) ; ::_thesis: (DataPart s1) . x = (DataPart s2) . x
then A6: x is Data-Location by A4, AMI_2:def_16, AMI_3:27;
thus (DataPart s1) . x = s1 . x by A5, A4, FUNCT_1:49
.= s2 . x by A6, A3
.= (DataPart s2) . x by A5, A4, FUNCT_1:49 ; ::_thesis: verum
end;
hence s1 = s2 by A1, A2; ::_thesis: verum
end;