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