:: AMI_6 semantic presentation begin theorem :: AMI_6:1 for T being InsType of the InstructionsF of SCM holds ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 ) proof let T be InsType of the InstructionsF of SCM; ::_thesis: ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 ) consider y being set such that A1: [T,y] in proj1 the InstructionsF of SCM by XTUPLE_0:def_12; consider x being set such that A2: [[T,y],x] in the InstructionsF of SCM by A1, XTUPLE_0:def_12; reconsider I = [T,y,x] as Instruction of SCM by A2; T = InsCode I by RECDEF_2:def_1; hence ( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 or T = 8 ) by AMI_5:5, NAT_1:32; ::_thesis: verum end; theorem Th2: :: AMI_6:2 JumpPart (halt SCM) = {} ; theorem :: AMI_6:3 for T being InsType of the InstructionsF of SCM st T = 0 holds JumpParts T = {0} proof let T be InsType of the InstructionsF of SCM; ::_thesis: ( T = 0 implies JumpParts T = {0} ) assume A1: T = 0 ; ::_thesis: JumpParts T = {0} hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {0} c= JumpParts T let a be set ; ::_thesis: ( a in JumpParts T implies a in {0} ) assume a in JumpParts T ; ::_thesis: a in {0} then consider I being Instruction of SCM such that A2: a = JumpPart I and A3: InsCode I = T ; I = halt SCM by A1, A3, AMI_5:7; hence a in {0} by A2, Th2, TARSKI:def_1; ::_thesis: verum end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {0} or a in JumpParts T ) assume a in {0} ; ::_thesis: a in JumpParts T then A: a = 0 by TARSKI:def_1; InsCode (halt SCM) = 0 by COMPOS_1:70; hence a in JumpParts T by A1, Th2, A; ::_thesis: verum end; theorem :: AMI_6:4 for T being InsType of the InstructionsF of SCM st T = 1 holds JumpParts T = {{}} proof let T be InsType of the InstructionsF of SCM; ::_thesis: ( T = 1 implies JumpParts T = {{}} ) assume A1: T = 1 ; ::_thesis: JumpParts T = {{}} hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {{}} c= JumpParts T let x be set ; ::_thesis: ( x in JumpParts T implies x in {{}} ) assume x in JumpParts T ; ::_thesis: x in {{}} then consider I being Instruction of SCM such that A2: x = JumpPart I and A3: InsCode I = T ; consider a, b being Data-Location such that A4: I = a := b by A1, A3, AMI_5:8; x = {} by A2, A4, RECDEF_2:def_2; hence x in {{}} by TARSKI:def_1; ::_thesis: verum end; set a = the Data-Location; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in JumpParts T ) assume x in {{}} ; ::_thesis: x in JumpParts T then x = {} by TARSKI:def_1; then A5: x = JumpPart ( the Data-Location := the Data-Location) by RECDEF_2:def_2; InsCode ( the Data-Location := the Data-Location) = 1 by RECDEF_2:def_1; hence x in JumpParts T by A5, A1; ::_thesis: verum end; theorem :: AMI_6:5 for T being InsType of the InstructionsF of SCM st T = 2 holds JumpParts T = {{}} proof let T be InsType of the InstructionsF of SCM; ::_thesis: ( T = 2 implies JumpParts T = {{}} ) assume A1: T = 2 ; ::_thesis: JumpParts T = {{}} hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {{}} c= JumpParts T let x be set ; ::_thesis: ( x in JumpParts T implies x in {{}} ) assume x in JumpParts T ; ::_thesis: x in {{}} then consider I being Instruction of SCM such that A2: x = JumpPart I and A3: InsCode I = T ; consider a, b being Data-Location such that A4: I = AddTo (a,b) by A1, A3, AMI_5:9; x = {} by A2, A4, RECDEF_2:def_2; hence x in {{}} by TARSKI:def_1; ::_thesis: verum end; set a = the Data-Location; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in JumpParts T ) assume x in {{}} ; ::_thesis: x in JumpParts T then x = {} by TARSKI:def_1; then A5: x = JumpPart (AddTo ( the Data-Location, the Data-Location)) by RECDEF_2:def_2; InsCode (AddTo ( the Data-Location, the Data-Location)) = 2 by RECDEF_2:def_1; hence x in JumpParts T by A5, A1; ::_thesis: verum end; theorem :: AMI_6:6 for T being InsType of the InstructionsF of SCM st T = 3 holds JumpParts T = {{}} proof let T be InsType of the InstructionsF of SCM; ::_thesis: ( T = 3 implies JumpParts T = {{}} ) assume A1: T = 3 ; ::_thesis: JumpParts T = {{}} hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {{}} c= JumpParts T let x be set ; ::_thesis: ( x in JumpParts T implies x in {{}} ) assume x in JumpParts T ; ::_thesis: x in {{}} then consider I being Instruction of SCM such that A2: x = JumpPart I and A3: InsCode I = T ; consider a, b being Data-Location such that A4: I = SubFrom (a,b) by A1, A3, AMI_5:10; x = {} by A2, A4, RECDEF_2:def_2; hence x in {{}} by TARSKI:def_1; ::_thesis: verum end; set a = the Data-Location; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in JumpParts T ) assume x in {{}} ; ::_thesis: x in JumpParts T then x = {} by TARSKI:def_1; then A5: x = JumpPart (SubFrom ( the Data-Location, the Data-Location)) by RECDEF_2:def_2; InsCode (SubFrom ( the Data-Location, the Data-Location)) = 3 by RECDEF_2:def_1; hence x in JumpParts T by A5, A1; ::_thesis: verum end; theorem :: AMI_6:7 for T being InsType of the InstructionsF of SCM st T = 4 holds JumpParts T = {{}} proof let T be InsType of the InstructionsF of SCM; ::_thesis: ( T = 4 implies JumpParts T = {{}} ) assume A1: T = 4 ; ::_thesis: JumpParts T = {{}} hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {{}} c= JumpParts T let x be set ; ::_thesis: ( x in JumpParts T implies x in {{}} ) assume x in JumpParts T ; ::_thesis: x in {{}} then consider I being Instruction of SCM such that A2: x = JumpPart I and A3: InsCode I = T ; consider a, b being Data-Location such that A4: I = MultBy (a,b) by A1, A3, AMI_5:11; x = {} by A2, A4, RECDEF_2:def_2; hence x in {{}} by TARSKI:def_1; ::_thesis: verum end; set a = the Data-Location; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in JumpParts T ) assume x in {{}} ; ::_thesis: x in JumpParts T then x = {} by TARSKI:def_1; then A5: x = JumpPart (MultBy ( the Data-Location, the Data-Location)) by RECDEF_2:def_2; InsCode (MultBy ( the Data-Location, the Data-Location)) = 4 by RECDEF_2:def_1; hence x in JumpParts T by A5, A1; ::_thesis: verum end; theorem :: AMI_6:8 for T being InsType of the InstructionsF of SCM st T = 5 holds JumpParts T = {{}} proof let T be InsType of the InstructionsF of SCM; ::_thesis: ( T = 5 implies JumpParts T = {{}} ) assume A1: T = 5 ; ::_thesis: JumpParts T = {{}} hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {{}} c= JumpParts T let x be set ; ::_thesis: ( x in JumpParts T implies x in {{}} ) assume x in JumpParts T ; ::_thesis: x in {{}} then consider I being Instruction of SCM such that A2: x = JumpPart I and A3: InsCode I = T ; consider a, b being Data-Location such that A4: I = Divide (a,b) by A1, A3, AMI_5:12; x = {} by A2, A4, RECDEF_2:def_2; hence x in {{}} by TARSKI:def_1; ::_thesis: verum end; set a = the Data-Location; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{}} or x in JumpParts T ) assume x in {{}} ; ::_thesis: x in JumpParts T then x = {} by TARSKI:def_1; then A5: x = JumpPart (Divide ( the Data-Location, the Data-Location)) by RECDEF_2:def_2; InsCode (Divide ( the Data-Location, the Data-Location)) = 5 by RECDEF_2:def_1; hence x in JumpParts T by A5, A1; ::_thesis: verum end; theorem Th9: :: AMI_6:9 for T being InsType of the InstructionsF of SCM st T = 6 holds dom (product" (JumpParts T)) = {1} proof let T be InsType of the InstructionsF of SCM; ::_thesis: ( T = 6 implies dom (product" (JumpParts T)) = {1} ) set i1 = the Element of NAT ; assume A1: T = 6 ; ::_thesis: dom (product" (JumpParts T)) = {1} A2: JumpPart (SCM-goto the Element of NAT ) = <* the Element of NAT *> by RECDEF_2:def_2; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {1} c= dom (product" (JumpParts T)) let x be set ; ::_thesis: ( x in dom (product" (JumpParts T)) implies x in {1} ) InsCode (SCM-goto the Element of NAT ) = 6 by RECDEF_2:def_1; then A3: JumpPart (SCM-goto the Element of NAT ) in JumpParts T by A1; assume x in dom (product" (JumpParts T)) ; ::_thesis: x in {1} then x in DOM (JumpParts T) by CARD_3:def_12; then x in dom (JumpPart (SCM-goto the Element of NAT )) by A3, CARD_3:108; hence x in {1} by A2, FINSEQ_1:2, FINSEQ_1:def_8; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {1} or x in dom (product" (JumpParts T)) ) assume A4: x in {1} ; ::_thesis: x in dom (product" (JumpParts T)) for f being Function st f in JumpParts T holds x in dom f proof let f be Function; ::_thesis: ( f in JumpParts T implies x in dom f ) assume f in JumpParts T ; ::_thesis: x in dom f then consider I being Instruction of SCM such that A5: f = JumpPart I and A6: InsCode I = T ; consider i1 being Element of NAT such that A7: I = SCM-goto i1 by A1, A6, AMI_5:13; f = <*i1*> by A5, A7, RECDEF_2:def_2; hence x in dom f by A4, FINSEQ_1:2, FINSEQ_1:def_8; ::_thesis: verum end; then x in DOM (JumpParts T) by CARD_3:109; hence x in dom (product" (JumpParts T)) by CARD_3:def_12; ::_thesis: verum end; theorem Th10: :: AMI_6:10 for T being InsType of the InstructionsF of SCM st T = 7 holds dom (product" (JumpParts T)) = {1} proof let T be InsType of the InstructionsF of SCM; ::_thesis: ( T = 7 implies dom (product" (JumpParts T)) = {1} ) set i1 = the Element of NAT ; set a = the Data-Location; assume A1: T = 7 ; ::_thesis: dom (product" (JumpParts T)) = {1} A2: JumpPart ( the Data-Location =0_goto the Element of NAT ) = <* the Element of NAT *> by RECDEF_2:def_2; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {1} c= dom (product" (JumpParts T)) let x be set ; ::_thesis: ( x in dom (product" (JumpParts T)) implies x in {1} ) InsCode ( the Data-Location =0_goto the Element of NAT ) = 7 by RECDEF_2:def_1; then A3: JumpPart ( the Data-Location =0_goto the Element of NAT ) in JumpParts T by A1; assume x in dom (product" (JumpParts T)) ; ::_thesis: x in {1} then x in DOM (JumpParts T) by CARD_3:def_12; then x in dom (JumpPart ( the Data-Location =0_goto the Element of NAT )) by A3, CARD_3:108; hence x in {1} by A2, FINSEQ_1:2, FINSEQ_1:38; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {1} or x in dom (product" (JumpParts T)) ) assume A4: x in {1} ; ::_thesis: x in dom (product" (JumpParts T)) for f being Function st f in JumpParts T holds x in dom f proof let f be Function; ::_thesis: ( f in JumpParts T implies x in dom f ) assume f in JumpParts T ; ::_thesis: x in dom f then consider I being Instruction of SCM such that A5: f = JumpPart I and A6: InsCode I = T ; consider i1 being Element of NAT , a being Data-Location such that A7: I = a =0_goto i1 by A1, A6, AMI_5:14; f = <*i1*> by A5, A7, RECDEF_2:def_2; hence x in dom f by A4, FINSEQ_1:2, FINSEQ_1:38; ::_thesis: verum end; then x in DOM (JumpParts T) by CARD_3:109; hence x in dom (product" (JumpParts T)) by CARD_3:def_12; ::_thesis: verum end; theorem Th11: :: AMI_6:11 for T being InsType of the InstructionsF of SCM st T = 8 holds dom (product" (JumpParts T)) = {1} proof let T be InsType of the InstructionsF of SCM; ::_thesis: ( T = 8 implies dom (product" (JumpParts T)) = {1} ) set i1 = the Element of NAT ; set a = the Data-Location; assume A1: T = 8 ; ::_thesis: dom (product" (JumpParts T)) = {1} A2: JumpPart ( the Data-Location >0_goto the Element of NAT ) = <* the Element of NAT *> by RECDEF_2:def_2; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {1} c= dom (product" (JumpParts T)) let x be set ; ::_thesis: ( x in dom (product" (JumpParts T)) implies x in {1} ) InsCode ( the Data-Location >0_goto the Element of NAT ) = 8 by RECDEF_2:def_1; then A3: JumpPart ( the Data-Location >0_goto the Element of NAT ) in JumpParts T by A1; assume x in dom (product" (JumpParts T)) ; ::_thesis: x in {1} then x in DOM (JumpParts T) by CARD_3:def_12; then x in dom (JumpPart ( the Data-Location >0_goto the Element of NAT )) by A3, CARD_3:108; hence x in {1} by A2, FINSEQ_1:2, FINSEQ_1:38; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {1} or x in dom (product" (JumpParts T)) ) assume A4: x in {1} ; ::_thesis: x in dom (product" (JumpParts T)) for f being Function st f in JumpParts T holds x in dom f proof let f be Function; ::_thesis: ( f in JumpParts T implies x in dom f ) assume f in JumpParts T ; ::_thesis: x in dom f then consider I being Instruction of SCM such that A5: f = JumpPart I and A6: InsCode I = T ; consider i1 being Element of NAT , a being Data-Location such that A7: I = a >0_goto i1 by A1, A6, AMI_5:15; f = <*i1*> by A5, A7, RECDEF_2:def_2; hence x in dom f by A4, FINSEQ_1:2, FINSEQ_1:38; ::_thesis: verum end; then x in DOM (JumpParts T) by CARD_3:109; hence x in dom (product" (JumpParts T)) by CARD_3:def_12; ::_thesis: verum end; theorem :: AMI_6:12 for k1 being Nat holds (product" (JumpParts (InsCode (SCM-goto k1)))) . 1 = NAT proof let k1 be Nat; ::_thesis: (product" (JumpParts (InsCode (SCM-goto k1)))) . 1 = NAT InsCode (SCM-goto k1) = 6 by RECDEF_2:def_1; then dom (product" (JumpParts (InsCode (SCM-goto k1)))) = {1} by Th9; then A1: 1 in dom (product" (JumpParts (InsCode (SCM-goto k1)))) by TARSKI:def_1; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: NAT c= (product" (JumpParts (InsCode (SCM-goto k1)))) . 1 let x be set ; ::_thesis: ( x in (product" (JumpParts (InsCode (SCM-goto k1)))) . 1 implies x in NAT ) assume x in (product" (JumpParts (InsCode (SCM-goto k1)))) . 1 ; ::_thesis: x in NAT then x in pi ((JumpParts (InsCode (SCM-goto k1))),1) by A1, CARD_3:def_12; then consider g being Function such that A2: g in JumpParts (InsCode (SCM-goto k1)) and A3: x = g . 1 by CARD_3:def_6; consider I being Instruction of SCM such that A4: g = JumpPart I and A5: InsCode I = InsCode (SCM-goto k1) by A2; InsCode I = 6 by A5, RECDEF_2:def_1; then consider i2 being Element of NAT such that A6: I = SCM-goto i2 by AMI_5:13; g = <*i2*> by A4, A6, RECDEF_2:def_2; then x = i2 by A3, FINSEQ_1:def_8; hence x in NAT ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NAT or x in (product" (JumpParts (InsCode (SCM-goto k1)))) . 1 ) assume x in NAT ; ::_thesis: x in (product" (JumpParts (InsCode (SCM-goto k1)))) . 1 then reconsider x = x as Element of NAT ; InsCode (SCM-goto k1) = 6 by RECDEF_2:def_1; then ( JumpPart (SCM-goto x) = <*x*> & InsCode (SCM-goto k1) = InsCode (SCM-goto x) ) by RECDEF_2:def_1, RECDEF_2:def_2; then A7: <*x*> in JumpParts (InsCode (SCM-goto k1)) ; <*x*> . 1 = x by FINSEQ_1:def_8; then x in pi ((JumpParts (InsCode (SCM-goto k1))),1) by A7, CARD_3:def_6; hence x in (product" (JumpParts (InsCode (SCM-goto k1)))) . 1 by A1, CARD_3:def_12; ::_thesis: verum end; theorem :: AMI_6:13 for a being Data-Location for k1 being Nat holds (product" (JumpParts (InsCode (a =0_goto k1)))) . 1 = NAT proof let a be Data-Location; ::_thesis: for k1 being Nat holds (product" (JumpParts (InsCode (a =0_goto k1)))) . 1 = NAT let k1 be Nat; ::_thesis: (product" (JumpParts (InsCode (a =0_goto k1)))) . 1 = NAT InsCode (a =0_goto k1) = 7 by RECDEF_2:def_1; then dom (product" (JumpParts (InsCode (a =0_goto k1)))) = {1} by Th10; then A1: 1 in dom (product" (JumpParts (InsCode (a =0_goto k1)))) by TARSKI:def_1; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: NAT c= (product" (JumpParts (InsCode (a =0_goto k1)))) . 1 let x be set ; ::_thesis: ( x in (product" (JumpParts (InsCode (a =0_goto k1)))) . 1 implies x in NAT ) assume x in (product" (JumpParts (InsCode (a =0_goto k1)))) . 1 ; ::_thesis: x in NAT then x in pi ((JumpParts (InsCode (a =0_goto k1))),1) by A1, CARD_3:def_12; then consider g being Function such that A2: g in JumpParts (InsCode (a =0_goto k1)) and A3: x = g . 1 by CARD_3:def_6; consider I being Instruction of SCM such that A4: g = JumpPart I and A5: InsCode I = InsCode (a =0_goto k1) by A2; InsCode I = 7 by A5, RECDEF_2:def_1; then consider i2 being Element of NAT , b being Data-Location such that A6: I = b =0_goto i2 by AMI_5:14; g = <*i2*> by A4, A6, RECDEF_2:def_2; then x = i2 by A3, FINSEQ_1:40; hence x in NAT ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NAT or x in (product" (JumpParts (InsCode (a =0_goto k1)))) . 1 ) assume x in NAT ; ::_thesis: x in (product" (JumpParts (InsCode (a =0_goto k1)))) . 1 then reconsider x = x as Element of NAT ; InsCode (a =0_goto k1) = 7 by RECDEF_2:def_1; then ( JumpPart (a =0_goto x) = <*x*> & InsCode (a =0_goto k1) = InsCode (a =0_goto x) ) by RECDEF_2:def_1, RECDEF_2:def_2; then A7: <*x*> in JumpParts (InsCode (a =0_goto k1)) ; <*x*> . 1 = x by FINSEQ_1:40; then x in pi ((JumpParts (InsCode (a =0_goto k1))),1) by A7, CARD_3:def_6; hence x in (product" (JumpParts (InsCode (a =0_goto k1)))) . 1 by A1, CARD_3:def_12; ::_thesis: verum end; theorem :: AMI_6:14 for a being Data-Location for k1 being Nat holds (product" (JumpParts (InsCode (a >0_goto k1)))) . 1 = NAT proof let a be Data-Location; ::_thesis: for k1 being Nat holds (product" (JumpParts (InsCode (a >0_goto k1)))) . 1 = NAT let k1 be Nat; ::_thesis: (product" (JumpParts (InsCode (a >0_goto k1)))) . 1 = NAT InsCode (a >0_goto k1) = 8 by RECDEF_2:def_1; then dom (product" (JumpParts (InsCode (a >0_goto k1)))) = {1} by Th11; then A1: 1 in dom (product" (JumpParts (InsCode (a >0_goto k1)))) by TARSKI:def_1; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: NAT c= (product" (JumpParts (InsCode (a >0_goto k1)))) . 1 let x be set ; ::_thesis: ( x in (product" (JumpParts (InsCode (a >0_goto k1)))) . 1 implies x in NAT ) assume x in (product" (JumpParts (InsCode (a >0_goto k1)))) . 1 ; ::_thesis: x in NAT then x in pi ((JumpParts (InsCode (a >0_goto k1))),1) by A1, CARD_3:def_12; then consider g being Function such that A2: g in JumpParts (InsCode (a >0_goto k1)) and A3: x = g . 1 by CARD_3:def_6; consider I being Instruction of SCM such that A4: g = JumpPart I and A5: InsCode I = InsCode (a >0_goto k1) by A2; InsCode I = 8 by A5, RECDEF_2:def_1; then consider i2 being Element of NAT , b being Data-Location such that A6: I = b >0_goto i2 by AMI_5:15; g = <*i2*> by A4, A6, RECDEF_2:def_2; then x = i2 by A3, FINSEQ_1:40; hence x in NAT ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in NAT or x in (product" (JumpParts (InsCode (a >0_goto k1)))) . 1 ) assume x in NAT ; ::_thesis: x in (product" (JumpParts (InsCode (a >0_goto k1)))) . 1 then reconsider x = x as Element of NAT ; InsCode (a >0_goto k1) = 8 by RECDEF_2:def_1; then ( JumpPart (a >0_goto x) = <*x*> & InsCode (a >0_goto k1) = InsCode (a >0_goto x) ) by RECDEF_2:def_1, RECDEF_2:def_2; then A7: <*x*> in JumpParts (InsCode (a >0_goto k1)) ; <*x*> . 1 = x by FINSEQ_1:40; then x in pi ((JumpParts (InsCode (a >0_goto k1))),1) by A7, CARD_3:def_6; hence x in (product" (JumpParts (InsCode (a >0_goto k1)))) . 1 by A1, CARD_3:def_12; ::_thesis: verum end; Lm1: for i being Instruction of SCM st ( for l being Element of NAT holds NIC (i,l) = {(succ l)} ) holds JUMP i is empty proof set p = 1; set q = 2; let i be Instruction of SCM; ::_thesis: ( ( for l being Element of NAT holds NIC (i,l) = {(succ l)} ) implies JUMP i is empty ) assume A1: for l being Element of NAT holds NIC (i,l) = {(succ l)} ; ::_thesis: JUMP i is empty set X = { (NIC (i,f)) where f is Element of NAT : verum } ; reconsider p = 1, q = 2 as Element of NAT ; assume not JUMP i is empty ; ::_thesis: contradiction then consider x being set such that A2: x in meet { (NIC (i,f)) where f is Element of NAT : verum } by XBOOLE_0:def_1; NIC (i,p) = {(succ p)} by A1; then {(succ p)} in { (NIC (i,f)) where f is Element of NAT : verum } ; then x in {(succ p)} by A2, SETFAM_1:def_1; then A3: x = succ p by TARSKI:def_1; NIC (i,q) = {(succ q)} by A1; then {(succ q)} in { (NIC (i,f)) where f is Element of NAT : verum } ; then x in {(succ q)} by A2, SETFAM_1:def_1; hence contradiction by A3, TARSKI:def_1; ::_thesis: verum end; registration cluster JUMP (halt SCM) -> empty ; coherence JUMP (halt SCM) is empty ; end; registration let a, b be Data-Location; clustera := b -> sequential ; coherence a := b is sequential proof let s be State of SCM; :: according to AMISTD_1:def_8 ::_thesis: (Exec ((a := b),s)) . (IC ) = succ (IC s) thus (Exec ((a := b),s)) . (IC ) = succ (IC s) by AMI_3:2; ::_thesis: verum end; cluster AddTo (a,b) -> sequential ; coherence AddTo (a,b) is sequential proof let s be State of SCM; :: according to AMISTD_1:def_8 ::_thesis: (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s) thus (Exec ((AddTo (a,b)),s)) . (IC ) = succ (IC s) by AMI_3:3; ::_thesis: verum end; cluster SubFrom (a,b) -> sequential ; coherence SubFrom (a,b) is sequential proof let s be State of SCM; :: according to AMISTD_1:def_8 ::_thesis: (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s) thus (Exec ((SubFrom (a,b)),s)) . (IC ) = succ (IC s) by AMI_3:4; ::_thesis: verum end; cluster MultBy (a,b) -> sequential ; coherence MultBy (a,b) is sequential proof let s be State of SCM; :: according to AMISTD_1:def_8 ::_thesis: (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) thus (Exec ((MultBy (a,b)),s)) . (IC ) = succ (IC s) by AMI_3:5; ::_thesis: verum end; cluster Divide (a,b) -> sequential ; coherence Divide (a,b) is sequential proof let s be State of SCM; :: according to AMISTD_1:def_8 ::_thesis: (Exec ((Divide (a,b)),s)) . (IC ) = succ (IC s) thus (Exec ((Divide (a,b)),s)) . (IC ) = succ (IC s) by AMI_3:6; ::_thesis: verum end; end; registration let a, b be Data-Location; cluster JUMP (a := b) -> empty ; coherence JUMP (a := b) is empty proof for l being Element of NAT holds NIC ((a := b),l) = {(succ l)} by AMISTD_1:12; hence JUMP (a := b) is empty by Lm1; ::_thesis: verum end; end; registration let a, b be Data-Location; cluster JUMP (AddTo (a,b)) -> empty ; coherence JUMP (AddTo (a,b)) is empty proof for l being Element of NAT holds NIC ((AddTo (a,b)),l) = {(succ l)} by AMISTD_1:12; hence JUMP (AddTo (a,b)) is empty by Lm1; ::_thesis: verum end; end; registration let a, b be Data-Location; cluster JUMP (SubFrom (a,b)) -> empty ; coherence JUMP (SubFrom (a,b)) is empty proof for l being Element of NAT holds NIC ((SubFrom (a,b)),l) = {(succ l)} by AMISTD_1:12; hence JUMP (SubFrom (a,b)) is empty by Lm1; ::_thesis: verum end; end; registration let a, b be Data-Location; cluster JUMP (MultBy (a,b)) -> empty ; coherence JUMP (MultBy (a,b)) is empty proof for l being Element of NAT holds NIC ((MultBy (a,b)),l) = {(succ l)} by AMISTD_1:12; hence JUMP (MultBy (a,b)) is empty by Lm1; ::_thesis: verum end; end; registration let a, b be Data-Location; cluster JUMP (Divide (a,b)) -> empty ; coherence JUMP (Divide (a,b)) is empty proof for l being Element of NAT holds NIC ((Divide (a,b)),l) = {(succ l)} by AMISTD_1:12; hence JUMP (Divide (a,b)) is empty by Lm1; ::_thesis: verum end; end; theorem Th15: :: AMI_6:15 for il being Element of NAT for k being Nat holds NIC ((SCM-goto k),il) = {k} proof let il be Element of NAT ; ::_thesis: for k being Nat holds NIC ((SCM-goto k),il) = {k} let k be Nat; ::_thesis: NIC ((SCM-goto k),il) = {k} now__::_thesis:_for_x_being_set_holds_ (_x_in_{k}_iff_x_in__{__(IC_(Exec_((SCM-goto_k),s)))_where_s_is_Element_of_product_(the_Values_of_SCM)_:_IC_s_=_il__}__) let x be set ; ::_thesis: ( x in {k} iff x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il } ) A1: now__::_thesis:_(_x_=_k_implies_x_in__{__(IC_(Exec_((SCM-goto_k),s)))_where_s_is_Element_of_product_(the_Values_of_SCM)_:_IC_s_=_il__}__) reconsider il1 = il as Element of Values (IC ) by MEMSTR_0:def_6; set I = SCM-goto k; set t = the State of SCM; set Q = the Instruction-Sequence of SCM; assume A2: x = k ; ::_thesis: x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il } reconsider n = il as Element of NAT ; reconsider u = the State of SCM +* ((IC ),il1) as Element of product (the_Values_of SCM) by CARD_3:107; reconsider P = the Instruction-Sequence of SCM +* (il,(SCM-goto k)) as Instruction-Sequence of SCM ; A3: P /. il = P . il by PBOOLE:143; IC in dom the State of SCM by MEMSTR_0:2; then A4: IC u = n by FUNCT_7:31; il in NAT ; then il in dom the Instruction-Sequence of SCM by PARTFUN1:def_2; then A5: P . n = SCM-goto k by FUNCT_7:31; then IC (Following (P,u)) = k by A3, A4, AMI_3:7; hence x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il } by A2, A4, A3, A5; ::_thesis: verum end; now__::_thesis:_(_x_in__{__(IC_(Exec_((SCM-goto_k),s)))_where_s_is_Element_of_product_(the_Values_of_SCM)_:_IC_s_=_il__}__implies_x_=_k_) assume x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il } ; ::_thesis: x = k then ex s being Element of product (the_Values_of SCM) st ( x = IC (Exec ((SCM-goto k),s)) & IC s = il ) ; hence x = k by AMI_3:7; ::_thesis: verum end; hence ( x in {k} iff x in { (IC (Exec ((SCM-goto k),s))) where s is Element of product (the_Values_of SCM) : IC s = il } ) by A1, TARSKI:def_1; ::_thesis: verum end; hence NIC ((SCM-goto k),il) = {k} by TARSKI:1; ::_thesis: verum end; theorem Th16: :: AMI_6:16 for k being Nat holds JUMP (SCM-goto k) = {k} proof let k be Nat; ::_thesis: JUMP (SCM-goto k) = {k} set X = { (NIC ((SCM-goto k),il)) where il is Element of NAT : verum } ; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_meet__{__(NIC_((SCM-goto_k),il))_where_il_is_Element_of_NAT_:_verum__}__implies_x_in_{k}_)_&_(_x_in_{k}_implies_x_in_meet__{__(NIC_((SCM-goto_k),il))_where_il_is_Element_of_NAT_:_verum__}__)_) let x be set ; ::_thesis: ( ( x in meet { (NIC ((SCM-goto k),il)) where il is Element of NAT : verum } implies x in {k} ) & ( x in {k} implies x in meet { (NIC ((SCM-goto k),il)) where il is Element of NAT : verum } ) ) hereby ::_thesis: ( x in {k} implies x in meet { (NIC ((SCM-goto k),il)) where il is Element of NAT : verum } ) set il1 = 1; A1: NIC ((SCM-goto k),1) in { (NIC ((SCM-goto k),il)) where il is Element of NAT : verum } ; assume x in meet { (NIC ((SCM-goto k),il)) where il is Element of NAT : verum } ; ::_thesis: x in {k} then x in NIC ((SCM-goto k),1) by A1, SETFAM_1:def_1; hence x in {k} by Th15; ::_thesis: verum end; assume x in {k} ; ::_thesis: x in meet { (NIC ((SCM-goto k),il)) where il is Element of NAT : verum } then A2: x = k by TARSKI:def_1; A3: now__::_thesis:_for_Y_being_set_st_Y_in__{__(NIC_((SCM-goto_k),il))_where_il_is_Element_of_NAT_:_verum__}__holds_ k_in_Y let Y be set ; ::_thesis: ( Y in { (NIC ((SCM-goto k),il)) where il is Element of NAT : verum } implies k in Y ) assume Y in { (NIC ((SCM-goto k),il)) where il is Element of NAT : verum } ; ::_thesis: k in Y then consider il being Element of NAT such that A4: Y = NIC ((SCM-goto k),il) ; NIC ((SCM-goto k),il) = {k} by Th15; hence k in Y by A4, TARSKI:def_1; ::_thesis: verum end; reconsider k = k as Element of NAT by ORDINAL1:def_12; NIC ((SCM-goto k),k) in { (NIC ((SCM-goto k),il)) where il is Element of NAT : verum } ; hence x in meet { (NIC ((SCM-goto k),il)) where il is Element of NAT : verum } by A2, A3, SETFAM_1:def_1; ::_thesis: verum end; hence JUMP (SCM-goto k) = {k} by TARSKI:1; ::_thesis: verum end; registration let i1 be Element of NAT ; cluster JUMP (SCM-goto i1) -> 1 -element ; coherence JUMP (SCM-goto i1) is 1 -element proof JUMP (SCM-goto i1) = {i1} by Th16; hence JUMP (SCM-goto i1) is 1 -element ; ::_thesis: verum end; end; theorem Th17: :: AMI_6:17 for a being Data-Location for il being Element of NAT for k being Nat holds NIC ((a =0_goto k),il) = {k,(succ il)} proof let a be Data-Location; ::_thesis: for il being Element of NAT for k being Nat holds NIC ((a =0_goto k),il) = {k,(succ il)} let il be Element of NAT ; ::_thesis: for k being Nat holds NIC ((a =0_goto k),il) = {k,(succ il)} let k be Nat; ::_thesis: NIC ((a =0_goto k),il) = {k,(succ il)} set t = the State of SCM; set Q = the Instruction-Sequence of SCM; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {k,(succ il)} c= NIC ((a =0_goto k),il) let x be set ; ::_thesis: ( x in NIC ((a =0_goto k),il) implies b1 in {k,(succ il)} ) assume x in NIC ((a =0_goto k),il) ; ::_thesis: b1 in {k,(succ il)} then consider s being Element of product (the_Values_of SCM) such that A1: ( x = IC (Exec ((a =0_goto k),s)) & IC s = il ) ; percases ( s . a = 0 or s . a <> 0 ) ; suppose s . a = 0 ; ::_thesis: b1 in {k,(succ il)} then x = k by A1, AMI_3:8; hence x in {k,(succ il)} by TARSKI:def_2; ::_thesis: verum end; suppose s . a <> 0 ; ::_thesis: b1 in {k,(succ il)} then x = succ il by A1, AMI_3:8; hence x in {k,(succ il)} by TARSKI:def_2; ::_thesis: verum end; end; end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {k,(succ il)} or x in NIC ((a =0_goto k),il) ) set I = a =0_goto k; A2: IC <> a by AMI_5:2; reconsider il1 = il as Element of Values (IC ) by MEMSTR_0:def_6; reconsider n = il as Element of NAT ; reconsider u = the State of SCM +* ((IC ),il1) as Element of product (the_Values_of SCM) by CARD_3:107; reconsider P = the Instruction-Sequence of SCM +* (il,(a =0_goto k)) as Instruction-Sequence of SCM ; assume A3: x in {k,(succ il)} ; ::_thesis: x in NIC ((a =0_goto k),il) percases ( x = k or x = succ il ) by A3, TARSKI:def_2; supposeA4: x = k ; ::_thesis: x in NIC ((a =0_goto k),il) reconsider v = u +* (a .--> 0) as Element of product (the_Values_of SCM) by CARD_3:107; A5: IC in dom the State of SCM by MEMSTR_0:2; A6: dom (a .--> 0) = {a} by FUNCOP_1:13; then not IC in dom (a .--> 0) by A2, TARSKI:def_1; then A7: IC v = IC u by FUNCT_4:11 .= n by A5, FUNCT_7:31 ; A8: P /. il = P . il by PBOOLE:143; il in NAT ; then il in dom the Instruction-Sequence of SCM by PARTFUN1:def_2; then A9: P . il = a =0_goto k by FUNCT_7:31; a in dom (a .--> 0) by A6, TARSKI:def_1; then v . a = (a .--> 0) . a by FUNCT_4:13 .= 0 by FUNCOP_1:72 ; then IC (Following (P,v)) = k by A7, A9, A8, AMI_3:8; hence x in NIC ((a =0_goto k),il) by A4, A7, A9, A8; ::_thesis: verum end; supposeA10: x = succ il ; ::_thesis: x in NIC ((a =0_goto k),il) reconsider v = u +* (a .--> 1) as Element of product (the_Values_of SCM) by CARD_3:107; A11: IC in dom the State of SCM by MEMSTR_0:2; A12: dom (a .--> 1) = {a} by FUNCOP_1:13; then not IC in dom (a .--> 1) by A2, TARSKI:def_1; then A13: IC v = IC u by FUNCT_4:11 .= n by A11, FUNCT_7:31 ; A14: P /. il = P . il by PBOOLE:143; il in NAT ; then il in dom the Instruction-Sequence of SCM by PARTFUN1:def_2; then A15: P . il = a =0_goto k by FUNCT_7:31; a in dom (a .--> 1) by A12, TARSKI:def_1; then v . a = (a .--> 1) . a by FUNCT_4:13 .= 1 by FUNCOP_1:72 ; then IC (Following (P,v)) = succ il by A13, A15, A14, AMI_3:8; hence x in NIC ((a =0_goto k),il) by A10, A13, A15, A14; ::_thesis: verum end; end; end; theorem Th18: :: AMI_6:18 for a being Data-Location for k being Nat holds JUMP (a =0_goto k) = {k} proof let a be Data-Location; ::_thesis: for k being Nat holds JUMP (a =0_goto k) = {k} let k be Nat; ::_thesis: JUMP (a =0_goto k) = {k} set X = { (NIC ((a =0_goto k),il)) where il is Element of NAT : verum } ; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_meet__{__(NIC_((a_=0_goto_k),il))_where_il_is_Element_of_NAT_:_verum__}__implies_x_in_{k}_)_&_(_x_in_{k}_implies_x_in_meet__{__(NIC_((a_=0_goto_k),il))_where_il_is_Element_of_NAT_:_verum__}__)_) let x be set ; ::_thesis: ( ( x in meet { (NIC ((a =0_goto k),il)) where il is Element of NAT : verum } implies x in {k} ) & ( x in {k} implies x in meet { (NIC ((a =0_goto k),il)) where il is Element of NAT : verum } ) ) A1: now__::_thesis:_for_Y_being_set_st_Y_in__{__(NIC_((a_=0_goto_k),il))_where_il_is_Element_of_NAT_:_verum__}__holds_ k_in_Y let Y be set ; ::_thesis: ( Y in { (NIC ((a =0_goto k),il)) where il is Element of NAT : verum } implies k in Y ) assume Y in { (NIC ((a =0_goto k),il)) where il is Element of NAT : verum } ; ::_thesis: k in Y then consider il being Element of NAT such that A2: Y = NIC ((a =0_goto k),il) ; NIC ((a =0_goto k),il) = {k,(succ il)} by Th17; hence k in Y by A2, TARSKI:def_2; ::_thesis: verum end; hereby ::_thesis: ( x in {k} implies x in meet { (NIC ((a =0_goto k),il)) where il is Element of NAT : verum } ) set il1 = 1; set il2 = 2; assume A3: x in meet { (NIC ((a =0_goto k),il)) where il is Element of NAT : verum } ; ::_thesis: x in {k} A4: NIC ((a =0_goto k),2) = {k,(succ 2)} by Th17; NIC ((a =0_goto k),2) in { (NIC ((a =0_goto k),il)) where il is Element of NAT : verum } ; then x in NIC ((a =0_goto k),2) by A3, SETFAM_1:def_1; then A5: ( x = k or x = succ 2 ) by A4, TARSKI:def_2; A6: NIC ((a =0_goto k),1) = {k,(succ 1)} by Th17; NIC ((a =0_goto k),1) in { (NIC ((a =0_goto k),il)) where il is Element of NAT : verum } ; then x in NIC ((a =0_goto k),1) by A3, SETFAM_1:def_1; then ( x = k or x = succ 1 ) by A6, TARSKI:def_2; hence x in {k} by A5, TARSKI:def_1; ::_thesis: verum end; assume x in {k} ; ::_thesis: x in meet { (NIC ((a =0_goto k),il)) where il is Element of NAT : verum } then A7: x = k by TARSKI:def_1; reconsider k = k as Element of NAT by ORDINAL1:def_12; NIC ((a =0_goto k),k) in { (NIC ((a =0_goto k),il)) where il is Element of NAT : verum } ; hence x in meet { (NIC ((a =0_goto k),il)) where il is Element of NAT : verum } by A7, A1, SETFAM_1:def_1; ::_thesis: verum end; hence JUMP (a =0_goto k) = {k} by TARSKI:1; ::_thesis: verum end; registration let a be Data-Location; let i1 be Element of NAT ; cluster JUMP (a =0_goto i1) -> 1 -element ; coherence JUMP (a =0_goto i1) is 1 -element proof JUMP (a =0_goto i1) = {i1} by Th18; hence JUMP (a =0_goto i1) is 1 -element ; ::_thesis: verum end; end; theorem Th19: :: AMI_6:19 for a being Data-Location for il being Element of NAT for k being Nat holds NIC ((a >0_goto k),il) = {k,(succ il)} proof let a be Data-Location; ::_thesis: for il being Element of NAT for k being Nat holds NIC ((a >0_goto k),il) = {k,(succ il)} let il be Element of NAT ; ::_thesis: for k being Nat holds NIC ((a >0_goto k),il) = {k,(succ il)} let k be Nat; ::_thesis: NIC ((a >0_goto k),il) = {k,(succ il)} set t = the State of SCM; set Q = the Instruction-Sequence of SCM; hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: {k,(succ il)} c= NIC ((a >0_goto k),il) let x be set ; ::_thesis: ( x in NIC ((a >0_goto k),il) implies b1 in {k,(succ il)} ) assume x in NIC ((a >0_goto k),il) ; ::_thesis: b1 in {k,(succ il)} then consider s being Element of product (the_Values_of SCM) such that A1: ( x = IC (Exec ((a >0_goto k),s)) & IC s = il ) ; percases ( s . a > 0 or s . a <= 0 ) ; suppose s . a > 0 ; ::_thesis: b1 in {k,(succ il)} then x = k by A1, AMI_3:9; hence x in {k,(succ il)} by TARSKI:def_2; ::_thesis: verum end; suppose s . a <= 0 ; ::_thesis: b1 in {k,(succ il)} then x = succ il by A1, AMI_3:9; hence x in {k,(succ il)} by TARSKI:def_2; ::_thesis: verum end; end; end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {k,(succ il)} or x in NIC ((a >0_goto k),il) ) set I = a >0_goto k; A2: IC <> a by AMI_5:2; reconsider il1 = il as Element of Values (IC ) by MEMSTR_0:def_6; reconsider u = the State of SCM +* ((IC ),il1) as Element of product (the_Values_of SCM) by CARD_3:107; reconsider P = the Instruction-Sequence of SCM +* (il,(a >0_goto k)) as Instruction-Sequence of SCM ; reconsider n = il1 as Element of NAT ; assume A3: x in {k,(succ il)} ; ::_thesis: x in NIC ((a >0_goto k),il) percases ( x = k or x = succ il ) by A3, TARSKI:def_2; supposeA4: x = k ; ::_thesis: x in NIC ((a >0_goto k),il) reconsider v = u +* (a .--> 1) as Element of product (the_Values_of SCM) by CARD_3:107; A5: IC in dom the State of SCM by MEMSTR_0:2; A6: dom (a .--> 1) = {a} by FUNCOP_1:13; then not IC in dom (a .--> 1) by A2, TARSKI:def_1; then A7: IC v = IC u by FUNCT_4:11 .= n by A5, FUNCT_7:31 ; A8: P /. il = P . il by PBOOLE:143; il in NAT ; then il in dom the Instruction-Sequence of SCM by PARTFUN1:def_2; then A9: P . il = a >0_goto k by FUNCT_7:31; a in dom (a .--> 1) by A6, TARSKI:def_1; then v . a = (a .--> 1) . a by FUNCT_4:13 .= 1 by FUNCOP_1:72 ; then IC (Following (P,v)) = k by A7, A9, A8, AMI_3:9; hence x in NIC ((a >0_goto k),il) by A4, A7, A9, A8; ::_thesis: verum end; supposeA10: x = succ il ; ::_thesis: x in NIC ((a >0_goto k),il) reconsider v = u +* (a .--> 0) as Element of product (the_Values_of SCM) by CARD_3:107; A11: IC in dom the State of SCM by MEMSTR_0:2; A12: dom (a .--> 0) = {a} by FUNCOP_1:13; then not IC in dom (a .--> 0) by A2, TARSKI:def_1; then A13: IC v = IC u by FUNCT_4:11 .= n by A11, FUNCT_7:31 ; A14: P /. il = P . il by PBOOLE:143; il in NAT ; then il in dom the Instruction-Sequence of SCM by PARTFUN1:def_2; then A15: P . il = a >0_goto k by FUNCT_7:31; a in dom (a .--> 0) by A12, TARSKI:def_1; then v . a = (a .--> 0) . a by FUNCT_4:13 .= 0 by FUNCOP_1:72 ; then IC (Following (P,v)) = succ il by A13, A15, A14, AMI_3:9; hence x in NIC ((a >0_goto k),il) by A10, A13, A15, A14; ::_thesis: verum end; end; end; theorem Th20: :: AMI_6:20 for a being Data-Location for k being Nat holds JUMP (a >0_goto k) = {k} proof let a be Data-Location; ::_thesis: for k being Nat holds JUMP (a >0_goto k) = {k} let k be Nat; ::_thesis: JUMP (a >0_goto k) = {k} set X = { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } ; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_meet__{__(NIC_((a_>0_goto_k),il))_where_il_is_Element_of_NAT_:_verum__}__implies_x_in_{k}_)_&_(_x_in_{k}_implies_x_in_meet__{__(NIC_((a_>0_goto_k),il))_where_il_is_Element_of_NAT_:_verum__}__)_) let x be set ; ::_thesis: ( ( x in meet { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } implies x in {k} ) & ( x in {k} implies x in meet { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } ) ) A1: now__::_thesis:_for_Y_being_set_st_Y_in__{__(NIC_((a_>0_goto_k),il))_where_il_is_Element_of_NAT_:_verum__}__holds_ k_in_Y let Y be set ; ::_thesis: ( Y in { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } implies k in Y ) assume Y in { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } ; ::_thesis: k in Y then consider il being Element of NAT such that A2: Y = NIC ((a >0_goto k),il) ; NIC ((a >0_goto k),il) = {k,(succ il)} by Th19; hence k in Y by A2, TARSKI:def_2; ::_thesis: verum end; hereby ::_thesis: ( x in {k} implies x in meet { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } ) set il1 = 1; set il2 = 2; assume A3: x in meet { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } ; ::_thesis: x in {k} A4: NIC ((a >0_goto k),2) = {k,(succ 2)} by Th19; NIC ((a >0_goto k),2) in { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } ; then x in NIC ((a >0_goto k),2) by A3, SETFAM_1:def_1; then A5: ( x = k or x = succ 2 ) by A4, TARSKI:def_2; A6: NIC ((a >0_goto k),1) = {k,(succ 1)} by Th19; NIC ((a >0_goto k),1) in { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } ; then x in NIC ((a >0_goto k),1) by A3, SETFAM_1:def_1; then ( x = k or x = succ 1 ) by A6, TARSKI:def_2; hence x in {k} by A5, TARSKI:def_1; ::_thesis: verum end; assume x in {k} ; ::_thesis: x in meet { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } then A7: x = k by TARSKI:def_1; reconsider k = k as Element of NAT by ORDINAL1:def_12; NIC ((a >0_goto k),k) in { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } ; hence x in meet { (NIC ((a >0_goto k),il)) where il is Element of NAT : verum } by A7, A1, SETFAM_1:def_1; ::_thesis: verum end; hence JUMP (a >0_goto k) = {k} by TARSKI:1; ::_thesis: verum end; registration let a be Data-Location; let i1 be Element of NAT ; cluster JUMP (a >0_goto i1) -> 1 -element ; coherence JUMP (a >0_goto i1) is 1 -element proof JUMP (a >0_goto i1) = {i1} by Th20; hence JUMP (a >0_goto i1) is 1 -element ; ::_thesis: verum end; end; theorem Th21: :: AMI_6:21 for il being Element of NAT holds SUCC (il,SCM) = {il,(succ il)} proof let il be Element of NAT ; ::_thesis: SUCC (il,SCM) = {il,(succ il)} set X = { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : verum } ; set N = {il,(succ il)}; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_union__{__((NIC_(I,il))_\_(JUMP_I))_where_I_is_Element_of_the_InstructionsF_of_SCM_:_verum__}__implies_x_in_{il,(succ_il)}_)_&_(_x_in_{il,(succ_il)}_implies_x_in_union__{__((NIC_(I,il))_\_(JUMP_I))_where_I_is_Element_of_the_InstructionsF_of_SCM_:_verum__}__)_) let x be set ; ::_thesis: ( ( x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : verum } implies x in {il,(succ il)} ) & ( x in {il,(succ il)} implies b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of SCM : verum } ) ) hereby ::_thesis: ( x in {il,(succ il)} implies b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of SCM : verum } ) assume x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : verum } ; ::_thesis: x in {il,(succ il)} then consider Y being set such that A1: x in Y and A2: Y in { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : verum } by TARSKI:def_4; consider i being Element of the InstructionsF of SCM such that A3: Y = (NIC (i,il)) \ (JUMP i) by A2; percases ( i = [0,{},{}] or ex a, b being Data-Location st i = a := b or ex a, b being Data-Location st i = AddTo (a,b) or ex a, b being Data-Location st i = SubFrom (a,b) or ex a, b being Data-Location st i = MultBy (a,b) or ex a, b being Data-Location st i = Divide (a,b) or ex k being Nat st i = SCM-goto k or ex a being Data-Location ex k being Nat st i = a =0_goto k or ex a being Data-Location ex k being Nat st i = a >0_goto k ) by AMI_3:24; suppose i = [0,{},{}] ; ::_thesis: x in {il,(succ il)} then x in {il} \ (JUMP (halt SCM)) by A1, A3, AMISTD_1:2; then x = il by TARSKI:def_1; hence x in {il,(succ il)} by TARSKI:def_2; ::_thesis: verum end; suppose ex a, b being Data-Location st i = a := b ; ::_thesis: x in {il,(succ il)} then consider a, b being Data-Location such that A4: i = a := b ; x in {(succ il)} \ (JUMP (a := b)) by A1, A3, A4, AMISTD_1:12; then x = succ il by TARSKI:def_1; hence x in {il,(succ il)} by TARSKI:def_2; ::_thesis: verum end; suppose ex a, b being Data-Location st i = AddTo (a,b) ; ::_thesis: x in {il,(succ il)} then consider a, b being Data-Location such that A5: i = AddTo (a,b) ; x in {(succ il)} \ (JUMP (AddTo (a,b))) by A1, A3, A5, AMISTD_1:12; then x = succ il by TARSKI:def_1; hence x in {il,(succ il)} by TARSKI:def_2; ::_thesis: verum end; suppose ex a, b being Data-Location st i = SubFrom (a,b) ; ::_thesis: x in {il,(succ il)} then consider a, b being Data-Location such that A6: i = SubFrom (a,b) ; x in {(succ il)} \ (JUMP (SubFrom (a,b))) by A1, A3, A6, AMISTD_1:12; then x = succ il by TARSKI:def_1; hence x in {il,(succ il)} by TARSKI:def_2; ::_thesis: verum end; suppose ex a, b being Data-Location st i = MultBy (a,b) ; ::_thesis: x in {il,(succ il)} then consider a, b being Data-Location such that A7: i = MultBy (a,b) ; x in {(succ il)} \ (JUMP (MultBy (a,b))) by A1, A3, A7, AMISTD_1:12; then x = succ il by TARSKI:def_1; hence x in {il,(succ il)} by TARSKI:def_2; ::_thesis: verum end; suppose ex a, b being Data-Location st i = Divide (a,b) ; ::_thesis: x in {il,(succ il)} then consider a, b being Data-Location such that A8: i = Divide (a,b) ; x in {(succ il)} \ (JUMP (Divide (a,b))) by A1, A3, A8, AMISTD_1:12; then x = succ il by TARSKI:def_1; hence x in {il,(succ il)} by TARSKI:def_2; ::_thesis: verum end; suppose ex k being Nat st i = SCM-goto k ; ::_thesis: x in {il,(succ il)} then consider k being Nat such that A9: i = SCM-goto k ; x in {k} \ (JUMP i) by A1, A3, A9, Th15; then x in {k} \ {k} by A9, Th16; hence x in {il,(succ il)} by XBOOLE_1:37; ::_thesis: verum end; suppose ex a being Data-Location ex k being Nat st i = a =0_goto k ; ::_thesis: x in {il,(succ il)} then consider a being Data-Location, k being Nat such that A10: i = a =0_goto k ; A11: NIC (i,il) = {k,(succ il)} by A10, Th17; x in NIC (i,il) by A1, A3, XBOOLE_0:def_5; then A12: ( x = k or x = succ il ) by A11, TARSKI:def_2; x in (NIC (i,il)) \ {k} by A1, A3, A10, Th18; then not x in {k} by XBOOLE_0:def_5; hence x in {il,(succ il)} by A12, TARSKI:def_1, TARSKI:def_2; ::_thesis: verum end; suppose ex a being Data-Location ex k being Nat st i = a >0_goto k ; ::_thesis: x in {il,(succ il)} then consider a being Data-Location, k being Nat such that A13: i = a >0_goto k ; A14: NIC (i,il) = {k,(succ il)} by A13, Th19; x in NIC (i,il) by A1, A3, XBOOLE_0:def_5; then A15: ( x = k or x = succ il ) by A14, TARSKI:def_2; x in (NIC (i,il)) \ {k} by A1, A3, A13, Th20; then not x in {k} by XBOOLE_0:def_5; hence x in {il,(succ il)} by A15, TARSKI:def_1, TARSKI:def_2; ::_thesis: verum end; end; end; assume A16: x in {il,(succ il)} ; ::_thesis: b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of SCM : verum } percases ( x = il or x = succ il ) by A16, TARSKI:def_2; supposeA17: x = il ; ::_thesis: b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of SCM : verum } set i = halt SCM; (NIC ((halt SCM),il)) \ (JUMP (halt SCM)) = {il} by AMISTD_1:2; then A18: {il} in { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : verum } ; x in {il} by A17, TARSKI:def_1; hence x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : verum } by A18, TARSKI:def_4; ::_thesis: verum end; supposeA19: x = succ il ; ::_thesis: b1 in union { ((NIC (b2,il)) \ (JUMP b2)) where I is Element of the InstructionsF of SCM : verum } set a = the Data-Location; set i = AddTo ( the Data-Location, the Data-Location); (NIC ((AddTo ( the Data-Location, the Data-Location)),il)) \ (JUMP (AddTo ( the Data-Location, the Data-Location))) = {(succ il)} by AMISTD_1:12; then A20: {(succ il)} in { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : verum } ; x in {(succ il)} by A19, TARSKI:def_1; hence x in union { ((NIC (I,il)) \ (JUMP I)) where I is Element of the InstructionsF of SCM : verum } by A20, TARSKI:def_4; ::_thesis: verum end; end; end; hence SUCC (il,SCM) = {il,(succ il)} by TARSKI:1; ::_thesis: verum end; theorem Th22: :: AMI_6:22 for k being Element of NAT holds ( k + 1 in SUCC (k,SCM) & ( for j being Element of NAT st j in SUCC (k,SCM) holds k <= j ) ) proof let k be Element of NAT ; ::_thesis: ( k + 1 in SUCC (k,SCM) & ( for j being Element of NAT st j in SUCC (k,SCM) holds k <= j ) ) reconsider fk = k as Element of NAT ; A1: SUCC (k,SCM) = {k,(succ fk)} by Th21; hence k + 1 in SUCC (k,SCM) by TARSKI:def_2; ::_thesis: for j being Element of NAT st j in SUCC (k,SCM) holds k <= j let j be Element of NAT ; ::_thesis: ( j in SUCC (k,SCM) implies k <= j ) assume A2: j in SUCC (k,SCM) ; ::_thesis: k <= j reconsider fk = k as Element of NAT ; percases ( j = k or j = succ fk ) by A1, A2, TARSKI:def_2; suppose j = k ; ::_thesis: k <= j hence k <= j ; ::_thesis: verum end; suppose j = succ fk ; ::_thesis: k <= j hence k <= j by NAT_1:11; ::_thesis: verum end; end; end; registration cluster SCM -> standard ; coherence SCM is standard by Th22, AMISTD_1:3; end; registration cluster InsCode (halt SCM) -> jump-only for InsType of the InstructionsF of SCM; coherence for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (halt SCM) holds b1 is jump-only proof now__::_thesis:_for_s_being_State_of_SCM for_o_being_Object_of_SCM for_I_being_Instruction_of_SCM_st_InsCode_I_=_InsCode_(halt_SCM)_&_o_in_Data-Locations_holds_ (Exec_(I,s))_._o_=_s_._o let s be State of SCM; ::_thesis: for o being Object of SCM for I being Instruction of SCM st InsCode I = InsCode (halt SCM) & o in Data-Locations holds (Exec (I,s)) . o = s . o let o be Object of SCM; ::_thesis: for I being Instruction of SCM st InsCode I = InsCode (halt SCM) & o in Data-Locations holds (Exec (I,s)) . o = s . o let I be Instruction of SCM; ::_thesis: ( InsCode I = InsCode (halt SCM) & o in Data-Locations implies (Exec (I,s)) . o = s . o ) assume that A1: InsCode I = InsCode (halt SCM) and o in Data-Locations ; ::_thesis: (Exec (I,s)) . o = s . o I = halt SCM by A1, AMI_5:7, COMPOS_1:70; hence (Exec (I,s)) . o = s . o by EXTPRO_1:def_3; ::_thesis: verum end; hence for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (halt SCM) holds b1 is jump-only by AMISTD_1:def_1; ::_thesis: verum end; end; registration cluster halt SCM -> jump-only ; coherence halt SCM is jump-only proof thus InsCode (halt SCM) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: verum end; end; registration let i1 be Element of NAT ; cluster InsCode (SCM-goto i1) -> jump-only for InsType of the InstructionsF of SCM; coherence for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (SCM-goto i1) holds b1 is jump-only proof let T be InsType of the InstructionsF of SCM; ::_thesis: ( T = InsCode (SCM-goto i1) implies T is jump-only ) assume A1: T = InsCode (SCM-goto i1) ; ::_thesis: T is jump-only let s be State of SCM; :: according to AMISTD_1:def_1 ::_thesis: for b1 being Element of the U1 of SCM for b2 being Element of the InstructionsF of SCM holds ( not InsCode b2 = T or not b1 in Data-Locations or (Exec (b2,s)) . b1 = s . b1 ) let o be Object of SCM; ::_thesis: for b1 being Element of the InstructionsF of SCM holds ( not InsCode b1 = T or not o in Data-Locations or (Exec (b1,s)) . o = s . o ) let I be Instruction of SCM; ::_thesis: ( not InsCode I = T or not o in Data-Locations or (Exec (I,s)) . o = s . o ) assume that A2: InsCode I = T and A3: o in Data-Locations ; ::_thesis: (Exec (I,s)) . o = s . o InsCode I = 6 by A2, A1, RECDEF_2:def_1; then A4: ex i2 being Element of NAT st I = SCM-goto i2 by AMI_5:13; o is Data-Location by A3, AMI_2:def_16, AMI_3:27; hence (Exec (I,s)) . o = s . o by A4, AMI_3:7; ::_thesis: verum end; end; registration let i1 be Element of NAT ; cluster SCM-goto i1 -> non ins-loc-free jump-only non sequential ; coherence ( SCM-goto i1 is jump-only & not SCM-goto i1 is sequential & not SCM-goto i1 is ins-loc-free ) proof thus InsCode (SCM-goto i1) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: ( not SCM-goto i1 is sequential & not SCM-goto i1 is ins-loc-free ) JUMP (SCM-goto i1) <> {} ; hence not SCM-goto i1 is sequential by AMISTD_1:13; ::_thesis: not SCM-goto i1 is ins-loc-free dom (JumpPart (SCM-goto i1)) = dom <*i1*> by RECDEF_2:def_2 .= {1} by FINSEQ_1:2, FINSEQ_1:def_8 ; hence not JumpPart (SCM-goto i1) is empty ; :: according to COMPOS_0:def_8 ::_thesis: verum end; end; registration let a be Data-Location; let i1 be Element of NAT ; cluster InsCode (a =0_goto i1) -> jump-only for InsType of the InstructionsF of SCM; coherence for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (a =0_goto i1) holds b1 is jump-only proof set S = SCM ; now__::_thesis:_for_s_being_State_of_SCM for_o_being_Object_of_SCM for_I_being_Instruction_of_SCM_st_InsCode_I_=_InsCode_(a_=0_goto_i1)_&_o_in_Data-Locations_holds_ (Exec_(I,s))_._o_=_s_._o let s be State of SCM; ::_thesis: for o being Object of SCM for I being Instruction of SCM st InsCode I = InsCode (a =0_goto i1) & o in Data-Locations holds (Exec (I,s)) . o = s . o let o be Object of SCM; ::_thesis: for I being Instruction of SCM st InsCode I = InsCode (a =0_goto i1) & o in Data-Locations holds (Exec (I,s)) . o = s . o let I be Instruction of SCM; ::_thesis: ( InsCode I = InsCode (a =0_goto i1) & o in Data-Locations implies (Exec (I,s)) . o = s . o ) assume that A1: InsCode I = InsCode (a =0_goto i1) and A2: o in Data-Locations ; ::_thesis: (Exec (I,s)) . o = s . o InsCode I = 7 by A1, RECDEF_2:def_1; then A3: ex i2 being Element of NAT ex b being Data-Location st I = b =0_goto i2 by AMI_5:14; o is Data-Location by A2, AMI_2:def_16, AMI_3:27; hence (Exec (I,s)) . o = s . o by A3, AMI_3:8; ::_thesis: verum end; hence for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (a =0_goto i1) holds b1 is jump-only by AMISTD_1:def_1; ::_thesis: verum end; cluster InsCode (a >0_goto i1) -> jump-only for InsType of the InstructionsF of SCM; coherence for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (a >0_goto i1) holds b1 is jump-only proof set S = SCM ; now__::_thesis:_for_s_being_State_of_SCM for_o_being_Object_of_SCM for_I_being_Instruction_of_SCM_st_InsCode_I_=_InsCode_(a_>0_goto_i1)_&_o_in_Data-Locations_holds_ (Exec_(I,s))_._o_=_s_._o let s be State of SCM; ::_thesis: for o being Object of SCM for I being Instruction of SCM st InsCode I = InsCode (a >0_goto i1) & o in Data-Locations holds (Exec (I,s)) . o = s . o let o be Object of SCM; ::_thesis: for I being Instruction of SCM st InsCode I = InsCode (a >0_goto i1) & o in Data-Locations holds (Exec (I,s)) . o = s . o let I be Instruction of SCM; ::_thesis: ( InsCode I = InsCode (a >0_goto i1) & o in Data-Locations implies (Exec (I,s)) . o = s . o ) assume that A4: InsCode I = InsCode (a >0_goto i1) and A5: o in Data-Locations ; ::_thesis: (Exec (I,s)) . o = s . o InsCode I = 8 by A4, RECDEF_2:def_1; then A6: ex i2 being Element of NAT ex b being Data-Location st I = b >0_goto i2 by AMI_5:15; o is Data-Location by A5, AMI_2:def_16, AMI_3:27; hence (Exec (I,s)) . o = s . o by A6, AMI_3:9; ::_thesis: verum end; hence for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (a >0_goto i1) holds b1 is jump-only by AMISTD_1:def_1; ::_thesis: verum end; end; registration let a be Data-Location; let i1 be Element of NAT ; clustera =0_goto i1 -> non ins-loc-free jump-only non sequential ; coherence ( a =0_goto i1 is jump-only & not a =0_goto i1 is sequential & not a =0_goto i1 is ins-loc-free ) proof thus InsCode (a =0_goto i1) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: ( not a =0_goto i1 is sequential & not a =0_goto i1 is ins-loc-free ) JUMP (a =0_goto i1) <> {} ; hence not a =0_goto i1 is sequential by AMISTD_1:13; ::_thesis: not a =0_goto i1 is ins-loc-free dom (JumpPart (a =0_goto i1)) = dom <*i1*> by RECDEF_2:def_2 .= {1} by FINSEQ_1:2, FINSEQ_1:38 ; hence not JumpPart (a =0_goto i1) is empty ; :: according to COMPOS_0:def_8 ::_thesis: verum end; clustera >0_goto i1 -> non ins-loc-free jump-only non sequential ; coherence ( a >0_goto i1 is jump-only & not a >0_goto i1 is sequential & not a >0_goto i1 is ins-loc-free ) proof thus InsCode (a >0_goto i1) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: ( not a >0_goto i1 is sequential & not a >0_goto i1 is ins-loc-free ) JUMP (a >0_goto i1) <> {} ; hence not a >0_goto i1 is sequential by AMISTD_1:13; ::_thesis: not a >0_goto i1 is ins-loc-free dom (JumpPart (a >0_goto i1)) = dom <*i1*> by RECDEF_2:def_2 .= {1} by FINSEQ_1:2, FINSEQ_1:38 ; hence not JumpPart (a >0_goto i1) is empty ; :: according to COMPOS_0:def_8 ::_thesis: verum end; end; Lm2: dl. 0 <> dl. 1 by AMI_3:10; registration let a, b be Data-Location; cluster InsCode (a := b) -> non jump-only for InsType of the InstructionsF of SCM; coherence for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (a := b) holds not b1 is jump-only proof set w = the State of SCM; set t = the State of SCM +* (((dl. 0),(dl. 1)) --> (0,1)); A1: InsCode (a := b) = 1 by RECDEF_2:def_1 .= InsCode ((dl. 0) := (dl. 1)) by RECDEF_2:def_1 ; A2: dl. 0 in Data-Locations by AMI_3:28; A3: dom (((dl. 0),(dl. 1)) --> (0,1)) = {(dl. 0),(dl. 1)} by FUNCT_4:62; then A4: dl. 1 in dom (((dl. 0),(dl. 1)) --> (0,1)) by TARSKI:def_2; dl. 0 in dom (((dl. 0),(dl. 1)) --> (0,1)) by A3, TARSKI:def_2; then A5: ( the State of SCM +* (((dl. 0),(dl. 1)) --> (0,1))) . (dl. 0) = (((dl. 0),(dl. 1)) --> (0,1)) . (dl. 0) by FUNCT_4:13 .= 0 by AMI_3:10, FUNCT_4:63 ; (Exec (((dl. 0) := (dl. 1)),( the State of SCM +* (((dl. 0),(dl. 1)) --> (0,1))))) . (dl. 0) = ( the State of SCM +* (((dl. 0),(dl. 1)) --> (0,1))) . (dl. 1) by AMI_3:2 .= (((dl. 0),(dl. 1)) --> (0,1)) . (dl. 1) by A4, FUNCT_4:13 .= 1 by FUNCT_4:63 ; hence for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (a := b) holds not b1 is jump-only by A1, A2, A5, AMISTD_1:def_1; ::_thesis: verum end; cluster InsCode (AddTo (a,b)) -> non jump-only for InsType of the InstructionsF of SCM; coherence for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (AddTo (a,b)) holds not b1 is jump-only proof set w = the State of SCM; set t = the State of SCM +* (((dl. 0),(dl. 1)) --> (0,1)); A6: InsCode (AddTo (a,b)) = 2 by RECDEF_2:def_1 .= InsCode (AddTo ((dl. 0),(dl. 1))) by RECDEF_2:def_1 ; A7: dom (((dl. 0),(dl. 1)) --> (0,1)) = {(dl. 0),(dl. 1)} by FUNCT_4:62; then dl. 0 in dom (((dl. 0),(dl. 1)) --> (0,1)) by TARSKI:def_2; then A8: ( the State of SCM +* (((dl. 0),(dl. 1)) --> (0,1))) . (dl. 0) = (((dl. 0),(dl. 1)) --> (0,1)) . (dl. 0) by FUNCT_4:13 .= 0 by AMI_3:10, FUNCT_4:63 ; A9: dl. 0 in Data-Locations by AMI_3:28; dl. 1 in dom (((dl. 0),(dl. 1)) --> (0,1)) by A7, TARSKI:def_2; then ( the State of SCM +* (((dl. 0),(dl. 1)) --> (0,1))) . (dl. 1) = (((dl. 0),(dl. 1)) --> (0,1)) . (dl. 1) by FUNCT_4:13 .= 1 by FUNCT_4:63 ; then ( dl. 0 <> IC & (Exec ((AddTo ((dl. 0),(dl. 1))),( the State of SCM +* (((dl. 0),(dl. 1)) --> (0,1))))) . (dl. 0) = 0 + 1 ) by A8, AMI_3:3, AMI_3:13; hence for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (AddTo (a,b)) holds not b1 is jump-only by A6, A8, A9, AMISTD_1:def_1; ::_thesis: verum end; cluster InsCode (SubFrom (a,b)) -> non jump-only for InsType of the InstructionsF of SCM; coherence for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (SubFrom (a,b)) holds not b1 is jump-only proof set w = the State of SCM; set t = the State of SCM +* (((dl. 0),(dl. 1)) --> (0,1)); A10: InsCode (SubFrom (a,b)) = 3 by RECDEF_2:def_1 .= InsCode (SubFrom ((dl. 0),(dl. 1))) by RECDEF_2:def_1 ; A11: dom (((dl. 0),(dl. 1)) --> (0,1)) = {(dl. 0),(dl. 1)} by FUNCT_4:62; then dl. 0 in dom (((dl. 0),(dl. 1)) --> (0,1)) by TARSKI:def_2; then A12: ( the State of SCM +* (((dl. 0),(dl. 1)) --> (0,1))) . (dl. 0) = (((dl. 0),(dl. 1)) --> (0,1)) . (dl. 0) by FUNCT_4:13 .= 0 by AMI_3:10, FUNCT_4:63 ; A13: dl. 0 in Data-Locations by AMI_3:28; dl. 1 in dom (((dl. 0),(dl. 1)) --> (0,1)) by A11, TARSKI:def_2; then A14: ( the State of SCM +* (((dl. 0),(dl. 1)) --> (0,1))) . (dl. 1) = (((dl. 0),(dl. 1)) --> (0,1)) . (dl. 1) by FUNCT_4:13 .= 1 by FUNCT_4:63 ; (Exec ((SubFrom ((dl. 0),(dl. 1))),( the State of SCM +* (((dl. 0),(dl. 1)) --> (0,1))))) . (dl. 0) = (( the State of SCM +* (((dl. 0),(dl. 1)) --> (0,1))) . (dl. 0)) - (( the State of SCM +* (((dl. 0),(dl. 1)) --> (0,1))) . (dl. 1)) by AMI_3:4 .= - 1 by A12, A14 ; hence for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (SubFrom (a,b)) holds not b1 is jump-only by A10, A12, A13, AMISTD_1:def_1; ::_thesis: verum end; cluster InsCode (MultBy (a,b)) -> non jump-only for InsType of the InstructionsF of SCM; coherence for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (MultBy (a,b)) holds not b1 is jump-only proof set w = the State of SCM; set t = the State of SCM +* (((dl. 0),(dl. 1)) --> (1,0)); A15: InsCode (MultBy (a,b)) = 4 by RECDEF_2:def_1 .= InsCode (MultBy ((dl. 0),(dl. 1))) by RECDEF_2:def_1 ; A16: dom (((dl. 0),(dl. 1)) --> (1,0)) = {(dl. 0),(dl. 1)} by FUNCT_4:62; then dl. 0 in dom (((dl. 0),(dl. 1)) --> (1,0)) by TARSKI:def_2; then A17: ( the State of SCM +* (((dl. 0),(dl. 1)) --> (1,0))) . (dl. 0) = (((dl. 0),(dl. 1)) --> (1,0)) . (dl. 0) by FUNCT_4:13 .= 1 by AMI_3:10, FUNCT_4:63 ; A18: dl. 0 in Data-Locations by AMI_3:28; dl. 1 in dom (((dl. 0),(dl. 1)) --> (1,0)) by A16, TARSKI:def_2; then A19: ( the State of SCM +* (((dl. 0),(dl. 1)) --> (1,0))) . (dl. 1) = (((dl. 0),(dl. 1)) --> (1,0)) . (dl. 1) by FUNCT_4:13 .= 0 by FUNCT_4:63 ; (Exec ((MultBy ((dl. 0),(dl. 1))),( the State of SCM +* (((dl. 0),(dl. 1)) --> (1,0))))) . (dl. 0) = (( the State of SCM +* (((dl. 0),(dl. 1)) --> (1,0))) . (dl. 0)) * (( the State of SCM +* (((dl. 0),(dl. 1)) --> (1,0))) . (dl. 1)) by AMI_3:5 .= 0 by A19 ; hence for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (MultBy (a,b)) holds not b1 is jump-only by A15, A17, A18, AMISTD_1:def_1; ::_thesis: verum end; cluster InsCode (Divide (a,b)) -> non jump-only for InsType of the InstructionsF of SCM; coherence for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (Divide (a,b)) holds not b1 is jump-only proof set w = the State of SCM; set t = the State of SCM +* (((dl. 0),(dl. 1)) --> (7,3)); A20: InsCode (Divide (a,b)) = 5 by RECDEF_2:def_1 .= InsCode (Divide ((dl. 0),(dl. 1))) by RECDEF_2:def_1 ; A21: dom (((dl. 0),(dl. 1)) --> (7,3)) = {(dl. 0),(dl. 1)} by FUNCT_4:62; then dl. 0 in dom (((dl. 0),(dl. 1)) --> (7,3)) by TARSKI:def_2; then A22: ( the State of SCM +* (((dl. 0),(dl. 1)) --> (7,3))) . (dl. 0) = (((dl. 0),(dl. 1)) --> (7,3)) . (dl. 0) by FUNCT_4:13 .= 7 by AMI_3:10, FUNCT_4:63 ; A23: 7 = (2 * 3) + 1 ; A24: dl. 0 in Data-Locations by AMI_3:28; dl. 1 in dom (((dl. 0),(dl. 1)) --> (7,3)) by A21, TARSKI:def_2; then ( the State of SCM +* (((dl. 0),(dl. 1)) --> (7,3))) . (dl. 1) = (((dl. 0),(dl. 1)) --> (7,3)) . (dl. 1) by FUNCT_4:13 .= 3 by FUNCT_4:63 ; then (Exec ((Divide ((dl. 0),(dl. 1))),( the State of SCM +* (((dl. 0),(dl. 1)) --> (7,3))))) . (dl. 0) = 7 div 3 by A22, Lm2, AMI_3:6 .= 2 by A23, NAT_D:def_1 ; hence for b1 being InsType of the InstructionsF of SCM st b1 = InsCode (Divide (a,b)) holds not b1 is jump-only by A20, A22, A24, AMISTD_1:def_1; ::_thesis: verum end; end; registration let a, b be Data-Location; clustera := b -> non jump-only ; coherence not a := b is jump-only proof thus not InsCode (a := b) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: verum end; cluster AddTo (a,b) -> non jump-only ; coherence not AddTo (a,b) is jump-only proof thus not InsCode (AddTo (a,b)) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: verum end; cluster SubFrom (a,b) -> non jump-only ; coherence not SubFrom (a,b) is jump-only proof thus not InsCode (SubFrom (a,b)) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: verum end; cluster MultBy (a,b) -> non jump-only ; coherence not MultBy (a,b) is jump-only proof thus not InsCode (MultBy (a,b)) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: verum end; cluster Divide (a,b) -> non jump-only ; coherence not Divide (a,b) is jump-only proof thus not InsCode (Divide (a,b)) is jump-only ; :: according to AMISTD_1:def_2 ::_thesis: verum end; end; registration cluster SCM -> with_explicit_jumps ; coherence SCM is with_explicit_jumps proof let I be Instruction of SCM; :: according to AMISTD_2:def_2 ::_thesis: I is with_explicit_jumps thus JUMP I c= rng (JumpPart I) :: according to AMISTD_2:def_1,XBOOLE_0:def_10 ::_thesis: proj2 (JumpPart I) c= JUMP I proof let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in JUMP I or f in rng (JumpPart I) ) assume A1: f in JUMP I ; ::_thesis: f in rng (JumpPart I) percases ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex k being Nat st I = SCM-goto k or ex a being Data-Location ex k1 being Nat st I = a =0_goto k1 or ex a being Data-Location ex k1 being Nat st I = a >0_goto k1 ) by AMI_3:24; suppose I = [0,{},{}] ; ::_thesis: f in rng (JumpPart I) hence f in rng (JumpPart I) by A1, AMI_3:26; ::_thesis: verum end; suppose ex a, b being Data-Location st I = a := b ; ::_thesis: f in rng (JumpPart I) hence f in rng (JumpPart I) by A1; ::_thesis: verum end; suppose ex a, b being Data-Location st I = AddTo (a,b) ; ::_thesis: f in rng (JumpPart I) hence f in rng (JumpPart I) by A1; ::_thesis: verum end; suppose ex a, b being Data-Location st I = SubFrom (a,b) ; ::_thesis: f in rng (JumpPart I) hence f in rng (JumpPart I) by A1; ::_thesis: verum end; suppose ex a, b being Data-Location st I = MultBy (a,b) ; ::_thesis: f in rng (JumpPart I) hence f in rng (JumpPart I) by A1; ::_thesis: verum end; suppose ex a, b being Data-Location st I = Divide (a,b) ; ::_thesis: f in rng (JumpPart I) hence f in rng (JumpPart I) by A1; ::_thesis: verum end; supposeA2: ex k being Nat st I = SCM-goto k ; ::_thesis: f in rng (JumpPart I) consider k1 being Nat such that A3: I = SCM-goto k1 by A2; A4: JumpPart (SCM-goto k1) = <*k1*> by RECDEF_2:def_2; A5: rng <*k1*> = {k1} by FINSEQ_1:39; JUMP (SCM-goto k1) = {k1} by Th16; hence f in rng (JumpPart I) by A1, A3, A4, A5; ::_thesis: verum end; supposeA6: ex a being Data-Location ex k1 being Nat st I = a =0_goto k1 ; ::_thesis: f in rng (JumpPart I) consider a being Data-Location, k1 being Nat such that A7: I = a =0_goto k1 by A6; A8: JumpPart (a =0_goto k1) = <*k1*> by RECDEF_2:def_2; A9: rng <*k1*> = {k1} by FINSEQ_1:39; JUMP (a =0_goto k1) = {k1} by Th18; hence f in rng (JumpPart I) by A1, A7, A8, A9; ::_thesis: verum end; supposeA10: ex a being Data-Location ex k1 being Nat st I = a >0_goto k1 ; ::_thesis: f in rng (JumpPart I) consider a being Data-Location, k1 being Nat such that A11: I = a >0_goto k1 by A10; A12: JumpPart (a >0_goto k1) = <*k1*> by RECDEF_2:def_2; A13: rng <*k1*> = {k1} by FINSEQ_1:39; JUMP (a >0_goto k1) = {k1} by Th20; hence f in rng (JumpPart I) by A1, A11, A12, A13; ::_thesis: verum end; end; end; let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in proj2 (JumpPart I) or f in JUMP I ) assume f in rng (JumpPart I) ; ::_thesis: f in JUMP I then consider k being set such that A14: k in dom (JumpPart I) and A15: f = (JumpPart I) . k by FUNCT_1:def_3; percases ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex k being Nat st I = SCM-goto k or ex a being Data-Location ex k being Nat st I = a =0_goto k or ex a being Data-Location ex k1 being Nat st I = a >0_goto k1 ) by AMI_3:24; suppose I = [0,{},{}] ; ::_thesis: f in JUMP I then dom (JumpPart I) = dom {} by RECDEF_2:def_2; hence f in JUMP I by A14; ::_thesis: verum end; suppose ex a, b being Data-Location st I = a := b ; ::_thesis: f in JUMP I then consider a, b being Data-Location such that A16: I = a := b ; k in dom {} by A14, A16, RECDEF_2:def_2; hence f in JUMP I ; ::_thesis: verum end; suppose ex a, b being Data-Location st I = AddTo (a,b) ; ::_thesis: f in JUMP I then consider a, b being Data-Location such that A17: I = AddTo (a,b) ; k in dom {} by A14, A17, RECDEF_2:def_2; hence f in JUMP I ; ::_thesis: verum end; suppose ex a, b being Data-Location st I = SubFrom (a,b) ; ::_thesis: f in JUMP I then consider a, b being Data-Location such that A18: I = SubFrom (a,b) ; k in dom {} by A14, A18, RECDEF_2:def_2; hence f in JUMP I ; ::_thesis: verum end; suppose ex a, b being Data-Location st I = MultBy (a,b) ; ::_thesis: f in JUMP I then consider a, b being Data-Location such that A19: I = MultBy (a,b) ; k in dom {} by A14, A19, RECDEF_2:def_2; hence f in JUMP I ; ::_thesis: verum end; suppose ex a, b being Data-Location st I = Divide (a,b) ; ::_thesis: f in JUMP I then consider a, b being Data-Location such that A20: I = Divide (a,b) ; k in dom {} by A14, A20, RECDEF_2:def_2; hence f in JUMP I ; ::_thesis: verum end; suppose ex k being Nat st I = SCM-goto k ; ::_thesis: f in JUMP I then consider k1 being Nat such that A21: I = SCM-goto k1 ; A22: JumpPart I = <*k1*> by A21, RECDEF_2:def_2; then k = 1 by A14, FINSEQ_1:90; then A23: f = k1 by A22, A15, FINSEQ_1:def_8; JUMP I = {k1} by A21, Th16; hence f in JUMP I by A23, TARSKI:def_1; ::_thesis: verum end; suppose ex a being Data-Location ex k being Nat st I = a =0_goto k ; ::_thesis: f in JUMP I then consider a being Data-Location, k1 being Nat such that A24: I = a =0_goto k1 ; A25: JumpPart I = <*k1*> by A24, RECDEF_2:def_2; then k = 1 by A14, FINSEQ_1:90; then A26: f = k1 by A25, A15, FINSEQ_1:40; JUMP I = {k1} by A24, Th18; hence f in JUMP I by A26, TARSKI:def_1; ::_thesis: verum end; suppose ex a being Data-Location ex k1 being Nat st I = a >0_goto k1 ; ::_thesis: f in JUMP I then consider a being Data-Location, k1 being Nat such that A27: I = a >0_goto k1 ; A28: JumpPart I = <*k1*> by A27, RECDEF_2:def_2; then k = 1 by A14, FINSEQ_1:90; then A29: f = k1 by A28, A15, FINSEQ_1:40; JUMP I = {k1} by A27, Th20; hence f in JUMP I by A29, TARSKI:def_1; ::_thesis: verum end; end; end; end; theorem Th23: :: AMI_6:23 for i1 being Element of NAT for k being Nat holds IncAddr ((SCM-goto i1),k) = SCM-goto (i1 + k) proof let i1 be Element of NAT ; ::_thesis: for k being Nat holds IncAddr ((SCM-goto i1),k) = SCM-goto (i1 + k) let k be Nat; ::_thesis: IncAddr ((SCM-goto i1),k) = SCM-goto (i1 + k) A1: JumpPart (IncAddr ((SCM-goto i1),k)) = k + (JumpPart (SCM-goto i1)) by COMPOS_0:def_9; then A2: dom (JumpPart (IncAddr ((SCM-goto i1),k))) = dom (JumpPart (SCM-goto i1)) by VALUED_1:def_2; A3: dom (JumpPart (SCM-goto (i1 + k))) = dom <*(i1 + k)*> by RECDEF_2:def_2 .= Seg 1 by FINSEQ_1:def_8 .= dom <*i1*> by FINSEQ_1:def_8 .= dom (JumpPart (SCM-goto i1)) by RECDEF_2:def_2 ; A4: for x being set st x in dom (JumpPart (SCM-goto i1)) holds (JumpPart (IncAddr ((SCM-goto i1),k))) . x = (JumpPart (SCM-goto (i1 + k))) . x proof let x be set ; ::_thesis: ( x in dom (JumpPart (SCM-goto i1)) implies (JumpPart (IncAddr ((SCM-goto i1),k))) . x = (JumpPart (SCM-goto (i1 + k))) . x ) assume A5: x in dom (JumpPart (SCM-goto i1)) ; ::_thesis: (JumpPart (IncAddr ((SCM-goto i1),k))) . x = (JumpPart (SCM-goto (i1 + k))) . x then x in dom <*i1*> by RECDEF_2:def_2; then A6: x = 1 by FINSEQ_1:90; set f = (JumpPart (SCM-goto i1)) . x; A7: (JumpPart (IncAddr ((SCM-goto i1),k))) . x = k + ((JumpPart (SCM-goto i1)) . x) by A5, A2, A1, VALUED_1:def_2; (JumpPart (SCM-goto i1)) . x = <*i1*> . x by RECDEF_2:def_2 .= i1 by A6, FINSEQ_1:def_8 ; hence (JumpPart (IncAddr ((SCM-goto i1),k))) . x = <*(i1 + k)*> . x by A6, A7, FINSEQ_1:def_8 .= (JumpPart (SCM-goto (i1 + k))) . x by RECDEF_2:def_2 ; ::_thesis: verum end; A8: AddressPart (IncAddr ((SCM-goto i1),k)) = AddressPart (SCM-goto i1) by COMPOS_0:def_9 .= {} by RECDEF_2:def_3 .= AddressPart (SCM-goto (i1 + k)) by RECDEF_2:def_3 ; A9: InsCode (IncAddr ((SCM-goto i1),k)) = InsCode (SCM-goto i1) by COMPOS_0:def_9 .= 6 by RECDEF_2:def_1 .= InsCode (SCM-goto (i1 + k)) by RECDEF_2:def_1 ; JumpPart (IncAddr ((SCM-goto i1),k)) = JumpPart (SCM-goto (i1 + k)) by A2, A3, A4, FUNCT_1:2; hence IncAddr ((SCM-goto i1),k) = SCM-goto (i1 + k) by A8, A9, COMPOS_0:1; ::_thesis: verum end; theorem Th24: :: AMI_6:24 for a being Data-Location for i1 being Element of NAT for k being Nat holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k) proof let a be Data-Location; ::_thesis: for i1 being Element of NAT for k being Nat holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k) let i1 be Element of NAT ; ::_thesis: for k being Nat holds IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k) let k be Nat; ::_thesis: IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k) A1: JumpPart (IncAddr ((a =0_goto i1),k)) = k + (JumpPart (a =0_goto i1)) by COMPOS_0:def_9; then A2: dom (JumpPart (IncAddr ((a =0_goto i1),k))) = dom (JumpPart (a =0_goto i1)) by VALUED_1:def_2; A3: dom (JumpPart (a =0_goto (i1 + k))) = dom <*(i1 + k)*> by RECDEF_2:def_2 .= Seg 1 by FINSEQ_1:38 .= dom <*i1*> by FINSEQ_1:38 .= dom (JumpPart (a =0_goto i1)) by RECDEF_2:def_2 ; A4: for x being set st x in dom (JumpPart (a =0_goto i1)) holds (JumpPart (IncAddr ((a =0_goto i1),k))) . x = (JumpPart (a =0_goto (i1 + k))) . x proof let x be set ; ::_thesis: ( x in dom (JumpPart (a =0_goto i1)) implies (JumpPart (IncAddr ((a =0_goto i1),k))) . x = (JumpPart (a =0_goto (i1 + k))) . x ) assume A5: x in dom (JumpPart (a =0_goto i1)) ; ::_thesis: (JumpPart (IncAddr ((a =0_goto i1),k))) . x = (JumpPart (a =0_goto (i1 + k))) . x then x in dom <*i1*> by RECDEF_2:def_2; then A6: x = 1 by FINSEQ_1:90; set f = (JumpPart (a =0_goto i1)) . x; A7: (JumpPart (IncAddr ((a =0_goto i1),k))) . x = k + ((JumpPart (a =0_goto i1)) . x) by A1, A2, A5, VALUED_1:def_2; (JumpPart (a =0_goto i1)) . x = <*i1*> . x by RECDEF_2:def_2 .= i1 by A6, FINSEQ_1:40 ; hence (JumpPart (IncAddr ((a =0_goto i1),k))) . x = <*(i1 + k)*> . x by A6, A7, FINSEQ_1:40 .= (JumpPart (a =0_goto (i1 + k))) . x by RECDEF_2:def_2 ; ::_thesis: verum end; A8: AddressPart (IncAddr ((a =0_goto i1),k)) = AddressPart (a =0_goto i1) by COMPOS_0:def_9 .= <*a*> by RECDEF_2:def_3 .= AddressPart (a =0_goto (i1 + k)) by RECDEF_2:def_3 ; A9: InsCode (IncAddr ((a =0_goto i1),k)) = InsCode (a =0_goto i1) by COMPOS_0:def_9 .= 7 by RECDEF_2:def_1 .= InsCode (a =0_goto (i1 + k)) by RECDEF_2:def_1 ; JumpPart (IncAddr ((a =0_goto i1),k)) = JumpPart (a =0_goto (i1 + k)) by A2, A3, A4, FUNCT_1:2; hence IncAddr ((a =0_goto i1),k) = a =0_goto (i1 + k) by A8, A9, COMPOS_0:1; ::_thesis: verum end; theorem Th25: :: AMI_6:25 for a being Data-Location for i1 being Element of NAT for k being Nat holds IncAddr ((a >0_goto i1),k) = a >0_goto (i1 + k) proof let a be Data-Location; ::_thesis: for i1 being Element of NAT for k being Nat holds IncAddr ((a >0_goto i1),k) = a >0_goto (i1 + k) let i1 be Element of NAT ; ::_thesis: for k being Nat holds IncAddr ((a >0_goto i1),k) = a >0_goto (i1 + k) let k be Nat; ::_thesis: IncAddr ((a >0_goto i1),k) = a >0_goto (i1 + k) A1: JumpPart (IncAddr ((a >0_goto i1),k)) = k + (JumpPart (a >0_goto i1)) by COMPOS_0:def_9; then A2: dom (JumpPart (IncAddr ((a >0_goto i1),k))) = dom (JumpPart (a >0_goto i1)) by VALUED_1:def_2; A3: dom (JumpPart (a >0_goto (i1 + k))) = dom <*(i1 + k)*> by RECDEF_2:def_2 .= Seg 1 by FINSEQ_1:38 .= dom <*i1*> by FINSEQ_1:38 .= dom (JumpPart (a >0_goto i1)) by RECDEF_2:def_2 ; A4: for x being set st x in dom (JumpPart (a >0_goto i1)) holds (JumpPart (IncAddr ((a >0_goto i1),k))) . x = (JumpPart (a >0_goto (i1 + k))) . x proof let x be set ; ::_thesis: ( x in dom (JumpPart (a >0_goto i1)) implies (JumpPart (IncAddr ((a >0_goto i1),k))) . x = (JumpPart (a >0_goto (i1 + k))) . x ) assume A5: x in dom (JumpPart (a >0_goto i1)) ; ::_thesis: (JumpPart (IncAddr ((a >0_goto i1),k))) . x = (JumpPart (a >0_goto (i1 + k))) . x then x in dom <*i1*> by RECDEF_2:def_2; then A6: x = 1 by FINSEQ_1:90; set f = (JumpPart (a >0_goto i1)) . x; A7: (JumpPart (IncAddr ((a >0_goto i1),k))) . x = k + ((JumpPart (a >0_goto i1)) . x) by A1, A2, A5, VALUED_1:def_2; (JumpPart (a >0_goto i1)) . x = <*i1*> . x by RECDEF_2:def_2 .= i1 by A6, FINSEQ_1:40 ; hence (JumpPart (IncAddr ((a >0_goto i1),k))) . x = <*(i1 + k)*> . x by A6, A7, FINSEQ_1:40 .= (JumpPart (a >0_goto (i1 + k))) . x by RECDEF_2:def_2 ; ::_thesis: verum end; A8: AddressPart (IncAddr ((a >0_goto i1),k)) = AddressPart (a >0_goto i1) by COMPOS_0:def_9 .= <*a*> by RECDEF_2:def_3 .= AddressPart (a >0_goto (i1 + k)) by RECDEF_2:def_3 ; A9: InsCode (IncAddr ((a >0_goto i1),k)) = InsCode (a >0_goto i1) by COMPOS_0:def_9 .= 8 by RECDEF_2:def_1 .= InsCode (a >0_goto (i1 + k)) by RECDEF_2:def_1 ; JumpPart (IncAddr ((a >0_goto i1),k)) = JumpPart (a >0_goto (i1 + k)) by A2, A3, A4, FUNCT_1:2; hence IncAddr ((a >0_goto i1),k) = a >0_goto (i1 + k) by A8, A9, COMPOS_0:1; ::_thesis: verum end; registration cluster SCM -> IC-relocable ; coherence SCM is IC-relocable proof thus SCM is IC-relocable ::_thesis: verum proof let I be Instruction of SCM; :: according to AMISTD_2:def_4 ::_thesis: I is IC-relocable percases ( I = [0,{},{}] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo (a,b) or ex a, b being Data-Location st I = SubFrom (a,b) or ex a, b being Data-Location st I = MultBy (a,b) or ex a, b being Data-Location st I = Divide (a,b) or ex k being Nat st I = SCM-goto k or ex a being Data-Location ex k being Nat st I = a =0_goto k or ex a being Data-Location ex k being Nat st I = a >0_goto k ) by AMI_3:24; suppose I = [0,{},{}] ; ::_thesis: I is IC-relocable hence I is IC-relocable by AMI_3:26; ::_thesis: verum end; suppose ex a, b being Data-Location st I = a := b ; ::_thesis: I is IC-relocable hence I is IC-relocable ; ::_thesis: verum end; suppose ex a, b being Data-Location st I = AddTo (a,b) ; ::_thesis: I is IC-relocable hence I is IC-relocable ; ::_thesis: verum end; suppose ex a, b being Data-Location st I = SubFrom (a,b) ; ::_thesis: I is IC-relocable hence I is IC-relocable ; ::_thesis: verum end; suppose ex a, b being Data-Location st I = MultBy (a,b) ; ::_thesis: I is IC-relocable hence I is IC-relocable ; ::_thesis: verum end; suppose ex a, b being Data-Location st I = Divide (a,b) ; ::_thesis: I is IC-relocable hence I is IC-relocable ; ::_thesis: verum end; supposeA1: ex k being Nat st I = SCM-goto k ; ::_thesis: I is IC-relocable let j, k be Nat; :: according to AMISTD_2:def_3 ::_thesis: for b1 being set holds K357((IC (Exec ((IncAddr (I,j)),b1))),k) = IC (Exec ((IncAddr (I,(j + k))),(IncIC (b1,k)))) let s1 be State of SCM; ::_thesis: K357((IC (Exec ((IncAddr (I,j)),s1))),k) = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) set s2 = IncIC (s1,k); consider k1 being Nat such that A2: I = SCM-goto k1 by A1; reconsider i1 = k1 as Element of NAT by ORDINAL1:def_12; IC (Exec (I,s1)) = k1 by A2, AMI_3:7; hence (IC (Exec ((IncAddr (I,j)),s1))) + k = (IC (Exec ((SCM-goto (j + k1)),s1))) + k by A2, Th23 .= (j + k1) + k by AMI_3:7 .= IC (Exec ((SCM-goto ((j + i1) + k)),(IncIC (s1,k)))) by AMI_3:7 .= IC (Exec ((SCM-goto ((j + k) + i1)),(IncIC (s1,k)))) .= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A2, Th23 ; ::_thesis: verum end; suppose ex a being Data-Location ex k being Nat st I = a =0_goto k ; ::_thesis: I is IC-relocable then consider a being Data-Location, k1 being Nat such that A3: I = a =0_goto k1 ; reconsider i1 = k1 as Element of NAT by ORDINAL1:def_12; let j, k be Nat; :: according to AMISTD_2:def_3 ::_thesis: for b1 being set holds K357((IC (Exec ((IncAddr (I,j)),b1))),k) = IC (Exec ((IncAddr (I,(j + k))),(IncIC (b1,k)))) let s1 be State of SCM; ::_thesis: K357((IC (Exec ((IncAddr (I,j)),s1))),k) = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) set s2 = IncIC (s1,k); ( a <> IC & dom ((IC ) .--> ((IC s1) + k)) = {(IC )} ) by AMI_5:2, FUNCOP_1:13; then not a in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def_1; then A4: s1 . a = (IncIC (s1,k)) . a by FUNCT_4:11; now__::_thesis:_(IC_(Exec_((IncAddr_(I,j)),s1)))_+_k_=_IC_(Exec_((IncAddr_(I,(j_+_k))),(IncIC_(s1,k)))) percases ( s1 . a = 0 or s1 . a <> 0 ) ; supposeA5: s1 . a = 0 ; ::_thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) then IC (Exec (I,s1)) = k1 by A3, AMI_3:8; hence (IC (Exec ((IncAddr (I,j)),s1))) + k = (IC (Exec ((a =0_goto (j + k1)),s1))) + k by A3, Th24 .= (j + k1) + k by A5, AMI_3:8 .= IC (Exec ((a =0_goto ((j + i1) + k)),(IncIC (s1,k)))) by A4, A5, AMI_3:8 .= IC (Exec ((a =0_goto ((j + k) + i1)),(IncIC (s1,k)))) .= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A3, Th24 ; ::_thesis: verum end; supposeA6: s1 . a <> 0 ; ::_thesis: (IC (Exec ((IncAddr (I,j)),s1))) + k = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) A7: IncAddr (I,j) = a =0_goto (i1 + j) by A3, Th24; A8: IncAddr (I,(j + k)) = a =0_goto (i1 + (j + k)) by A3, Th24; dom ((IC ) .--> ((IC s1) + k)) = {(IC )} by FUNCOP_1:13; then IC in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def_1; then A9: IC (IncIC (s1,k)) = ((IC ) .--> ((IC s1) + k)) . (IC ) by FUNCT_4:13 .= (IC s1) + k by FUNCOP_1:72 ; thus (IC (Exec ((IncAddr (I,j)),s1))) + k = (succ (IC s1)) + k by A7, A6, AMI_3:8 .= ((IC s1) + 1) + k .= succ (IC (IncIC (s1,k))) by A9 .= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A8, A6, A4, AMI_3:8 ; ::_thesis: verum end; end; end; hence K357((IC (Exec ((IncAddr (I,j)),s1))),k) = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) ; ::_thesis: verum end; suppose ex a being Data-Location ex k being Nat st I = a >0_goto k ; ::_thesis: I is IC-relocable then consider a being Data-Location, k1 being Nat such that A10: I = a >0_goto k1 ; reconsider i1 = k1 as Element of NAT by ORDINAL1:def_12; let j, k be Nat; :: according to AMISTD_2:def_3 ::_thesis: for b1 being set holds K357((IC (Exec ((IncAddr (I,j)),b1))),k) = IC (Exec ((IncAddr (I,(j + k))),(IncIC (b1,k)))) let s1 be State of SCM; ::_thesis: K357((IC (Exec ((IncAddr (I,j)),s1))),k) = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) set s2 = IncIC (s1,k); ( a <> IC & dom ((IC ) .--> ((IC s1) + k)) = {(IC )} ) by AMI_5:2, FUNCOP_1:13; then not a in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def_1; then A11: s1 . a = (IncIC (s1,k)) . a by FUNCT_4:11; percases ( s1 . a > 0 or s1 . a <= 0 ) ; supposeA12: s1 . a > 0 ; ::_thesis: K357((IC (Exec ((IncAddr (I,j)),s1))),k) = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) then IC (Exec (I,s1)) = k1 by A10, AMI_3:9; hence (IC (Exec ((IncAddr (I,j)),s1))) + k = (IC (Exec ((a >0_goto (j + k1)),s1))) + k by A10, Th25 .= (j + k1) + k by A12, AMI_3:9 .= IC (Exec ((a >0_goto ((j + i1) + k)),(IncIC (s1,k)))) by A11, A12, AMI_3:9 .= IC (Exec ((a >0_goto ((j + k) + i1)),(IncIC (s1,k)))) .= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A10, Th25 ; ::_thesis: verum end; supposeA13: s1 . a <= 0 ; ::_thesis: K357((IC (Exec ((IncAddr (I,j)),s1))),k) = IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) A14: IncAddr (I,j) = a >0_goto (i1 + j) by A10, Th25; A15: IncAddr (I,(j + k)) = a >0_goto (i1 + (j + k)) by A10, Th25; dom ((IC ) .--> ((IC s1) + k)) = {(IC )} by FUNCOP_1:13; then IC in dom ((IC ) .--> ((IC s1) + k)) by TARSKI:def_1; then A16: IC (IncIC (s1,k)) = ((IC ) .--> ((IC s1) + k)) . (IC ) by FUNCT_4:13 .= (IC s1) + k by FUNCOP_1:72 ; thus (IC (Exec ((IncAddr (I,j)),s1))) + k = (succ (IC s1)) + k by A14, A13, AMI_3:9 .= ((IC s1) + 1) + k .= succ (IC (IncIC (s1,k))) by A16 .= IC (Exec ((IncAddr (I,(j + k))),(IncIC (s1,k)))) by A15, A13, A11, AMI_3:9 ; ::_thesis: verum end; end; end; end; end; end; end;