:: Logical Correctness of Vector Calculation Programs
:: by Takaya Nishiyama , Hirofumi Fukura and Yatsuka Nakamura
::
:: Received July 13, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem :: PRGCOR_2:1
canceled;
theorem Th2: :: PRGCOR_2:2
:: deftheorem Def1 defines FS2XFS PRGCOR_2:def 1 :
:: deftheorem defines XFS2FS PRGCOR_2:def 2 :
theorem Th3: :: PRGCOR_2:3
theorem Th4: :: PRGCOR_2:4
:: deftheorem Def3 defines FS2XFS* PRGCOR_2:def 3 :
:: deftheorem Def4 defines XFS2FS* PRGCOR_2:def 4 :
theorem Th5: :: PRGCOR_2:5
:: deftheorem Def5 defines is_an_xrep_of PRGCOR_2:def 5 :
theorem :: PRGCOR_2:6
:: deftheorem Def6 defines IFLGT PRGCOR_2:def 6 :
for
x,
y,
a,
b,
c being
set holds
( (
x in y implies
IFLGT x,
y,
a,
b,
c = a ) & (
x = y implies
IFLGT x,
y,
a,
b,
c = b ) & ( not
x in y & not
x = y implies
IFLGT x,
y,
a,
b,
c = c ) );
theorem Th7: :: PRGCOR_2:7
:: deftheorem Def7 defines inner_prd_prg PRGCOR_2:def 7 :
theorem Th8: :: PRGCOR_2:8
theorem :: PRGCOR_2:9
theorem :: PRGCOR_2:10
:: deftheorem Def8 defines scalar_prd_prg PRGCOR_2:def 8 :
theorem :: PRGCOR_2:11
:: deftheorem Def9 defines vector_minus_prg PRGCOR_2:def 9 :
theorem :: PRGCOR_2:12
:: deftheorem Def10 defines vector_add_prg PRGCOR_2:def 10 :
theorem :: PRGCOR_2:13
:: deftheorem Def11 defines vector_sub_prg PRGCOR_2:def 11 :
theorem :: PRGCOR_2:14