let a1, a2 be Int-Location ; :: thesis: for l1, l2 being Instruction-Location of SCM+FSA st a1 >0_goto l1 = a2 >0_goto l2 holds
( a1 = a2 & l1 = l2 )
let l1, l2 be Instruction-Location of SCM+FSA ; :: thesis: ( a1 >0_goto l1 = a2 >0_goto l2 implies ( a1 = a2 & l1 = l2 ) )
assume A1: a1 >0_goto l1 = a2 >0_goto l2 ; :: thesis: ( a1 = a2 & l1 = l2 )
consider A1 being Data-Location , L1 being Instruction-Location of SCM such that
A2: ( a1 = A1 & l1 = L1 & a1 >0_goto l1 = A1 >0_goto L1 ) by SCMFSA_2:def 18;
consider A2 being Data-Location , L2 being Instruction-Location of SCM such that
A3: ( a2 = A2 & l2 = L2 & a2 >0_goto l2 = A2 >0_goto L2 ) by SCMFSA_2:def 18;
( <*L1,A1*> . 1 = L1 & <*L1,A1*> . 2 = A1 & <*L2,A2*> . 1 = L2 & <*L2,A2*> . 2 = A2 ) by FINSEQ_1:61;
hence ( a1 = a2 & l1 = l2 ) by A1, A2, A3, ZFMISC_1:33; :: thesis: verum