let a, b, c be Int-Location; ( a <> b implies not AddTo (b,c) destroys a )
assume A1:
a <> b
; not AddTo (b,c) destroys a
now for e being Int-Location
for l being Element of NAT
for f being FinSeq-Location holds
( a := e <> AddTo (b,c) & AddTo (a,e) <> AddTo (b,c) & SubFrom (a,e) <> AddTo (b,c) & MultBy (a,e) <> AddTo (b,c) & Divide (a,e) <> AddTo (b,c) & Divide (e,a) <> AddTo (b,c) & a := (f,e) <> AddTo (b,c) & a :=len f <> AddTo (b,c) )let e be
Int-Location;
for l being Element of NAT
for f being FinSeq-Location holds
( a := e <> AddTo (b,c) & AddTo (a,e) <> AddTo (b,c) & SubFrom (a,e) <> AddTo (b,c) & MultBy (a,e) <> AddTo (b,c) & Divide (a,e) <> AddTo (b,c) & Divide (e,a) <> AddTo (b,c) & a := (f,e) <> AddTo (b,c) & a :=len f <> AddTo (b,c) )let l be
Element of
NAT ;
for f being FinSeq-Location holds
( a := e <> AddTo (b,c) & AddTo (a,e) <> AddTo (b,c) & SubFrom (a,e) <> AddTo (b,c) & MultBy (a,e) <> AddTo (b,c) & Divide (a,e) <> AddTo (b,c) & Divide (e,a) <> AddTo (b,c) & a := (f,e) <> AddTo (b,c) & a :=len f <> AddTo (b,c) )let f be
FinSeq-Location ;
( a := e <> AddTo (b,c) & AddTo (a,e) <> AddTo (b,c) & SubFrom (a,e) <> AddTo (b,c) & MultBy (a,e) <> AddTo (b,c) & Divide (a,e) <> AddTo (b,c) & Divide (e,a) <> AddTo (b,c) & a := (f,e) <> AddTo (b,c) & a :=len f <> AddTo (b,c) )A2:
InsCode (AddTo (b,c)) = 2
by SCMFSA_2:19;
hence
a := e <> AddTo (
b,
c)
by SCMFSA_2:18;
( AddTo (a,e) <> AddTo (b,c) & SubFrom (a,e) <> AddTo (b,c) & MultBy (a,e) <> AddTo (b,c) & Divide (a,e) <> AddTo (b,c) & Divide (e,a) <> AddTo (b,c) & a := (f,e) <> AddTo (b,c) & a :=len f <> AddTo (b,c) )thus
AddTo (
a,
e)
<> AddTo (
b,
c)
by A1, SF_MASTR:2;
( SubFrom (a,e) <> AddTo (b,c) & MultBy (a,e) <> AddTo (b,c) & Divide (a,e) <> AddTo (b,c) & Divide (e,a) <> AddTo (b,c) & a := (f,e) <> AddTo (b,c) & a :=len f <> AddTo (b,c) )thus
SubFrom (
a,
e)
<> AddTo (
b,
c)
by A2, SCMFSA_2:20;
( MultBy (a,e) <> AddTo (b,c) & Divide (a,e) <> AddTo (b,c) & Divide (e,a) <> AddTo (b,c) & a := (f,e) <> AddTo (b,c) & a :=len f <> AddTo (b,c) )thus
MultBy (
a,
e)
<> AddTo (
b,
c)
by A2, SCMFSA_2:21;
( Divide (a,e) <> AddTo (b,c) & Divide (e,a) <> AddTo (b,c) & a := (f,e) <> AddTo (b,c) & a :=len f <> AddTo (b,c) )thus
(
Divide (
a,
e)
<> AddTo (
b,
c) &
Divide (
e,
a)
<> AddTo (
b,
c) )
by A2, SCMFSA_2:22;
( a := (f,e) <> AddTo (b,c) & a :=len f <> AddTo (b,c) )thus
a := (
f,
e)
<> AddTo (
b,
c)
by A2, SCMFSA_2:26;
a :=len f <> AddTo (b,c)thus
a :=len f <> AddTo (
b,
c)
by A2, SCMFSA_2:28;
verum end;
hence
not AddTo (b,c) destroys a
; verum