thus SCM is homogeneous :: thesis: ( SCM is with_explicit_jumps & SCM is without_implicit_jumps )

proof

let I, J be Instruction of SCM ; :: according to AMISTD_2:def 4 :: thesis: ( not InsCode I = InsCode J or dom (AddressPart I) = dom (AddressPart J) )
assume A1: InsCode I = InsCode J ; :: thesis: dom (AddressPart I) = dom (AddressPart J)
A2: ( J = [0 ,{} ] or ex a, b being Data-Location st J = a := b or ex a, b being Data-Location st J = AddTo a,b or ex a, b being Data-Location st J = SubFrom a,b or ex a, b being Data-Location st J = MultBy a,b or ex a, b being Data-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM st J = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a =0_goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a >0_goto i1 ) by AMI_3:69;

per cases ( I = [0 ,{} ] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo a,b or ex a, b being Data-Location st I = SubFrom a,b or ex a, b being Data-Location st I = MultBy a,b or ex a, b being Data-Location st I = Divide a,b or ex i1 being Instruction-Location of SCM st I = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a =0_goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a >0_goto i1 ) by AMI_3:69;

suppose I = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A2, AMI_3:71, AMI_5:37, MCART_1:7; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = a := b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider a, b being Data-Location such that
A3: I = a := b ;
A4: InsCode I = 1 by A3, MCART_1:7;

now

per cases ( J = [0 ,{} ] or ex a, b being Data-Location st J = a := b or ex a, b being Data-Location st J = AddTo a,b or ex a, b being Data-Location st J = SubFrom a,b or ex a, b being Data-Location st J = MultBy a,b or ex a, b being Data-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM st J = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a =0_goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a >0_goto i1 ) by AMI_3:69;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A3, AMI_3:71; :: thesis: verum

end;

suppose ex a, b being Data-Location st J = a := b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider d1, d2 being Data-Location such that
A5: J = d1 := d2 ;
thus dom (AddressPart I) = dom <*a,b*> by A3, MCART_1:def 2
.= Seg 2 by FINSEQ_3:29
.= dom <*d1,d2*> by FINSEQ_3:29
.= dom (AddressPart J) by A5, MCART_1:def 2 ; :: thesis: verum

end;

suppose ( ex a, b being Data-Location st J = AddTo a,b or ex a, b being Data-Location st J = SubFrom a,b or ex a, b being Data-Location st J = MultBy a,b or ex a, b being Data-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM st J = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a =0_goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a >0_goto i1 ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A4, MCART_1:7; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = AddTo a,b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider a, b being Data-Location such that
A6: I = AddTo a,b ;
A7: InsCode I = 2 by A6, MCART_1:7;

now

per cases ( J = [0 ,{} ] or ex a, b being Data-Location st J = AddTo a,b or ex a, b being Data-Location st J = a := b or ex a, b being Data-Location st J = SubFrom a,b or ex a, b being Data-Location st J = MultBy a,b or ex a, b being Data-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM st J = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a =0_goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a >0_goto i1 ) by AMI_3:69;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A6, AMI_3:71; :: thesis: verum

end;

suppose ex a, b being Data-Location st J = AddTo a,b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider d1, d2 being Data-Location such that
A8: J = AddTo d1,d2 ;
thus dom (AddressPart I) = dom <*a,b*> by A6, MCART_1:def 2
.= Seg 2 by FINSEQ_3:29
.= dom <*d1,d2*> by FINSEQ_3:29
.= dom (AddressPart J) by A8, MCART_1:def 2 ; :: thesis: verum

end;

suppose ( ex a, b being Data-Location st J = a := b or ex a, b being Data-Location st J = SubFrom a,b or ex a, b being Data-Location st J = MultBy a,b or ex a, b being Data-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM st J = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a =0_goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a >0_goto i1 ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A7, MCART_1:7; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = SubFrom a,b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider a, b being Data-Location such that
A9: I = SubFrom a,b ;
A10: InsCode I = 3 by A9, MCART_1:7;

now

per cases ( J = [0 ,{} ] or ex a, b being Data-Location st J = SubFrom a,b or ex a, b being Data-Location st J = a := b or ex a, b being Data-Location st J = AddTo a,b or ex a, b being Data-Location st J = MultBy a,b or ex a, b being Data-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM st J = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a =0_goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a >0_goto i1 ) by AMI_3:69;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A9, AMI_3:71; :: thesis: verum

end;

suppose ex a, b being Data-Location st J = SubFrom a,b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider d1, d2 being Data-Location such that
A11: J = SubFrom d1,d2 ;
thus dom (AddressPart I) = dom <*a,b*> by A9, MCART_1:def 2
.= Seg 2 by FINSEQ_3:29
.= dom <*d1,d2*> by FINSEQ_3:29
.= dom (AddressPart J) by A11, MCART_1:def 2 ; :: thesis: verum

end;

suppose ( ex a, b being Data-Location st J = a := b or ex a, b being Data-Location st J = AddTo a,b or ex a, b being Data-Location st J = MultBy a,b or ex a, b being Data-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM st J = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a =0_goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a >0_goto i1 ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A10, MCART_1:7; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = MultBy a,b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider a, b being Data-Location such that
A12: I = MultBy a,b ;
A13: InsCode I = 4 by A12, MCART_1:7;

now

per cases ( J = [0 ,{} ] or ex a, b being Data-Location st J = MultBy a,b or ex a, b being Data-Location st J = a := b or ex a, b being Data-Location st J = AddTo a,b or ex a, b being Data-Location st J = SubFrom a,b or ex a, b being Data-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM st J = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a =0_goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a >0_goto i1 ) by AMI_3:69;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A12, AMI_3:71; :: thesis: verum

end;

suppose ex a, b being Data-Location st J = MultBy a,b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider d1, d2 being Data-Location such that
A14: J = MultBy d1,d2 ;
thus dom (AddressPart I) = dom <*a,b*> by A12, MCART_1:def 2
.= Seg 2 by FINSEQ_3:29
.= dom <*d1,d2*> by FINSEQ_3:29
.= dom (AddressPart J) by A14, MCART_1:def 2 ; :: thesis: verum

end;

suppose ( ex a, b being Data-Location st J = a := b or ex a, b being Data-Location st J = AddTo a,b or ex a, b being Data-Location st J = SubFrom a,b or ex a, b being Data-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM st J = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a =0_goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a >0_goto i1 ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A13, MCART_1:7; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = Divide a,b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider a, b being Data-Location such that
A15: I = Divide a,b ;
A16: InsCode I = 5 by A15, MCART_1:7;

now

per cases ( J = [0 ,{} ] or ex a, b being Data-Location st J = Divide a,b or ex a, b being Data-Location st J = a := b or ex a, b being Data-Location st J = AddTo a,b or ex a, b being Data-Location st J = SubFrom a,b or ex a, b being Data-Location st J = MultBy a,b or ex i1 being Instruction-Location of SCM st J = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a =0_goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a >0_goto i1 ) by AMI_3:69;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A15, AMI_3:71; :: thesis: verum

end;

suppose ex a, b being Data-Location st J = Divide a,b ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider d1, d2 being Data-Location such that
A17: J = Divide d1,d2 ;
thus dom (AddressPart I) = dom <*a,b*> by A15, MCART_1:def 2
.= Seg 2 by FINSEQ_3:29
.= dom <*d1,d2*> by FINSEQ_3:29
.= dom (AddressPart J) by A17, MCART_1:def 2 ; :: thesis: verum

end;

suppose ( ex a, b being Data-Location st J = a := b or ex a, b being Data-Location st J = AddTo a,b or ex a, b being Data-Location st J = SubFrom a,b or ex a, b being Data-Location st J = MultBy a,b or ex i1 being Instruction-Location of SCM st J = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a =0_goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a >0_goto i1 ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A16, MCART_1:7; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM st I = goto i1 ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider i1 being Instruction-Location of SCM such that
A18: I = goto i1 ;
A19: InsCode I = 6 by A18, MCART_1:7;

now

per cases ( J = [0 ,{} ] or ex i2 being Instruction-Location of SCM st J = goto i2 or ex a, b being Data-Location st J = a := b or ex a, b being Data-Location st J = AddTo a,b or ex a, b being Data-Location st J = SubFrom a,b or ex a, b being Data-Location st J = MultBy a,b or ex a, b being Data-Location st J = Divide a,b or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a =0_goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a >0_goto i1 ) by AMI_3:69;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A18, AMI_3:71, AMI_5:37, MCART_1:7; :: thesis: verum

end;

suppose ex i2 being Instruction-Location of SCM st J = goto i2 ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider i2 being Instruction-Location of SCM such that
A20: J = goto i2 ;
thus dom (AddressPart I) = dom <*i1*> by A18, MCART_1:def 2
.= Seg 1 by FINSEQ_1:def 8
.= dom <*i2*> by FINSEQ_1:def 8
.= dom (AddressPart J) by A20, MCART_1:def 2 ; :: thesis: verum

end;

suppose ( ex a, b being Data-Location st J = a := b or ex a, b being Data-Location st J = AddTo a,b or ex a, b being Data-Location st J = SubFrom a,b or ex a, b being Data-Location st J = MultBy a,b or ex a, b being Data-Location st J = Divide a,b or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a =0_goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a >0_goto i1 ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A19, MCART_1:7; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

suppose ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a =0_goto i1 ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider a being Data-Location , i1 being Instruction-Location of SCM such that
A21: I = a =0_goto i1 ;
A22: InsCode I = 7 by A21, MCART_1:7;

now

per cases ( J = [0 ,{} ] or ex d1 being Data-Location ex i2 being Instruction-Location of SCM st J = d1 =0_goto i2 or ex a, b being Data-Location st J = a := b or ex a, b being Data-Location st J = AddTo a,b or ex a, b being Data-Location st J = SubFrom a,b or ex a, b being Data-Location st J = MultBy a,b or ex a, b being Data-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM st J = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a >0_goto i1 ) by AMI_3:69;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A21, AMI_3:71, AMI_5:37, MCART_1:7; :: thesis: verum

end;

suppose ex d1 being Data-Location ex i2 being Instruction-Location of SCM st J = d1 =0_goto i2 ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider d1 being Data-Location , i2 being Instruction-Location of SCM such that
A23: J = d1 =0_goto i2 ;
thus dom (AddressPart I) = dom <*i1,a*> by A21, MCART_1:def 2
.= Seg 2 by FINSEQ_3:29
.= dom <*i2,d1*> by FINSEQ_3:29
.= dom (AddressPart J) by A23, MCART_1:def 2 ; :: thesis: verum

end;

suppose ( ex a, b being Data-Location st J = a := b or ex a, b being Data-Location st J = AddTo a,b or ex a, b being Data-Location st J = SubFrom a,b or ex a, b being Data-Location st J = MultBy a,b or ex a, b being Data-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM st J = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a >0_goto i1 ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A22, MCART_1:7; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

suppose ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a >0_goto i1 ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider a being Data-Location , i1 being Instruction-Location of SCM such that
A24: I = a >0_goto i1 ;
A25: InsCode I = 8 by A24, MCART_1:7;

now

per cases ( J = [0 ,{} ] or ex d1 being Data-Location ex i2 being Instruction-Location of SCM st J = d1 >0_goto i2 or ex a, b being Data-Location st J = a := b or ex a, b being Data-Location st J = AddTo a,b or ex a, b being Data-Location st J = SubFrom a,b or ex a, b being Data-Location st J = MultBy a,b or ex a, b being Data-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM st J = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a =0_goto i1 ) by AMI_3:69;

suppose J = [0 ,{} ] ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A24, AMI_3:71, AMI_5:37, MCART_1:7; :: thesis: verum

end;

suppose ex d1 being Data-Location ex i2 being Instruction-Location of SCM st J = d1 >0_goto i2 ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider d1 being Data-Location , i2 being Instruction-Location of SCM such that
A26: J = d1 >0_goto i2 ;
thus dom (AddressPart I) = dom <*i1,a*> by A24, MCART_1:def 2
.= Seg 2 by FINSEQ_3:29
.= dom <*i2,d1*> by FINSEQ_3:29
.= dom (AddressPart J) by A26, MCART_1:def 2 ; :: thesis: verum

end;

suppose ( ex a, b being Data-Location st J = a := b or ex a, b being Data-Location st J = AddTo a,b or ex a, b being Data-Location st J = SubFrom a,b or ex a, b being Data-Location st J = MultBy a,b or ex a, b being Data-Location st J = Divide a,b or ex i1 being Instruction-Location of SCM st J = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st J = a =0_goto i1 ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A25, MCART_1:7; :: thesis: verum

end;

end;

end;

hence dom (AddressPart I) = dom (AddressPart J) ; :: thesis: verum

end;

end;

end;

thus SCM is with_explicit_jumps :: thesis: SCM is without_implicit_jumps

proof

let I be Instruction of SCM ; :: according to AMISTD_2:def 8 :: thesis: I is with_explicit_jumps
let f be set ; :: according to AMISTD_2:def 6 :: thesis: ( not f in JUMP I or ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT ) )
assume A27: f in JUMP I ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT )

per cases ( I = [0 ,{} ] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo a,b or ex a, b being Data-Location st I = SubFrom a,b or ex a, b being Data-Location st I = MultBy a,b or ex a, b being Data-Location st I = Divide a,b or ex i1 being Instruction-Location of SCM st I = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a =0_goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a >0_goto i1 ) by AMI_3:69;

suppose A28: I = [0 ,{} ] ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT )

thus ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT ) by A27, A28, AMI_3:71; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = a := b ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT )

then consider a, b being Data-Location such that
A29: I = a := b ;
thus ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT ) by A27, A29; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = AddTo a,b ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT )

then consider a, b being Data-Location such that
A30: I = AddTo a,b ;
thus ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT ) by A27, A30; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = SubFrom a,b ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT )

then consider a, b being Data-Location such that
A31: I = SubFrom a,b ;
thus ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT ) by A27, A31; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = MultBy a,b ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT )

then consider a, b being Data-Location such that
A32: I = MultBy a,b ;
thus ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT ) by A27, A32; :: thesis: verum

end;

suppose ex a, b being Data-Location st I = Divide a,b ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT )

then consider a, b being Data-Location such that
A33: I = Divide a,b ;
thus ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT ) by A27, A33; :: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM st I = goto i1 ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT )

then consider i1 being Instruction-Location of SCM such that
A34: I = goto i1 ;
JUMP (goto i1) = {i1} by Th47;
then A35: f = i1 by A27, A34, TARSKI:def 1;
take 1 ; :: thesis: ( 1 in dom (AddressPart I) & f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT )
A36: AddressPart (goto i1) = <*i1*> by MCART_1:def 2;
dom <*i1*> = Seg 1 by FINSEQ_1:def 8;
hence 1 in dom (AddressPart I) by A34, A36, FINSEQ_1:4, TARSKI:def 1; :: thesis: ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT )
thus ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT ) by A34, A35, A36, Th35, FINSEQ_1:def 8; :: thesis: verum

end;

suppose ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a =0_goto i1 ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT )

then consider a being Data-Location , i1 being Instruction-Location of SCM such that
A37: I = a =0_goto i1 ;
JUMP (a =0_goto i1) = {i1} by Th49;
then A38: f = i1 by A27, A37, TARSKI:def 1;
take 1 ; :: thesis: ( 1 in dom (AddressPart I) & f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT )
A39: AddressPart (a =0_goto i1) = <*i1,a*> by MCART_1:def 2;
dom <*i1,a*> = Seg 2 by FINSEQ_3:29;
hence 1 in dom (AddressPart I) by A37, A39, FINSEQ_1:4, TARSKI:def 2; :: thesis: ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT )
thus ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT ) by A37, A38, A39, Th36, FINSEQ_1:61; :: thesis: verum

end;

suppose ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a >0_goto i1 ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT )

then consider a being Data-Location , i1 being Instruction-Location of SCM such that
A40: I = a >0_goto i1 ;
JUMP (a >0_goto i1) = {i1} by Th51;
then A41: f = i1 by A27, A40, TARSKI:def 1;
take 1 ; :: thesis: ( 1 in dom (AddressPart I) & f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT )
A42: AddressPart (a >0_goto i1) = <*i1,a*> by MCART_1:def 2;
dom <*i1,a*> = Seg 2 by FINSEQ_3:29;
hence 1 in dom (AddressPart I) by A40, A42, FINSEQ_1:4, TARSKI:def 2; :: thesis: ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT )
thus ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT ) by A40, A41, A42, Th38, FINSEQ_1:61; :: thesis: verum

end;

end;

end;

let I be Instruction of SCM ; :: according to AMISTD_2:def 9 :: thesis: I is without_implicit_jumps
let f be set ; :: according to AMISTD_2:def 7 :: thesis: ( for b₁ being set holds
( not b₁ in dom (AddressPart I) or not f = (AddressPart I) . b₁ or not (product" (AddressParts (InsCode I))) . b₁ = NAT ) or f in JUMP I )
given k being set such that A43: k in dom (AddressPart I) and
A44: f = (AddressPart I) . k and
A45: (product" (AddressParts (InsCode I))) . k = NAT ; :: thesis: f in JUMP I

per cases ( I = [0 ,{} ] or ex a, b being Data-Location st I = a := b or ex a, b being Data-Location st I = AddTo a,b or ex a, b being Data-Location st I = SubFrom a,b or ex a, b being Data-Location st I = MultBy a,b or ex a, b being Data-Location st I = Divide a,b or ex i1 being Instruction-Location of SCM st I = goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a =0_goto i1 or ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a >0_goto i1 ) by AMI_3:69;

suppose I = [0 ,{} ] ; :: thesis: f in JUMP I

then dom (AddressPart I) = dom {} by MCART_1:def 2;
hence f in JUMP I by A43; :: 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
A46: I = a := b ;
k in dom <*a,b*> by A43, A46, MCART_1:def 2;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A45, A46, Th2, Th25, Th26; :: 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
A47: I = AddTo a,b ;
k in dom <*a,b*> by A43, A47, MCART_1:def 2;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A45, A47, Th2, Th27, Th28; :: 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
A48: I = SubFrom a,b ;
k in dom <*a,b*> by A43, A48, MCART_1:def 2;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A45, A48, Th2, Th29, Th30; :: 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
A49: I = MultBy a,b ;
k in dom <*a,b*> by A43, A49, MCART_1:def 2;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A45, A49, Th2, Th31, Th32; :: 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
A50: I = Divide a,b ;
k in dom <*a,b*> by A43, A50, MCART_1:def 2;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A45, A50, Th2, Th33, Th34; :: thesis: verum

end;

suppose ex i1 being Instruction-Location of SCM st I = goto i1 ; :: thesis: f in JUMP I

then consider i1 being Instruction-Location of SCM such that
A51: I = goto i1 ;
A52: AddressPart I = <*i1*> by A51, MCART_1:def 2;
then k = 1 by A43, Lm1;
then A53: f = i1 by A44, A52, FINSEQ_1:def 8;
JUMP I = {i1} by A51, Th47;
hence f in JUMP I by A53, TARSKI:def 1; :: thesis: verum

end;

suppose ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a =0_goto i1 ; :: thesis: f in JUMP I

then consider a being Data-Location , i1 being Instruction-Location of SCM such that
A54: I = a =0_goto i1 ;
A55: AddressPart I = <*i1,a*> by A54, MCART_1:def 2;
then ( k = 1 or k = 2 ) by A43, Lm2;
then A56: f = i1 by A44, A45, A54, A55, Th2, Th37, FINSEQ_1:61;
JUMP I = {i1} by A54, Th49;
hence f in JUMP I by A56, TARSKI:def 1; :: thesis: verum

end;

suppose ex a being Data-Location ex i1 being Instruction-Location of SCM st I = a >0_goto i1 ; :: thesis: f in JUMP I

then consider a being Data-Location , i1 being Instruction-Location of SCM such that
A57: I = a >0_goto i1 ;
A58: AddressPart I = <*i1,a*> by A57, MCART_1:def 2;
then ( k = 1 or k = 2 ) by A43, Lm2;
then A59: f = i1 by A44, A45, A57, A58, Th2, Th39, FINSEQ_1:61;
JUMP I = {i1} by A57, Th51;
hence f in JUMP I by A59, TARSKI:def 1; :: thesis: verum

end;

end;