let a, b, c be Int-Location; for f being FinSeq-Location holds not (f,c) := b destroys a
let f be FinSeq-Location ; not (f,c) := b destroys a
now for e being Int-Location
for h being FinSeq-Location holds
( a := e <> (f,c) := b & AddTo (a,e) <> (f,c) := b & SubFrom (a,e) <> (f,c) := b & MultBy (a,e) <> (f,c) := b & Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b & a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b )let e be
Int-Location;
for h being FinSeq-Location holds
( a := e <> (f,c) := b & AddTo (a,e) <> (f,c) := b & SubFrom (a,e) <> (f,c) := b & MultBy (a,e) <> (f,c) := b & Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b & a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b )let h be
FinSeq-Location ;
( a := e <> (f,c) := b & AddTo (a,e) <> (f,c) := b & SubFrom (a,e) <> (f,c) := b & MultBy (a,e) <> (f,c) := b & Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b & a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b )A1:
InsCode ((f,c) := b) = 10
by SCMFSA_2:27;
hence
a := e <> (
f,
c)
:= b
by SCMFSA_2:18;
( AddTo (a,e) <> (f,c) := b & SubFrom (a,e) <> (f,c) := b & MultBy (a,e) <> (f,c) := b & Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b & a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b )thus
AddTo (
a,
e)
<> (
f,
c)
:= b
by A1, SCMFSA_2:19;
( SubFrom (a,e) <> (f,c) := b & MultBy (a,e) <> (f,c) := b & Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b & a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b )thus
SubFrom (
a,
e)
<> (
f,
c)
:= b
by A1, SCMFSA_2:20;
( MultBy (a,e) <> (f,c) := b & Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b & a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b )thus
MultBy (
a,
e)
<> (
f,
c)
:= b
by A1, SCMFSA_2:21;
( Divide (e,a) <> (f,c) := b & Divide (a,e) <> (f,c) := b & a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b )thus
(
Divide (
e,
a)
<> (
f,
c)
:= b &
Divide (
a,
e)
<> (
f,
c)
:= b )
by A1, SCMFSA_2:22;
( a := (h,e) <> (f,c) := b & a :=len h <> (f,c) := b )thus
a := (
h,
e)
<> (
f,
c)
:= b
by A1, SCMFSA_2:26;
a :=len h <> (f,c) := bthus
a :=len h <> (
f,
c)
:= b
by A1, SCMFSA_2:28;
verum end;
hence
not (f,c) := b destroys a
; verum