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

theorem Th1: :: QC_LANG2:1  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 QC-WFF st 'not' p = 'not' q holds
p = q by FINSEQ_1:46;

theorem Th2: :: QC_LANG2:2  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 QC-WFF holds the_argument_of ('not' p) = p
proof end;

theorem Th3: :: QC_LANG2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, p1, q1 being Element of QC-WFF st p '&' q = p1 '&' q1 holds
( p = p1 & q = q1 )
proof end;

theorem Th4: :: QC_LANG2:4  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 QC-WFF st p is conjunctive holds
p = (the_left_argument_of p) '&' (the_right_argument_of p)
proof end;

theorem Th5: :: QC_LANG2:5  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 QC-WFF holds
( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q )
proof end;

theorem Th6: :: QC_LANG2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being bound_QC-variable
for p, q being Element of QC-WFF st All x,p = All y,q holds
( x = y & p = q )
proof end;

theorem Th7: :: QC_LANG2:7  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 QC-WFF st p is universal holds
p = All (bound_in p),(the_scope_of p)
proof end;

theorem Th8: :: QC_LANG2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for p being Element of QC-WFF holds
( bound_in (All x,p) = x & the_scope_of (All x,p) = p )
proof end;

definition
func FALSUM -> QC-formula equals :: QC_LANG2:def 1
'not' VERUM ;
correctness
coherence
'not' VERUM is QC-formula
;
;
let p, q be Element of QC-WFF ;
func p => q -> QC-formula equals :: QC_LANG2:def 2
'not' (p '&' ('not' q));
correctness
coherence
'not' (p '&' ('not' q)) is QC-formula
;
;
func p 'or' q -> QC-formula equals :: QC_LANG2:def 3
'not' (('not' p) '&' ('not' q));
correctness
coherence
'not' (('not' p) '&' ('not' q)) is QC-formula
;
;
end;

:: deftheorem defines FALSUM QC_LANG2:def 1 :
FALSUM = 'not' VERUM ;

:: deftheorem defines => QC_LANG2:def 2 :
for p, q being Element of QC-WFF holds p => q = 'not' (p '&' ('not' q));

:: deftheorem defines 'or' QC_LANG2:def 3 :
for p, q being Element of QC-WFF holds p 'or' q = 'not' (('not' p) '&' ('not' q));

definition
let p, q be Element of QC-WFF ;
func p <=> q -> QC-formula equals :: QC_LANG2:def 4
(p => q) '&' (q => p);
correctness
coherence
(p => q) '&' (q => p) is QC-formula
;
;
end;

:: deftheorem defines <=> QC_LANG2:def 4 :
for p, q being Element of QC-WFF holds p <=> q = (p => q) '&' (q => p);

definition
let x be bound_QC-variable;
let p be Element of QC-WFF ;
func Ex x,p -> QC-formula equals :: QC_LANG2:def 5
'not' (All x,('not' p));
correctness
coherence
'not' (All x,('not' p)) is QC-formula
;
;
end;

:: deftheorem defines Ex QC_LANG2:def 5 :
for x being bound_QC-variable
for p being Element of QC-WFF holds Ex x,p = 'not' (All x,('not' p));

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

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

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

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

theorem :: QC_LANG2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( FALSUM is negative & the_argument_of FALSUM = VERUM ) by Th2, QC_LANG1:def 18;

theorem :: QC_LANG2:14  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 QC-WFF holds p 'or' q = ('not' p) => q ;

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

theorem :: QC_LANG2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, p1, q1 being Element of QC-WFF st p 'or' q = p1 'or' q1 holds
( p = p1 & q = q1 )
proof end;

theorem Th17: :: QC_LANG2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, p1, q1 being Element of QC-WFF st p => q = p1 => q1 holds
( p = p1 & q = q1 )
proof end;

theorem :: QC_LANG2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q, p1, q1 being Element of QC-WFF st p <=> q = p1 <=> q1 holds
( p = p1 & q = q1 )
proof end;

theorem Th19: :: QC_LANG2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being bound_QC-variable
for p, q being Element of QC-WFF st Ex x,p = Ex y,q holds
( x = y & p = q )
proof end;

definition
let x, y be bound_QC-variable;
let p be Element of QC-WFF ;
func All x,y,p -> QC-formula equals :: QC_LANG2:def 6
All x,(All y,p);
correctness
coherence
All x,(All y,p) is QC-formula
;
;
func Ex x,y,p -> QC-formula equals :: QC_LANG2:def 7
Ex x,(Ex y,p);
correctness
coherence
Ex x,(Ex y,p) is QC-formula
;
;
end;

:: deftheorem defines All QC_LANG2:def 6 :
for x, y being bound_QC-variable
for p being Element of QC-WFF holds All x,y,p = All x,(All y,p);

:: deftheorem defines Ex QC_LANG2:def 7 :
for x, y being bound_QC-variable
for p being Element of QC-WFF holds Ex x,y,p = Ex x,(Ex y,p);

theorem :: QC_LANG2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being bound_QC-variable
for p being Element of QC-WFF holds
( All x,y,p = All x,(All y,p) & Ex x,y,p = Ex x,(Ex y,p) ) ;

theorem Th21: :: QC_LANG2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being Element of QC-WFF
for x1, x2, y1, y2 being bound_QC-variable st All x1,y1,p1 = All x2,y2,p2 holds
( x1 = x2 & y1 = y2 & p1 = p2 )
proof end;

theorem Th22: :: QC_LANG2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being bound_QC-variable
for p, q being Element of QC-WFF st All x,y,p = All z,q holds
( x = z & All y,p = q ) by Th6;

theorem Th23: :: QC_LANG2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being Element of QC-WFF
for x1, x2, y1, y2 being bound_QC-variable st Ex x1,y1,p1 = Ex x2,y2,p2 holds
( x1 = x2 & y1 = y2 & p1 = p2 )
proof end;

theorem Th24: :: QC_LANG2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being bound_QC-variable
for p, q being Element of QC-WFF st Ex x,y,p = Ex z,q holds
( x = z & Ex y,p = q ) by Th19;

theorem :: QC_LANG2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being bound_QC-variable
for p being Element of QC-WFF holds
( All x,y,p is universal & bound_in (All x,y,p) = x & the_scope_of (All x,y,p) = All y,p ) by Th8, QC_LANG1:def 20;

definition
let x, y, z be bound_QC-variable;
let p be Element of QC-WFF ;
func All x,y,z,p -> QC-formula equals :: QC_LANG2:def 8
All x,(All y,z,p);
correctness
coherence
All x,(All y,z,p) is QC-formula
;
;
func Ex x,y,z,p -> QC-formula equals :: QC_LANG2:def 9
Ex x,(Ex y,z,p);
correctness
coherence
Ex x,(Ex y,z,p) is QC-formula
;
;
end;

:: deftheorem defines All QC_LANG2:def 8 :
for x, y, z being bound_QC-variable
for p being Element of QC-WFF holds All x,y,z,p = All x,(All y,z,p);

:: deftheorem defines Ex QC_LANG2:def 9 :
for x, y, z being bound_QC-variable
for p being Element of QC-WFF holds Ex x,y,z,p = Ex x,(Ex y,z,p);

theorem :: QC_LANG2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being bound_QC-variable
for p being Element of QC-WFF holds
( All x,y,z,p = All x,(All y,z,p) & Ex x,y,z,p = Ex x,(Ex y,z,p) ) ;

theorem :: QC_LANG2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being Element of QC-WFF
for x1, x2, y1, y2, z1, z2 being bound_QC-variable st All x1,y1,z1,p1 = All x2,y2,z2,p2 holds
( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 )
proof end;

theorem :: QC_LANG2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being bound_QC-variable
for p, q being Element of QC-WFF
for t being bound_QC-variable st All x,y,z,p = All t,q holds
( x = t & All y,z,p = q ) by Th6;

theorem :: QC_LANG2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being bound_QC-variable
for p, q being Element of QC-WFF
for t, s being bound_QC-variable st All x,y,z,p = All t,s,q holds
( x = t & y = s & All z,p = q )
proof end;

theorem :: QC_LANG2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being Element of QC-WFF
for x1, x2, y1, y2, z1, z2 being bound_QC-variable st Ex x1,y1,z1,p1 = Ex x2,y2,z2,p2 holds
( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 )
proof end;

theorem :: QC_LANG2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being bound_QC-variable
for p, q being Element of QC-WFF
for t being bound_QC-variable st Ex x,y,z,p = Ex t,q holds
( x = t & Ex y,z,p = q ) by Th19;

theorem :: QC_LANG2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being bound_QC-variable
for p, q being Element of QC-WFF
for t, s being bound_QC-variable st Ex x,y,z,p = Ex t,s,q holds
( x = t & y = s & Ex z,p = q )
proof end;

theorem :: QC_LANG2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being bound_QC-variable
for p being Element of QC-WFF holds
( All x,y,z,p is universal & bound_in (All x,y,z,p) = x & the_scope_of (All x,y,z,p) = All y,z,p ) by Th8, QC_LANG1:def 20;

definition
let H be Element of QC-WFF ;
attr H is disjunctive means :: QC_LANG2:def 10
ex p, q being Element of QC-WFF st H = p 'or' q;
attr H is conditional means :Def11: :: QC_LANG2:def 11
ex p, q being Element of QC-WFF st H = p => q;
attr H is biconditional means :: QC_LANG2:def 12
ex p, q being Element of QC-WFF st H = p <=> q;
attr H is existential means :Def13: :: QC_LANG2:def 13
ex x being bound_QC-variable ex p being Element of QC-WFF st H = Ex x,p;
end;

:: deftheorem defines disjunctive QC_LANG2:def 10 :
for H being Element of QC-WFF holds
( H is disjunctive iff ex p, q being Element of QC-WFF st H = p 'or' q );

:: deftheorem Def11 defines conditional QC_LANG2:def 11 :
for H being Element of QC-WFF holds
( H is conditional iff ex p, q being Element of QC-WFF st H = p => q );

:: deftheorem defines biconditional QC_LANG2:def 12 :
for H being Element of QC-WFF holds
( H is biconditional iff ex p, q being Element of QC-WFF st H = p <=> q );

:: deftheorem Def13 defines existential QC_LANG2:def 13 :
for H being Element of QC-WFF holds
( H is existential iff ex x being bound_QC-variable ex p being Element of QC-WFF st H = Ex x,p );

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

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

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

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

theorem :: QC_LANG2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being bound_QC-variable
for p being Element of QC-WFF holds
( Ex x,y,p is existential & Ex x,y,z,p is existential ) by Def13;

definition
let H be Element of QC-WFF ;
func the_left_disjunct_of H -> QC-formula equals :: QC_LANG2:def 14
the_argument_of (the_left_argument_of (the_argument_of H));
correctness
coherence
the_argument_of (the_left_argument_of (the_argument_of H)) is QC-formula
;
;
func the_right_disjunct_of H -> QC-formula equals :: QC_LANG2:def 15
the_argument_of (the_right_argument_of (the_argument_of H));
correctness
coherence
the_argument_of (the_right_argument_of (the_argument_of H)) is QC-formula
;
;
func the_antecedent_of H -> QC-formula equals :: QC_LANG2:def 16
the_left_argument_of (the_argument_of H);
correctness
coherence
the_left_argument_of (the_argument_of H) is QC-formula
;
;
end;

:: deftheorem defines the_left_disjunct_of QC_LANG2:def 14 :
for H being Element of QC-WFF holds the_left_disjunct_of H = the_argument_of (the_left_argument_of (the_argument_of H));

:: deftheorem defines the_right_disjunct_of QC_LANG2:def 15 :
for H being Element of QC-WFF holds the_right_disjunct_of H = the_argument_of (the_right_argument_of (the_argument_of H));

:: deftheorem defines the_antecedent_of QC_LANG2:def 16 :
for H being Element of QC-WFF holds the_antecedent_of H = the_left_argument_of (the_argument_of H);

notation
let H be Element of QC-WFF ;
synonym the_consequent_of H for the_right_disjunct_of H;
end;

definition
let H be Element of QC-WFF ;
canceled;
func the_left_side_of H -> QC-formula equals :: QC_LANG2:def 18
the_antecedent_of (the_left_argument_of H);
correctness
coherence
the_antecedent_of (the_left_argument_of H) is QC-formula
;
;
func the_right_side_of H -> QC-formula equals :: QC_LANG2:def 19
the_consequent_of (the_left_argument_of H);
correctness
coherence
the_consequent_of (the_left_argument_of H) is QC-formula
;
;
end;

:: deftheorem QC_LANG2:def 17 :
canceled;

:: deftheorem defines the_left_side_of QC_LANG2:def 18 :
for H being Element of QC-WFF holds the_left_side_of H = the_antecedent_of (the_left_argument_of H);

:: deftheorem defines the_right_side_of QC_LANG2:def 19 :
for H being Element of QC-WFF holds the_right_side_of H = the_consequent_of (the_left_argument_of H);

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

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

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

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

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

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

theorem Th45: :: QC_LANG2:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being Element of QC-WFF holds
( the_left_disjunct_of (F 'or' G) = F & the_right_disjunct_of (F 'or' G) = G & the_argument_of (F 'or' G) = ('not' F) '&' ('not' G) )
proof end;

theorem Th46: :: QC_LANG2:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being Element of QC-WFF holds
( the_antecedent_of (F => G) = F & the_consequent_of (F => G) = G & the_argument_of (F => G) = F '&' ('not' G) )
proof end;

theorem Th47: :: QC_LANG2:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being Element of QC-WFF holds
( the_left_side_of (F <=> G) = F & the_right_side_of (F <=> G) = G & the_left_argument_of (F <=> G) = F => G & the_right_argument_of (F <=> G) = G => F )
proof end;

theorem :: QC_LANG2:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being bound_QC-variable
for H being Element of QC-WFF holds the_argument_of (Ex x,H) = All x,('not' H) by Th2;

theorem :: QC_LANG2:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF st H is disjunctive holds
( H is conditional & H is negative & the_argument_of H is conjunctive & the_left_argument_of (the_argument_of H) is negative & the_right_argument_of (the_argument_of H) is negative )
proof end;

theorem :: QC_LANG2:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF st H is conditional holds
( H is negative & the_argument_of H is conjunctive & the_right_argument_of (the_argument_of H) is negative )
proof end;

theorem :: QC_LANG2:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF st H is biconditional holds
( H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional )
proof end;

theorem :: QC_LANG2:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF st H is existential holds
( H is negative & the_argument_of H is universal & the_scope_of (the_argument_of H) is negative )
proof end;

theorem :: QC_LANG2:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF st H is disjunctive holds
H = (the_left_disjunct_of H) 'or' (the_right_disjunct_of H)
proof end;

theorem :: QC_LANG2:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF st H is conditional holds
H = (the_antecedent_of H) => (the_consequent_of H)
proof end;

theorem :: QC_LANG2:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF st H is biconditional holds
H = (the_left_side_of H) <=> (the_right_side_of H)
proof end;

theorem :: QC_LANG2:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF st H is existential holds
H = Ex (bound_in (the_argument_of H)),(the_argument_of (the_scope_of (the_argument_of H)))
proof end;

definition
let G, H be Element of QC-WFF ;
pred G is_immediate_constituent_of H means :Def20: :: QC_LANG2:def 20
( H = 'not' G or ex F being Element of QC-WFF st
( H = G '&' F or H = F '&' G ) or ex x being bound_QC-variable st H = All x,G );
end;

:: deftheorem Def20 defines is_immediate_constituent_of QC_LANG2:def 20 :
for G, H being Element of QC-WFF holds
( G is_immediate_constituent_of H iff ( H = 'not' G or ex F being Element of QC-WFF st
( H = G '&' F or H = F '&' G ) or ex x being bound_QC-variable st H = All x,G ) );

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

theorem Th58: :: QC_LANG2:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF holds not H is_immediate_constituent_of VERUM
proof end;

theorem Th59: :: QC_LANG2:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF
for k being Nat
for P being QC-pred_symbol of k
for V being QC-variable_list of k holds not H is_immediate_constituent_of P ! V
proof end;

theorem Th60: :: QC_LANG2:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, H being Element of QC-WFF holds
( F is_immediate_constituent_of 'not' H iff F = H )
proof end;

theorem :: QC_LANG2:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF holds
( H is_immediate_constituent_of FALSUM iff H = VERUM ) by Th60;

theorem Th62: :: QC_LANG2:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G, H being Element of QC-WFF holds
( F is_immediate_constituent_of G '&' H iff ( F = G or F = H ) )
proof end;

theorem Th63: :: QC_LANG2:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, H being Element of QC-WFF
for x being bound_QC-variable holds
( F is_immediate_constituent_of All x,H iff F = H )
proof end;

theorem Th64: :: QC_LANG2:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H, F being Element of QC-WFF st H is atomic holds
not F is_immediate_constituent_of H
proof end;

theorem Th65: :: QC_LANG2:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H, F being Element of QC-WFF st H is negative holds
( F is_immediate_constituent_of H iff F = the_argument_of H )
proof end;

theorem Th66: :: QC_LANG2:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H, F being Element of QC-WFF st H is conjunctive holds
( F is_immediate_constituent_of H iff ( F = the_left_argument_of H or F = the_right_argument_of H ) )
proof end;

theorem Th67: :: QC_LANG2:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H, F being Element of QC-WFF st H is universal holds
( F is_immediate_constituent_of H iff F = the_scope_of H )
proof end;

definition
let G, H be Element of QC-WFF ;
pred G is_subformula_of H means :Def21: :: QC_LANG2:def 21
ex n being Nat ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = G & L . n = H & ( for k being Nat st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) );
reflexivity
for G being Element of QC-WFF ex n being Nat ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = G & L . n = G & ( for k being Nat st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
proof end;
end;

:: deftheorem Def21 defines is_subformula_of QC_LANG2:def 21 :
for G, H being Element of QC-WFF holds
( G is_subformula_of H iff ex n being Nat ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = G & L . n = H & ( for k being Nat st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) );

definition
let H, F be Element of QC-WFF ;
pred H is_proper_subformula_of F means :Def22: :: QC_LANG2:def 22
( H is_subformula_of F & H <> F );
irreflexivity
for H being Element of QC-WFF holds
( not H is_subformula_of H or not H <> H )
;
end;

:: deftheorem Def22 defines is_proper_subformula_of QC_LANG2:def 22 :
for H, F being Element of QC-WFF holds
( H is_proper_subformula_of F iff ( H is_subformula_of F & H <> F ) );

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

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

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

theorem Th71: :: QC_LANG2:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H, F being Element of QC-WFF st H is_immediate_constituent_of F holds
len (@ H) < len (@ F)
proof end;

theorem Th72: :: QC_LANG2:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H, F being Element of QC-WFF st H is_immediate_constituent_of F holds
H is_subformula_of F
proof end;

theorem Th73: :: QC_LANG2:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H, F being Element of QC-WFF st H is_immediate_constituent_of F holds
H is_proper_subformula_of F
proof end;

theorem Th74: :: QC_LANG2:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H, F being Element of QC-WFF st H is_proper_subformula_of F holds
len (@ H) < len (@ F)
proof end;

theorem Th75: :: QC_LANG2:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H, F being Element of QC-WFF st H is_proper_subformula_of F holds
ex G being Element of QC-WFF st G is_immediate_constituent_of F
proof end;

theorem Th76: :: QC_LANG2:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G, H being Element of QC-WFF st F is_proper_subformula_of G & G is_proper_subformula_of H holds
F is_proper_subformula_of H
proof end;

theorem Th77: :: QC_LANG2:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G, H being Element of QC-WFF st F is_subformula_of G & G is_subformula_of H holds
F is_subformula_of H
proof end;

theorem Th78: :: QC_LANG2:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G, H being Element of QC-WFF st G is_subformula_of H & H is_subformula_of G holds
G = H
proof end;

theorem Th79: :: QC_LANG2:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G, H being Element of QC-WFF holds
( not G is_proper_subformula_of H or not H is_subformula_of G )
proof end;

theorem :: QC_LANG2:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G, H being Element of QC-WFF holds
( not G is_proper_subformula_of H or not H is_proper_subformula_of G )
proof end;

theorem Th81: :: QC_LANG2:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G, H being Element of QC-WFF holds
( not G is_subformula_of H or not H is_immediate_constituent_of G )
proof end;

theorem Th82: :: QC_LANG2:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G, H being Element of QC-WFF holds
( not G is_proper_subformula_of H or not H is_immediate_constituent_of G )
proof end;

theorem Th83: :: QC_LANG2:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G, H being Element of QC-WFF st ( ( F is_proper_subformula_of G & G is_subformula_of H ) or ( F is_subformula_of G & G is_proper_subformula_of H ) or ( F is_subformula_of G & G is_immediate_constituent_of H ) or ( F is_immediate_constituent_of G & G is_subformula_of H ) or ( F is_proper_subformula_of G & G is_immediate_constituent_of H ) or ( F is_immediate_constituent_of G & G is_proper_subformula_of H ) ) holds
F is_proper_subformula_of H
proof end;

theorem :: QC_LANG2:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF holds not F is_proper_subformula_of VERUM by Th58, Th75;

theorem Th85: :: QC_LANG2:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for k being Nat
for P being QC-pred_symbol of k
for V being QC-variable_list of k holds not F is_proper_subformula_of P ! V
proof end;

theorem Th86: :: QC_LANG2:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, H being Element of QC-WFF holds
( F is_subformula_of H iff F is_proper_subformula_of 'not' H )
proof end;

theorem :: QC_LANG2:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, H being Element of QC-WFF st 'not' F is_subformula_of H holds
F is_proper_subformula_of H
proof end;

theorem :: QC_LANG2:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF holds
( F is_proper_subformula_of FALSUM iff F is_subformula_of VERUM ) by Th86;

theorem Th89: :: QC_LANG2:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G, H being Element of QC-WFF holds
( ( F is_subformula_of G or F is_subformula_of H ) iff F is_proper_subformula_of G '&' H )
proof end;

theorem :: QC_LANG2:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G, H being Element of QC-WFF st F '&' G is_subformula_of H holds
( F is_proper_subformula_of H & G is_proper_subformula_of H )
proof end;

theorem Th91: :: QC_LANG2:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, H being Element of QC-WFF
for x being bound_QC-variable holds
( F is_subformula_of H iff F is_proper_subformula_of All x,H )
proof end;

theorem :: QC_LANG2:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H, F being Element of QC-WFF
for x being bound_QC-variable st All x,H is_subformula_of F holds
H is_proper_subformula_of F
proof end;

theorem :: QC_LANG2:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being Element of QC-WFF holds
( F '&' ('not' G) is_proper_subformula_of F => G & F is_proper_subformula_of F => G & 'not' G is_proper_subformula_of F => G & G is_proper_subformula_of F => G )
proof end;

theorem :: QC_LANG2:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being Element of QC-WFF holds
( ('not' F) '&' ('not' G) is_proper_subformula_of F 'or' G & 'not' F is_proper_subformula_of F 'or' G & 'not' G is_proper_subformula_of F 'or' G & F is_proper_subformula_of F 'or' G & G is_proper_subformula_of F 'or' G )
proof end;

theorem :: QC_LANG2:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H, F being Element of QC-WFF st H is atomic holds
not F is_proper_subformula_of H
proof end;

theorem :: QC_LANG2:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF st H is negative holds
the_argument_of H is_proper_subformula_of H
proof end;

theorem :: QC_LANG2:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF st H is conjunctive holds
( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H )
proof end;

theorem :: QC_LANG2:98  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF st H is universal holds
the_scope_of H is_proper_subformula_of H
proof end;

theorem Th99: :: QC_LANG2:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF holds
( H is_subformula_of VERUM iff H = VERUM )
proof end;

theorem Th100: :: QC_LANG2:100  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF
for k being Nat
for P being QC-pred_symbol of k
for V being QC-variable_list of k holds
( H is_subformula_of P ! V iff H = P ! V )
proof end;

theorem Th101: :: QC_LANG2:101  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF holds
( H is_subformula_of FALSUM iff ( H = FALSUM or H = VERUM ) )
proof end;

definition
let H be Element of QC-WFF ;
func Subformulae H -> set means :Def23: :: QC_LANG2:def 23
for a being set holds
( a in it iff ex F being Element of QC-WFF st
( F = a & F is_subformula_of H ) );
existence
ex b1 being set st
for a being set holds
( a in b1 iff ex F being Element of QC-WFF st
( F = a & F is_subformula_of H ) )
proof end;
uniqueness
for b1, b2 being set st ( for a being set holds
( a in b1 iff ex F being Element of QC-WFF st
( F = a & F is_subformula_of H ) ) ) & ( for a being set holds
( a in b2 iff ex F being Element of QC-WFF st
( F = a & F is_subformula_of H ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def23 defines Subformulae QC_LANG2:def 23 :
for H being Element of QC-WFF
for b2 being set holds
( b2 = Subformulae H iff for a being set holds
( a in b2 iff ex F being Element of QC-WFF st
( F = a & F is_subformula_of H ) ) );

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

theorem Th103: :: QC_LANG2:103  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G, H being Element of QC-WFF st G in Subformulae H holds
G is_subformula_of H
proof end;

theorem Th104: :: QC_LANG2:104  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, H being Element of QC-WFF st F is_subformula_of H holds
Subformulae F c= Subformulae H
proof end;

theorem :: QC_LANG2:105  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G, H being Element of QC-WFF st G in Subformulae H holds
Subformulae G c= Subformulae H
proof end;

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

theorem Th107: :: QC_LANG2:107  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Subformulae VERUM = {VERUM }
proof end;

theorem Th108: :: QC_LANG2:108  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for P being QC-pred_symbol of k
for V being QC-variable_list of k holds Subformulae (P ! V) = {(P ! V)}
proof end;

theorem :: QC_LANG2:109  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
Subformulae FALSUM = {VERUM ,FALSUM }
proof end;

theorem Th110: :: QC_LANG2:110  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF holds Subformulae ('not' H) = (Subformulae H) \/ {('not' H)}
proof end;

theorem Th111: :: QC_LANG2:111  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H, F being Element of QC-WFF holds Subformulae (H '&' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)}
proof end;

theorem Th112: :: QC_LANG2:112  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF
for x being bound_QC-variable holds Subformulae (All x,H) = (Subformulae H) \/ {(All x,H)}
proof end;

theorem Th113: :: QC_LANG2:113  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being Element of QC-WFF holds Subformulae (F => G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}
proof end;

theorem :: QC_LANG2:114  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being Element of QC-WFF holds Subformulae (F 'or' G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F),(('not' F) '&' ('not' G)),(F 'or' G)}
proof end;

theorem :: QC_LANG2:115  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being Element of QC-WFF holds Subformulae (F <=> G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G),('not' F),(G '&' ('not' F)),(G => F),(F <=> G)}
proof end;

theorem :: QC_LANG2:116  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF holds
( ( H = VERUM or H is atomic ) iff Subformulae H = {H} )
proof end;

theorem :: QC_LANG2:117  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF st H is negative holds
Subformulae H = (Subformulae (the_argument_of H)) \/ {H}
proof end;

theorem :: QC_LANG2:118  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF st H is conjunctive holds
Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H}
proof end;

theorem :: QC_LANG2:119  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H being Element of QC-WFF st H is universal holds
Subformulae H = (Subformulae (the_scope_of H)) \/ {H}
proof end;

theorem :: QC_LANG2:120  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H, G, F being Element of QC-WFF st ( H is_immediate_constituent_of G or H is_proper_subformula_of G or H is_subformula_of G ) & G in Subformulae F holds
H in Subformulae F
proof end;