let N be with_zero set ; :: thesis: for T being InsType of the InstructionsF of (STC N) holds JumpParts T =
let T be InsType of the InstructionsF of (STC N); :: thesis:
set A = { () where I is Instruction of (STC N) : InsCode I = T } ;
{0} = { () where I is Instruction of (STC N) : InsCode I = T }
proof
hereby :: according to XBOOLE_0:def 10,TARSKI:def 3 :: thesis: { () where I is Instruction of (STC N) : InsCode I = T } c=
let a be object ; :: thesis: ( a in implies b1 in { (JumpPart b2) where I is Instruction of (STC N) : InsCode b2 = T } )
assume a in ; :: thesis: b1 in { (JumpPart b2) where I is Instruction of (STC N) : InsCode b2 = 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;
per cases ( T = 0 or T = 1 ) by ;
suppose A4: T = 0 ; :: thesis: b1 in { (JumpPart b2) where I is Instruction of (STC N) : InsCode b2 = T }
reconsider I = [0,0,0] as Instruction of (STC N) by ;
A5: JumpPart I = 0 ;
InsCode I = 0 ;
hence a in { () where I is Instruction of (STC N) : InsCode I = T } by A1, A4, A5; :: thesis: verum
end;
suppose A6: T = 1 ; :: thesis: b1 in { (JumpPart b2) where I is Instruction of (STC N) : InsCode b2 = T }
reconsider I = [1,0,0] as Instruction of (STC N) by ;
A7: JumpPart I = 0 ;
InsCode I = 1 ;
hence a in { () where I is Instruction of (STC N) : InsCode I = T } by A1, A6, A7; :: thesis: verum
end;
end;
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { () where I is Instruction of (STC N) : InsCode I = T } or a in )
assume a in { () where I is Instruction of (STC N) : InsCode I = T } ; :: thesis:
then ex I being Instruction of (STC N) st
( a = JumpPart I & InsCode I = T ) ;
then a = 0 ;
hence a in by TARSKI:def 1; :: thesis: verum
end;
hence JumpParts T = ; :: thesis: verum