let i, j be Element of SCM-Instr ; :: according to COMPOS_0:def 5 :: 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)
InsCode i <= 8 by Th10;
then not not InsCode i = 0 & ... & not InsCode i = 8 by NAT_1:60;
per cases then ( InsCode i = 0 or not not InsCode i = 1 & ... & not InsCode i = 5 or InsCode i = 7 or InsCode i = 8 or InsCode i = 6 ) ;
suppose InsCode i = 0 ; :: thesis: dom (JumpPart i) = dom (JumpPart j)
then ( i in {[SCM-Halt,{},{}]} & j in {[SCM-Halt,{},{}]} ) by A1, Th9;
then ( i = [SCM-Halt,{},{}] & j = [SCM-Halt,{},{}] ) by TARSKI:def 1;
hence dom (JumpPart i) = dom (JumpPart j) ; :: thesis: verum
end;
suppose not not InsCode i = 1 & ... & not InsCode i = 5 ; :: thesis: dom (JumpPart i) = dom (JumpPart j)
then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm1;
hence dom (JumpPart i) = dom (JumpPart j) ; :: thesis: verum
end;
suppose ( InsCode i = 7 or InsCode i = 8 ) ; :: thesis: dom (JumpPart i) = dom (JumpPart j)
then ( dom (JumpPart i) = Seg 1 & dom (JumpPart j) = Seg 1 ) by A1, Lm2;
hence dom (JumpPart i) = dom (JumpPart j) ; :: thesis: verum
end;
suppose InsCode i = 6 ; :: thesis: dom (JumpPart i) = dom (JumpPart j)
then ( dom (JumpPart i) = Seg 1 & dom (JumpPart j) = Seg 1 ) by A1, Lm3;
hence dom (JumpPart i) = dom (JumpPart j) ; :: thesis: verum
end;
end;