thus SCM is homogeneous :: thesis: SCM is with_explicit_jumps

proof

let I, J be Instruction of SCM; :: according to COMPOS_1:def 33 :: thesis: ( not InsCode I = InsCode J or dom (JumpPart I) = dom (JumpPart J) )
assume A1: InsCode I = InsCode J ; :: thesis: dom (JumpPart I) = dom (JumpPart 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 k being natural number st J = SCM-goto k or ex a being Data-Location ex k being natural number st J = a =0_goto k or ex a being Data-Location ex k being natural number st J = a >0_goto k ) 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 k being natural number st I = SCM-goto k or ex a being Data-Location ex k being natural number st I = a =0_goto k or ex a being Data-Location ex k being natural number st I = a >0_goto k ) by AMI_3:69;

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

hence dom (JumpPart I) = dom (JumpPart J) by A1, A2, AMI_3:71, AMI_5:37, RECDEF_2:def 1; :: thesis: verum

end;

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

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

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 k being natural number st J = SCM-goto k or ex a being Data-Location ex k being natural number st J = a =0_goto k or ex a being Data-Location ex k being natural number st J = a >0_goto k ) by AMI_3:69;

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

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

end;

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

then consider d1, d2 being Data-Location such that
A5: J = d1 := d2 ;
thus dom (JumpPart I) = dom {} by A3, RECDEF_2:def 2
.= dom (JumpPart J) by A5, RECDEF_2: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 k being natural number st J = SCM-goto k or ex a being Data-Location ex k being natural number st J = a =0_goto k or ex a being Data-Location ex k being natural number st J = a >0_goto k ) ; :: thesis: dom (JumpPart I) = dom (JumpPart J)

hence dom (JumpPart I) = dom (JumpPart J) by A1, A4, RECDEF_2:def 1; :: thesis: verum

end;

end;

end;

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

end;

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

then consider a, b being Data-Location such that
A6: I = AddTo (a,b) ;
A7: InsCode I = 2 by A6, RECDEF_2:def 1;

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 k being natural number st J = SCM-goto k or ex a being Data-Location ex k being natural number st J = a =0_goto k or ex a being Data-Location ex k being natural number st J = a >0_goto k ) by AMI_3:69;

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

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

end;

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

then consider d1, d2 being Data-Location such that
A8: J = AddTo (d1,d2) ;
thus dom (JumpPart I) = dom {} by A6, RECDEF_2:def 2
.= dom (JumpPart J) by A8, RECDEF_2: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 k being natural number st J = SCM-goto k or ex a being Data-Location ex k being natural number st J = a =0_goto k or ex a being Data-Location ex k being natural number st J = a >0_goto k ) ; :: thesis: dom (JumpPart I) = dom (JumpPart J)

hence dom (JumpPart I) = dom (JumpPart J) by A1, A7, RECDEF_2:def 1; :: thesis: verum

end;

end;

end;

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

end;

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

then consider a, b being Data-Location such that
A9: I = SubFrom (a,b) ;
A10: InsCode I = 3 by A9, RECDEF_2:def 1;

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 k being natural number st J = SCM-goto k or ex a being Data-Location ex k being natural number st J = a =0_goto k or ex a being Data-Location ex k being natural number st J = a >0_goto k ) by AMI_3:69;

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

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

end;

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

then consider d1, d2 being Data-Location such that
A11: J = SubFrom (d1,d2) ;
thus dom (JumpPart I) = dom {} by A9, RECDEF_2:def 2
.= dom (JumpPart J) by A11, RECDEF_2: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 k being natural number st J = SCM-goto k or ex a being Data-Location ex k being natural number st J = a =0_goto k or ex a being Data-Location ex k being natural number st J = a >0_goto k ) ; :: thesis: dom (JumpPart I) = dom (JumpPart J)

hence dom (JumpPart I) = dom (JumpPart J) by A1, A10, RECDEF_2:def 1; :: thesis: verum

end;

end;

end;

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

end;

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

then consider a, b being Data-Location such that
A12: I = MultBy (a,b) ;
A13: InsCode I = 4 by A12, RECDEF_2:def 1;

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 k being natural number st J = SCM-goto k or ex a being Data-Location ex k being natural number st J = a =0_goto k or ex a being Data-Location ex k being natural number st J = a >0_goto k ) by AMI_3:69;

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

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

end;

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

then consider d1, d2 being Data-Location such that
A14: J = MultBy (d1,d2) ;
thus dom (JumpPart I) = dom {} by A12, RECDEF_2:def 2
.= dom (JumpPart J) by A14, RECDEF_2: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 k being natural number st J = SCM-goto k or ex a being Data-Location ex k being natural number st J = a =0_goto k or ex a being Data-Location ex k being natural number st J = a >0_goto k ) ; :: thesis: dom (JumpPart I) = dom (JumpPart J)

hence dom (JumpPart I) = dom (JumpPart J) by A1, A13, RECDEF_2:def 1; :: thesis: verum

end;

end;

end;

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

end;

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

then consider a, b being Data-Location such that
A15: I = Divide (a,b) ;
A16: InsCode I = 5 by A15, RECDEF_2:def 1;

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 k being natural number st J = SCM-goto k or ex a being Data-Location ex k being natural number st J = a =0_goto k or ex a being Data-Location ex k being natural number st J = a >0_goto k ) by AMI_3:69;

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

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

end;

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

then consider d1, d2 being Data-Location such that
A17: J = Divide (d1,d2) ;
thus dom (JumpPart I) = dom {} by A15, RECDEF_2:def 2
.= dom (JumpPart J) by A17, RECDEF_2: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 k being natural number st J = SCM-goto k or ex a being Data-Location ex k being natural number st J = a =0_goto k or ex a being Data-Location ex k being natural number st J = a >0_goto k ) ; :: thesis: dom (JumpPart I) = dom (JumpPart J)

hence dom (JumpPart I) = dom (JumpPart J) by A1, A16, RECDEF_2:def 1; :: thesis: verum

end;

end;

end;

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

end;

suppose ex k being natural number st I = SCM-goto k ; :: thesis: dom (JumpPart I) = dom (JumpPart J)

then consider k being natural number such that
A18: I = SCM-goto k ;
A19: InsCode I = 6 by A18, RECDEF_2:def 1;

now

per cases ( J = [0,{},{}] or ex k being natural number st J = SCM-goto k 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 k being natural number st J = a =0_goto k or ex a being Data-Location ex k being natural number st J = a >0_goto k ) by AMI_3:69;

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

hence dom (JumpPart I) = dom (JumpPart J) by A1, A18, AMI_3:71, AMI_5:37, RECDEF_2:def 1; :: thesis: verum

end;

suppose ex k being natural number st J = SCM-goto k ; :: thesis: dom (JumpPart I) = dom (JumpPart J)

then consider k1 being natural number such that
A20: J = SCM-goto k1 ;
thus dom (JumpPart I) = dom <*k*> by A18, RECDEF_2:def 2
.= Seg 1 by FINSEQ_1:def 8
.= dom <*k1*> by FINSEQ_1:def 8
.= dom (JumpPart J) by A20, RECDEF_2: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 k being natural number st J = a =0_goto k or ex a being Data-Location ex k being natural number st J = a >0_goto k ) ; :: thesis: dom (JumpPart I) = dom (JumpPart J)

hence dom (JumpPart I) = dom (JumpPart J) by A1, A19, RECDEF_2:def 1; :: thesis: verum

end;

end;

end;

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

end;

suppose ex a being Data-Location ex k being natural number st I = a =0_goto k ; :: thesis: dom (JumpPart I) = dom (JumpPart J)

then consider a being Data-Location , k being natural number such that
A21: I = a =0_goto k ;
A22: InsCode I = 7 by A21, RECDEF_2:def 1;

now

per cases ( J = [0,{},{}] or ex d1 being Data-Location ex k being natural number st J = d1 =0_goto k 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 k being natural number st J = SCM-goto k or ex a being Data-Location ex k being natural number st J = a >0_goto k ) by AMI_3:69;

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

hence dom (JumpPart I) = dom (JumpPart J) by A1, A21, AMI_3:71, AMI_5:37, RECDEF_2:def 1; :: thesis: verum

end;

suppose ex d1 being Data-Location ex k being natural number st J = d1 =0_goto k ; :: thesis: dom (JumpPart I) = dom (JumpPart J)

then consider d1 being Data-Location , k1 being natural number such that
A23: J = d1 =0_goto k1 ;
thus dom (JumpPart I) = dom <*k*> by A21, RECDEF_2:def 2
.= Seg 1 by FINSEQ_1:55
.= dom <*k1*> by FINSEQ_1:55
.= dom (JumpPart J) by A23, RECDEF_2: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 k being natural number st J = SCM-goto k or ex a being Data-Location ex k being natural number st J = a >0_goto k ) ; :: thesis: dom (JumpPart I) = dom (JumpPart J)

hence dom (JumpPart I) = dom (JumpPart J) by A1, A22, RECDEF_2:def 1; :: thesis: verum

end;

end;

end;

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

end;

suppose ex a being Data-Location ex k being natural number st I = a >0_goto k ; :: thesis: dom (JumpPart I) = dom (JumpPart J)

then consider a being Data-Location , k being natural number such that
A24: I = a >0_goto k ;
A25: InsCode I = 8 by A24, RECDEF_2:def 1;

now

per cases ( J = [0,{},{}] or ex d1 being Data-Location ex k being natural number st J = d1 >0_goto k 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 k being natural number st J = SCM-goto k or ex a being Data-Location ex k being natural number st J = a =0_goto k ) by AMI_3:69;

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

hence dom (JumpPart I) = dom (JumpPart J) by A1, A24, AMI_3:71, AMI_5:37, RECDEF_2:def 1; :: thesis: verum

end;

suppose ex d1 being Data-Location ex k being natural number st J = d1 >0_goto k ; :: thesis: dom (JumpPart I) = dom (JumpPart J)

then consider d1 being Data-Location , k1 being natural number such that
A26: J = d1 >0_goto k1 ;
thus dom (JumpPart I) = dom <*k*> by A24, RECDEF_2:def 2
.= Seg 1 by FINSEQ_1:55
.= dom <*k1*> by FINSEQ_1:55
.= dom (JumpPart J) by A26, RECDEF_2: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 k being natural number st J = SCM-goto k or ex a being Data-Location ex k being natural number st J = a =0_goto k ) ; :: thesis: dom (JumpPart I) = dom (JumpPart J)

hence dom (JumpPart I) = dom (JumpPart J) by A1, A25, RECDEF_2:def 1; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

thus SCM is with_explicit_jumps :: thesis: verum

proof

let I be Instruction of SCM; :: according to AMISTD_2:def 8 :: thesis: I is with_explicit_jumps
thus JUMP I c= rng (JumpPart I) :: according to AMISTD_2:def 6,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 A27: f in JUMP I ; :: thesis: f in rng (JumpPart 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 k being natural number st I = SCM-goto k or ex a being Data-Location ex k1 being natural number st I = a =0_goto k1 or ex a being Data-Location ex k1 being natural number st I = a >0_goto k1 ) by AMI_3:69;

suppose I = [0,{},{}] ; :: thesis: f in rng (JumpPart I)

hence f in rng (JumpPart I) by A27, AMI_3:71; :: 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 A27; :: 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 A27; :: 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 A27; :: 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 A27; :: 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 A27; :: thesis: verum

end;

suppose A28: ex k being natural number st I = SCM-goto k ; :: thesis: f in rng (JumpPart I)

consider k1 being natural number such that
A29: I = SCM-goto k1 by A28;
A30: JumpPart (SCM-goto k1) = <*k1*> by RECDEF_2:def 2;
X: rng <*k1*> = {k1} by FINSEQ_1:56;
JUMP (SCM-goto k1) = {k1} by Th47;
then f = k1 by A27, A29, TARSKI:def 1;
hence f in rng (JumpPart I) by A29, A30, X, TARSKI:def 1; :: thesis: verum

end;

suppose A31: ex a being Data-Location ex k1 being natural number st I = a =0_goto k1 ; :: thesis: f in rng (JumpPart I)

consider a being Data-Location , k1 being natural number such that
A32: I = a =0_goto k1 by A31;
A33: JumpPart (a =0_goto k1) = <*k1*> by RECDEF_2:def 2;
X: rng <*k1*> = {k1} by FINSEQ_1:56;
JUMP (a =0_goto k1) = {k1} by Th49;
then f = k1 by A27, A32, TARSKI:def 1;
hence f in rng (JumpPart I) by A32, A33, X, TARSKI:def 1; :: thesis: verum

end;

suppose A34: ex a being Data-Location ex k1 being natural number st I = a >0_goto k1 ; :: thesis: f in rng (JumpPart I)

consider a being Data-Location , k1 being natural number such that
A35: I = a >0_goto k1 by A34;
A36: JumpPart (a >0_goto k1) = <*k1*> by RECDEF_2:def 2;
X: rng <*k1*> = {k1} by FINSEQ_1:56;
JUMP (a >0_goto k1) = {k1} by Th51;
then f = k1 by A27, A35, TARSKI:def 1;
hence f in rng (JumpPart I) by A35, A36, X, TARSKI:def 1; :: 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
A37: k in dom (JumpPart I) and
B37: f = (JumpPart I) . k by FUNCT_1:def 5;

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 k being natural number st I = SCM-goto k or ex a being Data-Location ex k being natural number st I = a =0_goto k or ex a being Data-Location ex k1 being natural number st I = a >0_goto k1 ) by AMI_3:69;

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

then dom (JumpPart I) = dom {} by RECDEF_2: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 {} by A37, A40, 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
A41: I = AddTo (a,b) ;
k in dom {} by A37, A41, 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
A42: I = SubFrom (a,b) ;
k in dom {} by A37, A42, 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
A43: I = MultBy (a,b) ;
k in dom {} by A37, A43, 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
A44: I = Divide (a,b) ;
k in dom {} by A37, A44, RECDEF_2:def 2;
hence f in JUMP I ; :: thesis: verum

end;

suppose ex k being natural number st I = SCM-goto k ; :: thesis: f in JUMP I

then consider k1 being natural number such that
A45: I = SCM-goto k1 ;
A46: JumpPart I = <*k1*> by A45, RECDEF_2:def 2;
then k = 1 by A37, FINSEQ_1:111;
then A47: f = k1 by A46, B37, FINSEQ_1:def 8;
JUMP I = {k1} by A45, Th47;
hence f in JUMP I by A47, TARSKI:def 1; :: thesis: verum

end;

suppose ex a being Data-Location ex k being natural number st I = a =0_goto k ; :: thesis: f in JUMP I

then consider a being Data-Location , k1 being natural number such that
A48: I = a =0_goto k1 ;
A49: JumpPart I = <*k1*> by A48, RECDEF_2:def 2;
then k = 1 by A37, FINSEQ_1:111;
then A50: f = k1 by A49, B37, FINSEQ_1:57;
JUMP I = {k1} by A48, Th49;
hence f in JUMP I by A50, TARSKI:def 1; :: thesis: verum

end;

suppose ex a being Data-Location ex k1 being natural number st I = a >0_goto k1 ; :: thesis: f in JUMP I

then consider a being Data-Location , k1 being natural number such that
A51: I = a >0_goto k1 ;
A52: JumpPart I = <*k1*> by A51, RECDEF_2:def 2;
then k = 1 by A37, FINSEQ_1:111;
then A53: f = k1 by A52, B37, FINSEQ_1:57;
JUMP I = {k1} by A51, Th51;
hence f in JUMP I by A53, TARSKI:def 1; :: thesis: verum

end;

end;

end;