let k be Nat; :: thesis: for S being non empty standard-ins homogeneous J/A-independent set

for I being Element of S holds JumpParts (InsCode I) = JumpParts (InsCode (IncAddr (I,k)))

let S be non empty standard-ins homogeneous J/A-independent set ; :: thesis: for I being Element of S holds JumpParts (InsCode I) = JumpParts (InsCode (IncAddr (I,k)))

let I be Element of S; :: thesis: JumpParts (InsCode I) = JumpParts (InsCode (IncAddr (I,k)))

set A = { (JumpPart J) where J is Element of S : InsCode I = InsCode J } ;

set B = { (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J } ;

{ (JumpPart J) where J is Element of S : InsCode I = InsCode J } = { (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J }

for I being Element of S holds JumpParts (InsCode I) = JumpParts (InsCode (IncAddr (I,k)))

let S be non empty standard-ins homogeneous J/A-independent set ; :: thesis: for I being Element of S holds JumpParts (InsCode I) = JumpParts (InsCode (IncAddr (I,k)))

let I be Element of S; :: thesis: JumpParts (InsCode I) = JumpParts (InsCode (IncAddr (I,k)))

set A = { (JumpPart J) where J is Element of S : InsCode I = InsCode J } ;

set B = { (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J } ;

{ (JumpPart J) where J is Element of S : InsCode I = InsCode J } = { (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J }

proof

assume a in { (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J } ; :: thesis: a in { (JumpPart J) where J is Element of S : InsCode I = InsCode J }

then consider J being Element of S such that

A3: a = JumpPart J and

A4: InsCode J = InsCode (IncAddr (I,k)) ;

InsCode J = InsCode I by A4, Def8;

hence a in { (JumpPart J) where J is Element of S : InsCode I = InsCode J } by A3; :: thesis: verum

end;

hence
JumpParts (InsCode I) = JumpParts (InsCode (IncAddr (I,k)))
; :: thesis: verumhereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J } c= { (JumpPart J) where J is Element of S : InsCode I = InsCode J }

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J } or a in { (JumpPart J) where J is Element of S : InsCode I = InsCode J } )let a be object ; :: thesis: ( a in { (JumpPart J) where J is Element of S : InsCode I = InsCode J } implies a in { (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J } )

assume a in { (JumpPart J) where J is Element of S : InsCode I = InsCode J } ; :: thesis: a in { (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J }

then consider J being Element of S such that

A1: a = JumpPart J and

A2: InsCode J = InsCode I ;

InsCode J = InsCode (IncAddr (I,k)) by A2, Def8;

hence a in { (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J } by A1; :: thesis: verum

end;assume a in { (JumpPart J) where J is Element of S : InsCode I = InsCode J } ; :: thesis: a in { (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J }

then consider J being Element of S such that

A1: a = JumpPart J and

A2: InsCode J = InsCode I ;

InsCode J = InsCode (IncAddr (I,k)) by A2, Def8;

hence a in { (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J } by A1; :: thesis: verum

assume a in { (JumpPart J) where J is Element of S : InsCode (IncAddr (I,k)) = InsCode J } ; :: thesis: a in { (JumpPart J) where J is Element of S : InsCode I = InsCode J }

then consider J being Element of S such that

A3: a = JumpPart J and

A4: InsCode J = InsCode (IncAddr (I,k)) ;

InsCode J = InsCode I by A4, Def8;

hence a in { (JumpPart J) where J is Element of S : InsCode I = InsCode J } by A3; :: thesis: verum