let N be with_zero set ; :: thesis: for T being InsType of the InstructionsF of (STC N) holds JumpParts T = {0}

let T be InsType of the InstructionsF of (STC N); :: thesis: JumpParts T = {0}

set A = { (JumpPart I) where I is Instruction of (STC N) : InsCode I = T } ;

{0} = { (JumpPart I) where I is Instruction of (STC N) : InsCode I = T }

let T be InsType of the InstructionsF of (STC N); :: thesis: JumpParts T = {0}

set A = { (JumpPart I) where I is Instruction of (STC N) : InsCode I = T } ;

{0} = { (JumpPart I) where I is Instruction of (STC N) : InsCode I = T }

proof

assume a in { (JumpPart I) where I is Instruction of (STC N) : InsCode I = T } ; :: thesis: a in {0}

then ex I being Instruction of (STC N) st

( a = JumpPart I & InsCode I = T ) ;

then a = 0 ;

hence a in {0} by TARSKI:def 1; :: thesis: verum

end;

hence
JumpParts T = {0}
; :: thesis: verumhereby :: according to XBOOLE_0:def 10,TARSKI:def 3 :: thesis: { (JumpPart I) where I is Instruction of (STC N) : InsCode I = T } c= {0}

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { (JumpPart I) where I is Instruction of (STC N) : InsCode I = T } or a in {0} )let a be object ; :: thesis: ( a in {0} implies b_{1} in { (JumpPart b_{2}) where I is Instruction of (STC N) : InsCode b_{2} = T } )

assume a in {0} ; :: thesis: b_{1} in { (JumpPart b_{2}) where I is Instruction of (STC N) : InsCode b_{2} = T }

then A1: a = 0 by TARSKI:def 1;

A2: the InstructionsF of (STC N) = {[0,0,0],[1,0,0]} by AMISTD_1:def 7;

then A3: InsCodes the InstructionsF of (STC N) = {0,1} by MCART_1:91;

end;assume a in {0} ; :: thesis: b

then A1: a = 0 by TARSKI:def 1;

A2: the InstructionsF of (STC N) = {[0,0,0],[1,0,0]} by AMISTD_1:def 7;

then A3: InsCodes the InstructionsF of (STC N) = {0,1} by MCART_1:91;

per cases
( T = 0 or T = 1 )
by A3, TARSKI:def 2;

end;

suppose A4:
T = 0
; :: thesis: b_{1} in { (JumpPart b_{2}) where I is Instruction of (STC N) : InsCode b_{2} = T }

reconsider I = [0,0,0] as Instruction of (STC N) by A2, TARSKI:def 2;

A5: JumpPart I = 0 ;

InsCode I = 0 ;

hence a in { (JumpPart I) where I is Instruction of (STC N) : InsCode I = T } by A1, A4, A5; :: thesis: verum

end;A5: JumpPart I = 0 ;

InsCode I = 0 ;

hence a in { (JumpPart I) where I is Instruction of (STC N) : InsCode I = T } by A1, A4, A5; :: thesis: verum

suppose A6:
T = 1
; :: thesis: b_{1} in { (JumpPart b_{2}) where I is Instruction of (STC N) : InsCode b_{2} = T }

reconsider I = [1,0,0] as Instruction of (STC N) by A2, TARSKI:def 2;

A7: JumpPart I = 0 ;

InsCode I = 1 ;

hence a in { (JumpPart I) where I is Instruction of (STC N) : InsCode I = T } by A1, A6, A7; :: thesis: verum

end;A7: JumpPart I = 0 ;

InsCode I = 1 ;

hence a in { (JumpPart I) where I is Instruction of (STC N) : InsCode I = T } by A1, A6, A7; :: thesis: verum

assume a in { (JumpPart I) where I is Instruction of (STC N) : InsCode I = T } ; :: thesis: a in {0}

then ex I being Instruction of (STC N) st

( a = JumpPart I & InsCode I = T ) ;

then a = 0 ;

hence a in {0} by TARSKI:def 1; :: thesis: verum