:: 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;