let a1, a2 be Int-Location; :: thesis: for l1, l2 being Nat st a1 =0_goto l1 = a2 =0_goto l2 holds
( a1 = a2 & l1 = l2 )
let l1, l2 be Nat; :: 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 such that
A2: ( a1 = A1 & a1 =0_goto l1 = A1 =0_goto l1 ) by SCMFSA_2:def 14;
consider A2 being Data-Location such that
A3: ( a2 = A2 & a2 =0_goto l2 = A2 =0_goto l2 ) by SCMFSA_2:def 14;
A4: ( <*l2*> . 1 = l2 & <*A2*> . 1 = A2 ) by FINSEQ_1:40;
( <*l1*> . 1 = l1 & <*A1*> . 1 = A1 ) by FINSEQ_1:40;
hence ( a1 = a2 & l1 = l2 ) by A1, A2, A3, A4, XTUPLE_0:3; :: thesis: verum