:: 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;