let s be State of SCM+FSA; 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; 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 ; 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; ( 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
; ( ((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
;
( ((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
;
((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;
verum end; suppose
sa = sb
;
( ((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;
((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;
verum end; end;