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 I = [0 ,{} ] ; :: thesis: ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT )

hence ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT ) by A27, 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 )

hence ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT ) by A27; :: 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 )

hence ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT ) by A27; :: 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 )

hence ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT ) by A27; :: 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 )

hence ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT ) by A27; :: 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 )

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

end;

suppose A28: 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 )

take 1 ; :: thesis: ( 1 in dom (AddressPart I) & f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT )
consider i1 being Instruction-Location of SCM such that
A29: I = goto i1 by A28;
A30: 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 A29, A30, FINSEQ_1:4, TARSKI:def 1; :: thesis: ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT )
JUMP (goto i1) = {i1} by Th47;
then f = i1 by A27, A29, TARSKI:def 1;
hence ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT ) by A29, A30, Th35, FINSEQ_1:def 8; :: thesis: verum

end;

suppose A31: 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 )

take 1 ; :: thesis: ( 1 in dom (AddressPart I) & f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT )
consider a being Data-Location , i1 being Instruction-Location of SCM such that
A32: I = a =0_goto i1 by A31;
A33: 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 A32, A33, FINSEQ_1:4, TARSKI:def 2; :: thesis: ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT )
JUMP (a =0_goto i1) = {i1} by Th49;
then f = i1 by A27, A32, TARSKI:def 1;
hence ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT ) by A32, A33, Th36, FINSEQ_1:61; :: thesis: verum

end;

suppose A34: 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 )

take 1 ; :: thesis: ( 1 in dom (AddressPart I) & f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT )
consider a being Data-Location , i1 being Instruction-Location of SCM such that
A35: I = a >0_goto i1 by A34;
A36: 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 A35, A36, FINSEQ_1:4, TARSKI:def 2; :: thesis: ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT )
JUMP (a >0_goto i1) = {i1} by Th51;
then f = i1 by A27, A35, TARSKI:def 1;
hence ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT ) by A35, A36, 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 A37: k in dom (AddressPart I) and
A38: f = (AddressPart I) . k and
A39: (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 A37; :: 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
A40: I = a := b ;
k in dom <*a,b*> by A37, A40, MCART_1:def 2;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A39, A40, 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
A41: I = AddTo a,b ;
k in dom <*a,b*> by A37, A41, MCART_1:def 2;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A39, A41, 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
A42: I = SubFrom a,b ;
k in dom <*a,b*> by A37, A42, MCART_1:def 2;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A39, A42, 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
A43: I = MultBy a,b ;
k in dom <*a,b*> by A37, A43, MCART_1:def 2;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A39, A43, 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
A44: I = Divide a,b ;
k in dom <*a,b*> by A37, A44, MCART_1:def 2;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A39, A44, 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
A45: I = goto i1 ;
A46: AddressPart I = <*i1*> by A45, MCART_1:def 2;
then k = 1 by A37, Lm1;
then A47: f = i1 by A38, A46, FINSEQ_1:def 8;
JUMP I = {i1} by A45, Th47;
hence f in JUMP I by A47, 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
A48: I = a =0_goto i1 ;
A49: AddressPart I = <*i1,a*> by A48, MCART_1:def 2;
then ( k = 1 or k = 2 ) by A37, Lm2;
then A50: f = i1 by A38, A39, A48, A49, Th2, Th37, FINSEQ_1:61;
JUMP I = {i1} by A48, Th49;
hence f in JUMP I by A50, 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
A51: I = a >0_goto i1 ;
A52: AddressPart I = <*i1,a*> by A51, MCART_1:def 2;
then ( k = 1 or k = 2 ) by A37, Lm2;
then A53: f = i1 by A38, A39, A51, A52, Th2, Th39, FINSEQ_1:61;
JUMP I = {i1} by A51, Th51;
hence f in JUMP I by A53, TARSKI:def 1; :: thesis: verum

end;

end;