:: PARSP_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

Lm1: for F being non empty add-associative right_zeroed right_complementable LoopStr
for a, b being Element of F holds - (a - b) = b - a
proof end;

Lm2: for F being Field
for a, b, c, d being Element of F holds ((a - b) * (c - d)) - ((b - a) * (d - c)) = 0. F
proof end;

Lm3: for F being Field
for a, b, c, d being Element of F holds (a * (b - b)) - ((c - c) * d) = 0. F
proof end;

Lm4: for F being Field
for a, e, d, b, c, h being Element of F st a <> 0. F & (a * e) - (d * b) = 0. F & (a * c) - (h * b) = 0. F holds
(d * c) - (h * e) = 0. F
proof end;

Lm5: for F being Field
for a, b, c, d being Element of F st (a * b) - (c * d) = 0. F holds
(d * c) - (b * a) = 0. F
proof end;

Lm6: for F being Field
for b, a, e, d, c, h being Element of F st b <> 0. F & (a * e) - (d * b) = 0. F & (a * c) - (h * b) = 0. F holds
(d * c) - (h * e) = 0. F
proof end;

Lm7: for F being Field
for c, d, a, b being Element of F holds (c * d) * (a * b) = ((a * c) * d) * b
proof end;

Lm8: for F being Field
for a, b, c, d, f, g being Element of F st (a * b) - (c * d) = 0. F holds
(((a * f) * g) * b) - (((c * f) * g) * d) = 0. F
proof end;

Lm9: for F being Field
for a, b, c, d being Element of F holds (a - b) * (c - d) = (a * c) + ((- (a * d)) + (- (b * (c - d))))
proof end;

Lm10: for F being Field
for a, b, c, d being Element of F holds (a + b) + (c + d) = (a + (b + c)) + d
proof end;

Lm11: for F being non empty add-associative right_zeroed right_complementable LoopStr
for a, b, c being Element of F holds (b + a) - (c + a) = b - c
proof end;

Lm12: for F being non empty add-associative right_zeroed right_complementable LoopStr
for a, b being Element of F holds a + b = - ((- b) + (- a))
proof end;

Lm13: for F being Field
for a, b, c, d, e, f being Element of F st ((a - b) * (c - d)) - ((a - e) * (c - f)) = 0. F holds
((b - a) * (f - d)) - ((b - e) * (f - c)) = 0. F
proof end;

Lm14: for F being Field
for a, b, c being Element of F holds a - ((a + b) + (- c)) = c - b
proof end;

Lm15: for F being Field
for a, b, c, h, g, e being Element of F holds ((a - b) * (c - ((c + h) + (- g)))) - ((e - ((e + b) + (- a))) * (g - h)) = 0. F
proof end;

deffunc H1( Field) -> set = [:the carrier of $1,the carrier of $1,the carrier of $1:];

definition
let F be Field;
func c3add F -> BinOp of [:the carrier of F,the carrier of F,the carrier of F:] means :Def1: :: PARSP_1:def 1
for x, y being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds it . x,y = [((x `1 ) + (y `1 )),((x `2 ) + (y `2 )),((x `3 ) + (y `3 ))];
existence
ex b1 being BinOp of [:the carrier of F,the carrier of F,the carrier of F:] st
for x, y being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds b1 . x,y = [((x `1 ) + (y `1 )),((x `2 ) + (y `2 )),((x `3 ) + (y `3 ))]
proof end;
uniqueness
for b1, b2 being BinOp of [:the carrier of F,the carrier of F,the carrier of F:] st ( for x, y being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds b1 . x,y = [((x `1 ) + (y `1 )),((x `2 ) + (y `2 )),((x `3 ) + (y `3 ))] ) & ( for x, y being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds b2 . x,y = [((x `1 ) + (y `1 )),((x `2 ) + (y `2 )),((x `3 ) + (y `3 ))] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines c3add PARSP_1:def 1 :
for F being Field
for b2 being BinOp of [:the carrier of F,the carrier of F,the carrier of F:] holds
( b2 = c3add F iff for x, y being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds b2 . x,y = [((x `1 ) + (y `1 )),((x `2 ) + (y `2 )),((x `3 ) + (y `3 ))] );

definition
let F be Field;
let x, y be Element of [:the carrier of F,the carrier of F,the carrier of F:];
func x + y -> Element of [:the carrier of F,the carrier of F,the carrier of F:] equals :: PARSP_1:def 2
(c3add F) . x,y;
coherence
(c3add F) . x,y is Element of [:the carrier of F,the carrier of F,the carrier of F:] ;
end;

:: deftheorem defines + PARSP_1:def 2 :
for F being Field
for x, y being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds x + y = (c3add F) . x,y;

theorem :: PARSP_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARSP_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th3: :: PARSP_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for x, y being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds x + y = [((x `1 ) + (y `1 )),((x `2 ) + (y `2 )),((x `3 ) + (y `3 ))] by Def1;

theorem Th4: :: PARSP_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b, c, f, g, h being Element of F holds [a,b,c] + [f,g,h] = [(a + f),(b + g),(c + h)]
proof end;

definition
let F be Field;
func c3compl F -> UnOp of [:the carrier of F,the carrier of F,the carrier of F:] means :Def3: :: PARSP_1:def 3
for x being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds it . x = [(- (x `1 )),(- (x `2 )),(- (x `3 ))];
existence
ex b1 being UnOp of [:the carrier of F,the carrier of F,the carrier of F:] st
for x being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds b1 . x = [(- (x `1 )),(- (x `2 )),(- (x `3 ))]
proof end;
uniqueness
for b1, b2 being UnOp of [:the carrier of F,the carrier of F,the carrier of F:] st ( for x being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds b1 . x = [(- (x `1 )),(- (x `2 )),(- (x `3 ))] ) & ( for x being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds b2 . x = [(- (x `1 )),(- (x `2 )),(- (x `3 ))] ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines c3compl PARSP_1:def 3 :
for F being Field
for b2 being UnOp of [:the carrier of F,the carrier of F,the carrier of F:] holds
( b2 = c3compl F iff for x being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds b2 . x = [(- (x `1 )),(- (x `2 )),(- (x `3 ))] );

definition
let F be Field;
let x be Element of [:the carrier of F,the carrier of F,the carrier of F:];
func - x -> Element of [:the carrier of F,the carrier of F,the carrier of F:] equals :: PARSP_1:def 4
(c3compl F) . x;
coherence
(c3compl F) . x is Element of [:the carrier of F,the carrier of F,the carrier of F:] ;
end;

:: deftheorem defines - PARSP_1:def 4 :
for F being Field
for x being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds - x = (c3compl F) . x;

theorem :: PARSP_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARSP_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th7: :: PARSP_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for x being Element of [:the carrier of F,the carrier of F,the carrier of F:] holds - x = [(- (x `1 )),(- (x `2 )),(- (x `3 ))] by Def3;

definition
let S be set ;
mode Relation4 of S -> set means :Def5: :: PARSP_1:def 5
it c= [:S,S,S,S:];
existence
ex b1 being set st b1 c= [:S,S,S,S:] ;
end;

:: deftheorem Def5 defines Relation4 PARSP_1:def 5 :
for S, b2 being set holds
( b2 is Relation4 of S iff b2 c= [:S,S,S,S:] );

definition
attr c1 is strict;
struct ParStr -> 1-sorted ;
aggr ParStr(# carrier, 4_arg_relation #) -> ParStr ;
sel 4_arg_relation c1 -> Relation4 of the carrier of c1;
end;

registration
cluster non empty ParStr ;
existence
not for b1 being ParStr holds b1 is empty
proof end;
end;

definition
let PS be non empty ParStr ;
let a, b, c, d be Element of PS;
pred a,b '||' c,d means :Def6: :: PARSP_1:def 6
[a,b,c,d] in the 4_arg_relation of PS;
end;

:: deftheorem Def6 defines '||' PARSP_1:def 6 :
for PS being non empty ParStr
for a, b, c, d being Element of PS holds
( a,b '||' c,d iff [a,b,c,d] in the 4_arg_relation of PS );

definition
let F be Field;
func C3 F -> set equals :: PARSP_1:def 7
[:the carrier of F,the carrier of F,the carrier of F:];
coherence
[:the carrier of F,the carrier of F,the carrier of F:] is set ;
end;

:: deftheorem defines C3 PARSP_1:def 7 :
for F being Field holds C3 F = [:the carrier of F,the carrier of F,the carrier of F:];

registration
let F be Field;
cluster C3 F -> non empty ;
coherence
not C3 F is empty ;
end;

definition
let F be Field;
func 4C3 F -> set equals :: PARSP_1:def 8
[:(C3 F),(C3 F),(C3 F),(C3 F):];
coherence
[:(C3 F),(C3 F),(C3 F),(C3 F):] is set ;
end;

:: deftheorem defines 4C3 PARSP_1:def 8 :
for F being Field holds 4C3 F = [:(C3 F),(C3 F),(C3 F),(C3 F):];

registration
let F be Field;
cluster 4C3 F -> non empty ;
coherence
not 4C3 F is empty ;
end;

definition
let F be Field;
func PRs F -> set means :Def9: :: PARSP_1:def 9
for x being set holds
( x in it iff ( x in 4C3 F & ex a, b, c, d being Element of [:the carrier of F,the carrier of F,the carrier of F:] st
( x = [a,b,c,d] & (((a `1 ) - (b `1 )) * ((c `2 ) - (d `2 ))) - (((c `1 ) - (d `1 )) * ((a `2 ) - (b `2 ))) = 0. F & (((a `1 ) - (b `1 )) * ((c `3 ) - (d `3 ))) - (((c `1 ) - (d `1 )) * ((a `3 ) - (b `3 ))) = 0. F & (((a `2 ) - (b `2 )) * ((c `3 ) - (d `3 ))) - (((c `2 ) - (d `2 )) * ((a `3 ) - (b `3 ))) = 0. F ) ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x in 4C3 F & ex a, b, c, d being Element of [:the carrier of F,the carrier of F,the carrier of F:] st
( x = [a,b,c,d] & (((a `1 ) - (b `1 )) * ((c `2 ) - (d `2 ))) - (((c `1 ) - (d `1 )) * ((a `2 ) - (b `2 ))) = 0. F & (((a `1 ) - (b `1 )) * ((c `3 ) - (d `3 ))) - (((c `1 ) - (d `1 )) * ((a `3 ) - (b `3 ))) = 0. F & (((a `2 ) - (b `2 )) * ((c `3 ) - (d `3 ))) - (((c `2 ) - (d `2 )) * ((a `3 ) - (b `3 ))) = 0. F ) ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in 4C3 F & ex a, b, c, d being Element of [:the carrier of F,the carrier of F,the carrier of F:] st
( x = [a,b,c,d] & (((a `1 ) - (b `1 )) * ((c `2 ) - (d `2 ))) - (((c `1 ) - (d `1 )) * ((a `2 ) - (b `2 ))) = 0. F & (((a `1 ) - (b `1 )) * ((c `3 ) - (d `3 ))) - (((c `1 ) - (d `1 )) * ((a `3 ) - (b `3 ))) = 0. F & (((a `2 ) - (b `2 )) * ((c `3 ) - (d `3 ))) - (((c `2 ) - (d `2 )) * ((a `3 ) - (b `3 ))) = 0. F ) ) ) ) & ( for x being set holds
( x in b2 iff ( x in 4C3 F & ex a, b, c, d being Element of [:the carrier of F,the carrier of F,the carrier of F:] st
( x = [a,b,c,d] & (((a `1 ) - (b `1 )) * ((c `2 ) - (d `2 ))) - (((c `1 ) - (d `1 )) * ((a `2 ) - (b `2 ))) = 0. F & (((a `1 ) - (b `1 )) * ((c `3 ) - (d `3 ))) - (((c `1 ) - (d `1 )) * ((a `3 ) - (b `3 ))) = 0. F & (((a `2 ) - (b `2 )) * ((c `3 ) - (d `3 ))) - (((c `2 ) - (d `2 )) * ((a `3 ) - (b `3 ))) = 0. F ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines PRs PARSP_1:def 9 :
for F being Field
for b2 being set holds
( b2 = PRs F iff for x being set holds
( x in b2 iff ( x in 4C3 F & ex a, b, c, d being Element of [:the carrier of F,the carrier of F,the carrier of F:] st
( x = [a,b,c,d] & (((a `1 ) - (b `1 )) * ((c `2 ) - (d `2 ))) - (((c `1 ) - (d `1 )) * ((a `2 ) - (b `2 ))) = 0. F & (((a `1 ) - (b `1 )) * ((c `3 ) - (d `3 ))) - (((c `1 ) - (d `1 )) * ((a `3 ) - (b `3 ))) = 0. F & (((a `2 ) - (b `2 )) * ((c `3 ) - (d `3 ))) - (((c `2 ) - (d `2 )) * ((a `3 ) - (b `3 ))) = 0. F ) ) ) );

theorem :: PARSP_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARSP_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARSP_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARSP_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARSP_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th13: :: PARSP_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field holds PRs F c= [:(C3 F),(C3 F),(C3 F),(C3 F):]
proof end;

definition
let F be Field;
func PR F -> Relation4 of C3 F equals :: PARSP_1:def 10
 PRs F;
coherence
PRs F is Relation4 of C3 F
proof end;
end;

:: deftheorem defines PR PARSP_1:def 10 :
for F being Field holds PR F = PRs F;

definition
let F be Field;
func MPS F -> ParStr equals :: PARSP_1:def 11
 ParStr(# (C3 F),(PR F) #);
correctness
coherence
ParStr(# (C3 F),(PR F) #) is ParStr ;
;
end;

:: deftheorem defines MPS PARSP_1:def 11 :
for F being Field holds MPS F = ParStr(# (C3 F),(PR F) #);

registration
let F be Field;
cluster MPS F -> non empty strict ;
coherence
( MPS F is strict & not MPS F is empty )
proof end;
end;

theorem :: PARSP_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARSP_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARSP_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field holds the carrier of (MPS F) = C3 F ;

theorem :: PARSP_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field holds the 4_arg_relation of (MPS F) = PR F ;

theorem Th18: :: PARSP_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b, c, d being Element of (MPS F) holds
( a,b '||' c,d iff [a,b,c,d] in PR F ) by Def6;

theorem Th19: :: PARSP_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b, c, d being Element of (MPS F) holds
( [a,b,c,d] in PR F iff ( [a,b,c,d] in 4C3 F & ex e, f, g, h being Element of [:the carrier of F,the carrier of F,the carrier of F:] st
( [a,b,c,d] = [e,f,g,h] & (((e `1 ) - (f `1 )) * ((g `2 ) - (h `2 ))) - (((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) = 0. F & (((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 ))) - (((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 ))) = 0. F & (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) - (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) = 0. F ) ) ) by Def9;

theorem Th20: :: PARSP_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b, c, d being Element of (MPS F) holds
( a,b '||' c,d iff ( [a,b,c,d] in 4C3 F & ex e, f, g, h being Element of [:the carrier of F,the carrier of F,the carrier of F:] st
( [a,b,c,d] = [e,f,g,h] & (((e `1 ) - (f `1 )) * ((g `2 ) - (h `2 ))) - (((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) = 0. F & (((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 ))) - (((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 ))) = 0. F & (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) - (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) = 0. F ) ) )
proof end;

theorem :: PARSP_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field holds the carrier of (MPS F) = [:the carrier of F,the carrier of F,the carrier of F:] ;

theorem :: PARSP_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b, c, d being Element of (MPS F) holds [a,b,c,d] in 4C3 F ;

theorem Th23: :: PARSP_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b, c, d being Element of (MPS F) holds
( a,b '||' c,d iff ex e, f, g, h being Element of [:the carrier of F,the carrier of F,the carrier of F:] st
( [a,b,c,d] = [e,f,g,h] & (((e `1 ) - (f `1 )) * ((g `2 ) - (h `2 ))) - (((g `1 ) - (h `1 )) * ((e `2 ) - (f `2 ))) = 0. F & (((e `1 ) - (f `1 )) * ((g `3 ) - (h `3 ))) - (((g `1 ) - (h `1 )) * ((e `3 ) - (f `3 ))) = 0. F & (((e `2 ) - (f `2 )) * ((g `3 ) - (h `3 ))) - (((g `2 ) - (h `2 )) * ((e `3 ) - (f `3 ))) = 0. F ) )
proof end;

theorem Th24: :: PARSP_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b being Element of (MPS F) holds a,b '||' b,a
proof end;

theorem Th25: :: PARSP_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b, c being Element of (MPS F) holds a,b '||' c,c
proof end;

theorem Th26: :: PARSP_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b, p, q, r, s being Element of (MPS F) st a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s holds
a = b
proof end;

theorem Th27: :: PARSP_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b, c being Element of (MPS F) st a,b '||' a,c holds
b,a '||' b,c
proof end;

theorem Th28: :: PARSP_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Field
for a, b, c being Element of (MPS F) ex d being Element of (MPS F) st
( a,b '||' c,d & a,c '||' b,d )
proof end;

definition
let IT be non empty ParStr ;
attr IT is ParSp-like means :Def12: :: PARSP_1:def 12
for a, b, c, d, p, q, r, s being Element of IT holds
( a,b '||' b,a & a,b '||' c,c & ( a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s implies a = b ) & ( a,b '||' a,c implies b,a '||' b,c ) & ex x being Element of IT st
( a,b '||' c,x & a,c '||' b,x ) );
end;

:: deftheorem Def12 defines ParSp-like PARSP_1:def 12 :
for IT being non empty ParStr holds
( IT is ParSp-like iff for a, b, c, d, p, q, r, s being Element of IT holds
( a,b '||' b,a & a,b '||' c,c & ( a,b '||' p,q & a,b '||' r,s & not p,q '||' r,s implies a = b ) & ( a,b '||' a,c implies b,a '||' b,c ) & ex x being Element of IT st
( a,b '||' c,x & a,c '||' b,x ) ) );

registration
cluster non empty strict ParSp-like ParStr ;
existence
ex b1 being non empty ParStr st
( b1 is strict & b1 is ParSp-like )
proof end;
end;

definition
mode ParSp is non empty ParSp-like ParStr ;
end;

theorem :: PARSP_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARSP_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARSP_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARSP_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARSP_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: PARSP_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th35: :: PARSP_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp
for a, b being Element of PS holds a,b '||' a,b
proof end;

theorem Th36: :: PARSP_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp
for a, b, c, d being Element of PS st a,b '||' c,d holds
c,d '||' a,b
proof end;

theorem Th37: :: PARSP_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp
for a, b, c being Element of PS holds a,a '||' b,c
proof end;

theorem Th38: :: PARSP_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp
for a, b, c, d being Element of PS st a,b '||' c,d holds
b,a '||' c,d
proof end;

theorem Th39: :: PARSP_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp
for a, b, c, d being Element of PS st a,b '||' c,d holds
a,b '||' d,c
proof end;

theorem Th40: :: PARSP_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp
for a, b, c, d being Element of PS st a,b '||' c,d holds
( b,a '||' c,d & a,b '||' d,c & b,a '||' d,c & c,d '||' a,b & d,c '||' a,b & c,d '||' b,a & d,c '||' b,a )
proof end;

theorem Th41: :: PARSP_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp
for a, b, c being Element of PS st a,b '||' a,c holds
( a,c '||' a,b & b,a '||' a,c & a,b '||' c,a & a,c '||' b,a & b,a '||' c,a & c,a '||' a,b & c,a '||' b,a & b,a '||' b,c & a,b '||' b,c & b,a '||' c,b & b,c '||' b,a & a,b '||' c,b & c,b '||' b,a & b,c '||' a,b & c,b '||' a,b & c,a '||' c,b & a,c '||' c,b & c,a '||' b,c & a,c '||' b,c & c,b '||' c,a & b,c '||' c,a & c,b '||' a,c & b,c '||' a,c )
proof end;

theorem :: PARSP_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp
for a, b, c, d being Element of PS st ( a = b or c = d or ( a = c & b = d ) or ( a = d & b = c ) ) holds
a,b '||' c,d by Def12, Th35, Th37;

theorem Th43: :: PARSP_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp
for a, b, p, q, r, s being Element of PS st a <> b & p,q '||' a,b & a,b '||' r,s holds
p,q '||' r,s
proof end;

theorem :: PARSP_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp
for a, b, c being Element of PS st not a,b '||' a,c holds
( a <> b & b <> c & c <> a ) by Def12, Th35, Th37;

theorem :: PARSP_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp
for a, b, c, d being Element of PS st not a,b '||' c,d holds
( a <> b & c <> d ) by Def12, Th37;

theorem :: PARSP_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th47: :: PARSP_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp
for a, b, c being Element of PS st not a,b '||' a,c holds
( not a,c '||' a,b & not b,a '||' a,c & not a,b '||' c,a & not a,c '||' b,a & not b,a '||' c,a & not c,a '||' a,b & not c,a '||' b,a & not b,a '||' b,c & not a,b '||' b,c & not b,a '||' c,b & not b,c '||' b,a & not b,a '||' c,b & not c,b '||' b,a & not b,c '||' a,b & not c,b '||' a,b & not c,a '||' c,b & not a,c '||' c,b & not c,a '||' b,c & not a,c '||' b,c & not c,b '||' c,a & not b,c '||' c,a & not c,b '||' a,c & not b,c '||' a,c )
proof end;

theorem Th48: :: PARSP_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp
for a, b, c, d, p, q, r, s being Element of PS st not a,b '||' c,d & a,b '||' p,q & c,d '||' r,s & p <> q & r <> s holds
not p,q '||' r,s
proof end;

theorem Th49: :: PARSP_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp
for a, b, c, p, q, r being Element of PS st not a,b '||' a,c & a,b '||' p,q & a,c '||' p,r & b,c '||' q,r & p <> q holds
not p,q '||' p,r
proof end;

theorem Th50: :: PARSP_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp
for a, b, c, p, r being Element of PS st not a,b '||' a,c & a,c '||' p,r & b,c '||' p,r holds
p = r
proof end;

theorem Th51: :: PARSP_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp
for p, q, r, s being Element of PS st not p,q '||' p,r & p,r '||' p,s & q,r '||' q,s holds
r = s
proof end;

theorem :: PARSP_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp
for a, b, c, p, q, r, s being Element of PS st not a,b '||' a,c & a,b '||' p,q & a,c '||' p,r & a,c '||' p,s & b,c '||' q,r & b,c '||' q,s holds
r = s
proof end;

theorem Th53: :: PARSP_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp
for a, b, c, d being Element of PS st a,b '||' a,c & a,b '||' a,d holds
a,b '||' c,d
proof end;

theorem :: PARSP_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp st ( for a, b being Element of PS holds a = b ) holds
for p, q, r, s being Element of PS holds p,q '||' r,s
proof end;

theorem :: PARSP_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp st ex a, b being Element of PS st
( a <> b & ( for c being Element of PS holds a,b '||' a,c ) ) holds
for p, q, r, s being Element of PS holds p,q '||' r,s
proof end;

theorem :: PARSP_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for PS being ParSp
for a, b, c, p, q being Element of PS st not a,b '||' a,c & p <> q & p,q '||' p,a & p,q '||' p,b holds
not p,q '||' p,c
proof end;