thus SCM R is homogeneous :: thesis:

proof

let I, J be Instruction of (SCM R); :: according to COMPOS_1:def 12 :: thesis:
assume A1: InsCode I = InsCode J ; :: thesis:
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:7;

per cases by SCMRING2:7;

suppose A3: I = [0,{},{}] ; :: thesis:

then I = halt (SCM R) by SCMRING2:21;
then InsCode I = 0 by Th8;
hence dom (I `2_3) = dom (J `2_3) by A1, A2, A3, RECDEF_2:def 1; :: thesis:

end;

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

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

now

per cases by SCMRING2:7;

suppose J = [0,{},{}] ; :: thesis:

then J = halt (SCM R) by SCMRING2:21;
hence dom (I `2_3) = dom (J `2_3) by A1, A5, Th8; :: thesis:

end;

suppose ex a, b being Data-Location of R st J = a := b ; :: thesis:

then consider d1, d2 being Data-Location of R such that
A6: J = d1 := d2 ;
thus dom (JumpPart I) = dom {} by A4, RECDEF_2:def 2
.= dom (JumpPart J) by A6, RECDEF_2:def 2 ; :: thesis:

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:

hence dom (I `2_3) = dom (J `2_3) by A1, A5, RECDEF_2:def 1; :: thesis:

end;

end;

end;

hence dom (I `2_3) = dom (J `2_3) ; :: thesis:

end;

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

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

now

per cases by SCMRING2:7;

suppose J = [0,{},{}] ; :: thesis:

then J = halt (SCM R) by SCMRING2:21;
hence dom (I `2_3) = dom (J `2_3) by A1, A8, Th8; :: thesis:

end;

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

then consider d1, d2 being Data-Location of R such that
A9: J = AddTo (d1,d2) ;
thus dom (JumpPart I) = dom {} by A7, RECDEF_2:def 2
.= dom (JumpPart J) by A9, RECDEF_2:def 2 ; :: thesis:

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:

hence dom (I `2_3) = dom (J `2_3) by A1, A8, RECDEF_2:def 1; :: thesis:

end;

end;

end;

hence dom (I `2_3) = dom (J `2_3) ; :: thesis:

end;

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

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

now

per cases by SCMRING2:7;

suppose J = [0,{},{}] ; :: thesis:

then J = halt (SCM R) by SCMRING2:21;
hence dom (I `2_3) = dom (J `2_3) by A1, A11, Th8; :: thesis:

end;

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

then consider d1, d2 being Data-Location of R such that
A12: J = SubFrom (d1,d2) ;
thus dom (JumpPart I) = dom {} by A10, RECDEF_2:def 2
.= dom (JumpPart J) by A12, RECDEF_2:def 2 ; :: thesis:

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:

hence dom (I `2_3) = dom (J `2_3) by A1, A11, RECDEF_2:def 1; :: thesis:

end;

end;

end;

hence dom (I `2_3) = dom (J `2_3) ; :: thesis:

end;

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

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

now

per cases by SCMRING2:7;

suppose J = [0,{},{}] ; :: thesis:

then J = halt (SCM R) by SCMRING2:21;
hence dom (I `2_3) = dom (J `2_3) by A1, A14, Th8; :: thesis:

end;

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

then consider d1, d2 being Data-Location of R such that
A15: J = MultBy (d1,d2) ;
thus dom (JumpPart I) = dom {} by A13, RECDEF_2:def 2
.= dom (JumpPart J) by A15, RECDEF_2:def 2 ; :: thesis:

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:

hence dom (I `2_3) = dom (J `2_3) by A1, A14, RECDEF_2:def 1; :: thesis:

end;

end;

end;

hence dom (I `2_3) = dom (J `2_3) ; :: thesis:

end;

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

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

now

per cases by SCMRING2:7;

suppose J = [0,{},{}] ; :: thesis:

then J = halt (SCM R) by SCMRING2:21;
hence dom (I `2_3) = dom (J `2_3) by A1, A17, Th8; :: thesis:

end;

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

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

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:

hence dom (I `2_3) = dom (J `2_3) by A1, A17, RECDEF_2:def 1; :: thesis:

end;

end;

end;

hence dom (I `2_3) = dom (J `2_3) ; :: thesis:

end;

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

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, RECDEF_2:def 1;

now

per cases by SCMRING2:7;

suppose J = [0,{},{}] ; :: thesis:

then J = halt (SCM R) by SCMRING2:21;
hence dom (I `2_3) = dom (J `2_3) by A1, A20, Th8; :: thesis:

end;

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

then consider d1 being Data-Location of R, i2 being Element of NAT such that
A21: J = d1 =0_goto i2 ;
thus dom (JumpPart I) = dom <*i1*> by A19, RECDEF_2:def 2
.= Seg 1 by FINSEQ_1:38
.= dom <*i2*> by FINSEQ_1:38
.= dom (JumpPart J) by A21, RECDEF_2:def 2 ; :: thesis:

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:

hence dom (I `2_3) = dom (J `2_3) by A1, A20, RECDEF_2:def 1; :: thesis:

end;

end;

end;

hence dom (I `2_3) = dom (J `2_3) ; :: thesis:

end;

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

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, RECDEF_2:def 1;

now

per cases by SCMRING2:7;

suppose J = [0,{},{}] ; :: thesis:

then J = halt (SCM R) by SCMRING2:21;
hence dom (I `2_3) = dom (J `2_3) by A1, A23, Th8; :: thesis:

end;

suppose ex a being Data-Location of R ex r being Element of R st J = a := r ; :: thesis:

then consider b being Data-Location of R, r1 being Element of R such that
A24: J = b := r1 ;
thus dom (JumpPart I) = dom {} by A22, RECDEF_2:def 2
.= dom (JumpPart J) by A24, RECDEF_2:def 2 ; :: thesis:

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:

hence dom (I `2_3) = dom (J `2_3) by A1, A23, RECDEF_2:def 1; :: thesis:

end;

end;

end;

hence dom (I `2_3) = dom (J `2_3) ; :: thesis:

end;

end;

end;

thus SCM R is with_explicit_jumps :: thesis:

proof

let I be Instruction of (SCM R); :: according to AMISTD_2:def 2 :: thesis:
thus JUMP I c= rng (JumpPart I) :: according to AMISTD_2:def 1,XBOOLE_0:def 10 :: thesis:

proof

let f be set ; :: according to TARSKI:def 3 :: thesis:
assume A25: f in JUMP I ; :: thesis:

per cases by SCMRING2:7;

suppose A26: I = [0,{},{}] ; :: thesis:

JUMP (halt (SCM R)) is empty ;
hence f in rng (JumpPart I) by A25, A26, SCMRING2:21; :: thesis:

end;

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

hence f in rng (JumpPart I) by A25; :: thesis:

end;

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

hence f in rng (JumpPart I) by A25; :: thesis:

end;

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

hence f in rng (JumpPart I) by A25; :: thesis:

end;

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

hence f in rng (JumpPart I) by A25; :: thesis:

end;

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

consider i1 being Element of NAT such that
A28: I = goto (i1,R) by A27;
A29: JumpPart (goto (i1,R)) = <*i1*> by RECDEF_2:def 2;
rng <*i1*> = {i1} by FINSEQ_1:39;
hence f in rng (JumpPart I) by A25, A28, A29, Th60; :: thesis:

end;

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

consider a being Data-Location of R, i1 being Element of NAT such that
A32: I = a =0_goto i1 by A31;
A33: JumpPart (a =0_goto i1) = <*i1*> by RECDEF_2:def 2;
rng <*i1*> = {i1} by FINSEQ_1:39;
hence f in rng (JumpPart I) by A25, A32, A33, Th63; :: thesis:

end;

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

hence f in rng (JumpPart I) by A25; :: thesis:

end;

end;

end;

let f be set ; :: according to TARSKI:def 3 :: thesis:
assume f in rng (JumpPart I) ; :: thesis:
then consider k being set such that
A35: k in dom (JumpPart I) and
A36: f = (JumpPart I) . k by FUNCT_1:def 3;

per cases by SCMRING2:7;

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

then I = halt (SCM R) by SCMRING2:21;
hence f in JUMP I by A35; :: thesis:

end;

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

then consider a, b being Data-Location of R such that
A37: I = a := b ;
k in dom {} by A35, A37, RECDEF_2:def 2;
hence f in JUMP I ; :: thesis:

end;

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

then consider a, b being Data-Location of R such that
A38: I = AddTo (a,b) ;
k in dom {} by A35, A38, RECDEF_2:def 2;
hence f in JUMP I ; :: thesis:

end;

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

then consider a, b being Data-Location of R such that
A39: I = SubFrom (a,b) ;
k in dom {} by A35, A39, RECDEF_2:def 2;
hence f in JUMP I ; :: thesis:

end;

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

then consider a, b being Data-Location of R such that
A40: I = MultBy (a,b) ;
k in dom {} by A35, A40, RECDEF_2:def 2;
hence f in JUMP I ; :: thesis:

end;

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

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

end;

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

then consider a being Data-Location of R, i1 being Element of NAT such that
A44: I = a =0_goto i1 ;
A45: JumpPart I = <*i1*> by A44, RECDEF_2:def 2;
then k = 1 by A35, Lm1;
then A46: f = i1 by A45, A36, FINSEQ_1:40;
JUMP I = {i1} by A44, Th63;
hence f in JUMP I by A46, TARSKI:def 1; :: thesis:

end;

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

then consider a being Data-Location of R, r being Element of R such that
A47: I = a := r ;
k in dom {} by A35, A47, RECDEF_2:def 2;
hence f in JUMP I ; :: thesis:

end;

end;

end;