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

proof

let I, J be Instruction of (SCM R); :: 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 of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) by SCMRING2:8;

per cases ( I = [0 ,{} ] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo a,b or ex a, b being Data-Location of R st I = SubFrom a,b or ex a, b being Data-Location of R st I = MultBy a,b or ex i1 being Element of NAT st I = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:8;

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

then I = halt (SCM R) by SCMRING2:30;
then InsCode I = 0 by Th8;
hence dom (AddressPart I) = dom (AddressPart J) by A1, A2, A3, MCART_1:def 1; :: thesis: verum

end;

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

then consider a, b being Data-Location of R such that
A4: I = a := b ;
A5: InsCode I = 1 by A4, MCART_1:def 1;

now

per cases ( J = [0 ,{} ] or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) by SCMRING2:8;

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

then J = halt (SCM R) by SCMRING2:30;
hence dom (AddressPart I) = dom (AddressPart J) by A1, A5, Th8; :: thesis: verum

end;

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

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

end;

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

hence dom (AddressPart I) = dom (AddressPart J) by A1, A5, MCART_1:def 1; :: thesis: verum

end;

end;

end;

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

end;

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

then consider a, b being Data-Location of R such that
A7: I = AddTo a,b ;
A8: InsCode I = 2 by A7, MCART_1:def 1;

now

per cases ( J = [0 ,{} ] or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) by SCMRING2:8;

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

then J = halt (SCM R) by SCMRING2:30;
hence dom (AddressPart I) = dom (AddressPart J) by A1, A8, Th8; :: thesis: verum

end;

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

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

end;

suppose ( ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A8, MCART_1:def 1; :: thesis: verum

end;

end;

end;

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

end;

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

then consider a, b being Data-Location of R such that
A10: I = SubFrom a,b ;
A11: InsCode I = 3 by A10, MCART_1:def 1;

now

per cases ( J = [0 ,{} ] or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) by SCMRING2:8;

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

then J = halt (SCM R) by SCMRING2:30;
hence dom (AddressPart I) = dom (AddressPart J) by A1, A11, Th8; :: thesis: verum

end;

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

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

end;

suppose ( ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A11, MCART_1:def 1; :: thesis: verum

end;

end;

end;

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

end;

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

then consider a, b being Data-Location of R such that
A13: I = MultBy a,b ;
A14: InsCode I = 4 by A13, MCART_1:def 1;

now

per cases ( J = [0 ,{} ] or ex a, b being Data-Location of R st J = MultBy a,b or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = SubFrom a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) by SCMRING2:8;

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

then J = halt (SCM R) by SCMRING2:30;
hence dom (AddressPart I) = dom (AddressPart J) by A1, A14, Th8; :: thesis: verum

end;

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

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

end;

suppose ( ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = SubFrom a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A14, MCART_1:def 1; :: thesis: verum

end;

end;

end;

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

end;

suppose ex i1 being Element of NAT st I = goto i1,R ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider i1 being Element of NAT such that
A16: I = goto i1,R ;
A17: InsCode I = 6 by A16, MCART_1:def 1;

now

per cases ( J = [0 ,{} ] or ex i2 being Element of NAT st J = goto i2,R or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) by SCMRING2:8;

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

then J = halt (SCM R) by SCMRING2:30;
hence dom (AddressPart I) = dom (AddressPart J) by A1, A17, Th8; :: thesis: verum

end;

suppose ex i2 being Element of NAT st J = goto i2,R ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider i2 being Element of NAT such that
A18: J = goto i2,R ;
thus dom (AddressPart I) = dom <*i1*> by A16, MCART_1:def 2
.= Seg 1 by FINSEQ_1:def 8
.= dom <*i2*> by FINSEQ_1:def 8
.= dom (AddressPart J) by A18, MCART_1:def 2 ; :: thesis: verum

end;

suppose ( ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st J = a := r ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A17, MCART_1:def 1; :: thesis: verum

end;

end;

end;

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

end;

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

then consider a being Data-Location of R, i1 being Element of NAT such that
A19: I = a =0_goto i1 ;
A20: InsCode I = 7 by A19, MCART_1:def 1;

now

per cases ( J = [0 ,{} ] or ex d1 being Data-Location of R ex i2 being Element of NAT st J = d1 =0_goto i2 or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex r being Element of R st J = a := r ) by SCMRING2:8;

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

then J = halt (SCM R) by SCMRING2:30;
hence dom (AddressPart I) = dom (AddressPart J) by A1, A20, Th8; :: thesis: verum

end;

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

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

end;

suppose ( ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex r being Element of R st J = a := r ) ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

hence dom (AddressPart I) = dom (AddressPart J) by A1, A20, MCART_1:def 1; :: thesis: verum

end;

end;

end;

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

end;

suppose ex a being Data-Location of R ex r being Element of R st I = a := r ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider a being Data-Location of R, r being Element of R such that
A22: I = a := r ;
A23: InsCode I = 5 by A22, MCART_1:def 1;

now

per cases ( J = [0 ,{} ] or ex a being Data-Location of R ex r being Element of R st J = a := r or ex a, b being Data-Location of R st J = a := b or ex a, b being Data-Location of R st J = AddTo a,b or ex a, b being Data-Location of R st J = SubFrom a,b or ex a, b being Data-Location of R st J = MultBy a,b or ex i1 being Element of NAT st J = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st J = a =0_goto i1 ) by SCMRING2:8;

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

then J = halt (SCM R) by SCMRING2:30;
hence dom (AddressPart I) = dom (AddressPart J) by A1, A23, Th8; :: thesis: verum

end;

suppose ex a being Data-Location of R ex r being Element of R st J = a := r ; :: thesis: dom (AddressPart I) = dom (AddressPart J)

then consider b being Data-Location of R, r1 being Element of R such that
A24: J = b := r1 ;
thus dom (AddressPart I) = dom <*a,r*> by A22, MCART_1:def 2
.= Seg 2 by FINSEQ_3:29
.= dom <*b,r1*> by FINSEQ_3:29
.= dom (AddressPart J) by A24, MCART_1:def 2 ; :: thesis: verum

end;

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

hence dom (AddressPart I) = dom (AddressPart J) by A1, A23, MCART_1:def 1; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

A25: SCM-Data-Loc <> NAT by AMI_2:12;
thus SCM R is with_explicit_jumps :: thesis: SCM R is without_implicit_jumps

proof

let I be Instruction of (SCM R); :: 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 A26: 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 of R st I = a := b or ex a, b being Data-Location of R st I = AddTo a,b or ex a, b being Data-Location of R st I = SubFrom a,b or ex a, b being Data-Location of R st I = MultBy a,b or ex i1 being Element of NAT st I = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:8;

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

JUMP (halt (SCM R)) is empty ;
hence ex b₁ being set st
( b₁ in dom (AddressPart I) & f = (AddressPart I) . b₁ & (product" (AddressParts (InsCode I))) . b₁ = NAT ) by A26, A27, SCMRING2:30; :: thesis: verum

end;

suppose ex a, b being Data-Location of R 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 A26; :: thesis: verum

end;

suppose ex a, b being Data-Location of R 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 A26; :: thesis: verum

end;

suppose ex a, b being Data-Location of R 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 A26; :: thesis: verum

end;

suppose ex a, b being Data-Location of R 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 A26; :: thesis: verum

end;

suppose A28: ex i1 being Element of NAT st I = goto i1,R ; :: 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 Element of NAT such that
A29: I = goto i1,R by A28;
A30: AddressPart (goto i1,R) = <*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,R) = {i1} by Th60;
then f = i1 by A26, A29, TARSKI:def 1;
hence ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT ) by A29, A30, Th50, FINSEQ_1:def 8; :: thesis: verum

end;

suppose A31: ex a being Data-Location of R ex i1 being Element of NAT 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 of R, i1 being Element of NAT 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 Th63;
then f = i1 by A26, A32, TARSKI:def 1;
hence ( f = (AddressPart I) . 1 & (product" (AddressParts (InsCode I))) . 1 = NAT ) by A32, A33, Th51, FINSEQ_1:61; :: thesis: verum

end;

suppose ex a being Data-Location of R ex r being Element of R st I = a := r ; :: 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 A26; :: thesis: verum

end;

end;

end;

let I be Instruction of (SCM R); :: 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 A34: k in dom (AddressPart I) and
A35: f = (AddressPart I) . k and
A36: (product" (AddressParts (InsCode I))) . k = NAT ; :: thesis: f in JUMP I

per cases ( I = [0 ,{} ] or ex a, b being Data-Location of R st I = a := b or ex a, b being Data-Location of R st I = AddTo a,b or ex a, b being Data-Location of R st I = SubFrom a,b or ex a, b being Data-Location of R st I = MultBy a,b or ex i1 being Element of NAT st I = goto i1,R or ex a being Data-Location of R ex i1 being Element of NAT st I = a =0_goto i1 or ex a being Data-Location of R ex r being Element of R st I = a := r ) by SCMRING2:8;

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

then I = halt (SCM R) by SCMRING2:30;
then dom (AddressPart I) = dom {} by Th24;
hence f in JUMP I by A34; :: thesis: verum

end;

suppose ex a, b being Data-Location of R st I = a := b ; :: thesis: f in JUMP I

then consider a, b being Data-Location of R such that
A37: I = a := b ;
k in dom <*a,b*> by A34, A37, MCART_1:def 2;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A36, A37, Th4, Th40, Th41; :: thesis: verum

end;

suppose ex a, b being Data-Location of R st I = AddTo a,b ; :: thesis: f in JUMP I

then consider a, b being Data-Location of R such that
A38: I = AddTo a,b ;
k in dom <*a,b*> by A34, A38, MCART_1:def 2;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A36, A38, Th4, Th42, Th43; :: thesis: verum

end;

suppose ex a, b being Data-Location of R st I = SubFrom a,b ; :: thesis: f in JUMP I

then consider a, b being Data-Location of R such that
A39: I = SubFrom a,b ;
k in dom <*a,b*> by A34, A39, MCART_1:def 2;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A36, A39, Th4, Th44, Th45; :: thesis: verum

end;

suppose ex a, b being Data-Location of R st I = MultBy a,b ; :: thesis: f in JUMP I

then consider a, b being Data-Location of R such that
A40: I = MultBy a,b ;
k in dom <*a,b*> by A34, A40, MCART_1:def 2;
then ( k = 1 or k = 2 ) by Lm2;
hence f in JUMP I by A36, A40, Th4, Th46, Th47; :: thesis: verum

end;

suppose ex i1 being Element of NAT st I = goto i1,R ; :: thesis: f in JUMP I

then consider i1 being Element of NAT such that
A41: I = goto i1,R ;
A42: AddressPart I = <*i1*> by A41, MCART_1:def 2;
then k = 1 by A34, Lm1;
then A43: f = i1 by A35, A42, FINSEQ_1:def 8;
JUMP I = {i1} by A41, Th60;
hence f in JUMP I by A43, TARSKI:def 1; :: thesis: verum

end;

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

then consider a being Data-Location of R, i1 being Element of NAT such that
A44: I = a =0_goto i1 ;
A45: AddressPart I = <*i1,a*> by A44, MCART_1:def 2;
then ( k = 1 or k = 2 ) by A34, Lm2;
then A46: f = i1 by A35, A36, A44, A45, Th4, Th52, FINSEQ_1:61;
JUMP I = {i1} by A44, Th63;
hence f in JUMP I by A46, TARSKI:def 1; :: thesis: verum

end;

suppose ex a being Data-Location of R ex r being Element of R st I = a := r ; :: thesis: f in JUMP I

then consider a being Data-Location of R, r being Element of R such that
A47: I = a := r ;
k in dom <*a,r*> by A34, A47, MCART_1:def 2;
then A48: ( k = 1 or k = 2 ) by Lm2;
(product" (AddressParts (InsCode I))) . 2 = the carrier of R by A47, Th49;
hence f in JUMP I by A36, A25, A47, A48, Th48, SCMRING1:def 2; :: thesis: verum

end;

end;