let II, I be Instruction of SCM ; :: thesis: for k being Element of NAT st ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 ) & IncAddr II,k = I holds
II = I
let k be Element of NAT ; :: thesis: ( ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 ) & IncAddr II,k = I implies II = I )
assume that
A1: ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 ) and
A2: IncAddr II,k = I ; :: thesis: II = I
InsCode II = InsCode I by A2, Th13;
hence II = I by A1, A2, Def3; :: thesis: verum