let s be State of SCM+FSA; :: thesis: for aa, bb being Int-Location
for f being FinSeq-Location
for p being Instruction-Sequence of SCM+FSA st 1 <= s . aa & s . aa <= len (s . f) & 1 <= s . bb & s . bb <= len (s . f) & s . (intloc 0) = 1 holds
( ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . aa) = (s . f) . (s . bb) & ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . bb) = (s . f) . (s . aa) )
let aa, bb be Int-Location; :: thesis: for f being FinSeq-Location
for p being Instruction-Sequence of SCM+FSA st 1 <= s . aa & s . aa <= len (s . f) & 1 <= s . bb & s . bb <= len (s . f) & s . (intloc 0) = 1 holds
( ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . aa) = (s . f) . (s . bb) & ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . bb) = (s . f) . (s . aa) )
let f be FinSeq-Location ; :: thesis: for p being Instruction-Sequence of SCM+FSA st 1 <= s . aa & s . aa <= len (s . f) & 1 <= s . bb & s . bb <= len (s . f) & s . (intloc 0) = 1 holds
( ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . aa) = (s . f) . (s . bb) & ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . bb) = (s . f) . (s . aa) )
let p be Instruction-Sequence of SCM+FSA; :: thesis: ( 1 <= s . aa & s . aa <= len (s . f) & 1 <= s . bb & s . bb <= len (s . f) & s . (intloc 0) = 1 implies ( ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . aa) = (s . f) . (s . bb) & ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . bb) = (s . f) . (s . aa) ) )
set a = aa;
set b = bb;
assume that
A1: 1 <= s . aa and
A2: s . aa <= len (s . f) and
A3: 1 <= s . bb and
A4: s . bb <= len (s . f) and
A5: s . (intloc 0) = 1 ; :: thesis: ( ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . aa) = (s . f) . (s . bb) & ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . bb) = (s . f) . (s . aa) )
A6: (IExec ((swap (f,aa,bb)),p,s)) . f = ((s . f) +* ((s . aa),((s . f) . (s . bb)))) +* ((s . bb),((s . f) . (s . aa))) by A1, A2, A3, A4, A5, Th31;
reconsider sa = s . aa as Element of NAT by A1, INT_1:3;
A7: sa in dom (s . f) by A1, A2, FINSEQ_3:25;
A8: dom ((s . f) +* ((s . aa),((s . f) . (s . bb)))) = dom (s . f) by FUNCT_7:30;
reconsider sb = s . bb as Element of NAT by A3, INT_1:3;
A9: sb in dom (s . f) by A3, A4, FINSEQ_3:25;
per cases ( sa <> sb or sa = sb ) ;
suppose sa <> sb ; :: thesis: ( ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . aa) = (s . f) . (s . bb) & ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . bb) = (s . f) . (s . aa) )
hence ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . aa) = ((s . f) +* ((s . aa),((s . f) . (s . bb)))) . (s . aa) by A6, FUNCT_7:32
.= (s . f) . (s . bb) by A7, FUNCT_7:31 ;
:: thesis: ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . bb) = (s . f) . (s . aa)
thus ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . bb) = (s . f) . (s . aa) by A9, A6, A8, FUNCT_7:31; :: thesis: verum
end;
suppose sa = sb ; :: thesis: ( ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . aa) = (s . f) . (s . bb) & ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . bb) = (s . f) . (s . aa) )
hence ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . aa) = (s . f) . (s . bb) by A7, A6, A8, FUNCT_7:31; :: thesis: ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . bb) = (s . f) . (s . aa)
thus ((IExec ((swap (f,aa,bb)),p,s)) . f) . (s . bb) = (s . f) . (s . aa) by A9, A6, A8, FUNCT_7:31; :: thesis: verum
end;
end;