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

definition
let D be set ;
attr D is with_VERUM means :Def1: :: HILBERT1:def 1
<*0*> in D;
end;

:: deftheorem Def1 defines with_VERUM HILBERT1:def 1 :
for D being set holds
( D is with_VERUM iff <*0*> in D );

definition
let D be set ;
attr D is with_implication means :Def2: :: HILBERT1:def 2
for p, q being FinSequence st p in D & q in D holds
(<*1*> ^ p) ^ q in D;
end;

:: deftheorem Def2 defines with_implication HILBERT1:def 2 :
for D being set holds
( D is with_implication iff for p, q being FinSequence st p in D & q in D holds
(<*1*> ^ p) ^ q in D );

definition
let D be set ;
attr D is with_conjunction means :Def3: :: HILBERT1:def 3
for p, q being FinSequence st p in D & q in D holds
(<*2*> ^ p) ^ q in D;
end;

:: deftheorem Def3 defines with_conjunction HILBERT1:def 3 :
for D being set holds
( D is with_conjunction iff for p, q being FinSequence st p in D & q in D holds
(<*2*> ^ p) ^ q in D );

definition
let D be set ;
attr D is with_propositional_variables means :Def4: :: HILBERT1:def 4
for n being Nat holds <*(3 + n)*> in D;
end;

:: deftheorem Def4 defines with_propositional_variables HILBERT1:def 4 :
for D being set holds
( D is with_propositional_variables iff for n being Nat holds <*(3 + n)*> in D );

definition
let D be set ;
attr D is HP-closed means :Def5: :: HILBERT1:def 5
( D c= NAT * & D is with_VERUM & D is with_implication & D is with_conjunction & D is with_propositional_variables );
end;

:: deftheorem Def5 defines HP-closed HILBERT1:def 5 :
for D being set holds
( D is HP-closed iff ( D c= NAT * & D is with_VERUM & D is with_implication & D is with_conjunction & D is with_propositional_variables ) );

Lm1: for D being set st D is HP-closed holds
not D is empty
proof end;

registration
cluster HP-closed -> non empty with_VERUM with_implication with_conjunction with_propositional_variables set ;
coherence
for b1 being set st b1 is HP-closed holds
( b1 is with_VERUM & b1 is with_implication & b1 is with_conjunction & b1 is with_propositional_variables & not b1 is empty ) by Def5, Lm1;
cluster with_VERUM with_implication with_conjunction with_propositional_variables -> HP-closed Element of K40((NAT * ));
coherence
for b1 being Subset of (NAT * ) st b1 is with_VERUM & b1 is with_implication & b1 is with_conjunction & b1 is with_propositional_variables holds
b1 is HP-closed by Def5;
end;

definition
func HP-WFF -> set means :Def6: :: HILBERT1:def 6
( it is HP-closed & ( for D being set st D is HP-closed holds
it c= D ) );
existence
ex b1 being set st
( b1 is HP-closed & ( for D being set st D is HP-closed holds
b1 c= D ) )
proof end;
uniqueness
for b1, b2 being set st b1 is HP-closed & ( for D being set st D is HP-closed holds
b1 c= D ) & b2 is HP-closed & ( for D being set st D is HP-closed holds
b2 c= D ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines HP-WFF HILBERT1:def 6 :
for b1 being set holds
( b1 = HP-WFF iff ( b1 is HP-closed & ( for D being set st D is HP-closed holds
b1 c= D ) ) );

registration
cluster HP-WFF -> non empty with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ;
coherence
HP-WFF is HP-closed by Def6;
end;

registration
cluster non empty with_VERUM with_implication with_conjunction with_propositional_variables HP-closed set ;
existence
ex b1 being set st
( b1 is HP-closed & not b1 is empty )
proof end;
end;

registration
cluster HP-WFF -> non empty functional with_VERUM with_implication with_conjunction with_propositional_variables HP-closed ;
coherence
HP-WFF is functional
proof end;
end;

registration
cluster -> FinSequence-like Element of HP-WFF ;
coherence
for b1 being Element of HP-WFF holds b1 is FinSequence-like
proof end;
end;

definition
mode HP-formula is Element of HP-WFF ;
end;

definition
func VERUM -> HP-formula equals :: HILBERT1:def 7
<*0*>;
correctness
coherence
<*0*> is HP-formula;
by Def1;
let p, q be Element of HP-WFF ;
func p => q -> HP-formula equals :: HILBERT1:def 8
(<*1*> ^ p) ^ q;
coherence
(<*1*> ^ p) ^ q is HP-formula by Def2;
func p '&' q -> HP-formula equals :: HILBERT1:def 9
(<*2*> ^ p) ^ q;
correctness
coherence
(<*2*> ^ p) ^ q is HP-formula;
by Def3;
end;

:: deftheorem defines VERUM HILBERT1:def 7 :
VERUM = <*0*>;

:: deftheorem defines => HILBERT1:def 8 :
for p, q being Element of HP-WFF holds p => q = (<*1*> ^ p) ^ q;

:: deftheorem defines '&' HILBERT1:def 9 :
for p, q being Element of HP-WFF holds p '&' q = (<*2*> ^ p) ^ q;

definition
let T be Subset of HP-WFF ;
attr T is Hilbert_theory means :Def10: :: HILBERT1:def 10
( VERUM in T & ( for p, q, r being Element of HP-WFF holds
( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & ( p in T & p => q in T implies q in T ) ) ) );
correctness
;
end;

:: deftheorem Def10 defines Hilbert_theory HILBERT1:def 10 :
for T being Subset of HP-WFF holds
( T is Hilbert_theory iff ( VERUM in T & ( for p, q, r being Element of HP-WFF holds
( p => (q => p) in T & (p => (q => r)) => ((p => q) => (p => r)) in T & (p '&' q) => p in T & (p '&' q) => q in T & p => (q => (p '&' q)) in T & ( p in T & p => q in T implies q in T ) ) ) ) );

definition
let X be Subset of HP-WFF ;
func CnPos X -> Subset of HP-WFF means :Def11: :: HILBERT1:def 11
for r being Element of HP-WFF holds
( r in it iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T );
existence
ex b1 being Subset of HP-WFF st
for r being Element of HP-WFF holds
( r in b1 iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T )
proof end;
uniqueness
for b1, b2 being Subset of HP-WFF st ( for r being Element of HP-WFF holds
( r in b1 iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) ) & ( for r being Element of HP-WFF holds
( r in b2 iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines CnPos HILBERT1:def 11 :
for X, b2 being Subset of HP-WFF holds
( b2 = CnPos X iff for r being Element of HP-WFF holds
( r in b2 iff for T being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
r in T ) );

definition
func HP_TAUT -> Subset of HP-WFF equals :: HILBERT1:def 12
 CnPos ({} HP-WFF );
correctness
coherence
CnPos ({} HP-WFF ) is Subset of HP-WFF ;
;
end;

:: deftheorem defines HP_TAUT HILBERT1:def 12 :
HP_TAUT = CnPos ({} HP-WFF );

theorem Th1: :: HILBERT1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of HP-WFF holds VERUM in CnPos X
proof end;

theorem Th2: :: HILBERT1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of HP-WFF
for p, q being Element of HP-WFF holds p => (q => (p '&' q)) in CnPos X
proof end;

theorem Th3: :: HILBERT1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of HP-WFF
for p, q, r being Element of HP-WFF holds (p => (q => r)) => ((p => q) => (p => r)) in CnPos X
proof end;

theorem Th4: :: HILBERT1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of HP-WFF
for p, q being Element of HP-WFF holds p => (q => p) in CnPos X
proof end;

theorem Th5: :: HILBERT1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of HP-WFF
for p, q being Element of HP-WFF holds (p '&' q) => p in CnPos X
proof end;

theorem Th6: :: HILBERT1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of HP-WFF
for p, q being Element of HP-WFF holds (p '&' q) => q in CnPos X
proof end;

theorem Th7: :: HILBERT1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of HP-WFF
for p, q being Element of HP-WFF st p in CnPos X & p => q in CnPos X holds
q in CnPos X
proof end;

theorem Th8: :: HILBERT1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T, X being Subset of HP-WFF st T is Hilbert_theory & X c= T holds
CnPos X c= T
proof end;

theorem Th9: :: HILBERT1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of HP-WFF holds X c= CnPos X
proof end;

theorem Th10: :: HILBERT1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being Subset of HP-WFF st X c= Y holds
CnPos X c= CnPos Y
proof end;

Lm2: for X being Subset of HP-WFF holds CnPos (CnPos X) c= CnPos X
proof end;

theorem :: HILBERT1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being Subset of HP-WFF holds CnPos (CnPos X) = CnPos X
proof end;

Lm3: for X being Subset of HP-WFF holds CnPos X is Hilbert_theory
proof end;

registration
let X be Subset of HP-WFF ;
cluster CnPos X -> Hilbert_theory ;
coherence
CnPos X is Hilbert_theory by Lm3;
end;

theorem Th12: :: HILBERT1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Subset of HP-WFF holds
( T is Hilbert_theory iff CnPos T = T )
proof end;

theorem :: HILBERT1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Subset of HP-WFF st T is Hilbert_theory holds
HP_TAUT c= T
proof end;

registration
cluster HP_TAUT -> Hilbert_theory ;
coherence
HP_TAUT is Hilbert_theory ;
end;

theorem Th14: :: HILBERT1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of HP-WFF holds p => p in HP_TAUT
proof end;

theorem Th15: :: HILBERT1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q, p being Element of HP-WFF st q in HP_TAUT holds
p => q in HP_TAUT
proof end;

theorem :: HILBERT1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of HP-WFF holds p => VERUM in HP_TAUT
proof end;

theorem :: HILBERT1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF holds (p => q) => (p => p) in HP_TAUT
proof end;

theorem :: HILBERT1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q, p being Element of HP-WFF holds (q => p) => (p => p) in HP_TAUT
proof end;

theorem Th19: :: HILBERT1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q, r, p being Element of HP-WFF holds (q => r) => ((p => q) => (p => r)) in HP_TAUT
proof end;

theorem Th20: :: HILBERT1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r being Element of HP-WFF st p => (q => r) in HP_TAUT holds
q => (p => r) in HP_TAUT
proof end;

theorem Th21: :: HILBERT1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r being Element of HP-WFF holds (p => q) => ((q => r) => (p => r)) in HP_TAUT
proof end;

theorem Th22: :: HILBERT1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r being Element of HP-WFF st p => q in HP_TAUT holds
(q => r) => (p => r) in HP_TAUT
proof end;

theorem Th23: :: HILBERT1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r being Element of HP-WFF st p => q in HP_TAUT & q => r in HP_TAUT holds
p => r in HP_TAUT
proof end;

Lm4: for q, r, p, s being Element of HP-WFF holds (((q => r) => (p => r)) => s) => ((p => q) => s) in HP_TAUT
proof end;

theorem Th24: :: HILBERT1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r, s being Element of HP-WFF holds (p => (q => r)) => ((s => q) => (p => (s => r))) in HP_TAUT
proof end;

theorem :: HILBERT1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r being Element of HP-WFF holds ((p => q) => r) => (q => r) in HP_TAUT
proof end;

theorem Th26: :: HILBERT1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r being Element of HP-WFF holds (p => (q => r)) => (q => (p => r)) in HP_TAUT
proof end;

theorem Th27: :: HILBERT1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF holds (p => (p => q)) => (p => q) in HP_TAUT
proof end;

theorem :: HILBERT1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q, p being Element of HP-WFF holds q => ((q => p) => p) in HP_TAUT
proof end;

theorem Th29: :: HILBERT1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for s, q, p being Element of HP-WFF st s => (q => p) in HP_TAUT & q in HP_TAUT holds
s => p in HP_TAUT
proof end;

theorem Th30: :: HILBERT1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being Element of HP-WFF holds p => (p '&' p) in HP_TAUT
proof end;

theorem Th31: :: HILBERT1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF holds
( p '&' q in HP_TAUT iff ( p in HP_TAUT & q in HP_TAUT ) )
proof end;

theorem :: HILBERT1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF holds
( p '&' q in HP_TAUT iff q '&' p in HP_TAUT )
proof end;

theorem Th33: :: HILBERT1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r being Element of HP-WFF holds ((p '&' q) => r) => (p => (q => r)) in HP_TAUT
proof end;

theorem Th34: :: HILBERT1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, r being Element of HP-WFF holds (p => (q => r)) => ((p '&' q) => r) in HP_TAUT
proof end;

theorem Th35: :: HILBERT1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for r, p, q being Element of HP-WFF holds (r => p) => ((r => q) => (r => (p '&' q))) in HP_TAUT
proof end;

theorem Th36: :: HILBERT1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF holds ((p => q) '&' p) => q in HP_TAUT
proof end;

theorem :: HILBERT1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, s being Element of HP-WFF holds (((p => q) '&' p) '&' s) => q in HP_TAUT
proof end;

theorem :: HILBERT1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q, s, p being Element of HP-WFF holds (q => s) => ((p '&' q) => s) in HP_TAUT
proof end;

theorem Th39: :: HILBERT1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q, s, p being Element of HP-WFF holds (q => s) => ((q '&' p) => s) in HP_TAUT
proof end;

theorem Th40: :: HILBERT1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, s, q being Element of HP-WFF holds ((p '&' s) => q) => ((p '&' s) => (q '&' s)) in HP_TAUT
proof end;

theorem Th41: :: HILBERT1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, s being Element of HP-WFF holds (p => q) => ((p '&' s) => (q '&' s)) in HP_TAUT
proof end;

theorem Th42: :: HILBERT1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, s being Element of HP-WFF holds ((p => q) '&' (p '&' s)) => (q '&' s) in HP_TAUT
proof end;

theorem Th43: :: HILBERT1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being Element of HP-WFF holds (p '&' q) => (q '&' p) in HP_TAUT
proof end;

theorem Th44: :: HILBERT1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, s being Element of HP-WFF holds ((p => q) '&' (p '&' s)) => (s '&' q) in HP_TAUT
proof end;

theorem Th45: :: HILBERT1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, s being Element of HP-WFF holds (p => q) => ((p '&' s) => (s '&' q)) in HP_TAUT
proof end;

theorem Th46: :: HILBERT1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, s being Element of HP-WFF holds (p => q) => ((s '&' p) => (s '&' q)) in HP_TAUT
proof end;

theorem :: HILBERT1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, s, q being Element of HP-WFF holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT
proof end;

theorem :: HILBERT1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, s being Element of HP-WFF holds ((p => q) '&' (p => s)) => (p => (q '&' s)) in HP_TAUT
proof end;

Lm5: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => q in HP_TAUT
proof end;

Lm6: for p, q, s being Element of HP-WFF holds (((p '&' q) '&' s) '&' ((p '&' q) '&' s)) => (((p '&' q) '&' s) '&' q) in HP_TAUT
proof end;

Lm7: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (((p '&' q) '&' s) '&' q) in HP_TAUT
proof end;

Lm8: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' s) in HP_TAUT
proof end;

Lm9: for p, q, s being Element of HP-WFF holds (((p '&' q) '&' s) '&' q) => ((p '&' s) '&' q) in HP_TAUT
proof end;

Lm10: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((p '&' s) '&' q) in HP_TAUT
proof end;

Lm11: for p, s, q being Element of HP-WFF holds ((p '&' s) '&' q) => ((s '&' p) '&' q) in HP_TAUT
proof end;

Lm12: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((s '&' p) '&' q) in HP_TAUT
proof end;

Lm13: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => ((s '&' q) '&' p) in HP_TAUT
proof end;

Lm14: for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' (s '&' q)) in HP_TAUT
proof end;

Lm15: for p, s, q being Element of HP-WFF holds (p '&' (s '&' q)) => (p '&' (q '&' s)) in HP_TAUT
proof end;

theorem :: HILBERT1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, s being Element of HP-WFF holds ((p '&' q) '&' s) => (p '&' (q '&' s)) in HP_TAUT
proof end;

Lm16: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((s '&' q) '&' p) in HP_TAUT
proof end;

Lm17: for s, q, p being Element of HP-WFF holds ((s '&' q) '&' p) => ((q '&' s) '&' p) in HP_TAUT
proof end;

Lm18: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((q '&' s) '&' p) in HP_TAUT
proof end;

Lm19: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((p '&' s) '&' q) in HP_TAUT
proof end;

Lm20: for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => (p '&' (s '&' q)) in HP_TAUT
proof end;

theorem :: HILBERT1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, s being Element of HP-WFF holds (p '&' (q '&' s)) => ((p '&' q) '&' s) in HP_TAUT
proof end;