:: QC_LANG2 semantic presentation
begin
theorem Th1: :: QC_LANG2:1
for A being QC-alphabet
for p being Element of QC-WFF A holds the_argument_of ('not' p) = p
proof
let A be QC-alphabet ; ::_thesis: for p being Element of QC-WFF A holds the_argument_of ('not' p) = p
let p be Element of QC-WFF A; ::_thesis: the_argument_of ('not' p) = p
'not' p is negative by QC_LANG1:def_19;
hence the_argument_of ('not' p) = p by QC_LANG1:def_24; ::_thesis: verum
end;
theorem Th2: :: QC_LANG2:2
for A being QC-alphabet
for p, q, p1, q1 being Element of QC-WFF A st p '&' q = p1 '&' q1 holds
( p = p1 & q = q1 )
proof
let A be QC-alphabet ; ::_thesis: for p, q, p1, q1 being Element of QC-WFF A st p '&' q = p1 '&' q1 holds
( p = p1 & q = q1 )
let p, q, p1, q1 be Element of QC-WFF A; ::_thesis: ( p '&' q = p1 '&' q1 implies ( p = p1 & q = q1 ) )
assume A1: p '&' q = p1 '&' q1 ; ::_thesis: ( p = p1 & q = q1 )
( (<*[2,0]*> ^ (@ p)) ^ (@ q) = <*[2,0]*> ^ ((@ p) ^ (@ q)) & (<*[2,0]*> ^ (@ p1)) ^ (@ q1) = <*[2,0]*> ^ ((@ p1) ^ (@ q1)) ) by FINSEQ_1:32;
then A2: (@ p) ^ (@ q) = (@ p1) ^ (@ q1) by A1, FINSEQ_1:33;
then A3: ( len (@ p1) <= len (@ p) implies ex sq being FinSequence st @ p = (@ p1) ^ sq ) by FINSEQ_1:47;
A4: ( len (@ p) <= len (@ p1) implies ex sq being FinSequence st @ p1 = (@ p) ^ sq ) by A2, FINSEQ_1:47;
hence p = p1 by A3, QC_LANG1:13; ::_thesis: q = q1
( ex sq being FinSequence st @ p1 = (@ p) ^ sq implies p1 = p ) by QC_LANG1:13;
hence q = q1 by A1, A3, A4, FINSEQ_1:33, QC_LANG1:13; ::_thesis: verum
end;
theorem Th3: :: QC_LANG2:3
for A being QC-alphabet
for p being Element of QC-WFF A st p is conjunctive holds
p = (the_left_argument_of p) '&' (the_right_argument_of p)
proof
let A be QC-alphabet ; ::_thesis: for p being Element of QC-WFF A st p is conjunctive holds
p = (the_left_argument_of p) '&' (the_right_argument_of p)
let p be Element of QC-WFF A; ::_thesis: ( p is conjunctive implies p = (the_left_argument_of p) '&' (the_right_argument_of p) )
given p1, q1 being Element of QC-WFF A such that A1: p = p1 '&' q1 ; :: according to QC_LANG1:def_20 ::_thesis: p = (the_left_argument_of p) '&' (the_right_argument_of p)
A2: p is conjunctive by A1, QC_LANG1:def_20;
then p1 = the_left_argument_of p by A1, QC_LANG1:def_25;
hence p = (the_left_argument_of p) '&' (the_right_argument_of p) by A1, A2, QC_LANG1:def_26; ::_thesis: verum
end;
theorem Th4: :: QC_LANG2:4
for A being QC-alphabet
for p, q being Element of QC-WFF A holds
( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q )
proof
let A be QC-alphabet ; ::_thesis: for p, q being Element of QC-WFF A holds
( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q )
let p, q be Element of QC-WFF A; ::_thesis: ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q )
p '&' q is conjunctive by QC_LANG1:def_20;
hence ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q ) by QC_LANG1:def_25, QC_LANG1:def_26; ::_thesis: verum
end;
theorem Th5: :: QC_LANG2:5
for A being QC-alphabet
for x, y being bound_QC-variable of A
for p, q being Element of QC-WFF A st All (x,p) = All (y,q) holds
( x = y & p = q )
proof
let A be QC-alphabet ; ::_thesis: for x, y being bound_QC-variable of A
for p, q being Element of QC-WFF A st All (x,p) = All (y,q) holds
( x = y & p = q )
let x, y be bound_QC-variable of A; ::_thesis: for p, q being Element of QC-WFF A st All (x,p) = All (y,q) holds
( x = y & p = q )
let p, q be Element of QC-WFF A; ::_thesis: ( All (x,p) = All (y,q) implies ( x = y & p = q ) )
A1: ( (<*[3,0]*> ^ <*x*>) ^ (@ p) = <*[3,0]*> ^ (<*x*> ^ (@ p)) & (<*[3,0]*> ^ <*y*>) ^ (@ q) = <*[3,0]*> ^ (<*y*> ^ (@ q)) ) by FINSEQ_1:32;
A2: ( (<*x*> ^ (@ p)) . 1 = x & (<*y*> ^ (@ q)) . 1 = y ) by FINSEQ_1:41;
assume A3: All (x,p) = All (y,q) ; ::_thesis: ( x = y & p = q )
hence x = y by A1, A2, FINSEQ_1:33; ::_thesis: p = q
<*x*> ^ (@ p) = <*y*> ^ (@ q) by A3, A1, FINSEQ_1:33;
hence p = q by A2, FINSEQ_1:33; ::_thesis: verum
end;
theorem Th6: :: QC_LANG2:6
for A being QC-alphabet
for p being Element of QC-WFF A st p is universal holds
p = All ((bound_in p),(the_scope_of p))
proof
let A be QC-alphabet ; ::_thesis: for p being Element of QC-WFF A st p is universal holds
p = All ((bound_in p),(the_scope_of p))
let p be Element of QC-WFF A; ::_thesis: ( p is universal implies p = All ((bound_in p),(the_scope_of p)) )
given x being bound_QC-variable of A, q being Element of QC-WFF A such that A1: p = All (x,q) ; :: according to QC_LANG1:def_21 ::_thesis: p = All ((bound_in p),(the_scope_of p))
A2: p is universal by A1, QC_LANG1:def_21;
then x = bound_in p by A1, QC_LANG1:def_27;
hence p = All ((bound_in p),(the_scope_of p)) by A1, A2, QC_LANG1:def_28; ::_thesis: verum
end;
theorem Th7: :: QC_LANG2:7
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A holds
( bound_in (All (x,p)) = x & the_scope_of (All (x,p)) = p )
proof
let A be QC-alphabet ; ::_thesis: for x being bound_QC-variable of A
for p being Element of QC-WFF A holds
( bound_in (All (x,p)) = x & the_scope_of (All (x,p)) = p )
let x be bound_QC-variable of A; ::_thesis: for p being Element of QC-WFF A holds
( bound_in (All (x,p)) = x & the_scope_of (All (x,p)) = p )
let p be Element of QC-WFF A; ::_thesis: ( bound_in (All (x,p)) = x & the_scope_of (All (x,p)) = p )
All (x,p) is universal by QC_LANG1:def_21;
then All (x,p) = All ((bound_in (All (x,p))),(the_scope_of (All (x,p)))) by Th6;
hence ( bound_in (All (x,p)) = x & the_scope_of (All (x,p)) = p ) by Th5; ::_thesis: verum
end;
definition
let A be QC-alphabet ;
func FALSUM A -> QC-formula of A equals :: QC_LANG2:def 1
'not' (VERUM A);
correctness
coherence
'not' (VERUM A) is QC-formula of A;
;
let p, q be Element of QC-WFF A;
funcp => q -> QC-formula of A equals :: QC_LANG2:def 2
'not' (p '&' ('not' q));
correctness
coherence
'not' (p '&' ('not' q)) is QC-formula of A;
;
funcp 'or' q -> QC-formula of A equals :: QC_LANG2:def 3
'not' (('not' p) '&' ('not' q));
correctness
coherence
'not' (('not' p) '&' ('not' q)) is QC-formula of A;
;
end;
:: deftheorem defines FALSUM QC_LANG2:def_1_:_
for A being QC-alphabet holds FALSUM A = 'not' (VERUM A);
:: deftheorem defines => QC_LANG2:def_2_:_
for A being QC-alphabet
for p, q being Element of QC-WFF A holds p => q = 'not' (p '&' ('not' q));
:: deftheorem defines 'or' QC_LANG2:def_3_:_
for A being QC-alphabet
for p, q being Element of QC-WFF A holds p 'or' q = 'not' (('not' p) '&' ('not' q));
definition
let A be QC-alphabet ;
let p, q be Element of QC-WFF A;
funcp <=> q -> QC-formula of A equals :: QC_LANG2:def 4
(p => q) '&' (q => p);
correctness
coherence
(p => q) '&' (q => p) is QC-formula of A;
;
end;
:: deftheorem defines <=> QC_LANG2:def_4_:_
for A being QC-alphabet
for p, q being Element of QC-WFF A holds p <=> q = (p => q) '&' (q => p);
definition
let A be QC-alphabet ;
let x be bound_QC-variable of A;
let p be Element of QC-WFF A;
func Ex (x,p) -> QC-formula of A equals :: QC_LANG2:def 5
'not' (All (x,('not' p)));
correctness
coherence
'not' (All (x,('not' p))) is QC-formula of A;
;
end;
:: deftheorem defines Ex QC_LANG2:def_5_:_
for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A holds Ex (x,p) = 'not' (All (x,('not' p)));
theorem :: QC_LANG2:8
for A being QC-alphabet holds
( FALSUM A is negative & the_argument_of (FALSUM A) = VERUM A ) by Th1, QC_LANG1:def_19;
theorem :: QC_LANG2:9
for A being QC-alphabet
for p, q being Element of QC-WFF A holds p 'or' q = ('not' p) => q ;
theorem :: QC_LANG2:10
for A being QC-alphabet
for p, q, p1, q1 being Element of QC-WFF A st p 'or' q = p1 'or' q1 holds
( p = p1 & q = q1 )
proof
let A be QC-alphabet ; ::_thesis: for p, q, p1, q1 being Element of QC-WFF A st p 'or' q = p1 'or' q1 holds
( p = p1 & q = q1 )
let p, q, p1, q1 be Element of QC-WFF A; ::_thesis: ( p 'or' q = p1 'or' q1 implies ( p = p1 & q = q1 ) )
assume p 'or' q = p1 'or' q1 ; ::_thesis: ( p = p1 & q = q1 )
then ('not' p) '&' ('not' q) = ('not' p1) '&' ('not' q1) by FINSEQ_1:33;
then ( 'not' p = 'not' p1 & 'not' q = 'not' q1 ) by Th2;
hence ( p = p1 & q = q1 ) by FINSEQ_1:33; ::_thesis: verum
end;
theorem Th11: :: QC_LANG2:11
for A being QC-alphabet
for p, q, p1, q1 being Element of QC-WFF A st p => q = p1 => q1 holds
( p = p1 & q = q1 )
proof
let A be QC-alphabet ; ::_thesis: for p, q, p1, q1 being Element of QC-WFF A st p => q = p1 => q1 holds
( p = p1 & q = q1 )
let p, q, p1, q1 be Element of QC-WFF A; ::_thesis: ( p => q = p1 => q1 implies ( p = p1 & q = q1 ) )
assume p => q = p1 => q1 ; ::_thesis: ( p = p1 & q = q1 )
then A1: p '&' ('not' q) = p1 '&' ('not' q1) by FINSEQ_1:33;
hence p = p1 by Th2; ::_thesis: q = q1
'not' q = 'not' q1 by A1, Th2;
hence q = q1 by FINSEQ_1:33; ::_thesis: verum
end;
theorem :: QC_LANG2:12
for A being QC-alphabet
for p, q, p1, q1 being Element of QC-WFF A st p <=> q = p1 <=> q1 holds
( p = p1 & q = q1 )
proof
let A be QC-alphabet ; ::_thesis: for p, q, p1, q1 being Element of QC-WFF A st p <=> q = p1 <=> q1 holds
( p = p1 & q = q1 )
let p, q, p1, q1 be Element of QC-WFF A; ::_thesis: ( p <=> q = p1 <=> q1 implies ( p = p1 & q = q1 ) )
assume p <=> q = p1 <=> q1 ; ::_thesis: ( p = p1 & q = q1 )
then p => q = p1 => q1 by Th2;
hence ( p = p1 & q = q1 ) by Th11; ::_thesis: verum
end;
theorem Th13: :: QC_LANG2:13
for A being QC-alphabet
for x, y being bound_QC-variable of A
for p, q being Element of QC-WFF A st Ex (x,p) = Ex (y,q) holds
( x = y & p = q )
proof
let A be QC-alphabet ; ::_thesis: for x, y being bound_QC-variable of A
for p, q being Element of QC-WFF A st Ex (x,p) = Ex (y,q) holds
( x = y & p = q )
let x, y be bound_QC-variable of A; ::_thesis: for p, q being Element of QC-WFF A st Ex (x,p) = Ex (y,q) holds
( x = y & p = q )
let p, q be Element of QC-WFF A; ::_thesis: ( Ex (x,p) = Ex (y,q) implies ( x = y & p = q ) )
assume Ex (x,p) = Ex (y,q) ; ::_thesis: ( x = y & p = q )
then A1: All (x,('not' p)) = All (y,('not' q)) by FINSEQ_1:33;
then 'not' p = 'not' q by Th5;
hence ( x = y & p = q ) by A1, Th5, FINSEQ_1:33; ::_thesis: verum
end;
definition
let A be QC-alphabet ;
let x, y be bound_QC-variable of A;
let p be Element of QC-WFF A;
func All (x,y,p) -> QC-formula of A equals :: QC_LANG2:def 6
All (x,(All (y,p)));
correctness
coherence
All (x,(All (y,p))) is QC-formula of A;
;
func Ex (x,y,p) -> QC-formula of A equals :: QC_LANG2:def 7
Ex (x,(Ex (y,p)));
correctness
coherence
Ex (x,(Ex (y,p))) is QC-formula of A;
;
end;
:: deftheorem defines All QC_LANG2:def_6_:_
for A being QC-alphabet
for x, y being bound_QC-variable of A
for p being Element of QC-WFF A holds All (x,y,p) = All (x,(All (y,p)));
:: deftheorem defines Ex QC_LANG2:def_7_:_
for A being QC-alphabet
for x, y being bound_QC-variable of A
for p being Element of QC-WFF A holds Ex (x,y,p) = Ex (x,(Ex (y,p)));
theorem :: QC_LANG2:14
for A being QC-alphabet
for x, y being bound_QC-variable of A
for p being Element of QC-WFF A holds
( All (x,y,p) = All (x,(All (y,p))) & Ex (x,y,p) = Ex (x,(Ex (y,p))) ) ;
theorem Th15: :: QC_LANG2:15
for A being QC-alphabet
for p1, p2 being Element of QC-WFF A
for x1, x2, y1, y2 being bound_QC-variable of A st All (x1,y1,p1) = All (x2,y2,p2) holds
( x1 = x2 & y1 = y2 & p1 = p2 )
proof
let A be QC-alphabet ; ::_thesis: for p1, p2 being Element of QC-WFF A
for x1, x2, y1, y2 being bound_QC-variable of A st All (x1,y1,p1) = All (x2,y2,p2) holds
( x1 = x2 & y1 = y2 & p1 = p2 )
let p1, p2 be Element of QC-WFF A; ::_thesis: for x1, x2, y1, y2 being bound_QC-variable of A st All (x1,y1,p1) = All (x2,y2,p2) holds
( x1 = x2 & y1 = y2 & p1 = p2 )
let x1, x2, y1, y2 be bound_QC-variable of A; ::_thesis: ( All (x1,y1,p1) = All (x2,y2,p2) implies ( x1 = x2 & y1 = y2 & p1 = p2 ) )
assume A1: All (x1,y1,p1) = All (x2,y2,p2) ; ::_thesis: ( x1 = x2 & y1 = y2 & p1 = p2 )
thus x1 = x2 by A1, Th5; ::_thesis: ( y1 = y2 & p1 = p2 )
All (y1,p1) = All (y2,p2) by A1, Th5;
hence ( y1 = y2 & p1 = p2 ) by Th5; ::_thesis: verum
end;
theorem :: QC_LANG2:16
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p, q being Element of QC-WFF A st All (x,y,p) = All (z,q) holds
( x = z & All (y,p) = q ) by Th5;
theorem Th17: :: QC_LANG2:17
for A being QC-alphabet
for p1, p2 being Element of QC-WFF A
for x1, x2, y1, y2 being bound_QC-variable of A st Ex (x1,y1,p1) = Ex (x2,y2,p2) holds
( x1 = x2 & y1 = y2 & p1 = p2 )
proof
let A be QC-alphabet ; ::_thesis: for p1, p2 being Element of QC-WFF A
for x1, x2, y1, y2 being bound_QC-variable of A st Ex (x1,y1,p1) = Ex (x2,y2,p2) holds
( x1 = x2 & y1 = y2 & p1 = p2 )
let p1, p2 be Element of QC-WFF A; ::_thesis: for x1, x2, y1, y2 being bound_QC-variable of A st Ex (x1,y1,p1) = Ex (x2,y2,p2) holds
( x1 = x2 & y1 = y2 & p1 = p2 )
let x1, x2, y1, y2 be bound_QC-variable of A; ::_thesis: ( Ex (x1,y1,p1) = Ex (x2,y2,p2) implies ( x1 = x2 & y1 = y2 & p1 = p2 ) )
assume A1: Ex (x1,y1,p1) = Ex (x2,y2,p2) ; ::_thesis: ( x1 = x2 & y1 = y2 & p1 = p2 )
thus x1 = x2 by A1, Th13; ::_thesis: ( y1 = y2 & p1 = p2 )
Ex (y1,p1) = Ex (y2,p2) by A1, Th13;
hence ( y1 = y2 & p1 = p2 ) by Th13; ::_thesis: verum
end;
theorem :: QC_LANG2:18
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p, q being Element of QC-WFF A st Ex (x,y,p) = Ex (z,q) holds
( x = z & Ex (y,p) = q ) by Th13;
theorem :: QC_LANG2:19
for A being QC-alphabet
for x, y being bound_QC-variable of A
for p being Element of QC-WFF A 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 Th7, QC_LANG1:def_21;
definition
let A be QC-alphabet ;
let x, y, z be bound_QC-variable of A;
let p be Element of QC-WFF A;
func All (x,y,z,p) -> QC-formula of A equals :: QC_LANG2:def 8
All (x,(All (y,z,p)));
correctness
coherence
All (x,(All (y,z,p))) is QC-formula of A;
;
func Ex (x,y,z,p) -> QC-formula of A equals :: QC_LANG2:def 9
Ex (x,(Ex (y,z,p)));
correctness
coherence
Ex (x,(Ex (y,z,p))) is QC-formula of A;
;
end;
:: deftheorem defines All QC_LANG2:def_8_:_
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p being Element of QC-WFF A holds All (x,y,z,p) = All (x,(All (y,z,p)));
:: deftheorem defines Ex QC_LANG2:def_9_:_
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p being Element of QC-WFF A holds Ex (x,y,z,p) = Ex (x,(Ex (y,z,p)));
theorem :: QC_LANG2:20
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p being Element of QC-WFF A 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:21
for A being QC-alphabet
for p1, p2 being Element of QC-WFF A
for x1, x2, y1, y2, z1, z2 being bound_QC-variable of A st All (x1,y1,z1,p1) = All (x2,y2,z2,p2) holds
( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 )
proof
let A be QC-alphabet ; ::_thesis: for p1, p2 being Element of QC-WFF A
for x1, x2, y1, y2, z1, z2 being bound_QC-variable of A st All (x1,y1,z1,p1) = All (x2,y2,z2,p2) holds
( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 )
let p1, p2 be Element of QC-WFF A; ::_thesis: for x1, x2, y1, y2, z1, z2 being bound_QC-variable of A st All (x1,y1,z1,p1) = All (x2,y2,z2,p2) holds
( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 )
let x1, x2, y1, y2, z1, z2 be bound_QC-variable of A; ::_thesis: ( All (x1,y1,z1,p1) = All (x2,y2,z2,p2) implies ( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 ) )
assume A1: All (x1,y1,z1,p1) = All (x2,y2,z2,p2) ; ::_thesis: ( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 )
thus x1 = x2 by A1, Th5; ::_thesis: ( y1 = y2 & z1 = z2 & p1 = p2 )
All (y1,z1,p1) = All (y2,z2,p2) by A1, Th5;
hence ( y1 = y2 & z1 = z2 & p1 = p2 ) by Th15; ::_thesis: verum
end;
theorem :: QC_LANG2:22
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p, q being Element of QC-WFF A
for t being bound_QC-variable of A st All (x,y,z,p) = All (t,q) holds
( x = t & All (y,z,p) = q ) by Th5;
theorem :: QC_LANG2:23
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p, q being Element of QC-WFF A
for t, s being bound_QC-variable of A st All (x,y,z,p) = All (t,s,q) holds
( x = t & y = s & All (z,p) = q )
proof
let A be QC-alphabet ; ::_thesis: for x, y, z being bound_QC-variable of A
for p, q being Element of QC-WFF A
for t, s being bound_QC-variable of A st All (x,y,z,p) = All (t,s,q) holds
( x = t & y = s & All (z,p) = q )
let x, y, z be bound_QC-variable of A; ::_thesis: for p, q being Element of QC-WFF A
for t, s being bound_QC-variable of A st All (x,y,z,p) = All (t,s,q) holds
( x = t & y = s & All (z,p) = q )
let p, q be Element of QC-WFF A; ::_thesis: for t, s being bound_QC-variable of A st All (x,y,z,p) = All (t,s,q) holds
( x = t & y = s & All (z,p) = q )
let t, s be bound_QC-variable of A; ::_thesis: ( All (x,y,z,p) = All (t,s,q) implies ( x = t & y = s & All (z,p) = q ) )
assume A1: All (x,y,z,p) = All (t,s,q) ; ::_thesis: ( x = t & y = s & All (z,p) = q )
hence x = t by Th5; ::_thesis: ( y = s & All (z,p) = q )
All (y,z,p) = All (s,q) by A1, Th5;
hence ( y = s & All (z,p) = q ) by Th5; ::_thesis: verum
end;
theorem :: QC_LANG2:24
for A being QC-alphabet
for p1, p2 being Element of QC-WFF A
for x1, x2, y1, y2, z1, z2 being bound_QC-variable of A st Ex (x1,y1,z1,p1) = Ex (x2,y2,z2,p2) holds
( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 )
proof
let A be QC-alphabet ; ::_thesis: for p1, p2 being Element of QC-WFF A
for x1, x2, y1, y2, z1, z2 being bound_QC-variable of A st Ex (x1,y1,z1,p1) = Ex (x2,y2,z2,p2) holds
( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 )
let p1, p2 be Element of QC-WFF A; ::_thesis: for x1, x2, y1, y2, z1, z2 being bound_QC-variable of A st Ex (x1,y1,z1,p1) = Ex (x2,y2,z2,p2) holds
( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 )
let x1, x2, y1, y2, z1, z2 be bound_QC-variable of A; ::_thesis: ( Ex (x1,y1,z1,p1) = Ex (x2,y2,z2,p2) implies ( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 ) )
assume A1: Ex (x1,y1,z1,p1) = Ex (x2,y2,z2,p2) ; ::_thesis: ( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 )
thus x1 = x2 by A1, Th13; ::_thesis: ( y1 = y2 & z1 = z2 & p1 = p2 )
Ex (y1,z1,p1) = Ex (y2,z2,p2) by A1, Th13;
hence ( y1 = y2 & z1 = z2 & p1 = p2 ) by Th17; ::_thesis: verum
end;
theorem :: QC_LANG2:25
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p, q being Element of QC-WFF A
for t being bound_QC-variable of A st Ex (x,y,z,p) = Ex (t,q) holds
( x = t & Ex (y,z,p) = q ) by Th13;
theorem :: QC_LANG2:26
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p, q being Element of QC-WFF A
for t, s being bound_QC-variable of A st Ex (x,y,z,p) = Ex (t,s,q) holds
( x = t & y = s & Ex (z,p) = q )
proof
let A be QC-alphabet ; ::_thesis: for x, y, z being bound_QC-variable of A
for p, q being Element of QC-WFF A
for t, s being bound_QC-variable of A st Ex (x,y,z,p) = Ex (t,s,q) holds
( x = t & y = s & Ex (z,p) = q )
let x, y, z be bound_QC-variable of A; ::_thesis: for p, q being Element of QC-WFF A
for t, s being bound_QC-variable of A st Ex (x,y,z,p) = Ex (t,s,q) holds
( x = t & y = s & Ex (z,p) = q )
let p, q be Element of QC-WFF A; ::_thesis: for t, s being bound_QC-variable of A st Ex (x,y,z,p) = Ex (t,s,q) holds
( x = t & y = s & Ex (z,p) = q )
let t, s be bound_QC-variable of A; ::_thesis: ( Ex (x,y,z,p) = Ex (t,s,q) implies ( x = t & y = s & Ex (z,p) = q ) )
assume A1: Ex (x,y,z,p) = Ex (t,s,q) ; ::_thesis: ( x = t & y = s & Ex (z,p) = q )
hence x = t by Th13; ::_thesis: ( y = s & Ex (z,p) = q )
Ex (y,z,p) = Ex (s,q) by A1, Th13;
hence ( y = s & Ex (z,p) = q ) by Th13; ::_thesis: verum
end;
theorem :: QC_LANG2:27
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p being Element of QC-WFF A 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 Th7, QC_LANG1:def_21;
definition
let A be QC-alphabet ;
let H be Element of QC-WFF A;
attrH is disjunctive means :: QC_LANG2:def 10
ex p, q being Element of QC-WFF A st H = p 'or' q;
attrH is conditional means :Def11: :: QC_LANG2:def 11
ex p, q being Element of QC-WFF A st H = p => q;
attrH is biconditional means :: QC_LANG2:def 12
ex p, q being Element of QC-WFF A st H = p <=> q;
attrH is existential means :Def13: :: QC_LANG2:def 13
ex x being bound_QC-variable of A ex p being Element of QC-WFF A st H = Ex (x,p);
end;
:: deftheorem defines disjunctive QC_LANG2:def_10_:_
for A being QC-alphabet
for H being Element of QC-WFF A holds
( H is disjunctive iff ex p, q being Element of QC-WFF A st H = p 'or' q );
:: deftheorem Def11 defines conditional QC_LANG2:def_11_:_
for A being QC-alphabet
for H being Element of QC-WFF A holds
( H is conditional iff ex p, q being Element of QC-WFF A st H = p => q );
:: deftheorem defines biconditional QC_LANG2:def_12_:_
for A being QC-alphabet
for H being Element of QC-WFF A holds
( H is biconditional iff ex p, q being Element of QC-WFF A st H = p <=> q );
:: deftheorem Def13 defines existential QC_LANG2:def_13_:_
for A being QC-alphabet
for H being Element of QC-WFF A holds
( H is existential iff ex x being bound_QC-variable of A ex p being Element of QC-WFF A st H = Ex (x,p) );
theorem :: QC_LANG2:28
for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p being Element of QC-WFF A holds
( Ex (x,y,p) is existential & Ex (x,y,z,p) is existential ) by Def13;
definition
let A be QC-alphabet ;
let H be Element of QC-WFF A;
func the_left_disjunct_of H -> QC-formula of A 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 of A;
;
func the_right_disjunct_of H -> QC-formula of A 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 of A;
;
func the_antecedent_of H -> QC-formula of A 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 of A;
;
end;
:: deftheorem defines the_left_disjunct_of QC_LANG2:def_14_:_
for A being QC-alphabet
for H being Element of QC-WFF A 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 A being QC-alphabet
for H being Element of QC-WFF A 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 A being QC-alphabet
for H being Element of QC-WFF A holds the_antecedent_of H = the_left_argument_of (the_argument_of H);
notation
let A be QC-alphabet ;
let H be Element of QC-WFF A;
synonym the_consequent_of H for the_right_disjunct_of H;
end;
definition
let A be QC-alphabet ;
let H be Element of QC-WFF A;
func the_left_side_of H -> QC-formula of A equals :: QC_LANG2:def 17
the_antecedent_of (the_left_argument_of H);
correctness
coherence
the_antecedent_of (the_left_argument_of H) is QC-formula of A;
;
func the_right_side_of H -> QC-formula of A equals :: QC_LANG2:def 18
the_consequent_of (the_left_argument_of H);
correctness
coherence
the_consequent_of (the_left_argument_of H) is QC-formula of A;
;
end;
:: deftheorem defines the_left_side_of QC_LANG2:def_17_:_
for A being QC-alphabet
for H being Element of QC-WFF A holds the_left_side_of H = the_antecedent_of (the_left_argument_of H);
:: deftheorem defines the_right_side_of QC_LANG2:def_18_:_
for A being QC-alphabet
for H being Element of QC-WFF A holds the_right_side_of H = the_consequent_of (the_left_argument_of H);
theorem Th29: :: QC_LANG2:29
for A being QC-alphabet
for F, G being Element of QC-WFF A 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
let A be QC-alphabet ; ::_thesis: for F, G being Element of QC-WFF A 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) )
let F, G be Element of QC-WFF A; ::_thesis: ( 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) )
thus the_left_disjunct_of (F 'or' G) = the_argument_of (the_left_argument_of (('not' F) '&' ('not' G))) by Th1
.= the_argument_of ('not' F) by Th4
.= F by Th1 ; ::_thesis: ( the_right_disjunct_of (F 'or' G) = G & the_argument_of (F 'or' G) = ('not' F) '&' ('not' G) )
thus the_right_disjunct_of (F 'or' G) = the_argument_of (the_right_argument_of (('not' F) '&' ('not' G))) by Th1
.= the_argument_of ('not' G) by Th4
.= G by Th1 ; ::_thesis: the_argument_of (F 'or' G) = ('not' F) '&' ('not' G)
thus the_argument_of (F 'or' G) = ('not' F) '&' ('not' G) by Th1; ::_thesis: verum
end;
theorem Th30: :: QC_LANG2:30
for A being QC-alphabet
for F, G being Element of QC-WFF A holds
( the_antecedent_of (F => G) = F & the_consequent_of (F => G) = G & the_argument_of (F => G) = F '&' ('not' G) )
proof
let A be QC-alphabet ; ::_thesis: for F, G being Element of QC-WFF A holds
( the_antecedent_of (F => G) = F & the_consequent_of (F => G) = G & the_argument_of (F => G) = F '&' ('not' G) )
let F, G be Element of QC-WFF A; ::_thesis: ( the_antecedent_of (F => G) = F & the_consequent_of (F => G) = G & the_argument_of (F => G) = F '&' ('not' G) )
thus the_antecedent_of (F => G) = the_left_argument_of (F '&' ('not' G)) by Th1
.= F by Th4 ; ::_thesis: ( the_consequent_of (F => G) = G & the_argument_of (F => G) = F '&' ('not' G) )
thus the_consequent_of (F => G) = the_argument_of (the_right_argument_of (F '&' ('not' G))) by Th1
.= the_argument_of ('not' G) by Th4
.= G by Th1 ; ::_thesis: the_argument_of (F => G) = F '&' ('not' G)
thus the_argument_of (F => G) = F '&' ('not' G) by Th1; ::_thesis: verum
end;
theorem Th31: :: QC_LANG2:31
for A being QC-alphabet
for F, G being Element of QC-WFF A 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
let A be QC-alphabet ; ::_thesis: for F, G being Element of QC-WFF A 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 )
let F, G be Element of QC-WFF A; ::_thesis: ( 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 )
( the_antecedent_of (F => G) = F & the_consequent_of (F => G) = G ) by Th30;
hence ( 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 ) by Th4; ::_thesis: verum
end;
theorem :: QC_LANG2:32
for A being QC-alphabet
for x being bound_QC-variable of A
for H being Element of QC-WFF A holds the_argument_of (Ex (x,H)) = All (x,('not' H)) by Th1;
theorem :: QC_LANG2:33
for A being QC-alphabet
for H being Element of QC-WFF A 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
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A 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 )
let H be Element of QC-WFF A; ::_thesis: ( H is disjunctive implies ( 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 ) )
given F, G being Element of QC-WFF A such that A1: H = F 'or' G ; :: according to QC_LANG2:def_10 ::_thesis: ( 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 )
F 'or' G = ('not' F) => G ;
hence H is conditional by A1, Def11; ::_thesis: ( 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 )
thus H is negative by A1, QC_LANG1:def_19; ::_thesis: ( 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 )
A2: the_argument_of H = ('not' F) '&' ('not' G) by A1, Th1;
hence the_argument_of H is conjunctive by QC_LANG1:def_20; ::_thesis: ( the_left_argument_of (the_argument_of H) is negative & the_right_argument_of (the_argument_of H) is negative )
( the_left_argument_of (the_argument_of H) = 'not' F & the_right_argument_of (the_argument_of H) = 'not' G ) by A2, Th4;
hence ( the_left_argument_of (the_argument_of H) is negative & the_right_argument_of (the_argument_of H) is negative ) by QC_LANG1:def_19; ::_thesis: verum
end;
theorem :: QC_LANG2:34
for A being QC-alphabet
for H being Element of QC-WFF A 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
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A st H is conditional holds
( H is negative & the_argument_of H is conjunctive & the_right_argument_of (the_argument_of H) is negative )
let H be Element of QC-WFF A; ::_thesis: ( H is conditional implies ( H is negative & the_argument_of H is conjunctive & the_right_argument_of (the_argument_of H) is negative ) )
given F, G being Element of QC-WFF A such that A1: H = F => G ; :: according to QC_LANG2:def_11 ::_thesis: ( H is negative & the_argument_of H is conjunctive & the_right_argument_of (the_argument_of H) is negative )
( the_argument_of ('not' (F '&' ('not' G))) = F '&' ('not' G) & the_right_argument_of (F '&' ('not' G)) = 'not' G ) by Th1, Th4;
hence ( H is negative & the_argument_of H is conjunctive & the_right_argument_of (the_argument_of H) is negative ) by A1, QC_LANG1:def_19, QC_LANG1:def_20; ::_thesis: verum
end;
theorem :: QC_LANG2:35
for A being QC-alphabet
for H being Element of QC-WFF A st H is biconditional holds
( H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional )
proof
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A st H is biconditional holds
( H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional )
let H be Element of QC-WFF A; ::_thesis: ( H is biconditional implies ( H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional ) )
given F, G being Element of QC-WFF A such that A1: H = F <=> G ; :: according to QC_LANG2:def_12 ::_thesis: ( H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional )
( the_left_argument_of ((F => G) '&' (G => F)) = F => G & the_right_argument_of ((F => G) '&' (G => F)) = G => F ) by Th4;
hence ( H is conjunctive & the_left_argument_of H is conditional & the_right_argument_of H is conditional ) by A1, Def11, QC_LANG1:def_20; ::_thesis: verum
end;
theorem :: QC_LANG2:36
for A being QC-alphabet
for H being Element of QC-WFF A st H is existential holds
( H is negative & the_argument_of H is universal & the_scope_of (the_argument_of H) is negative )
proof
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A st H is existential holds
( H is negative & the_argument_of H is universal & the_scope_of (the_argument_of H) is negative )
let H be Element of QC-WFF A; ::_thesis: ( H is existential implies ( H is negative & the_argument_of H is universal & the_scope_of (the_argument_of H) is negative ) )
given x being bound_QC-variable of A, H1 being Element of QC-WFF A such that A1: H = Ex (x,H1) ; :: according to QC_LANG2:def_13 ::_thesis: ( H is negative & the_argument_of H is universal & the_scope_of (the_argument_of H) is negative )
( the_argument_of ('not' (All (x,('not' H1)))) = All (x,('not' H1)) & the_scope_of (All (x,('not' H1))) = 'not' H1 ) by Th1, Th7;
hence ( H is negative & the_argument_of H is universal & the_scope_of (the_argument_of H) is negative ) by A1, QC_LANG1:def_19, QC_LANG1:def_21; ::_thesis: verum
end;
theorem :: QC_LANG2:37
for A being QC-alphabet
for H being Element of QC-WFF A st H is disjunctive holds
H = (the_left_disjunct_of H) 'or' (the_right_disjunct_of H)
proof
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A st H is disjunctive holds
H = (the_left_disjunct_of H) 'or' (the_right_disjunct_of H)
let H be Element of QC-WFF A; ::_thesis: ( H is disjunctive implies H = (the_left_disjunct_of H) 'or' (the_right_disjunct_of H) )
given F, G being Element of QC-WFF A such that A1: H = F 'or' G ; :: according to QC_LANG2:def_10 ::_thesis: H = (the_left_disjunct_of H) 'or' (the_right_disjunct_of H)
the_left_disjunct_of H = F by A1, Th29;
hence H = (the_left_disjunct_of H) 'or' (the_right_disjunct_of H) by A1, Th29; ::_thesis: verum
end;
theorem :: QC_LANG2:38
for A being QC-alphabet
for H being Element of QC-WFF A st H is conditional holds
H = (the_antecedent_of H) => (the_consequent_of H)
proof
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A st H is conditional holds
H = (the_antecedent_of H) => (the_consequent_of H)
let H be Element of QC-WFF A; ::_thesis: ( H is conditional implies H = (the_antecedent_of H) => (the_consequent_of H) )
given F, G being Element of QC-WFF A such that A1: H = F => G ; :: according to QC_LANG2:def_11 ::_thesis: H = (the_antecedent_of H) => (the_consequent_of H)
the_antecedent_of H = F by A1, Th30;
hence H = (the_antecedent_of H) => (the_consequent_of H) by A1, Th30; ::_thesis: verum
end;
theorem :: QC_LANG2:39
for A being QC-alphabet
for H being Element of QC-WFF A st H is biconditional holds
H = (the_left_side_of H) <=> (the_right_side_of H)
proof
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A st H is biconditional holds
H = (the_left_side_of H) <=> (the_right_side_of H)
let H be Element of QC-WFF A; ::_thesis: ( H is biconditional implies H = (the_left_side_of H) <=> (the_right_side_of H) )
given F, G being Element of QC-WFF A such that A1: H = F <=> G ; :: according to QC_LANG2:def_12 ::_thesis: H = (the_left_side_of H) <=> (the_right_side_of H)
the_left_side_of H = F by A1, Th31;
hence H = (the_left_side_of H) <=> (the_right_side_of H) by A1, Th31; ::_thesis: verum
end;
theorem :: QC_LANG2:40
for A being QC-alphabet
for H being Element of QC-WFF A st H is existential holds
H = Ex ((bound_in (the_argument_of H)),(the_argument_of (the_scope_of (the_argument_of H))))
proof
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A st H is existential holds
H = Ex ((bound_in (the_argument_of H)),(the_argument_of (the_scope_of (the_argument_of H))))
let H be Element of QC-WFF A; ::_thesis: ( H is existential implies H = Ex ((bound_in (the_argument_of H)),(the_argument_of (the_scope_of (the_argument_of H)))) )
given x being bound_QC-variable of A, H1 being Element of QC-WFF A such that A1: H = Ex (x,H1) ; :: according to QC_LANG2:def_13 ::_thesis: H = Ex ((bound_in (the_argument_of H)),(the_argument_of (the_scope_of (the_argument_of H))))
A2: the_argument_of ('not' H1) = H1 by Th1;
( the_argument_of ('not' (All (x,('not' H1)))) = All (x,('not' H1)) & the_scope_of (All (x,('not' H1))) = 'not' H1 ) by Th1, Th7;
hence H = Ex ((bound_in (the_argument_of H)),(the_argument_of (the_scope_of (the_argument_of H)))) by A1, A2, Th7; ::_thesis: verum
end;
definition
let A be QC-alphabet ;
let G, H be Element of QC-WFF A;
predG is_immediate_constituent_of H means :Def19: :: QC_LANG2:def 19
( H = 'not' G or ex F being Element of QC-WFF A st
( H = G '&' F or H = F '&' G ) or ex x being bound_QC-variable of A st H = All (x,G) );
end;
:: deftheorem Def19 defines is_immediate_constituent_of QC_LANG2:def_19_:_
for A being QC-alphabet
for G, H being Element of QC-WFF A holds
( G is_immediate_constituent_of H iff ( H = 'not' G or ex F being Element of QC-WFF A st
( H = G '&' F or H = F '&' G ) or ex x being bound_QC-variable of A st H = All (x,G) ) );
theorem Th41: :: QC_LANG2:41
for A being QC-alphabet
for H being Element of QC-WFF A holds not H is_immediate_constituent_of VERUM A
proof
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A holds not H is_immediate_constituent_of VERUM A
let H be Element of QC-WFF A; ::_thesis: not H is_immediate_constituent_of VERUM A
( not VERUM A is negative & not VERUM A is conjunctive & not VERUM A is universal ) by QC_LANG1:20;
then ( not VERUM A = 'not' H & ( for H1 being Element of QC-WFF A holds
( not VERUM A = H '&' H1 & not VERUM A = H1 '&' H ) ) & ( for x being bound_QC-variable of A holds not VERUM A = All (x,H) ) ) by QC_LANG1:def_19, QC_LANG1:def_20, QC_LANG1:def_21;
hence not H is_immediate_constituent_of VERUM A by Def19; ::_thesis: verum
end;
theorem Th42: :: QC_LANG2:42
for A being QC-alphabet
for H being Element of QC-WFF A
for k being Element of NAT
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds not H is_immediate_constituent_of P ! V
proof
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A
for k being Element of NAT
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds not H is_immediate_constituent_of P ! V
let H be Element of QC-WFF A; ::_thesis: for k being Element of NAT
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds not H is_immediate_constituent_of P ! V
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds not H is_immediate_constituent_of P ! V
let P be QC-pred_symbol of k,A; ::_thesis: for V being QC-variable_list of k,A holds not H is_immediate_constituent_of P ! V
let V be QC-variable_list of k,A; ::_thesis: not H is_immediate_constituent_of P ! V
assume A1: H is_immediate_constituent_of P ! V ; ::_thesis: contradiction
A2: P ! V is atomic by QC_LANG1:def_18;
then A3: ((@ (P ! V)) . 1) `1 <> 3 by QC_LANG1:19;
A4: ((@ (P ! V)) . 1) `1 <> 2 by A2, QC_LANG1:19;
A5: now__::_thesis:_for_H1_being_Element_of_QC-WFF_A_holds_
(_not_P_!_V_=_H_'&'_H1_&_not_P_!_V_=_H1_'&'_H_)
given H1 being Element of QC-WFF A such that A6: ( P ! V = H '&' H1 or P ! V = H1 '&' H ) ; ::_thesis: contradiction
( H '&' H1 is conjunctive & H1 '&' H is conjunctive ) by QC_LANG1:def_20;
hence contradiction by A4, A6, QC_LANG1:18; ::_thesis: verum
end;
'not' H is negative by QC_LANG1:def_19;
then A7: ((@ ('not' H)) . 1) `1 = 1 by QC_LANG1:18;
((@ (P ! V)) . 1) `1 <> 1 by A2, QC_LANG1:19;
then consider z being bound_QC-variable of A such that
A8: P ! V = All (z,H) by A1, A7, A5, Def19;
All (z,H) is universal by QC_LANG1:def_21;
hence contradiction by A3, A8, QC_LANG1:18; ::_thesis: verum
end;
theorem Th43: :: QC_LANG2:43
for A being QC-alphabet
for F, H being Element of QC-WFF A holds
( F is_immediate_constituent_of 'not' H iff F = H )
proof
let A be QC-alphabet ; ::_thesis: for F, H being Element of QC-WFF A holds
( F is_immediate_constituent_of 'not' H iff F = H )
let F, H be Element of QC-WFF A; ::_thesis: ( F is_immediate_constituent_of 'not' H iff F = H )
thus ( F is_immediate_constituent_of 'not' H implies F = H ) ::_thesis: ( F = H implies F is_immediate_constituent_of 'not' H )
proof
'not' H is negative by QC_LANG1:def_19;
then A1: ((@ ('not' H)) . 1) `1 = 1 by QC_LANG1:18;
A2: now__::_thesis:_for_H1_being_Element_of_QC-WFF_A_holds_
(_not_'not'_H_=_F_'&'_H1_&_not_'not'_H_=_H1_'&'_F_)
given H1 being Element of QC-WFF A such that A3: ( 'not' H = F '&' H1 or 'not' H = H1 '&' F ) ; ::_thesis: contradiction
( F '&' H1 is conjunctive & H1 '&' F is conjunctive ) by QC_LANG1:def_20;
hence contradiction by A1, A3, QC_LANG1:18; ::_thesis: verum
end;
A4: now__::_thesis:_for_x_being_bound_QC-variable_of_A_holds_not_'not'_H_=_All_(x,F)
given x being bound_QC-variable of A such that A5: 'not' H = All (x,F) ; ::_thesis: contradiction
All (x,F) is universal by QC_LANG1:def_21;
hence contradiction by A1, A5, QC_LANG1:18; ::_thesis: verum
end;
assume ( 'not' H = 'not' F or ex H1 being Element of QC-WFF A st
( 'not' H = F '&' H1 or 'not' H = H1 '&' F ) or ex x being bound_QC-variable of A st 'not' H = All (x,F) ) ; :: according to QC_LANG2:def_19 ::_thesis: F = H
hence F = H by A2, A4, FINSEQ_1:33; ::_thesis: verum
end;
thus ( F = H implies F is_immediate_constituent_of 'not' H ) by Def19; ::_thesis: verum
end;
theorem :: QC_LANG2:44
for A being QC-alphabet
for H being Element of QC-WFF A holds
( H is_immediate_constituent_of FALSUM A iff H = VERUM A ) by Th43;
theorem Th45: :: QC_LANG2:45
for A being QC-alphabet
for F, G, H being Element of QC-WFF A holds
( F is_immediate_constituent_of G '&' H iff ( F = G or F = H ) )
proof
let A be QC-alphabet ; ::_thesis: for F, G, H being Element of QC-WFF A holds
( F is_immediate_constituent_of G '&' H iff ( F = G or F = H ) )
let F, G, H be Element of QC-WFF A; ::_thesis: ( F is_immediate_constituent_of G '&' H iff ( F = G or F = H ) )
thus ( not F is_immediate_constituent_of G '&' H or F = G or F = H ) ::_thesis: ( ( F = G or F = H ) implies F is_immediate_constituent_of G '&' H )
proof
G '&' H is conjunctive by QC_LANG1:def_20;
then A1: ((@ (G '&' H)) . 1) `1 = 2 by QC_LANG1:18;
A2: now__::_thesis:_not_G_'&'_H_=_'not'_F
A3: 'not' F is negative by QC_LANG1:def_19;
assume G '&' H = 'not' F ; ::_thesis: contradiction
hence contradiction by A1, A3, QC_LANG1:18; ::_thesis: verum
end;
A4: now__::_thesis:_for_x_being_bound_QC-variable_of_A_holds_not_G_'&'_H_=_All_(x,F)
given x being bound_QC-variable of A such that A5: G '&' H = All (x,F) ; ::_thesis: contradiction
All (x,F) is universal by QC_LANG1:def_21;
hence contradiction by A1, A5, QC_LANG1:18; ::_thesis: verum
end;
assume ( G '&' H = 'not' F or ex H1 being Element of QC-WFF A st
( G '&' H = F '&' H1 or G '&' H = H1 '&' F ) or ex x being bound_QC-variable of A st G '&' H = All (x,F) ) ; :: according to QC_LANG2:def_19 ::_thesis: ( F = G or F = H )
hence ( F = G or F = H ) by A2, A4, Th2; ::_thesis: verum
end;
assume ( F = G or F = H ) ; ::_thesis: F is_immediate_constituent_of G '&' H
hence F is_immediate_constituent_of G '&' H by Def19; ::_thesis: verum
end;
theorem Th46: :: QC_LANG2:46
for A being QC-alphabet
for F, H being Element of QC-WFF A
for x being bound_QC-variable of A holds
( F is_immediate_constituent_of All (x,H) iff F = H )
proof
let A be QC-alphabet ; ::_thesis: for F, H being Element of QC-WFF A
for x being bound_QC-variable of A holds
( F is_immediate_constituent_of All (x,H) iff F = H )
let F, H be Element of QC-WFF A; ::_thesis: for x being bound_QC-variable of A holds
( F is_immediate_constituent_of All (x,H) iff F = H )
let x be bound_QC-variable of A; ::_thesis: ( F is_immediate_constituent_of All (x,H) iff F = H )
thus ( F is_immediate_constituent_of All (x,H) implies F = H ) ::_thesis: ( F = H implies F is_immediate_constituent_of All (x,H) )
proof
All (x,H) is universal by QC_LANG1:def_21;
then A1: ((@ (All (x,H))) . 1) `1 = 3 by QC_LANG1:18;
A2: now__::_thesis:_not_All_(x,H)_=_'not'_F
A3: 'not' F is negative by QC_LANG1:def_19;
assume All (x,H) = 'not' F ; ::_thesis: contradiction
hence contradiction by A1, A3, QC_LANG1:18; ::_thesis: verum
end;
A4: now__::_thesis:_for_G_being_Element_of_QC-WFF_A_holds_
(_not_All_(x,H)_=_F_'&'_G_&_not_All_(x,H)_=_G_'&'_F_)
given G being Element of QC-WFF A such that A5: ( All (x,H) = F '&' G or All (x,H) = G '&' F ) ; ::_thesis: contradiction
( F '&' G is conjunctive & G '&' F is conjunctive ) by QC_LANG1:def_20;
hence contradiction by A1, A5, QC_LANG1:18; ::_thesis: verum
end;
assume ( All (x,H) = 'not' F or ex H1 being Element of QC-WFF A st
( All (x,H) = F '&' H1 or All (x,H) = H1 '&' F ) or ex y being bound_QC-variable of A st All (x,H) = All (y,F) ) ; :: according to QC_LANG2:def_19 ::_thesis: F = H
hence F = H by A2, A4, Th5; ::_thesis: verum
end;
thus ( F = H implies F is_immediate_constituent_of All (x,H) ) by Def19; ::_thesis: verum
end;
theorem Th47: :: QC_LANG2:47
for A being QC-alphabet
for H, F being Element of QC-WFF A st H is atomic holds
not F is_immediate_constituent_of H
proof
let A be QC-alphabet ; ::_thesis: for H, F being Element of QC-WFF A st H is atomic holds
not F is_immediate_constituent_of H
let H, F be Element of QC-WFF A; ::_thesis: ( H is atomic implies not F is_immediate_constituent_of H )
assume ex k being Element of NAT ex P being QC-pred_symbol of k,A ex V being QC-variable_list of k,A st H = P ! V ; :: according to QC_LANG1:def_18 ::_thesis: not F is_immediate_constituent_of H
hence not F is_immediate_constituent_of H by Th42; ::_thesis: verum
end;
theorem Th48: :: QC_LANG2:48
for A being QC-alphabet
for H, F being Element of QC-WFF A st H is negative holds
( F is_immediate_constituent_of H iff F = the_argument_of H )
proof
let A be QC-alphabet ; ::_thesis: for H, F being Element of QC-WFF A st H is negative holds
( F is_immediate_constituent_of H iff F = the_argument_of H )
let H, F be Element of QC-WFF A; ::_thesis: ( H is negative implies ( F is_immediate_constituent_of H iff F = the_argument_of H ) )
assume H is negative ; ::_thesis: ( F is_immediate_constituent_of H iff F = the_argument_of H )
then H = 'not' (the_argument_of H) by QC_LANG1:def_24;
hence ( F is_immediate_constituent_of H iff F = the_argument_of H ) by Th43; ::_thesis: verum
end;
theorem Th49: :: QC_LANG2:49
for A being QC-alphabet
for H, F being Element of QC-WFF A 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
let A be QC-alphabet ; ::_thesis: for H, F being Element of QC-WFF A 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 ) )
let H, F be Element of QC-WFF A; ::_thesis: ( H is conjunctive implies ( F is_immediate_constituent_of H iff ( F = the_left_argument_of H or F = the_right_argument_of H ) ) )
assume H is conjunctive ; ::_thesis: ( F is_immediate_constituent_of H iff ( F = the_left_argument_of H or F = the_right_argument_of H ) )
then H = (the_left_argument_of H) '&' (the_right_argument_of H) by Th3;
hence ( F is_immediate_constituent_of H iff ( F = the_left_argument_of H or F = the_right_argument_of H ) ) by Th45; ::_thesis: verum
end;
theorem Th50: :: QC_LANG2:50
for A being QC-alphabet
for H, F being Element of QC-WFF A st H is universal holds
( F is_immediate_constituent_of H iff F = the_scope_of H )
proof
let A be QC-alphabet ; ::_thesis: for H, F being Element of QC-WFF A st H is universal holds
( F is_immediate_constituent_of H iff F = the_scope_of H )
let H, F be Element of QC-WFF A; ::_thesis: ( H is universal implies ( F is_immediate_constituent_of H iff F = the_scope_of H ) )
assume H is universal ; ::_thesis: ( F is_immediate_constituent_of H iff F = the_scope_of H )
then H = All ((bound_in H),(the_scope_of H)) by Th6;
hence ( F is_immediate_constituent_of H iff F = the_scope_of H ) by Th46; ::_thesis: verum
end;
definition
let A be QC-alphabet ;
let G, H be Element of QC-WFF A;
predG is_subformula_of H means :Def20: :: QC_LANG2:def 20
ex n being Element of NAT ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = G & L . n = H & ( for k being Element of NAT st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) );
reflexivity
for G being Element of QC-WFF A ex n being Element of NAT ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = G & L . n = G & ( for k being Element of NAT st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
proof
let H be Element of QC-WFF A; ::_thesis: ex n being Element of NAT ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = H & L . n = H & ( for k being Element of NAT st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
reconsider L = <*H*> as FinSequence ;
take 1 ; ::_thesis: ex L being FinSequence st
( 1 <= 1 & len L = 1 & L . 1 = H & L . 1 = H & ( for k being Element of NAT st 1 <= k & k < 1 holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
take L ; ::_thesis: ( 1 <= 1 & len L = 1 & L . 1 = H & L . 1 = H & ( for k being Element of NAT st 1 <= k & k < 1 holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
thus ( 1 <= 1 & len L = 1 & L . 1 = H & L . 1 = H ) by FINSEQ_1:40; ::_thesis: for k being Element of NAT st 1 <= k & k < 1 holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 )
let k be Element of NAT ; ::_thesis: ( 1 <= k & k < 1 implies ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) )
assume ( 1 <= k & k < 1 ) ; ::_thesis: ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 )
hence ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ; ::_thesis: verum
end;
end;
:: deftheorem Def20 defines is_subformula_of QC_LANG2:def_20_:_
for A being QC-alphabet
for G, H being Element of QC-WFF A holds
( G is_subformula_of H iff ex n being Element of NAT ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = G & L . n = H & ( for k being Element of NAT st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) );
definition
let A be QC-alphabet ;
let H, F be Element of QC-WFF A;
predH is_proper_subformula_of F means :Def21: :: QC_LANG2:def 21
( H is_subformula_of F & H <> F );
irreflexivity
for H being Element of QC-WFF A holds
( not H is_subformula_of H or not H <> H ) ;
end;
:: deftheorem Def21 defines is_proper_subformula_of QC_LANG2:def_21_:_
for A being QC-alphabet
for H, F being Element of QC-WFF A holds
( H is_proper_subformula_of F iff ( H is_subformula_of F & H <> F ) );
theorem Th51: :: QC_LANG2:51
for A being QC-alphabet
for H, F being Element of QC-WFF A st H is_immediate_constituent_of F holds
len (@ H) < len (@ F)
proof
let A be QC-alphabet ; ::_thesis: for H, F being Element of QC-WFF A st H is_immediate_constituent_of F holds
len (@ H) < len (@ F)
let H, F be Element of QC-WFF A; ::_thesis: ( H is_immediate_constituent_of F implies len (@ H) < len (@ F) )
A1: ( F = VERUM A or F is atomic or F is negative or F is conjunctive or F is universal ) by QC_LANG1:9;
assume H is_immediate_constituent_of F ; ::_thesis: len (@ H) < len (@ F)
then ( ( F is negative & H = the_argument_of F ) or ( F is conjunctive & H = the_left_argument_of F ) or ( F is conjunctive & H = the_right_argument_of F ) or ( F is universal & H = the_scope_of F ) ) by A1, Th41, Th47, Th48, Th49, Th50;
hence len (@ H) < len (@ F) by QC_LANG1:14, QC_LANG1:15, QC_LANG1:16; ::_thesis: verum
end;
theorem Th52: :: QC_LANG2:52
for A being QC-alphabet
for H, F being Element of QC-WFF A st H is_immediate_constituent_of F holds
H is_subformula_of F
proof
let A be QC-alphabet ; ::_thesis: for H, F being Element of QC-WFF A st H is_immediate_constituent_of F holds
H is_subformula_of F
let H, F be Element of QC-WFF A; ::_thesis: ( H is_immediate_constituent_of F implies H is_subformula_of F )
assume A1: H is_immediate_constituent_of F ; ::_thesis: H is_subformula_of F
take n = 2; :: according to QC_LANG2:def_20 ::_thesis: ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
take L = <*H,F*>; ::_thesis: ( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
thus 1 <= n ; ::_thesis: ( len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
thus len L = n by FINSEQ_1:44; ::_thesis: ( L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
thus ( L . 1 = H & L . n = F ) by FINSEQ_1:44; ::_thesis: for k being Element of NAT st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 )
let k be Element of NAT ; ::_thesis: ( 1 <= k & k < n implies ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) )
assume that
A2: 1 <= k and
A3: k < n ; ::_thesis: ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 )
take H ; ::_thesis: ex H1 being Element of QC-WFF A st
( L . k = H & L . (k + 1) = H1 & H is_immediate_constituent_of H1 )
take F ; ::_thesis: ( L . k = H & L . (k + 1) = F & H is_immediate_constituent_of F )
k < 1 + 1 by A3;
then k <= 1 by NAT_1:13;
then k = 1 by A2, XXREAL_0:1;
hence ( L . k = H & L . (k + 1) = F ) by FINSEQ_1:44; ::_thesis: H is_immediate_constituent_of F
thus H is_immediate_constituent_of F by A1; ::_thesis: verum
end;
theorem Th53: :: QC_LANG2:53
for A being QC-alphabet
for H, F being Element of QC-WFF A st H is_immediate_constituent_of F holds
H is_proper_subformula_of F
proof
let A be QC-alphabet ; ::_thesis: for H, F being Element of QC-WFF A st H is_immediate_constituent_of F holds
H is_proper_subformula_of F
let H, F be Element of QC-WFF A; ::_thesis: ( H is_immediate_constituent_of F implies H is_proper_subformula_of F )
assume A1: H is_immediate_constituent_of F ; ::_thesis: H is_proper_subformula_of F
hence H is_subformula_of F by Th52; :: according to QC_LANG2:def_21 ::_thesis: H <> F
assume H = F ; ::_thesis: contradiction
then len (@ H) = len (@ F) ;
hence contradiction by A1, Th51; ::_thesis: verum
end;
theorem Th54: :: QC_LANG2:54
for A being QC-alphabet
for H, F being Element of QC-WFF A st H is_proper_subformula_of F holds
len (@ H) < len (@ F)
proof
let A be QC-alphabet ; ::_thesis: for H, F being Element of QC-WFF A st H is_proper_subformula_of F holds
len (@ H) < len (@ F)
let H, F be Element of QC-WFF A; ::_thesis: ( H is_proper_subformula_of F implies len (@ H) < len (@ F) )
given n being Element of NAT , L being FinSequence such that A1: 1 <= n and
len L = n and
A2: L . 1 = H and
A3: L . n = F and
A4: for k being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being Element of QC-WFF A st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ; :: according to QC_LANG2:def_20,QC_LANG2:def_21 ::_thesis: ( not H <> F or len (@ H) < len (@ F) )
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 < n implies for H1 being Element of QC-WFF A st L . ($1 + 1) = H1 holds
len (@ H) < len (@ H1) );
A5: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume that
A6: ( 1 <= k & k < n implies for H1 being Element of QC-WFF A st L . (k + 1) = H1 holds
len (@ H) < len (@ H1) ) and
A7: 1 <= k + 1 and
A8: k + 1 < n ; ::_thesis: for H1 being Element of QC-WFF A st L . ((k + 1) + 1) = H1 holds
len (@ H) < len (@ H1)
consider F1, G being Element of QC-WFF A such that
A9: L . (k + 1) = F1 and
A10: ( L . ((k + 1) + 1) = G & F1 is_immediate_constituent_of G ) by A4, A7, A8;
let H1 be Element of QC-WFF A; ::_thesis: ( L . ((k + 1) + 1) = H1 implies len (@ H) < len (@ H1) )
assume A11: L . ((k + 1) + 1) = H1 ; ::_thesis: len (@ H) < len (@ H1)
A12: now__::_thesis:_(_ex_m_being_Nat_st_k_=_m_+_1_implies_len_(@_H)_<_len_(@_H1)_)
given m being Nat such that A13: k = m + 1 ; ::_thesis: len (@ H) < len (@ H1)
len (@ H) < len (@ F1) by A6, A8, A9, A13, NAT_1:11, NAT_1:13;
hence len (@ H) < len (@ H1) by A11, A10, Th51, XXREAL_0:2; ::_thesis: verum
end;
( k = 0 implies len (@ H) < len (@ H1) ) by A2, A11, A9, A10, Th51;
hence len (@ H) < len (@ H1) by A12, NAT_1:6; ::_thesis: verum
end;
assume H <> F ; ::_thesis: len (@ H) < len (@ F)
then 1 < n by A1, A2, A3, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A14: n = 2 + k by NAT_1:10;
A15: S1[ 0 ] ;
A16: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A15, A5);
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A17: (1 + 1) + k = (1 + k) + 1 ;
then 1 + k < n by A14, NAT_1:13;
hence len (@ H) < len (@ F) by A3, A16, A14, A17, NAT_1:11; ::_thesis: verum
end;
theorem Th55: :: QC_LANG2:55
for A being QC-alphabet
for H, F being Element of QC-WFF A st H is_proper_subformula_of F holds
ex G being Element of QC-WFF A st G is_immediate_constituent_of F
proof
let A be QC-alphabet ; ::_thesis: for H, F being Element of QC-WFF A st H is_proper_subformula_of F holds
ex G being Element of QC-WFF A st G is_immediate_constituent_of F
let H, F be Element of QC-WFF A; ::_thesis: ( H is_proper_subformula_of F implies ex G being Element of QC-WFF A st G is_immediate_constituent_of F )
given n being Element of NAT , L being FinSequence such that A1: 1 <= n and
len L = n and
A2: L . 1 = H and
A3: L . n = F and
A4: for k being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being Element of QC-WFF A st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ; :: according to QC_LANG2:def_20,QC_LANG2:def_21 ::_thesis: ( not H <> F or ex G being Element of QC-WFF A st G is_immediate_constituent_of F )
assume H <> F ; ::_thesis: ex G being Element of QC-WFF A st G is_immediate_constituent_of F
then 1 < n by A1, A2, A3, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A5: n = 2 + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
(1 + 1) + k = (1 + k) + 1 ;
then 1 + k < n by A5, NAT_1:13;
then consider H1, F1 being Element of QC-WFF A such that
L . (1 + k) = H1 and
A6: ( L . ((1 + k) + 1) = F1 & H1 is_immediate_constituent_of F1 ) by A4, NAT_1:11;
take H1 ; ::_thesis: H1 is_immediate_constituent_of F
thus H1 is_immediate_constituent_of F by A3, A5, A6; ::_thesis: verum
end;
theorem Th56: :: QC_LANG2:56
for A being QC-alphabet
for F, G, H being Element of QC-WFF A st F is_proper_subformula_of G & G is_proper_subformula_of H holds
F is_proper_subformula_of H
proof
let A be QC-alphabet ; ::_thesis: for F, G, H being Element of QC-WFF A st F is_proper_subformula_of G & G is_proper_subformula_of H holds
F is_proper_subformula_of H
let F, G, H be Element of QC-WFF A; ::_thesis: ( F is_proper_subformula_of G & G is_proper_subformula_of H implies F is_proper_subformula_of H )
assume that
A1: F is_proper_subformula_of G and
A2: G is_proper_subformula_of H ; ::_thesis: F is_proper_subformula_of H
F is_subformula_of G by A1, Def21;
then consider n being Element of NAT , L being FinSequence such that
A3: 1 <= n and
A4: len L = n and
A5: L . 1 = F and
A6: L . n = G and
A7: for k being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being Element of QC-WFF A st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) by Def20;
1 < n by A1, A3, A5, A6, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A8: n = 2 + k by NAT_1:10;
G is_subformula_of H by A2, Def21;
then consider m being Element of NAT , L9 being FinSequence such that
A9: 1 <= m and
A10: len L9 = m and
A11: L9 . 1 = G and
A12: L9 . m = H and
A13: for k being Element of NAT st 1 <= k & k < m holds
ex H1, F1 being Element of QC-WFF A st
( L9 . k = H1 & L9 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) by Def20;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
reconsider L1 = L | (Seg (1 + k)) as FinSequence by FINSEQ_1:15;
thus F is_subformula_of H :: according to QC_LANG2:def_21 ::_thesis: F <> H
proof
take l = (1 + k) + m; :: according to QC_LANG2:def_20 ::_thesis: ex L being FinSequence st
( 1 <= l & len L = l & L . 1 = F & L . l = H & ( for k being Element of NAT st 1 <= k & k < l holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
take K = L1 ^ L9; ::_thesis: ( 1 <= l & len K = l & K . 1 = F & K . l = H & ( for k being Element of NAT st 1 <= k & k < l holds
ex G1, H1 being Element of QC-WFF A st
( K . k = G1 & K . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
A14: ((1 + k) + m) - (1 + k) = m ;
m <= m + (1 + k) by NAT_1:11;
hence 1 <= l by A9, XXREAL_0:2; ::_thesis: ( len K = l & K . 1 = F & K . l = H & ( for k being Element of NAT st 1 <= k & k < l holds
ex G1, H1 being Element of QC-WFF A st
( K . k = G1 & K . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
(1 + 1) + k = (1 + k) + 1 ;
then A15: 1 + k <= n by A8, NAT_1:11;
then A16: len L1 = 1 + k by A4, FINSEQ_1:17;
hence A17: len K = l by A10, FINSEQ_1:22; ::_thesis: ( K . 1 = F & K . l = H & ( for k being Element of NAT st 1 <= k & k < l holds
ex G1, H1 being Element of QC-WFF A st
( K . k = G1 & K . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
A18: now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_1_+_k_holds_
K_._j_=_L_._j
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= 1 + k implies K . j = L . j )
assume ( 1 <= j & j <= 1 + k ) ; ::_thesis: K . j = L . j
then A19: j in Seg (1 + k) by FINSEQ_1:1;
then j in dom L1 by A4, A15, FINSEQ_1:17;
then K . j = L1 . j by FINSEQ_1:def_7;
hence K . j = L . j by A19, FUNCT_1:49; ::_thesis: verum
end;
1 <= 1 + k by NAT_1:11;
hence K . 1 = F by A5, A18; ::_thesis: ( K . l = H & ( for k being Element of NAT st 1 <= k & k < l holds
ex G1, H1 being Element of QC-WFF A st
( K . k = G1 & K . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
(len L1) + 1 <= (len L1) + m by A9, XREAL_1:7;
then len L1 < l by A16, NAT_1:13;
then K . l = L9 . (l - (len L1)) by A17, FINSEQ_1:24;
hence K . l = H by A4, A12, A15, A14, FINSEQ_1:17; ::_thesis: for k being Element of NAT st 1 <= k & k < l holds
ex G1, H1 being Element of QC-WFF A st
( K . k = G1 & K . (k + 1) = H1 & G1 is_immediate_constituent_of H1 )
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < l implies ex G1, H1 being Element of QC-WFF A st
( K . j = G1 & K . (j + 1) = H1 & G1 is_immediate_constituent_of H1 ) )
assume that
A20: 1 <= j and
A21: j < l ; ::_thesis: ex G1, H1 being Element of QC-WFF A st
( K . j = G1 & K . (j + 1) = H1 & G1 is_immediate_constituent_of H1 )
j + 0 <= j + 1 by XREAL_1:7;
then A22: 1 <= j + 1 by A20, XXREAL_0:2;
A23: now__::_thesis:_(_j_<_1_+_k_implies_ex_F1,_G1_being_Element_of_QC-WFF_A_st_
(_K_._j_=_F1_&_K_._(j_+_1)_=_G1_&_F1_is_immediate_constituent_of_G1_)_)
assume A24: j < 1 + k ; ::_thesis: ex F1, G1 being Element of QC-WFF A st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
then A25: j + 1 <= 1 + k by NAT_1:13;
then j + 1 <= n by A15, XXREAL_0:2;
then j < n by NAT_1:13;
then consider F1, G1 being Element of QC-WFF A such that
A26: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A7, A20;
take F1 = F1; ::_thesis: ex G1 being Element of QC-WFF A st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
take G1 = G1; ::_thesis: ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
thus ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A18, A20, A22, A24, A25, A26; ::_thesis: verum
end;
A27: now__::_thesis:_(_1_+_k_<_j_implies_ex_F1,_G1_being_Element_of_QC-WFF_A_st_
(_K_._j_=_F1_&_K_._(j_+_1)_=_G1_&_F1_is_immediate_constituent_of_G1_)_)
A28: j + 1 <= l by A21, NAT_1:13;
assume A29: 1 + k < j ; ::_thesis: ex F1, G1 being Element of QC-WFF A st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
then A30: 1 + k < j + 1 by NAT_1:13;
(1 + k) + 1 <= j by A29, NAT_1:13;
then consider j1 being Nat such that
A31: j = ((1 + k) + 1) + j1 by NAT_1:10;
reconsider j1 = j1 as Element of NAT by ORDINAL1:def_12;
j - (1 + k) < l - (1 + k) by A21, XREAL_1:9;
then consider F1, G1 being Element of QC-WFF A such that
A32: ( L9 . (1 + j1) = F1 & L9 . ((1 + j1) + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A13, A31, NAT_1:11;
take F1 = F1; ::_thesis: ex G1 being Element of QC-WFF A st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
take G1 = G1; ::_thesis: ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
A33: ((1 + j1) + (1 + k)) - (1 + k) = ((1 + j1) + (1 + k)) + (- (1 + k)) ;
(j + 1) - (len L1) = 1 + (j + (- (len L1)))
.= (1 + j1) + 1 by A4, A15, A31, A33, FINSEQ_1:17 ;
hence ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A16, A17, A21, A29, A30, A28, A33, A32, FINSEQ_1:24; ::_thesis: verum
end;
now__::_thesis:_(_j_=_1_+_k_implies_ex_F1,_G1_being_Element_of_QC-WFF_A_st_
(_K_._j_=_F1_&_K_._(j_+_1)_=_G1_&_F1_is_immediate_constituent_of_G1_)_)
A34: ( j + 1 <= l & (j + 1) - j = (j + 1) + (- j) ) by A21, NAT_1:13;
assume A35: j = 1 + k ; ::_thesis: ex F1, G1 being Element of QC-WFF A st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
then j < (1 + k) + 1 by NAT_1:13;
then consider F1, G1 being Element of QC-WFF A such that
A36: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A7, A8, A20;
take F1 = F1; ::_thesis: ex G1 being Element of QC-WFF A st
( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
take G1 = G1; ::_thesis: ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
1 + k < j + 1 by A35, NAT_1:13;
hence ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A6, A11, A8, A16, A17, A18, A20, A35, A34, A36, FINSEQ_1:24; ::_thesis: verum
end;
hence ex G1, H1 being Element of QC-WFF A st
( K . j = G1 & K . (j + 1) = H1 & G1 is_immediate_constituent_of H1 ) by A23, A27, XXREAL_0:1; ::_thesis: verum
end;
len (@ F) < len (@ G) by A1, Th54;
hence F <> H by A2, Th54; ::_thesis: verum
end;
theorem Th57: :: QC_LANG2:57
for A being QC-alphabet
for F, G, H being Element of QC-WFF A st F is_subformula_of G & G is_subformula_of H holds
F is_subformula_of H
proof
let A be QC-alphabet ; ::_thesis: for F, G, H being Element of QC-WFF A st F is_subformula_of G & G is_subformula_of H holds
F is_subformula_of H
let F, G, H be Element of QC-WFF A; ::_thesis: ( F is_subformula_of G & G is_subformula_of H implies F is_subformula_of H )
assume that
A1: F is_subformula_of G and
A2: G is_subformula_of H ; ::_thesis: F is_subformula_of H
now__::_thesis:_(_F_<>_G_implies_F_is_subformula_of_H_)
assume F <> G ; ::_thesis: F is_subformula_of H
then A3: F is_proper_subformula_of G by A1, Def21;
now__::_thesis:_(_G_<>_H_implies_F_is_subformula_of_H_)
assume G <> H ; ::_thesis: F is_subformula_of H
then G is_proper_subformula_of H by A2, Def21;
then F is_proper_subformula_of H by A3, Th56;
hence F is_subformula_of H by Def21; ::_thesis: verum
end;
hence F is_subformula_of H by A1; ::_thesis: verum
end;
hence F is_subformula_of H by A2; ::_thesis: verum
end;
theorem Th58: :: QC_LANG2:58
for A being QC-alphabet
for G, H being Element of QC-WFF A st G is_subformula_of H & H is_subformula_of G holds
G = H
proof
let A be QC-alphabet ; ::_thesis: for G, H being Element of QC-WFF A st G is_subformula_of H & H is_subformula_of G holds
G = H
let G, H be Element of QC-WFF A; ::_thesis: ( G is_subformula_of H & H is_subformula_of G implies G = H )
assume that
A1: G is_subformula_of H and
A2: H is_subformula_of G ; ::_thesis: G = H
assume A3: G <> H ; ::_thesis: contradiction
then G is_proper_subformula_of H by A1, Def21;
then A4: len (@ G) < len (@ H) by Th54;
H is_proper_subformula_of G by A2, A3, Def21;
hence contradiction by A4, Th54; ::_thesis: verum
end;
theorem Th59: :: QC_LANG2:59
for A being QC-alphabet
for G, H being Element of QC-WFF A holds
( not G is_proper_subformula_of H or not H is_subformula_of G )
proof
let A be QC-alphabet ; ::_thesis: for G, H being Element of QC-WFF A holds
( not G is_proper_subformula_of H or not H is_subformula_of G )
let G, H be Element of QC-WFF A; ::_thesis: ( not G is_proper_subformula_of H or not H is_subformula_of G )
assume ( G is_subformula_of H & G <> H & H is_subformula_of G ) ; :: according to QC_LANG2:def_21 ::_thesis: contradiction
hence contradiction by Th58; ::_thesis: verum
end;
theorem :: QC_LANG2:60
for A being QC-alphabet
for G, H being Element of QC-WFF A holds
( not G is_proper_subformula_of H or not H is_proper_subformula_of G )
proof
let A be QC-alphabet ; ::_thesis: for G, H being Element of QC-WFF A holds
( not G is_proper_subformula_of H or not H is_proper_subformula_of G )
let G, H be Element of QC-WFF A; ::_thesis: ( not G is_proper_subformula_of H or not H is_proper_subformula_of G )
assume that
A1: G is_subformula_of H and
G <> H and
A2: H is_proper_subformula_of G ; :: according to QC_LANG2:def_21 ::_thesis: contradiction
thus contradiction by A1, A2, Th59; ::_thesis: verum
end;
theorem Th61: :: QC_LANG2:61
for A being QC-alphabet
for G, H being Element of QC-WFF A holds
( not G is_subformula_of H or not H is_immediate_constituent_of G ) by Th53, Th59;
theorem Th62: :: QC_LANG2:62
for A being QC-alphabet
for G, H being Element of QC-WFF A holds
( not G is_proper_subformula_of H or not H is_immediate_constituent_of G )
proof
let A be QC-alphabet ; ::_thesis: for G, H being Element of QC-WFF A holds
( not G is_proper_subformula_of H or not H is_immediate_constituent_of G )
let G, H be Element of QC-WFF A; ::_thesis: ( not G is_proper_subformula_of H or not H is_immediate_constituent_of G )
assume that
A1: G is_subformula_of H and
G <> H and
A2: H is_immediate_constituent_of G ; :: according to QC_LANG2:def_21 ::_thesis: contradiction
thus contradiction by A1, A2, Th53, Th59; ::_thesis: verum
end;
theorem Th63: :: QC_LANG2:63
for A being QC-alphabet
for F, G, H being Element of QC-WFF A 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
let A be QC-alphabet ; ::_thesis: for F, G, H being Element of QC-WFF A 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
let F, G, H be Element of QC-WFF A; ::_thesis: ( ( ( 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 ) ) implies F is_proper_subformula_of H )
assume A1: ( ( 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 ) ) ; ::_thesis: F is_proper_subformula_of H
then ( F is_subformula_of G & G is_subformula_of H ) by Def21, Th52;
hence F is_subformula_of H by Th57; :: according to QC_LANG2:def_21 ::_thesis: F <> H
thus F <> H by A1, Th59, Th61, Th62; ::_thesis: verum
end;
theorem Th64: :: QC_LANG2:64
for A being QC-alphabet
for F being Element of QC-WFF A holds not F is_proper_subformula_of VERUM A
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A holds not F is_proper_subformula_of VERUM A
let F be Element of QC-WFF A; ::_thesis: not F is_proper_subformula_of VERUM A
assume F is_proper_subformula_of VERUM A ; ::_thesis: contradiction
then consider G being Element of QC-WFF A such that
A1: G is_immediate_constituent_of VERUM A by Th55;
thus contradiction by A1, Th41; ::_thesis: verum
end;
theorem Th65: :: QC_LANG2:65
for A being QC-alphabet
for F being Element of QC-WFF A
for k being Element of NAT
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds not F is_proper_subformula_of P ! V
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for k being Element of NAT
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds not F is_proper_subformula_of P ! V
let F be Element of QC-WFF A; ::_thesis: for k being Element of NAT
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds not F is_proper_subformula_of P ! V
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds not F is_proper_subformula_of P ! V
let P be QC-pred_symbol of k,A; ::_thesis: for V being QC-variable_list of k,A holds not F is_proper_subformula_of P ! V
let V be QC-variable_list of k,A; ::_thesis: not F is_proper_subformula_of P ! V
assume F is_proper_subformula_of P ! V ; ::_thesis: contradiction
then ex G being Element of QC-WFF A st G is_immediate_constituent_of P ! V by Th55;
hence contradiction by Th42; ::_thesis: verum
end;
theorem Th66: :: QC_LANG2:66
for A being QC-alphabet
for F, H being Element of QC-WFF A holds
( F is_subformula_of H iff F is_proper_subformula_of 'not' H )
proof
let A be QC-alphabet ; ::_thesis: for F, H being Element of QC-WFF A holds
( F is_subformula_of H iff F is_proper_subformula_of 'not' H )
let F, H be Element of QC-WFF A; ::_thesis: ( F is_subformula_of H iff F is_proper_subformula_of 'not' H )
H is_immediate_constituent_of 'not' H by Th43;
hence ( F is_subformula_of H implies F is_proper_subformula_of 'not' H ) by Th63; ::_thesis: ( F is_proper_subformula_of 'not' H implies F is_subformula_of H )
given n being Element of NAT , L being FinSequence such that A1: 1 <= n and
A2: len L = n and
A3: L . 1 = F and
A4: L . n = 'not' H and
A5: for k being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being Element of QC-WFF A st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ; :: according to QC_LANG2:def_20,QC_LANG2:def_21 ::_thesis: ( not F <> 'not' H or F is_subformula_of H )
assume F <> 'not' H ; ::_thesis: F is_subformula_of H
then 1 < n by A1, A3, A4, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A6: n = 2 + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
reconsider L1 = L | (Seg (1 + k)) as FinSequence by FINSEQ_1:15;
take m = 1 + k; :: according to QC_LANG2:def_20 ::_thesis: ex L being FinSequence st
( 1 <= m & len L = m & L . 1 = F & L . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
take L1 ; ::_thesis: ( 1 <= m & len L1 = m & L1 . 1 = F & L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
thus A7: 1 <= m by NAT_1:11; ::_thesis: ( len L1 = m & L1 . 1 = F & L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
1 + k <= (1 + k) + 1 by NAT_1:11;
hence len L1 = m by A2, A6, FINSEQ_1:17; ::_thesis: ( L1 . 1 = F & L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
A8: now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_m_holds_
L1_._j_=_L_._j
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= m implies L1 . j = L . j )
assume ( 1 <= j & j <= m ) ; ::_thesis: L1 . j = L . j
then j in Seg (1 + k) by FINSEQ_1:1;
hence L1 . j = L . j by FUNCT_1:49; ::_thesis: verum
end;
hence L1 . 1 = F by A3, A7; ::_thesis: ( L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
m < m + 1 by NAT_1:13;
then consider F1, G1 being Element of QC-WFF A such that
A9: L . m = F1 and
A10: ( L . (m + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A5, A6, NAT_1:11;
F1 = H by A4, A6, A10, Th43;
hence L1 . m = H by A7, A8, A9; ::_thesis: for k being Element of NAT st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 )
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < m implies ex G1, H1 being Element of QC-WFF A st
( L1 . j = G1 & L1 . (j + 1) = H1 & G1 is_immediate_constituent_of H1 ) )
assume that
A11: 1 <= j and
A12: j < m ; ::_thesis: ex G1, H1 being Element of QC-WFF A st
( L1 . j = G1 & L1 . (j + 1) = H1 & G1 is_immediate_constituent_of H1 )
m <= m + 1 by NAT_1:11;
then j < n by A6, A12, XXREAL_0:2;
then consider F1, G1 being Element of QC-WFF A such that
A13: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A5, A11;
take F1 ; ::_thesis: ex H1 being Element of QC-WFF A st
( L1 . j = F1 & L1 . (j + 1) = H1 & F1 is_immediate_constituent_of H1 )
take G1 ; ::_thesis: ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
( 1 <= 1 + j & j + 1 <= m ) by A11, A12, NAT_1:13;
hence ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A8, A11, A12, A13; ::_thesis: verum
end;
theorem :: QC_LANG2:67
for A being QC-alphabet
for F, H being Element of QC-WFF A st 'not' F is_subformula_of H holds
F is_proper_subformula_of H
proof
let A be QC-alphabet ; ::_thesis: for F, H being Element of QC-WFF A st 'not' F is_subformula_of H holds
F is_proper_subformula_of H
let F, H be Element of QC-WFF A; ::_thesis: ( 'not' F is_subformula_of H implies F is_proper_subformula_of H )
F is_proper_subformula_of 'not' F by Th66;
hence ( 'not' F is_subformula_of H implies F is_proper_subformula_of H ) by Th63; ::_thesis: verum
end;
theorem :: QC_LANG2:68
for A being QC-alphabet
for F being Element of QC-WFF A holds
( F is_proper_subformula_of FALSUM A iff F is_subformula_of VERUM A ) by Th66;
theorem Th69: :: QC_LANG2:69
for A being QC-alphabet
for F, G, H being Element of QC-WFF A holds
( ( F is_subformula_of G or F is_subformula_of H ) iff F is_proper_subformula_of G '&' H )
proof
let A be QC-alphabet ; ::_thesis: for F, G, H being Element of QC-WFF A holds
( ( F is_subformula_of G or F is_subformula_of H ) iff F is_proper_subformula_of G '&' H )
let F, G, H be Element of QC-WFF A; ::_thesis: ( ( F is_subformula_of G or F is_subformula_of H ) iff F is_proper_subformula_of G '&' H )
( G is_immediate_constituent_of G '&' H & H is_immediate_constituent_of G '&' H ) by Th45;
hence ( ( F is_subformula_of G or F is_subformula_of H ) implies F is_proper_subformula_of G '&' H ) by Th63; ::_thesis: ( not F is_proper_subformula_of G '&' H or F is_subformula_of G or F is_subformula_of H )
given n being Element of NAT , L being FinSequence such that A1: 1 <= n and
A2: len L = n and
A3: L . 1 = F and
A4: L . n = G '&' H and
A5: for k being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being Element of QC-WFF A st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ; :: according to QC_LANG2:def_20,QC_LANG2:def_21 ::_thesis: ( not F <> G '&' H or F is_subformula_of G or F is_subformula_of H )
assume F <> G '&' H ; ::_thesis: ( F is_subformula_of G or F is_subformula_of H )
then 1 < n by A1, A3, A4, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A6: n = 2 + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
(1 + 1) + k = (1 + k) + 1 ;
then 1 + k < n by A6, NAT_1:13;
then consider H1, G1 being Element of QC-WFF A such that
A7: L . (1 + k) = H1 and
A8: ( L . ((1 + k) + 1) = G1 & H1 is_immediate_constituent_of G1 ) by A5, NAT_1:11;
reconsider L1 = L | (Seg (1 + k)) as FinSequence by FINSEQ_1:15;
F is_subformula_of H1
proof
take m = 1 + k; :: according to QC_LANG2:def_20 ::_thesis: ex L being FinSequence st
( 1 <= m & len L = m & L . 1 = F & L . m = H1 & ( for k being Element of NAT st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
take L1 ; ::_thesis: ( 1 <= m & len L1 = m & L1 . 1 = F & L1 . m = H1 & ( for k being Element of NAT st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
thus A9: 1 <= m by NAT_1:11; ::_thesis: ( len L1 = m & L1 . 1 = F & L1 . m = H1 & ( for k being Element of NAT st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
1 + k <= (1 + k) + 1 by NAT_1:11;
hence len L1 = m by A2, A6, FINSEQ_1:17; ::_thesis: ( L1 . 1 = F & L1 . m = H1 & ( for k being Element of NAT st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
A10: now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_m_holds_
L1_._j_=_L_._j
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= m implies L1 . j = L . j )
assume ( 1 <= j & j <= m ) ; ::_thesis: L1 . j = L . j
then j in Seg (1 + k) by FINSEQ_1:1;
hence L1 . j = L . j by FUNCT_1:49; ::_thesis: verum
end;
hence L1 . 1 = F by A3, A9; ::_thesis: ( L1 . m = H1 & ( for k being Element of NAT st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
thus L1 . m = H1 by A7, A9, A10; ::_thesis: for k being Element of NAT st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 )
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < m implies ex G1, H1 being Element of QC-WFF A st
( L1 . j = G1 & L1 . (j + 1) = H1 & G1 is_immediate_constituent_of H1 ) )
assume that
A11: 1 <= j and
A12: j < m ; ::_thesis: ex G1, H1 being Element of QC-WFF A st
( L1 . j = G1 & L1 . (j + 1) = H1 & G1 is_immediate_constituent_of H1 )
m <= m + 1 by NAT_1:11;
then j < n by A6, A12, XXREAL_0:2;
then consider F1, G1 being Element of QC-WFF A such that
A13: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A5, A11;
take F1 ; ::_thesis: ex H1 being Element of QC-WFF A st
( L1 . j = F1 & L1 . (j + 1) = H1 & F1 is_immediate_constituent_of H1 )
take G1 ; ::_thesis: ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
( 1 <= 1 + j & j + 1 <= m ) by A11, A12, NAT_1:13;
hence ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A10, A11, A12, A13; ::_thesis: verum
end;
hence ( F is_subformula_of G or F is_subformula_of H ) by A4, A6, A8, Th45; ::_thesis: verum
end;
theorem :: QC_LANG2:70
for A being QC-alphabet
for F, G, H being Element of QC-WFF A st F '&' G is_subformula_of H holds
( F is_proper_subformula_of H & G is_proper_subformula_of H )
proof
let A be QC-alphabet ; ::_thesis: for F, G, H being Element of QC-WFF A st F '&' G is_subformula_of H holds
( F is_proper_subformula_of H & G is_proper_subformula_of H )
let F, G, H be Element of QC-WFF A; ::_thesis: ( F '&' G is_subformula_of H implies ( F is_proper_subformula_of H & G is_proper_subformula_of H ) )
( F is_proper_subformula_of F '&' G & G is_proper_subformula_of F '&' G ) by Th69;
hence ( F '&' G is_subformula_of H implies ( F is_proper_subformula_of H & G is_proper_subformula_of H ) ) by Th63; ::_thesis: verum
end;
theorem Th71: :: QC_LANG2:71
for A being QC-alphabet
for F, H being Element of QC-WFF A
for x being bound_QC-variable of A holds
( F is_subformula_of H iff F is_proper_subformula_of All (x,H) )
proof
let A be QC-alphabet ; ::_thesis: for F, H being Element of QC-WFF A
for x being bound_QC-variable of A holds
( F is_subformula_of H iff F is_proper_subformula_of All (x,H) )
let F, H be Element of QC-WFF A; ::_thesis: for x being bound_QC-variable of A holds
( F is_subformula_of H iff F is_proper_subformula_of All (x,H) )
let x be bound_QC-variable of A; ::_thesis: ( F is_subformula_of H iff F is_proper_subformula_of All (x,H) )
H is_immediate_constituent_of All (x,H) by Th46;
hence ( F is_subformula_of H implies F is_proper_subformula_of All (x,H) ) by Th63; ::_thesis: ( F is_proper_subformula_of All (x,H) implies F is_subformula_of H )
given n being Element of NAT , L being FinSequence such that A1: 1 <= n and
A2: len L = n and
A3: L . 1 = F and
A4: L . n = All (x,H) and
A5: for k being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being Element of QC-WFF A st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ; :: according to QC_LANG2:def_20,QC_LANG2:def_21 ::_thesis: ( not F <> All (x,H) or F is_subformula_of H )
assume F <> All (x,H) ; ::_thesis: F is_subformula_of H
then 1 < n by A1, A3, A4, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A6: n = 2 + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
reconsider L1 = L | (Seg (1 + k)) as FinSequence by FINSEQ_1:15;
take m = 1 + k; :: according to QC_LANG2:def_20 ::_thesis: ex L being FinSequence st
( 1 <= m & len L = m & L . 1 = F & L . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
take L1 ; ::_thesis: ( 1 <= m & len L1 = m & L1 . 1 = F & L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
thus A7: 1 <= m by NAT_1:11; ::_thesis: ( len L1 = m & L1 . 1 = F & L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
1 + k <= (1 + k) + 1 by NAT_1:11;
hence len L1 = m by A2, A6, FINSEQ_1:17; ::_thesis: ( L1 . 1 = F & L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
A8: now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_m_holds_
L1_._j_=_L_._j
let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= m implies L1 . j = L . j )
assume ( 1 <= j & j <= m ) ; ::_thesis: L1 . j = L . j
then j in Seg (1 + k) by FINSEQ_1:1;
hence L1 . j = L . j by FUNCT_1:49; ::_thesis: verum
end;
hence L1 . 1 = F by A3, A7; ::_thesis: ( L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
m < m + 1 by NAT_1:13;
then consider F1, G1 being Element of QC-WFF A such that
A9: L . m = F1 and
A10: ( L . (m + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A5, A6, NAT_1:11;
F1 = H by A4, A6, A10, Th46;
hence L1 . m = H by A7, A8, A9; ::_thesis: for k being Element of NAT st 1 <= k & k < m holds
ex G1, H1 being Element of QC-WFF A st
( L1 . k = G1 & L1 . (k + 1) = H1 & G1 is_immediate_constituent_of H1 )
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < m implies ex G1, H1 being Element of QC-WFF A st
( L1 . j = G1 & L1 . (j + 1) = H1 & G1 is_immediate_constituent_of H1 ) )
assume that
A11: 1 <= j and
A12: j < m ; ::_thesis: ex G1, H1 being Element of QC-WFF A st
( L1 . j = G1 & L1 . (j + 1) = H1 & G1 is_immediate_constituent_of H1 )
m <= m + 1 by NAT_1:11;
then j < n by A6, A12, XXREAL_0:2;
then consider F1, G1 being Element of QC-WFF A such that
A13: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A5, A11;
take F1 ; ::_thesis: ex H1 being Element of QC-WFF A st
( L1 . j = F1 & L1 . (j + 1) = H1 & F1 is_immediate_constituent_of H1 )
take G1 ; ::_thesis: ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 )
( 1 <= 1 + j & j + 1 <= m ) by A11, A12, NAT_1:13;
hence ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A8, A11, A12, A13; ::_thesis: verum
end;
theorem :: QC_LANG2:72
for A being QC-alphabet
for H, F being Element of QC-WFF A
for x being bound_QC-variable of A st All (x,H) is_subformula_of F holds
H is_proper_subformula_of F
proof
let A be QC-alphabet ; ::_thesis: for H, F being Element of QC-WFF A
for x being bound_QC-variable of A st All (x,H) is_subformula_of F holds
H is_proper_subformula_of F
let H, F be Element of QC-WFF A; ::_thesis: for x being bound_QC-variable of A st All (x,H) is_subformula_of F holds
H is_proper_subformula_of F
let x be bound_QC-variable of A; ::_thesis: ( All (x,H) is_subformula_of F implies H is_proper_subformula_of F )
H is_proper_subformula_of All (x,H) by Th71;
hence ( All (x,H) is_subformula_of F implies H is_proper_subformula_of F ) by Th63; ::_thesis: verum
end;
theorem :: QC_LANG2:73
for A being QC-alphabet
for F, G being Element of QC-WFF A 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
let A be QC-alphabet ; ::_thesis: for F, G being Element of QC-WFF A 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 )
let F, G be Element of QC-WFF A; ::_thesis: ( 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 )
thus A1: F '&' ('not' G) is_proper_subformula_of F => G by Th66; ::_thesis: ( F is_proper_subformula_of F => G & 'not' G is_proper_subformula_of F => G & G is_proper_subformula_of F => G )
( F is_proper_subformula_of F '&' ('not' G) & 'not' G is_proper_subformula_of F '&' ('not' G) ) by Th69;
hence A2: ( F is_proper_subformula_of F => G & 'not' G is_proper_subformula_of F => G ) by A1, Th56; ::_thesis: G is_proper_subformula_of F => G
G is_proper_subformula_of 'not' G by Th66;
hence G is_proper_subformula_of F => G by A2, Th56; ::_thesis: verum
end;
theorem :: QC_LANG2:74
for A being QC-alphabet
for F, G being Element of QC-WFF A 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
let A be QC-alphabet ; ::_thesis: for F, G being Element of QC-WFF A 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 )
let F, G be Element of QC-WFF A; ::_thesis: ( ('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 )
thus A1: ('not' F) '&' ('not' G) is_proper_subformula_of F 'or' G by Th66; ::_thesis: ( '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 )
( 'not' F is_proper_subformula_of ('not' F) '&' ('not' G) & 'not' G is_proper_subformula_of ('not' F) '&' ('not' G) ) by Th69;
hence A2: ( 'not' F is_proper_subformula_of F 'or' G & 'not' G is_proper_subformula_of F 'or' G ) by A1, Th56; ::_thesis: ( F is_proper_subformula_of F 'or' G & G is_proper_subformula_of F 'or' G )
( G is_proper_subformula_of 'not' G & F is_proper_subformula_of 'not' F ) by Th66;
hence ( F is_proper_subformula_of F 'or' G & G is_proper_subformula_of F 'or' G ) by A2, Th56; ::_thesis: verum
end;
theorem :: QC_LANG2:75
for A being QC-alphabet
for H, F being Element of QC-WFF A st H is atomic holds
not F is_proper_subformula_of H
proof
let A be QC-alphabet ; ::_thesis: for H, F being Element of QC-WFF A st H is atomic holds
not F is_proper_subformula_of H
let H, F be Element of QC-WFF A; ::_thesis: ( H is atomic implies not F is_proper_subformula_of H )
assume ex k being Element of NAT ex P being QC-pred_symbol of k,A ex V being QC-variable_list of k,A st H = P ! V ; :: according to QC_LANG1:def_18 ::_thesis: not F is_proper_subformula_of H
hence not F is_proper_subformula_of H by Th65; ::_thesis: verum
end;
theorem :: QC_LANG2:76
for A being QC-alphabet
for H being Element of QC-WFF A st H is negative holds
the_argument_of H is_proper_subformula_of H
proof
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A st H is negative holds
the_argument_of H is_proper_subformula_of H
let H be Element of QC-WFF A; ::_thesis: ( H is negative implies the_argument_of H is_proper_subformula_of H )
assume H is negative ; ::_thesis: the_argument_of H is_proper_subformula_of H
then the_argument_of H is_immediate_constituent_of H by Th48;
hence the_argument_of H is_proper_subformula_of H by Th53; ::_thesis: verum
end;
theorem :: QC_LANG2:77
for A being QC-alphabet
for H being Element of QC-WFF A 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
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A 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 )
let H be Element of QC-WFF A; ::_thesis: ( H is conjunctive implies ( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H ) )
assume H is conjunctive ; ::_thesis: ( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H )
then ( the_left_argument_of H is_immediate_constituent_of H & the_right_argument_of H is_immediate_constituent_of H ) by Th49;
hence ( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H ) by Th53; ::_thesis: verum
end;
theorem :: QC_LANG2:78
for A being QC-alphabet
for H being Element of QC-WFF A st H is universal holds
the_scope_of H is_proper_subformula_of H
proof
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A st H is universal holds
the_scope_of H is_proper_subformula_of H
let H be Element of QC-WFF A; ::_thesis: ( H is universal implies the_scope_of H is_proper_subformula_of H )
assume H is universal ; ::_thesis: the_scope_of H is_proper_subformula_of H
then the_scope_of H is_immediate_constituent_of H by Th50;
hence the_scope_of H is_proper_subformula_of H by Th53; ::_thesis: verum
end;
theorem Th79: :: QC_LANG2:79
for A being QC-alphabet
for H being Element of QC-WFF A holds
( H is_subformula_of VERUM A iff H = VERUM A )
proof
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A holds
( H is_subformula_of VERUM A iff H = VERUM A )
let H be Element of QC-WFF A; ::_thesis: ( H is_subformula_of VERUM A iff H = VERUM A )
thus ( H is_subformula_of VERUM A implies H = VERUM A ) ::_thesis: ( H = VERUM A implies H is_subformula_of VERUM A )
proof
assume A1: H is_subformula_of VERUM A ; ::_thesis: H = VERUM A
assume H <> VERUM A ; ::_thesis: contradiction
then H is_proper_subformula_of VERUM A by A1, Def21;
hence contradiction by Th64; ::_thesis: verum
end;
thus ( H = VERUM A implies H is_subformula_of VERUM A ) ; ::_thesis: verum
end;
theorem Th80: :: QC_LANG2:80
for A being QC-alphabet
for H being Element of QC-WFF A
for k being Element of NAT
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds
( H is_subformula_of P ! V iff H = P ! V )
proof
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A
for k being Element of NAT
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds
( H is_subformula_of P ! V iff H = P ! V )
let H be Element of QC-WFF A; ::_thesis: for k being Element of NAT
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds
( H is_subformula_of P ! V iff H = P ! V )
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds
( H is_subformula_of P ! V iff H = P ! V )
let P be QC-pred_symbol of k,A; ::_thesis: for V being QC-variable_list of k,A holds
( H is_subformula_of P ! V iff H = P ! V )
let V be QC-variable_list of k,A; ::_thesis: ( H is_subformula_of P ! V iff H = P ! V )
thus ( H is_subformula_of P ! V implies H = P ! V ) ::_thesis: ( H = P ! V implies H is_subformula_of P ! V )
proof
assume A1: H is_subformula_of P ! V ; ::_thesis: H = P ! V
assume H <> P ! V ; ::_thesis: contradiction
then H is_proper_subformula_of P ! V by A1, Def21;
then ex F being Element of QC-WFF A st F is_immediate_constituent_of P ! V by Th55;
hence contradiction by Th42; ::_thesis: verum
end;
thus ( H = P ! V implies H is_subformula_of P ! V ) ; ::_thesis: verum
end;
theorem Th81: :: QC_LANG2:81
for A being QC-alphabet
for H being Element of QC-WFF A holds
( H is_subformula_of FALSUM A iff ( H = FALSUM A or H = VERUM A ) )
proof
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A holds
( H is_subformula_of FALSUM A iff ( H = FALSUM A or H = VERUM A ) )
let H be Element of QC-WFF A; ::_thesis: ( H is_subformula_of FALSUM A iff ( H = FALSUM A or H = VERUM A ) )
thus ( not H is_subformula_of FALSUM A or H = FALSUM A or H = VERUM A ) ::_thesis: ( ( H = FALSUM A or H = VERUM A ) implies H is_subformula_of FALSUM A )
proof
assume ( H is_subformula_of FALSUM A & H <> FALSUM A ) ; ::_thesis: H = VERUM A
then H is_proper_subformula_of FALSUM A by Def21;
then H is_subformula_of VERUM A by Th66;
hence H = VERUM A by Th79; ::_thesis: verum
end;
VERUM A is_immediate_constituent_of FALSUM A by Def19;
then VERUM A is_proper_subformula_of FALSUM A by Th53;
hence ( ( H = FALSUM A or H = VERUM A ) implies H is_subformula_of FALSUM A ) by Def21; ::_thesis: verum
end;
definition
let A be QC-alphabet ;
let H be Element of QC-WFF A;
func Subformulae H -> set means :Def22: :: QC_LANG2:def 22
for a being set holds
( a in it iff ex F being Element of QC-WFF A 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 A st
( F = a & F is_subformula_of H ) )
proof
defpred S1[ set ] means ex F being Element of QC-WFF A st
( F = $1 & F is_subformula_of H );
consider X being set such that
A1: for a being set holds
( a in X iff ( a in QC-WFF A & S1[a] ) ) from XBOOLE_0:sch_1();
take X ; ::_thesis: for a being set holds
( a in X iff ex F being Element of QC-WFF A st
( F = a & F is_subformula_of H ) )
let a be set ; ::_thesis: ( a in X iff ex F being Element of QC-WFF A st
( F = a & F is_subformula_of H ) )
thus ( a in X implies ex F being Element of QC-WFF A st
( F = a & F is_subformula_of H ) ) by A1; ::_thesis: ( ex F being Element of QC-WFF A st
( F = a & F is_subformula_of H ) implies a in X )
given F being Element of QC-WFF A such that A2: ( F = a & F is_subformula_of H ) ; ::_thesis: a in X
thus a in X by A1, A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for a being set holds
( a in b1 iff ex F being Element of QC-WFF A st
( F = a & F is_subformula_of H ) ) ) & ( for a being set holds
( a in b2 iff ex F being Element of QC-WFF A st
( F = a & F is_subformula_of H ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means ex F being Element of QC-WFF A st
( F = $1 & F is_subformula_of H );
let X, Y be set ; ::_thesis: ( ( for a being set holds
( a in X iff ex F being Element of QC-WFF A st
( F = a & F is_subformula_of H ) ) ) & ( for a being set holds
( a in Y iff ex F being Element of QC-WFF A st
( F = a & F is_subformula_of H ) ) ) implies X = Y )
assume that
A3: for a being set holds
( a in X iff S1[a] ) and
A4: for a being set holds
( a in Y iff S1[a] ) ; ::_thesis: X = Y
thus X = Y from XBOOLE_0:sch_2(A3, A4); ::_thesis: verum
end;
end;
:: deftheorem Def22 defines Subformulae QC_LANG2:def_22_:_
for A being QC-alphabet
for H being Element of QC-WFF A
for b3 being set holds
( b3 = Subformulae H iff for a being set holds
( a in b3 iff ex F being Element of QC-WFF A st
( F = a & F is_subformula_of H ) ) );
theorem Th82: :: QC_LANG2:82
for A being QC-alphabet
for G, H being Element of QC-WFF A st G in Subformulae H holds
G is_subformula_of H
proof
let A be QC-alphabet ; ::_thesis: for G, H being Element of QC-WFF A st G in Subformulae H holds
G is_subformula_of H
let G, H be Element of QC-WFF A; ::_thesis: ( G in Subformulae H implies G is_subformula_of H )
assume G in Subformulae H ; ::_thesis: G is_subformula_of H
then ex F being Element of QC-WFF A st
( F = G & F is_subformula_of H ) by Def22;
hence G is_subformula_of H ; ::_thesis: verum
end;
theorem Th83: :: QC_LANG2:83
for A being QC-alphabet
for F, H being Element of QC-WFF A st F is_subformula_of H holds
Subformulae F c= Subformulae H
proof
let A be QC-alphabet ; ::_thesis: for F, H being Element of QC-WFF A st F is_subformula_of H holds
Subformulae F c= Subformulae H
let F, H be Element of QC-WFF A; ::_thesis: ( F is_subformula_of H implies Subformulae F c= Subformulae H )
assume A1: F is_subformula_of H ; ::_thesis: Subformulae F c= Subformulae H
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Subformulae F or a in Subformulae H )
assume a in Subformulae F ; ::_thesis: a in Subformulae H
then consider F1 being Element of QC-WFF A such that
A2: F1 = a and
A3: F1 is_subformula_of F by Def22;
F1 is_subformula_of H by A1, A3, Th57;
hence a in Subformulae H by A2, Def22; ::_thesis: verum
end;
theorem :: QC_LANG2:84
for A being QC-alphabet
for G, H being Element of QC-WFF A st G in Subformulae H holds
Subformulae G c= Subformulae H by Th82, Th83;
theorem Th85: :: QC_LANG2:85
for A being QC-alphabet holds Subformulae (VERUM A) = {(VERUM A)}
proof
let A be QC-alphabet ; ::_thesis: Subformulae (VERUM A) = {(VERUM A)}
thus Subformulae (VERUM A) c= {(VERUM A)} :: according to XBOOLE_0:def_10 ::_thesis: {(VERUM A)} c= Subformulae (VERUM A)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Subformulae (VERUM A) or a in {(VERUM A)} )
assume a in Subformulae (VERUM A) ; ::_thesis: a in {(VERUM A)}
then consider F being Element of QC-WFF A such that
A1: F = a and
A2: F is_subformula_of VERUM A by Def22;
F = VERUM A by A2, Th79;
hence a in {(VERUM A)} by A1, TARSKI:def_1; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {(VERUM A)} or a in Subformulae (VERUM A) )
assume a in {(VERUM A)} ; ::_thesis: a in Subformulae (VERUM A)
then a = VERUM A by TARSKI:def_1;
hence a in Subformulae (VERUM A) by Def22; ::_thesis: verum
end;
theorem Th86: :: QC_LANG2:86
for A being QC-alphabet
for k being Element of NAT
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds Subformulae (P ! V) = {(P ! V)}
proof
let A be QC-alphabet ; ::_thesis: for k being Element of NAT
for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds Subformulae (P ! V) = {(P ! V)}
let k be Element of NAT ; ::_thesis: for P being QC-pred_symbol of k,A
for V being QC-variable_list of k,A holds Subformulae (P ! V) = {(P ! V)}
let P be QC-pred_symbol of k,A; ::_thesis: for V being QC-variable_list of k,A holds Subformulae (P ! V) = {(P ! V)}
let V be QC-variable_list of k,A; ::_thesis: Subformulae (P ! V) = {(P ! V)}
thus Subformulae (P ! V) c= {(P ! V)} :: according to XBOOLE_0:def_10 ::_thesis: {(P ! V)} c= Subformulae (P ! V)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Subformulae (P ! V) or a in {(P ! V)} )
assume a in Subformulae (P ! V) ; ::_thesis: a in {(P ! V)}
then consider F being Element of QC-WFF A such that
A1: F = a and
A2: F is_subformula_of P ! V by Def22;
F = P ! V by A2, Th80;
hence a in {(P ! V)} by A1, TARSKI:def_1; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {(P ! V)} or a in Subformulae (P ! V) )
assume a in {(P ! V)} ; ::_thesis: a in Subformulae (P ! V)
then a = P ! V by TARSKI:def_1;
hence a in Subformulae (P ! V) by Def22; ::_thesis: verum
end;
theorem :: QC_LANG2:87
for A being QC-alphabet holds Subformulae (FALSUM A) = {(VERUM A),(FALSUM A)}
proof
let A be QC-alphabet ; ::_thesis: Subformulae (FALSUM A) = {(VERUM A),(FALSUM A)}
thus Subformulae (FALSUM A) c= {(VERUM A),(FALSUM A)} :: according to XBOOLE_0:def_10 ::_thesis: {(VERUM A),(FALSUM A)} c= Subformulae (FALSUM A)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Subformulae (FALSUM A) or a in {(VERUM A),(FALSUM A)} )
assume a in Subformulae (FALSUM A) ; ::_thesis: a in {(VERUM A),(FALSUM A)}
then ex F being Element of QC-WFF A st
( F = a & F is_subformula_of FALSUM A ) by Def22;
then ( a = FALSUM A or a = VERUM A ) by Th81;
hence a in {(VERUM A),(FALSUM A)} by TARSKI:def_2; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {(VERUM A),(FALSUM A)} or a in Subformulae (FALSUM A) )
assume A1: a in {(VERUM A),(FALSUM A)} ; ::_thesis: a in Subformulae (FALSUM A)
then A2: ( a = VERUM A or a = FALSUM A ) by TARSKI:def_2;
reconsider a = a as Element of QC-WFF A by A1, TARSKI:def_2;
a is_subformula_of FALSUM A by A2, Th81;
hence a in Subformulae (FALSUM A) by Def22; ::_thesis: verum
end;
theorem Th88: :: QC_LANG2:88
for A being QC-alphabet
for H being Element of QC-WFF A holds Subformulae ('not' H) = (Subformulae H) \/ {('not' H)}
proof
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A holds Subformulae ('not' H) = (Subformulae H) \/ {('not' H)}
let H be Element of QC-WFF A; ::_thesis: Subformulae ('not' H) = (Subformulae H) \/ {('not' H)}
thus Subformulae ('not' H) c= (Subformulae H) \/ {('not' H)} :: according to XBOOLE_0:def_10 ::_thesis: (Subformulae H) \/ {('not' H)} c= Subformulae ('not' H)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Subformulae ('not' H) or a in (Subformulae H) \/ {('not' H)} )
assume a in Subformulae ('not' H) ; ::_thesis: a in (Subformulae H) \/ {('not' H)}
then consider F being Element of QC-WFF A such that
A1: F = a and
A2: F is_subformula_of 'not' H by Def22;
now__::_thesis:_(_F_<>_'not'_H_implies_a_in_Subformulae_H_)
assume F <> 'not' H ; ::_thesis: a in Subformulae H
then F is_proper_subformula_of 'not' H by A2, Def21;
then F is_subformula_of H by Th66;
hence a in Subformulae H by A1, Def22; ::_thesis: verum
end;
then ( a in Subformulae H or a in {('not' H)} ) by A1, TARSKI:def_1;
hence a in (Subformulae H) \/ {('not' H)} by XBOOLE_0:def_3; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (Subformulae H) \/ {('not' H)} or a in Subformulae ('not' H) )
assume A3: a in (Subformulae H) \/ {('not' H)} ; ::_thesis: a in Subformulae ('not' H)
A4: now__::_thesis:_(_a_in_Subformulae_H_implies_a_in_Subformulae_('not'_H)_)
assume a in Subformulae H ; ::_thesis: a in Subformulae ('not' H)
then consider F being Element of QC-WFF A such that
A5: F = a and
A6: F is_subformula_of H by Def22;
H is_immediate_constituent_of 'not' H by Def19;
then H is_proper_subformula_of 'not' H by Th53;
then H is_subformula_of 'not' H by Def21;
then F is_subformula_of 'not' H by A6, Th57;
hence a in Subformulae ('not' H) by A5, Def22; ::_thesis: verum
end;
now__::_thesis:_(_a_in_{('not'_H)}_implies_a_in_Subformulae_('not'_H)_)
assume a in {('not' H)} ; ::_thesis: a in Subformulae ('not' H)
then a = 'not' H by TARSKI:def_1;
hence a in Subformulae ('not' H) by Def22; ::_thesis: verum
end;
hence a in Subformulae ('not' H) by A3, A4, XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th89: :: QC_LANG2:89
for A being QC-alphabet
for H, F being Element of QC-WFF A holds Subformulae (H '&' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)}
proof
let A be QC-alphabet ; ::_thesis: for H, F being Element of QC-WFF A holds Subformulae (H '&' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)}
let H, F be Element of QC-WFF A; ::_thesis: Subformulae (H '&' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)}
thus Subformulae (H '&' F) c= ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} :: according to XBOOLE_0:def_10 ::_thesis: ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} c= Subformulae (H '&' F)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Subformulae (H '&' F) or a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} )
assume a in Subformulae (H '&' F) ; ::_thesis: a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)}
then consider G being Element of QC-WFF A such that
A1: G = a and
A2: G is_subformula_of H '&' F by Def22;
now__::_thesis:_(_G_<>_H_'&'_F_implies_a_in_(Subformulae_H)_\/_(Subformulae_F)_)
assume G <> H '&' F ; ::_thesis: a in (Subformulae H) \/ (Subformulae F)
then G is_proper_subformula_of H '&' F by A2, Def21;
then ( G is_subformula_of H or G is_subformula_of F ) by Th69;
then ( a in Subformulae H or a in Subformulae F ) by A1, Def22;
hence a in (Subformulae H) \/ (Subformulae F) by XBOOLE_0:def_3; ::_thesis: verum
end;
then ( a in (Subformulae H) \/ (Subformulae F) or a in {(H '&' F)} ) by A1, TARSKI:def_1;
hence a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} by XBOOLE_0:def_3; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} or a in Subformulae (H '&' F) )
assume A3: a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} ; ::_thesis: a in Subformulae (H '&' F)
A4: now__::_thesis:_(_a_in_{(H_'&'_F)}_implies_a_in_Subformulae_(H_'&'_F)_)
assume a in {(H '&' F)} ; ::_thesis: a in Subformulae (H '&' F)
then a = H '&' F by TARSKI:def_1;
hence a in Subformulae (H '&' F) by Def22; ::_thesis: verum
end;
A5: now__::_thesis:_(_a_in_Subformulae_F_implies_a_in_Subformulae_(H_'&'_F)_)
assume a in Subformulae F ; ::_thesis: a in Subformulae (H '&' F)
then consider G being Element of QC-WFF A such that
A6: G = a and
A7: G is_subformula_of F by Def22;
F is_immediate_constituent_of H '&' F by Th45;
then F is_proper_subformula_of H '&' F by Th53;
then F is_subformula_of H '&' F by Def21;
then G is_subformula_of H '&' F by A7, Th57;
hence a in Subformulae (H '&' F) by A6, Def22; ::_thesis: verum
end;
A8: now__::_thesis:_(_a_in_Subformulae_H_implies_a_in_Subformulae_(H_'&'_F)_)
assume a in Subformulae H ; ::_thesis: a in Subformulae (H '&' F)
then consider G being Element of QC-WFF A such that
A9: G = a and
A10: G is_subformula_of H by Def22;
H is_immediate_constituent_of H '&' F by Th45;
then H is_proper_subformula_of H '&' F by Th53;
then H is_subformula_of H '&' F by Def21;
then G is_subformula_of H '&' F by A10, Th57;
hence a in Subformulae (H '&' F) by A9, Def22; ::_thesis: verum
end;
( not a in (Subformulae H) \/ (Subformulae F) or a in Subformulae H or a in Subformulae F ) by XBOOLE_0:def_3;
hence a in Subformulae (H '&' F) by A3, A8, A5, A4, XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th90: :: QC_LANG2:90
for A being QC-alphabet
for H being Element of QC-WFF A
for x being bound_QC-variable of A holds Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}
proof
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A
for x being bound_QC-variable of A holds Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}
let H be Element of QC-WFF A; ::_thesis: for x being bound_QC-variable of A holds Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}
let x be bound_QC-variable of A; ::_thesis: Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}
thus Subformulae (All (x,H)) c= (Subformulae H) \/ {(All (x,H))} :: according to XBOOLE_0:def_10 ::_thesis: (Subformulae H) \/ {(All (x,H))} c= Subformulae (All (x,H))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Subformulae (All (x,H)) or a in (Subformulae H) \/ {(All (x,H))} )
assume a in Subformulae (All (x,H)) ; ::_thesis: a in (Subformulae H) \/ {(All (x,H))}
then consider F being Element of QC-WFF A such that
A1: F = a and
A2: F is_subformula_of All (x,H) by Def22;
now__::_thesis:_(_F_<>_All_(x,H)_implies_a_in_Subformulae_H_)
assume F <> All (x,H) ; ::_thesis: a in Subformulae H
then F is_proper_subformula_of All (x,H) by A2, Def21;
then F is_subformula_of H by Th71;
hence a in Subformulae H by A1, Def22; ::_thesis: verum
end;
then ( a in Subformulae H or a in {(All (x,H))} ) by A1, TARSKI:def_1;
hence a in (Subformulae H) \/ {(All (x,H))} by XBOOLE_0:def_3; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (Subformulae H) \/ {(All (x,H))} or a in Subformulae (All (x,H)) )
assume A3: a in (Subformulae H) \/ {(All (x,H))} ; ::_thesis: a in Subformulae (All (x,H))
A4: now__::_thesis:_(_a_in_Subformulae_H_implies_a_in_Subformulae_(All_(x,H))_)
assume a in Subformulae H ; ::_thesis: a in Subformulae (All (x,H))
then consider F being Element of QC-WFF A such that
A5: F = a and
A6: F is_subformula_of H by Def22;
H is_immediate_constituent_of All (x,H) by Th46;
then H is_proper_subformula_of All (x,H) by Th53;
then H is_subformula_of All (x,H) by Def21;
then F is_subformula_of All (x,H) by A6, Th57;
hence a in Subformulae (All (x,H)) by A5, Def22; ::_thesis: verum
end;
now__::_thesis:_(_a_in_{(All_(x,H))}_implies_a_in_Subformulae_(All_(x,H))_)
assume a in {(All (x,H))} ; ::_thesis: a in Subformulae (All (x,H))
then a = All (x,H) by TARSKI:def_1;
hence a in Subformulae (All (x,H)) by Def22; ::_thesis: verum
end;
hence a in Subformulae (All (x,H)) by A3, A4, XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th91: :: QC_LANG2:91
for A being QC-alphabet
for F, G being Element of QC-WFF A holds Subformulae (F => G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}
proof
let A be QC-alphabet ; ::_thesis: for F, G being Element of QC-WFF A holds Subformulae (F => G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}
let F, G be Element of QC-WFF A; ::_thesis: Subformulae (F => G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}
thus Subformulae (F => G) = (Subformulae (F '&' ('not' G))) \/ {(F => G)} by Th88
.= (((Subformulae F) \/ (Subformulae ('not' G))) \/ {(F '&' ('not' G))}) \/ {(F => G)} by Th89
.= (((Subformulae F) \/ ((Subformulae G) \/ {('not' G)})) \/ {(F '&' ('not' G))}) \/ {(F => G)} by Th88
.= ((((Subformulae F) \/ (Subformulae G)) \/ {('not' G)}) \/ {(F '&' ('not' G))}) \/ {(F => G)} by XBOOLE_1:4
.= (((Subformulae F) \/ (Subformulae G)) \/ {('not' G)}) \/ ({(F '&' ('not' G))} \/ {(F => G)}) by XBOOLE_1:4
.= ((Subformulae F) \/ (Subformulae G)) \/ ({('not' G)} \/ ({(F '&' ('not' G))} \/ {(F => G)})) by XBOOLE_1:4
.= ((Subformulae F) \/ (Subformulae G)) \/ ({('not' G)} \/ {(F '&' ('not' G)),(F => G)}) by ENUMSET1:1
.= ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)} by ENUMSET1:2 ; ::_thesis: verum
end;
theorem :: QC_LANG2:92
for A being QC-alphabet
for F, G being Element of QC-WFF A holds Subformulae (F 'or' G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F),(('not' F) '&' ('not' G)),(F 'or' G)}
proof
let A be QC-alphabet ; ::_thesis: for F, G being Element of QC-WFF A holds Subformulae (F 'or' G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F),(('not' F) '&' ('not' G)),(F 'or' G)}
let F, G be Element of QC-WFF A; ::_thesis: Subformulae (F 'or' G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F),(('not' F) '&' ('not' G)),(F 'or' G)}
thus Subformulae (F 'or' G) = (Subformulae (('not' F) '&' ('not' G))) \/ {(F 'or' G)} by Th88
.= (((Subformulae ('not' F)) \/ (Subformulae ('not' G))) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by Th89
.= (((Subformulae ('not' F)) \/ ((Subformulae G) \/ {('not' G)})) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by Th88
.= ((((Subformulae F) \/ {('not' F)}) \/ ((Subformulae G) \/ {('not' G)})) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by Th88
.= (((Subformulae F) \/ (((Subformulae G) \/ {('not' G)}) \/ {('not' F)})) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by XBOOLE_1:4
.= (((Subformulae F) \/ ((Subformulae G) \/ ({('not' G)} \/ {('not' F)}))) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by XBOOLE_1:4
.= (((Subformulae F) \/ ((Subformulae G) \/ {('not' G),('not' F)})) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by ENUMSET1:1
.= ((((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F)}) \/ {(('not' F) '&' ('not' G))}) \/ {(F 'or' G)} by XBOOLE_1:4
.= (((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F)}) \/ ({(('not' F) '&' ('not' G))} \/ {(F 'or' G)}) by XBOOLE_1:4
.= (((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F)}) \/ {(('not' F) '&' ('not' G)),(F 'or' G)} by ENUMSET1:1
.= ((Subformulae F) \/ (Subformulae G)) \/ ({('not' G),('not' F)} \/ {(('not' F) '&' ('not' G)),(F 'or' G)}) by XBOOLE_1:4
.= ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),('not' F),(('not' F) '&' ('not' G)),(F 'or' G)} by ENUMSET1:5 ; ::_thesis: verum
end;
theorem :: QC_LANG2:93
for A being QC-alphabet
for F, G being Element of QC-WFF A 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
let A be QC-alphabet ; ::_thesis: for F, G being Element of QC-WFF A holds Subformulae (F <=> G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G),('not' F),(G '&' ('not' F)),(G => F),(F <=> G)}
let F, G be Element of QC-WFF A; ::_thesis: Subformulae (F <=> G) = ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G),('not' F),(G '&' ('not' F)),(G => F),(F <=> G)}
thus Subformulae (F <=> G) = ((Subformulae (F => G)) \/ (Subformulae (G => F))) \/ {(F <=> G)} by Th89
.= ((((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}) \/ (Subformulae (G => F))) \/ {(F <=> G)} by Th91
.= ((((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}) \/ (((Subformulae F) \/ (Subformulae G)) \/ {('not' F),(G '&' ('not' F)),(G => F)})) \/ {(F <=> G)} by Th91
.= (((Subformulae F) \/ (Subformulae G)) \/ ((((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G)}) \/ {('not' F),(G '&' ('not' F)),(G => F)})) \/ {(F <=> G)} by XBOOLE_1:4
.= (((Subformulae F) \/ (Subformulae G)) \/ (((Subformulae F) \/ (Subformulae G)) \/ ({('not' G),(F '&' ('not' G)),(F => G)} \/ {('not' F),(G '&' ('not' F)),(G => F)}))) \/ {(F <=> G)} by XBOOLE_1:4
.= ((((Subformulae F) \/ (Subformulae G)) \/ ((Subformulae F) \/ (Subformulae G))) \/ ({('not' G),(F '&' ('not' G)),(F => G)} \/ {('not' F),(G '&' ('not' F)),(G => F)})) \/ {(F <=> G)} by XBOOLE_1:4
.= (((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G),('not' F),(G '&' ('not' F)),(G => F)}) \/ {(F <=> G)} by ENUMSET1:13
.= ((Subformulae F) \/ (Subformulae G)) \/ ({('not' G),(F '&' ('not' G)),(F => G),('not' F),(G '&' ('not' F)),(G => F)} \/ {(F <=> G)}) by XBOOLE_1:4
.= ((Subformulae F) \/ (Subformulae G)) \/ {('not' G),(F '&' ('not' G)),(F => G),('not' F),(G '&' ('not' F)),(G => F),(F <=> G)} by ENUMSET1:21 ; ::_thesis: verum
end;
theorem :: QC_LANG2:94
for A being QC-alphabet
for H being Element of QC-WFF A holds
( ( H = VERUM A or H is atomic ) iff Subformulae H = {H} )
proof
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A holds
( ( H = VERUM A or H is atomic ) iff Subformulae H = {H} )
let H be Element of QC-WFF A; ::_thesis: ( ( H = VERUM A or H is atomic ) iff Subformulae H = {H} )
( H is atomic implies Subformulae H = {H} )
proof
assume ex k being Element of NAT ex P being QC-pred_symbol of k,A ex V being QC-variable_list of k,A st H = P ! V ; :: according to QC_LANG1:def_18 ::_thesis: Subformulae H = {H}
hence Subformulae H = {H} by Th86; ::_thesis: verum
end;
hence ( ( H = VERUM A or H is atomic ) implies Subformulae H = {H} ) by Th85; ::_thesis: ( not Subformulae H = {H} or H = VERUM A or H is atomic )
assume A1: Subformulae H = {H} ; ::_thesis: ( H = VERUM A or H is atomic )
A2: now__::_thesis:_not_H_=_'not'_(the_argument_of_H)
assume H = 'not' (the_argument_of H) ; ::_thesis: contradiction
then A3: the_argument_of H is_immediate_constituent_of H by Th43;
then the_argument_of H is_proper_subformula_of H by Th53;
then the_argument_of H is_subformula_of H by Def21;
then A4: the_argument_of H in Subformulae H by Def22;
len (@ (the_argument_of H)) <> len (@ H) by A3, Th51;
hence contradiction by A1, A4, TARSKI:def_1; ::_thesis: verum
end;
A5: now__::_thesis:_not_H_=_(the_left_argument_of_H)_'&'_(the_right_argument_of_H)
assume H = (the_left_argument_of H) '&' (the_right_argument_of H) ; ::_thesis: contradiction
then A6: the_left_argument_of H is_immediate_constituent_of H by Th45;
then the_left_argument_of H is_proper_subformula_of H by Th53;
then the_left_argument_of H is_subformula_of H by Def21;
then A7: the_left_argument_of H in Subformulae H by Def22;
len (@ (the_left_argument_of H)) <> len (@ H) by A6, Th51;
hence contradiction by A1, A7, TARSKI:def_1; ::_thesis: verum
end;
assume ( H <> VERUM A & not H is atomic ) ; ::_thesis: contradiction
then ( H is negative or H is conjunctive or H is universal ) by QC_LANG1:9;
then ( H = 'not' (the_argument_of H) or H = (the_left_argument_of H) '&' (the_right_argument_of H) or H = All ((bound_in H),(the_scope_of H)) ) by Th3, Th6, QC_LANG1:def_24;
then A8: the_scope_of H is_immediate_constituent_of H by A2, A5, Th46;
then the_scope_of H is_proper_subformula_of H by Th53;
then the_scope_of H is_subformula_of H by Def21;
then A9: the_scope_of H in Subformulae H by Def22;
len (@ (the_scope_of H)) <> len (@ H) by A8, Th51;
hence contradiction by A1, A9, TARSKI:def_1; ::_thesis: verum
end;
theorem :: QC_LANG2:95
for A being QC-alphabet
for H being Element of QC-WFF A st H is negative holds
Subformulae H = (Subformulae (the_argument_of H)) \/ {H}
proof
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A st H is negative holds
Subformulae H = (Subformulae (the_argument_of H)) \/ {H}
let H be Element of QC-WFF A; ::_thesis: ( H is negative implies Subformulae H = (Subformulae (the_argument_of H)) \/ {H} )
assume H is negative ; ::_thesis: Subformulae H = (Subformulae (the_argument_of H)) \/ {H}
then H = 'not' (the_argument_of H) by QC_LANG1:def_24;
hence Subformulae H = (Subformulae (the_argument_of H)) \/ {H} by Th88; ::_thesis: verum
end;
theorem :: QC_LANG2:96
for A being QC-alphabet
for H being Element of QC-WFF A st H is conjunctive holds
Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H}
proof
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A st H is conjunctive holds
Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H}
let H be Element of QC-WFF A; ::_thesis: ( H is conjunctive implies Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} )
assume H is conjunctive ; ::_thesis: Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H}
then H = (the_left_argument_of H) '&' (the_right_argument_of H) by Th3;
hence Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} by Th89; ::_thesis: verum
end;
theorem :: QC_LANG2:97
for A being QC-alphabet
for H being Element of QC-WFF A st H is universal holds
Subformulae H = (Subformulae (the_scope_of H)) \/ {H}
proof
let A be QC-alphabet ; ::_thesis: for H being Element of QC-WFF A st H is universal holds
Subformulae H = (Subformulae (the_scope_of H)) \/ {H}
let H be Element of QC-WFF A; ::_thesis: ( H is universal implies Subformulae H = (Subformulae (the_scope_of H)) \/ {H} )
assume H is universal ; ::_thesis: Subformulae H = (Subformulae (the_scope_of H)) \/ {H}
then H = All ((bound_in H),(the_scope_of H)) by Th6;
hence Subformulae H = (Subformulae (the_scope_of H)) \/ {H} by Th90; ::_thesis: verum
end;
theorem :: QC_LANG2:98
for A being QC-alphabet
for H, G, F being Element of QC-WFF A 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
let A be QC-alphabet ; ::_thesis: for H, G, F being Element of QC-WFF A 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
let H, G, F be Element of QC-WFF A; ::_thesis: ( ( H is_immediate_constituent_of G or H is_proper_subformula_of G or H is_subformula_of G ) & G in Subformulae F implies H in Subformulae F )
assume that
A1: ( H is_immediate_constituent_of G or H is_proper_subformula_of G or H is_subformula_of G ) and
A2: G in Subformulae F ; ::_thesis: H in Subformulae F
( H is_proper_subformula_of G or H is_subformula_of G ) by A1, Th53;
then A3: H is_subformula_of G by Def21;
G is_subformula_of F by A2, Th82;
then H is_subformula_of F by A3, Th57;
hence H in Subformulae F by Def22; ::_thesis: verum
end;