:: QC_LANG4 semantic presentation
begin
theorem Th1: :: QC_LANG4:1
for A being QC-alphabet
for F, G being Element of QC-WFF A st F is_subformula_of G holds
len (@ F) <= len (@ G)
proof
let A be QC-alphabet ; ::_thesis: for F, G being Element of QC-WFF A st F is_subformula_of G holds
len (@ F) <= len (@ G)
let F, G be Element of QC-WFF A; ::_thesis: ( F is_subformula_of G implies len (@ F) <= len (@ G) )
assume A1: F is_subformula_of G ; ::_thesis: len (@ F) <= len (@ G)
percases ( F = G or F <> G ) ;
suppose F = G ; ::_thesis: len (@ F) <= len (@ G)
hence len (@ F) <= len (@ G) ; ::_thesis: verum
end;
suppose F <> G ; ::_thesis: len (@ F) <= len (@ G)
then F is_proper_subformula_of G by A1, QC_LANG2:def_21;
hence len (@ F) <= len (@ G) by QC_LANG2:54; ::_thesis: verum
end;
end;
end;
theorem :: QC_LANG4:2
for A being QC-alphabet
for F, G being Element of QC-WFF A st F is_subformula_of G & len (@ F) = len (@ G) holds
F = G
proof
let A be QC-alphabet ; ::_thesis: for F, G being Element of QC-WFF A st F is_subformula_of G & len (@ F) = len (@ G) holds
F = G
let F, G be Element of QC-WFF A; ::_thesis: ( F is_subformula_of G & len (@ F) = len (@ G) implies F = G )
assume that
A1: F is_subformula_of G and
A2: len (@ F) = len (@ G) ; ::_thesis: F = G
now__::_thesis:_not_F_<>_G
assume F <> G ; ::_thesis: contradiction
then F is_proper_subformula_of G by A1, QC_LANG2:def_21;
hence contradiction by A2, QC_LANG2:54; ::_thesis: verum
end;
hence F = G ; ::_thesis: verum
end;
definition
let A be QC-alphabet ;
let p be Element of QC-WFF A;
func list_of_immediate_constituents p -> FinSequence of QC-WFF A equals :Def1: :: QC_LANG4:def 1
<*> (QC-WFF A) if ( p = VERUM A or p is atomic )
<*(the_argument_of p)*> if p is negative
<*(the_left_argument_of p),(the_right_argument_of p)*> if p is conjunctive
otherwise <*(the_scope_of p)*>;
coherence
( ( ( p = VERUM A or p is atomic ) implies <*> (QC-WFF A) is FinSequence of QC-WFF A ) & ( p is negative implies <*(the_argument_of p)*> is FinSequence of QC-WFF A ) & ( p is conjunctive implies <*(the_left_argument_of p),(the_right_argument_of p)*> is FinSequence of QC-WFF A ) & ( p = VERUM A or p is atomic or p is negative or p is conjunctive or <*(the_scope_of p)*> is FinSequence of QC-WFF A ) ) ;
consistency
for b1 being FinSequence of QC-WFF A holds
( ( ( p = VERUM A or p is atomic ) & p is negative implies ( b1 = <*> (QC-WFF A) iff b1 = <*(the_argument_of p)*> ) ) & ( ( p = VERUM A or p is atomic ) & p is conjunctive implies ( b1 = <*> (QC-WFF A) iff b1 = <*(the_left_argument_of p),(the_right_argument_of p)*> ) ) & ( p is negative & p is conjunctive implies ( b1 = <*(the_argument_of p)*> iff b1 = <*(the_left_argument_of p),(the_right_argument_of p)*> ) ) ) by QC_LANG1:20;
end;
:: deftheorem Def1 defines list_of_immediate_constituents QC_LANG4:def_1_:_
for A being QC-alphabet
for p being Element of QC-WFF A holds
( ( ( p = VERUM A or p is atomic ) implies list_of_immediate_constituents p = <*> (QC-WFF A) ) & ( p is negative implies list_of_immediate_constituents p = <*(the_argument_of p)*> ) & ( p is conjunctive implies list_of_immediate_constituents p = <*(the_left_argument_of p),(the_right_argument_of p)*> ) & ( p = VERUM A or p is atomic or p is negative or p is conjunctive or list_of_immediate_constituents p = <*(the_scope_of p)*> ) );
theorem Th3: :: QC_LANG4:3
for A being QC-alphabet
for k being Element of NAT
for F, G being Element of QC-WFF A st k in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . k holds
G is_immediate_constituent_of F
proof
let A be QC-alphabet ; ::_thesis: for k being Element of NAT
for F, G being Element of QC-WFF A st k in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . k holds
G is_immediate_constituent_of F
let k be Element of NAT ; ::_thesis: for F, G being Element of QC-WFF A st k in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . k holds
G is_immediate_constituent_of F
let F, G be Element of QC-WFF A; ::_thesis: ( k in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . k implies G is_immediate_constituent_of F )
assume that
A1: k in dom (list_of_immediate_constituents F) and
A2: G = (list_of_immediate_constituents F) . k ; ::_thesis: G is_immediate_constituent_of F
A3: list_of_immediate_constituents F <> <*> (QC-WFF A) by A1;
A4: ( F <> VERUM A & not F is atomic ) by Def1, A3;
percases ( F is negative or F is universal or F is conjunctive or F is universal ) by A4, QC_LANG1:9;
supposeA5: F is negative ; ::_thesis: G is_immediate_constituent_of F
then A6: list_of_immediate_constituents F = <*(the_argument_of F)*> by Def1;
then k in Seg 1 by A1, FINSEQ_1:def_8;
then k = 1 by FINSEQ_1:2, TARSKI:def_1;
then G = the_argument_of F by A2, A6, FINSEQ_1:def_8;
hence G is_immediate_constituent_of F by A5, QC_LANG2:48; ::_thesis: verum
end;
supposeA7: F is universal ; ::_thesis: G is_immediate_constituent_of F
then A8: not F is conjunctive by QC_LANG1:20;
( not F is atomic & not F is negative ) by A7, QC_LANG1:20;
then A9: list_of_immediate_constituents F = <*(the_scope_of F)*> by A8, Def1, A4;
then k in Seg 1 by A1, FINSEQ_1:def_8;
then k = 1 by FINSEQ_1:2, TARSKI:def_1;
then G = the_scope_of F by A2, A9, FINSEQ_1:def_8;
hence G is_immediate_constituent_of F by A7, QC_LANG2:50; ::_thesis: verum
end;
supposeA10: F is conjunctive ; ::_thesis: G is_immediate_constituent_of F
A11: <*(the_left_argument_of F),(the_right_argument_of F)*> . 2 = the_right_argument_of F by FINSEQ_1:44;
A12: <*(the_left_argument_of F),(the_right_argument_of F)*> . 1 = the_left_argument_of F by FINSEQ_1:44;
A13: list_of_immediate_constituents F = <*(the_left_argument_of F),(the_right_argument_of F)*> by A10, Def1;
len <*(the_left_argument_of F),(the_right_argument_of F)*> = 2 by FINSEQ_1:44;
then A14: k in {1,2} by A1, A13, FINSEQ_1:2, FINSEQ_1:def_3;
now__::_thesis:_G_is_immediate_constituent_of_F
percases ( k = 1 or k = 2 ) by A14, TARSKI:def_2;
suppose k = 1 ; ::_thesis: G is_immediate_constituent_of F
hence G is_immediate_constituent_of F by A2, A10, A13, A12, QC_LANG2:49; ::_thesis: verum
end;
suppose k = 2 ; ::_thesis: G is_immediate_constituent_of F
hence G is_immediate_constituent_of F by A2, A10, A13, A11, QC_LANG2:49; ::_thesis: verum
end;
end;
end;
hence G is_immediate_constituent_of F ; ::_thesis: verum
end;
supposeA15: F is universal ; ::_thesis: G is_immediate_constituent_of F
then A16: not F is conjunctive by QC_LANG1:20;
( not F is atomic & not F is negative ) by A15, QC_LANG1:20;
then A17: list_of_immediate_constituents F = <*(the_scope_of F)*> by A16, Def1, A4;
then k in Seg 1 by A1, FINSEQ_1:def_8;
then k = 1 by FINSEQ_1:2, TARSKI:def_1;
then G = the_scope_of F by A2, A17, FINSEQ_1:def_8;
hence G is_immediate_constituent_of F by A15, QC_LANG2:50; ::_thesis: verum
end;
end;
end;
theorem Th4: :: QC_LANG4:4
for A being QC-alphabet
for F being Element of QC-WFF A holds rng (list_of_immediate_constituents F) = { G where G is Element of QC-WFF A : G is_immediate_constituent_of F }
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A holds rng (list_of_immediate_constituents F) = { G where G is Element of QC-WFF A : G is_immediate_constituent_of F }
let F be Element of QC-WFF A; ::_thesis: rng (list_of_immediate_constituents F) = { G where G is Element of QC-WFF A : G is_immediate_constituent_of F }
thus rng (list_of_immediate_constituents F) c= { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } :: according to XBOOLE_0:def_10 ::_thesis: { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } c= rng (list_of_immediate_constituents F)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (list_of_immediate_constituents F) or y in { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } )
assume A1: y in rng (list_of_immediate_constituents F) ; ::_thesis: y in { G where G is Element of QC-WFF A : G is_immediate_constituent_of F }
rng (list_of_immediate_constituents F) c= QC-WFF A by FINSEQ_1:def_4;
then reconsider G = y as Element of QC-WFF A by A1;
ex x being set st
( x in dom (list_of_immediate_constituents F) & y = (list_of_immediate_constituents F) . x ) by A1, FUNCT_1:def_3;
then G is_immediate_constituent_of F by Th3;
hence y in { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } ; ::_thesis: verum
end;
thus { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } c= rng (list_of_immediate_constituents F) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } or x in rng (list_of_immediate_constituents F) )
assume x in { G where G is Element of QC-WFF A : G is_immediate_constituent_of F } ; ::_thesis: x in rng (list_of_immediate_constituents F)
then consider G being Element of QC-WFF A such that
A2: x = G and
A3: G is_immediate_constituent_of F ;
ex n being Element of NAT st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n )
proof
A4: F <> VERUM A by A3, QC_LANG2:41;
percases ( F is negative or F is conjunctive or F is universal ) by A3, A4, QC_LANG1:9, QC_LANG2:47;
suppose F is negative ; ::_thesis: ex n being Element of NAT st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n )
then A5: ( list_of_immediate_constituents F = <*(the_argument_of F)*> & G = the_argument_of F ) by A3, Def1, QC_LANG2:48;
consider n being Element of NAT such that
A6: n = 1 ;
( dom <*(the_argument_of F)*> = Seg 1 & <*(the_argument_of F)*> . n = the_argument_of F ) by A6, FINSEQ_1:def_8;
hence ex n being Element of NAT st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) by A6, A5, FINSEQ_1:3; ::_thesis: verum
end;
supposeA7: F is conjunctive ; ::_thesis: ex n being Element of NAT st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n )
A8: <*(the_left_argument_of F),(the_right_argument_of F)*> . 2 = the_right_argument_of F by FINSEQ_1:44;
len <*(the_left_argument_of F),(the_right_argument_of F)*> = 2 by FINSEQ_1:44;
then A9: dom <*(the_left_argument_of F),(the_right_argument_of F)*> = Seg 2 by FINSEQ_1:def_3;
A10: list_of_immediate_constituents F = <*(the_left_argument_of F),(the_right_argument_of F)*> by A7, Def1;
A11: <*(the_left_argument_of F),(the_right_argument_of F)*> . 1 = the_left_argument_of F by FINSEQ_1:44;
now__::_thesis:_ex_n_being_Element_of_NAT_st_
(_n_in_dom_(list_of_immediate_constituents_F)_&_G_=_(list_of_immediate_constituents_F)_._n_)
percases ( G = the_left_argument_of F or G = the_right_argument_of F ) by A3, A7, QC_LANG2:49;
supposeA12: G = the_left_argument_of F ; ::_thesis: ex n being Element of NAT st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n )
1 in {1,2} by TARSKI:def_2;
hence ex n being Element of NAT st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) by A10, A11, A9, A12, FINSEQ_1:2; ::_thesis: verum
end;
suppose G = the_right_argument_of F ; ::_thesis: ex n being Element of NAT st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n )
hence ex n being Element of NAT st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) by A10, A8, A9, FINSEQ_1:3; ::_thesis: verum
end;
end;
end;
hence ex n being Element of NAT st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) ; ::_thesis: verum
end;
supposeA13: F is universal ; ::_thesis: ex n being Element of NAT st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n )
then A14: not F is conjunctive by QC_LANG1:20;
( not F is atomic & not F is negative ) by A13, QC_LANG1:20;
then A15: list_of_immediate_constituents F = <*(the_scope_of F)*> by A14, Def1, A4;
consider n being Element of NAT such that
A16: n = 1 ;
A17: G = the_scope_of F by A3, A13, QC_LANG2:50;
( dom <*(the_scope_of F)*> = Seg 1 & <*(the_scope_of F)*> . n = the_scope_of F ) by A16, FINSEQ_1:def_8;
hence ex n being Element of NAT st
( n in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . n ) by A15, A16, A17, FINSEQ_1:3; ::_thesis: verum
end;
end;
end;
hence x in rng (list_of_immediate_constituents F) by A2, FUNCT_1:def_3; ::_thesis: verum
end;
end;
definition
let A be QC-alphabet ;
let p be Element of QC-WFF A;
func tree_of_subformulae p -> finite DecoratedTree of QC-WFF A means :Def2: :: QC_LANG4:def 2
( it . {} = p & ( for x being Element of dom it holds succ (it,x) = list_of_immediate_constituents (it . x) ) );
existence
ex b1 being finite DecoratedTree of QC-WFF A st
( b1 . {} = p & ( for x being Element of dom b1 holds succ (b1,x) = list_of_immediate_constituents (b1 . x) ) )
proof
deffunc H1( Element of QC-WFF A) -> Element of NAT = len (@ $1);
deffunc H2( Element of QC-WFF A) -> FinSequence of QC-WFF A = list_of_immediate_constituents $1;
consider W being finite-branching DecoratedTree of QC-WFF A such that
A1: ( W . {} = p & ( for x being Element of dom W
for w being Element of QC-WFF A st w = W . x holds
succ (W,x) = H2(w) ) ) from TREES_9:sch_2();
A2: for t, t9 being Element of dom W
for d being Element of QC-WFF A st t9 in succ t & d = W . t9 holds
H1(d) < H1(W . t)
proof
let t, t9 be Element of dom W; ::_thesis: for d being Element of QC-WFF A st t9 in succ t & d = W . t9 holds
H1(d) < H1(W . t)
let d be Element of QC-WFF A; ::_thesis: ( t9 in succ t & d = W . t9 implies H1(d) < H1(W . t) )
assume that
A3: t9 in succ t and
A4: d = W . t9 ; ::_thesis: H1(d) < H1(W . t)
consider n being Element of NAT such that
A5: t9 = t ^ <*n*> and
t ^ <*n*> in dom W by A3;
A6: W . t9 = (succ (W,t)) . (n + 1) by A5, TREES_9:40
.= (list_of_immediate_constituents (W . t)) . (n + 1) by A1 ;
dom (list_of_immediate_constituents (W . t)) = dom (succ (W,t)) by A1
.= dom (t succ) by TREES_9:38 ;
then n + 1 in dom (list_of_immediate_constituents (W . t)) by A5, TREES_9:39;
hence H1(d) < H1(W . t) by A4, A6, Th3, QC_LANG2:51; ::_thesis: verum
end;
W is finite from TREES_9:sch_3(A2);
then reconsider W = W as finite DecoratedTree of QC-WFF A ;
take W ; ::_thesis: ( W . {} = p & ( for x being Element of dom W holds succ (W,x) = list_of_immediate_constituents (W . x) ) )
thus ( W . {} = p & ( for x being Element of dom W holds succ (W,x) = list_of_immediate_constituents (W . x) ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being finite DecoratedTree of QC-WFF A st b1 . {} = p & ( for x being Element of dom b1 holds succ (b1,x) = list_of_immediate_constituents (b1 . x) ) & b2 . {} = p & ( for x being Element of dom b2 holds succ (b2,x) = list_of_immediate_constituents (b2 . x) ) holds
b1 = b2
proof
let t1, t2 be finite DecoratedTree of QC-WFF A; ::_thesis: ( t1 . {} = p & ( for x being Element of dom t1 holds succ (t1,x) = list_of_immediate_constituents (t1 . x) ) & t2 . {} = p & ( for x being Element of dom t2 holds succ (t2,x) = list_of_immediate_constituents (t2 . x) ) implies t1 = t2 )
A7: for t1, t2 being finite DecoratedTree of QC-WFF A st t1 . {} = p & ( for x being Element of dom t1 holds succ (t1,x) = list_of_immediate_constituents (t1 . x) ) & t2 . {} = p & ( for x being Element of dom t2 holds succ (t2,x) = list_of_immediate_constituents (t2 . x) ) holds
t1 c= t2
proof
let t1, t2 be finite DecoratedTree of QC-WFF A; ::_thesis: ( t1 . {} = p & ( for x being Element of dom t1 holds succ (t1,x) = list_of_immediate_constituents (t1 . x) ) & t2 . {} = p & ( for x being Element of dom t2 holds succ (t2,x) = list_of_immediate_constituents (t2 . x) ) implies t1 c= t2 )
assume that
A8: t1 . {} = p and
A9: for x being Element of dom t1 holds succ (t1,x) = list_of_immediate_constituents (t1 . x) and
A10: t2 . {} = p and
A11: for x being Element of dom t2 holds succ (t2,x) = list_of_immediate_constituents (t2 . x) ; ::_thesis: t1 c= t2
defpred S1[ set ] means ( $1 in dom t2 & t1 . $1 = t2 . $1 );
A12: for t being Element of dom t1
for n being Element of NAT st S1[t] & t ^ <*n*> in dom t1 holds
S1[t ^ <*n*>]
proof
let t be Element of dom t1; ::_thesis: for n being Element of NAT st S1[t] & t ^ <*n*> in dom t1 holds
S1[t ^ <*n*>]
let n be Element of NAT ; ::_thesis: ( S1[t] & t ^ <*n*> in dom t1 implies S1[t ^ <*n*>] )
assume that
A13: S1[t] and
A14: t ^ <*n*> in dom t1 ; ::_thesis: S1[t ^ <*n*>]
reconsider t9 = t as Element of dom t2 by A13;
A15: succ (t1,t) = list_of_immediate_constituents (t2 . t9) by A9, A13
.= succ (t2,t9) by A11 ;
t ^ <*n*> in succ t by A14;
then n < card (succ t) by TREES_9:7;
then n < len (t succ) by TREES_9:def_5;
then n < len (succ (t1,t)) by TREES_9:28;
then n < len (t9 succ) by A15, TREES_9:28;
then n < card (succ t9) by TREES_9:def_5;
then A16: t9 ^ <*n*> in succ t9 by TREES_9:7;
hence t ^ <*n*> in dom t2 ; ::_thesis: t1 . (t ^ <*n*>) = t2 . (t ^ <*n*>)
thus t1 . (t ^ <*n*>) = (succ (t2,t9)) . (n + 1) by A14, A15, TREES_9:40
.= t2 . (t ^ <*n*>) by A16, TREES_9:40 ; ::_thesis: verum
end;
A17: S1[ {} ] by A8, A10, TREES_1:22;
A18: for t being Element of dom t1 holds S1[t] from TREES_2:sch_1(A17, A12);
then for t being set st t in dom t1 holds
t in dom t2 ;
then A19: dom t1 c= dom t2 by TARSKI:def_3;
for x being set st x in dom t1 holds
t1 . x = t2 . x by A18;
hence t1 c= t2 by A19, GRFUNC_1:2; ::_thesis: verum
end;
assume ( t1 . {} = p & ( for x being Element of dom t1 holds succ (t1,x) = list_of_immediate_constituents (t1 . x) ) & t2 . {} = p & ( for x being Element of dom t2 holds succ (t2,x) = list_of_immediate_constituents (t2 . x) ) ) ; ::_thesis: t1 = t2
then ( t1 c= t2 & t2 c= t1 ) by A7;
hence t1 = t2 by XBOOLE_0:def_10; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines tree_of_subformulae QC_LANG4:def_2_:_
for A being QC-alphabet
for p being Element of QC-WFF A
for b3 being finite DecoratedTree of QC-WFF A holds
( b3 = tree_of_subformulae p iff ( b3 . {} = p & ( for x being Element of dom b3 holds succ (b3,x) = list_of_immediate_constituents (b3 . x) ) ) );
theorem Th5: :: QC_LANG4:5
for A being QC-alphabet
for F being Element of QC-WFF A holds F in rng (tree_of_subformulae F)
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A holds F in rng (tree_of_subformulae F)
let F be Element of QC-WFF A; ::_thesis: F in rng (tree_of_subformulae F)
( (tree_of_subformulae F) . {} = F & {} in dom (tree_of_subformulae F) ) by Def2, TREES_1:22;
hence F in rng (tree_of_subformulae F) by FUNCT_1:def_3; ::_thesis: verum
end;
theorem Th6: :: QC_LANG4:6
for A being QC-alphabet
for n being Element of NAT
for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) st t ^ <*n*> in dom (tree_of_subformulae F) holds
ex G being Element of QC-WFF A st
( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t )
proof
let A be QC-alphabet ; ::_thesis: for n being Element of NAT
for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) st t ^ <*n*> in dom (tree_of_subformulae F) holds
ex G being Element of QC-WFF A st
( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t )
let n be Element of NAT ; ::_thesis: for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) st t ^ <*n*> in dom (tree_of_subformulae F) holds
ex G being Element of QC-WFF A st
( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t )
let F be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F) st t ^ <*n*> in dom (tree_of_subformulae F) holds
ex G being Element of QC-WFF A st
( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t )
let t be Element of dom (tree_of_subformulae F); ::_thesis: ( t ^ <*n*> in dom (tree_of_subformulae F) implies ex G being Element of QC-WFF A st
( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t ) )
A1: succ t = { (t ^ <*k*>) where k is Element of NAT : t ^ <*k*> in dom (tree_of_subformulae F) } ;
assume t ^ <*n*> in dom (tree_of_subformulae F) ; ::_thesis: ex G being Element of QC-WFF A st
( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t )
then consider t9 being Element of dom (tree_of_subformulae F) such that
A2: t9 = t ^ <*n*> ;
A3: rng (list_of_immediate_constituents ((tree_of_subformulae F) . t)) = { G1 where G1 is Element of QC-WFF A : G1 is_immediate_constituent_of (tree_of_subformulae F) . t } by Th4;
consider G being Element of QC-WFF A such that
A4: G = (tree_of_subformulae F) . t9 ;
t9 in { (t ^ <*k*>) where k is Element of NAT : t ^ <*k*> in dom (tree_of_subformulae F) } by A2;
then G in rng (succ ((tree_of_subformulae F),t)) by A4, A1, TREES_9:41;
then G in rng (list_of_immediate_constituents ((tree_of_subformulae F) . t)) by Def2;
hence ex G being Element of QC-WFF A st
( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t ) by A2, A4, A3; ::_thesis: verum
end;
theorem Th7: :: QC_LANG4:7
for A being QC-alphabet
for H, F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) holds
( H is_immediate_constituent_of (tree_of_subformulae F) . t iff ex n being Element of NAT st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) )
proof
let A be QC-alphabet ; ::_thesis: for H, F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) holds
( H is_immediate_constituent_of (tree_of_subformulae F) . t iff ex n being Element of NAT st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) )
let H, F be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F) holds
( H is_immediate_constituent_of (tree_of_subformulae F) . t iff ex n being Element of NAT st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) )
let t be Element of dom (tree_of_subformulae F); ::_thesis: ( H is_immediate_constituent_of (tree_of_subformulae F) . t iff ex n being Element of NAT st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) )
now__::_thesis:_(_H_is_immediate_constituent_of_(tree_of_subformulae_F)_._t_implies_ex_n_being_Element_of_NAT_st_
(_t_^_<*n*>_in_dom_(tree_of_subformulae_F)_&_H_=_(tree_of_subformulae_F)_._(t_^_<*n*>)_)_)
set G = (tree_of_subformulae F) . t;
assume H is_immediate_constituent_of (tree_of_subformulae F) . t ; ::_thesis: ex n being Element of NAT st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) )
then H in { H1 where H1 is Element of QC-WFF A : H1 is_immediate_constituent_of (tree_of_subformulae F) . t } ;
then A1: H in rng (list_of_immediate_constituents ((tree_of_subformulae F) . t)) by Th4;
succ ((tree_of_subformulae F),t) = list_of_immediate_constituents ((tree_of_subformulae F) . t) by Def2;
then consider t9 being Element of dom (tree_of_subformulae F) such that
A2: H = (tree_of_subformulae F) . t9 and
A3: t9 in succ t by A1, TREES_9:42;
ex n being Element of NAT st
( t9 = t ^ <*n*> & t ^ <*n*> in dom (tree_of_subformulae F) ) by A3;
hence ex n being Element of NAT st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) by A2; ::_thesis: verum
end;
hence ( H is_immediate_constituent_of (tree_of_subformulae F) . t implies ex n being Element of NAT st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) ) ; ::_thesis: ( ex n being Element of NAT st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) implies H is_immediate_constituent_of (tree_of_subformulae F) . t )
given n being Element of NAT such that A4: t ^ <*n*> in dom (tree_of_subformulae F) and
A5: H = (tree_of_subformulae F) . (t ^ <*n*>) ; ::_thesis: H is_immediate_constituent_of (tree_of_subformulae F) . t
ex G being Element of QC-WFF A st
( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t ) by A4, Th6;
hence H is_immediate_constituent_of (tree_of_subformulae F) . t by A5; ::_thesis: verum
end;
theorem Th8: :: QC_LANG4:8
for A being QC-alphabet
for G, F, H being Element of QC-WFF A st G in rng (tree_of_subformulae F) & H is_immediate_constituent_of G holds
H in rng (tree_of_subformulae F)
proof
let A be QC-alphabet ; ::_thesis: for G, F, H being Element of QC-WFF A st G in rng (tree_of_subformulae F) & H is_immediate_constituent_of G holds
H in rng (tree_of_subformulae F)
let G, F, H be Element of QC-WFF A; ::_thesis: ( G in rng (tree_of_subformulae F) & H is_immediate_constituent_of G implies H in rng (tree_of_subformulae F) )
assume that
A1: G in rng (tree_of_subformulae F) and
A2: H is_immediate_constituent_of G ; ::_thesis: H in rng (tree_of_subformulae F)
consider x being set such that
A3: x in dom (tree_of_subformulae F) and
A4: G = (tree_of_subformulae F) . x by A1, FUNCT_1:def_3;
consider t being Element of dom (tree_of_subformulae F) such that
A5: t = x by A3;
ex n being Element of NAT st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) by A2, A4, A5, Th7;
hence H in rng (tree_of_subformulae F) by FUNCT_1:def_3; ::_thesis: verum
end;
theorem Th9: :: QC_LANG4:9
for A being QC-alphabet
for G, F, H being Element of QC-WFF A st G in rng (tree_of_subformulae F) & H is_subformula_of G holds
H in rng (tree_of_subformulae F)
proof
let A be QC-alphabet ; ::_thesis: for G, F, H being Element of QC-WFF A st G in rng (tree_of_subformulae F) & H is_subformula_of G holds
H in rng (tree_of_subformulae F)
let G, F, H be Element of QC-WFF A; ::_thesis: ( G in rng (tree_of_subformulae F) & H is_subformula_of G implies H in rng (tree_of_subformulae F) )
assume that
A1: G in rng (tree_of_subformulae F) and
A2: H is_subformula_of G ; ::_thesis: H in rng (tree_of_subformulae F)
consider n being Element of NAT , L being FinSequence such that
A3: 1 <= n and
A4: len L = n and
A5: L . 1 = H and
A6: L . n = G and
A7: for k being Element of NAT st 1 <= k & k < n holds
ex H1, G1 being Element of QC-WFF A st
( L . k = H1 & L . (k + 1) = G1 & H1 is_immediate_constituent_of G1 ) by A2, QC_LANG2:def_20;
defpred S1[ Nat] means ex H9 being Element of QC-WFF A st
( H9 = L . ($1 + 1) & $1 + 1 in dom L & H9 in rng (tree_of_subformulae F) );
A8: for k being Nat st k <> 0 & S1[k] holds
ex m being Nat st
( m < k & S1[m] )
proof
A9: Seg n = dom L by A4, FINSEQ_1:def_3;
let k be Nat; ::_thesis: ( k <> 0 & S1[k] implies ex m being Nat st
( m < k & S1[m] ) )
assume that
A10: k <> 0 and
A11: S1[k] ; ::_thesis: ex m being Nat st
( m < k & S1[m] )
consider m being Nat such that
A12: m + 1 = k by A10, NAT_1:6;
0 < k by A10, NAT_1:3;
then A13: 0 + 1 <= k by NAT_1:13;
Seg (len L) = dom L by FINSEQ_1:def_3;
then A14: k + 1 <= n by A4, A11, FINSEQ_1:1;
then ( k in NAT & k < n ) by NAT_1:13, ORDINAL1:def_12;
then A15: ex H1, G1 being Element of QC-WFF A st
( L . k = H1 & L . (k + 1) = G1 & H1 is_immediate_constituent_of G1 ) by A7, A13;
k <= n by A14, NAT_1:13;
then A16: k in dom L by A13, A9, FINSEQ_1:1;
m < k by A12, NAT_1:13;
hence ex m being Nat st
( m < k & S1[m] ) by A11, A12, A15, A16, Th8; ::_thesis: verum
end;
A17: ex k being Nat st S1[k]
proof
0 <> n by A3;
then A18: ex k being Nat st k + 1 = n by NAT_1:6;
Seg n = dom L by A4, FINSEQ_1:def_3;
hence ex k being Nat st S1[k] by A1, A6, A18, FINSEQ_1:3; ::_thesis: verum
end;
S1[ 0 ] from NAT_1:sch_7(A17, A8);
hence H in rng (tree_of_subformulae F) by A5; ::_thesis: verum
end;
theorem Th10: :: QC_LANG4:10
for A being QC-alphabet
for G, F being Element of QC-WFF A holds
( G in rng (tree_of_subformulae F) iff G is_subformula_of F )
proof
let A be QC-alphabet ; ::_thesis: for G, F being Element of QC-WFF A holds
( G in rng (tree_of_subformulae F) iff G is_subformula_of F )
let G, F be Element of QC-WFF A; ::_thesis: ( G in rng (tree_of_subformulae F) iff G is_subformula_of F )
now__::_thesis:_(_G_in_rng_(tree_of_subformulae_F)_implies_G_is_subformula_of_F_)
set T = dom (tree_of_subformulae F);
defpred S1[ set ] means ex H being Element of QC-WFF A st
( (tree_of_subformulae F) . $1 = H & H is_subformula_of F );
assume G in rng (tree_of_subformulae F) ; ::_thesis: G is_subformula_of F
then consider t being set such that
A1: t in dom (tree_of_subformulae F) and
A2: (tree_of_subformulae F) . t = G by FUNCT_1:def_3;
reconsider t = t as Element of dom (tree_of_subformulae F) by A1;
A3: for t being Element of dom (tree_of_subformulae F)
for n being Element of NAT st S1[t] & t ^ <*n*> in dom (tree_of_subformulae F) holds
S1[t ^ <*n*>]
proof
let t be Element of dom (tree_of_subformulae F); ::_thesis: for n being Element of NAT st S1[t] & t ^ <*n*> in dom (tree_of_subformulae F) holds
S1[t ^ <*n*>]
let n be Element of NAT ; ::_thesis: ( S1[t] & t ^ <*n*> in dom (tree_of_subformulae F) implies S1[t ^ <*n*>] )
assume that
A4: S1[t] and
A5: t ^ <*n*> in dom (tree_of_subformulae F) ; ::_thesis: S1[t ^ <*n*>]
(tree_of_subformulae F) . (t ^ <*n*>) is Element of QC-WFF A by A5, FUNCT_1:102;
then consider H9 being Element of QC-WFF A such that
A6: (tree_of_subformulae F) . (t ^ <*n*>) = H9 ;
consider H being Element of QC-WFF A such that
A7: (tree_of_subformulae F) . t = H and
A8: H is_subformula_of F by A4;
ex G9 being Element of QC-WFF A st
( G9 = (tree_of_subformulae F) . (t ^ <*n*>) & G9 is_immediate_constituent_of (tree_of_subformulae F) . t ) by A5, Th6;
then H9 is_subformula_of H by A7, A6, QC_LANG2:52;
hence S1[t ^ <*n*>] by A8, A6, QC_LANG2:57; ::_thesis: verum
end;
A9: S1[ {} ]
proof
take F ; ::_thesis: ( (tree_of_subformulae F) . {} = F & F is_subformula_of F )
thus ( (tree_of_subformulae F) . {} = F & F is_subformula_of F ) by Def2; ::_thesis: verum
end;
for t being Element of dom (tree_of_subformulae F) holds S1[t] from TREES_2:sch_1(A9, A3);
then ex H being Element of QC-WFF A st
( (tree_of_subformulae F) . t = H & H is_subformula_of F ) ;
hence G is_subformula_of F by A2; ::_thesis: verum
end;
hence ( G in rng (tree_of_subformulae F) implies G is_subformula_of F ) ; ::_thesis: ( G is_subformula_of F implies G in rng (tree_of_subformulae F) )
assume G is_subformula_of F ; ::_thesis: G in rng (tree_of_subformulae F)
hence G in rng (tree_of_subformulae F) by Th5, Th9; ::_thesis: verum
end;
theorem :: QC_LANG4:11
for A being QC-alphabet
for F being Element of QC-WFF A holds rng (tree_of_subformulae F) = Subformulae F
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A holds rng (tree_of_subformulae F) = Subformulae F
let F be Element of QC-WFF A; ::_thesis: rng (tree_of_subformulae F) = Subformulae F
thus rng (tree_of_subformulae F) c= Subformulae F :: according to XBOOLE_0:def_10 ::_thesis: Subformulae F c= rng (tree_of_subformulae F)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (tree_of_subformulae F) or y in Subformulae F )
assume A1: y in rng (tree_of_subformulae F) ; ::_thesis: y in Subformulae F
then y is Element of QC-WFF A by RELAT_1:167;
then consider G being Element of QC-WFF A such that
A2: G = y ;
G is_subformula_of F by A1, A2, Th10;
hence y in Subformulae F by A2, QC_LANG2:def_22; ::_thesis: verum
end;
thus Subformulae F c= rng (tree_of_subformulae F) ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Subformulae F or y in rng (tree_of_subformulae F) )
assume y in Subformulae F ; ::_thesis: y in rng (tree_of_subformulae F)
then ex G being Element of QC-WFF A st
( G = y & G is_subformula_of F ) by QC_LANG2:def_22;
hence y in rng (tree_of_subformulae F) by Th10; ::_thesis: verum
end;
end;
theorem :: QC_LANG4:12
for A being QC-alphabet
for F being Element of QC-WFF A
for t9, t being Element of dom (tree_of_subformulae F) st t9 in succ t holds
(tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for t9, t being Element of dom (tree_of_subformulae F) st t9 in succ t holds
(tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t
let F be Element of QC-WFF A; ::_thesis: for t9, t being Element of dom (tree_of_subformulae F) st t9 in succ t holds
(tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t
let t9, t be Element of dom (tree_of_subformulae F); ::_thesis: ( t9 in succ t implies (tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t )
assume t9 in succ t ; ::_thesis: (tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t
then ex n being Element of NAT st
( t9 = t ^ <*n*> & t ^ <*n*> in dom (tree_of_subformulae F) ) ;
hence (tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t by Th7; ::_thesis: verum
end;
theorem Th13: :: QC_LANG4:13
for A being QC-alphabet
for F being Element of QC-WFF A
for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_prefix_of t9 holds
(tree_of_subformulae F) . t9 is_subformula_of (tree_of_subformulae F) . t
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_prefix_of t9 holds
(tree_of_subformulae F) . t9 is_subformula_of (tree_of_subformulae F) . t
let F be Element of QC-WFF A; ::_thesis: for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_prefix_of t9 holds
(tree_of_subformulae F) . t9 is_subformula_of (tree_of_subformulae F) . t
let t, t9 be Element of dom (tree_of_subformulae F); ::_thesis: ( t is_a_prefix_of t9 implies (tree_of_subformulae F) . t9 is_subformula_of (tree_of_subformulae F) . t )
assume t is_a_prefix_of t9 ; ::_thesis: (tree_of_subformulae F) . t9 is_subformula_of (tree_of_subformulae F) . t
then consider r being FinSequence such that
A1: t9 = t ^ r by TREES_1:1;
reconsider r = r as FinSequence of NAT by A1, FINSEQ_1:36;
consider n being Element of NAT such that
A2: n = len r ;
defpred S1[ set , set ] means ex G being QC-formula of A ex m, k1 being Nat ex r1 being FinSequence st
( G = $2 & m = $1 & m + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) );
A3: for k being Nat st k in Seg (n + 1) holds
ex x being set st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (n + 1) implies ex x being set st S1[k,x] )
assume k in Seg (n + 1) ; ::_thesis: ex x being set st S1[k,x]
then k <= n + 1 by FINSEQ_1:1;
then consider k1 being Nat such that
A4: k + k1 = n + 1 by NAT_1:10;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def_12;
r | (Seg k1) is FinSequence by FINSEQ_1:15;
then consider r1 being FinSequence such that
A5: r1 = r | (Seg k1) ;
t ^ r1 in dom (tree_of_subformulae F)
proof
ex q being FinSequence st
( q = r | (Seg k1) & q is_a_prefix_of r ) by TREES_9:32;
hence t ^ r1 in dom (tree_of_subformulae F) by A1, A5, FINSEQ_6:13, TREES_1:20; ::_thesis: verum
end;
then reconsider t1 = t ^ r1 as Element of dom (tree_of_subformulae F) ;
consider G being QC-formula of A such that
A6: G = (tree_of_subformulae F) . t1 ;
take G ; ::_thesis: S1[k,G]
take G ; ::_thesis: ex m, k1 being Nat ex r1 being FinSequence st
( G = G & m = k & m + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) )
take k ; ::_thesis: ex k1 being Nat ex r1 being FinSequence st
( G = G & k = k & k + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) )
take k1 ; ::_thesis: ex r1 being FinSequence st
( G = G & k = k & k + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) )
take r1 ; ::_thesis: ( G = G & k = k & k + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) )
thus ( G = G & k = k & k + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) ) by A4, A5, A6; ::_thesis: verum
end;
ex L being FinSequence st
( dom L = Seg (n + 1) & ( for k being Nat st k in Seg (n + 1) holds
S1[k,L . k] ) ) from FINSEQ_1:sch_1(A3);
then consider L being FinSequence such that
A7: dom L = Seg (n + 1) and
A8: for k being Nat st k in Seg (n + 1) holds
ex G being QC-formula of A ex m, k1 being Nat ex r1 being FinSequence st
( G = L . k & m = k & m + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) ) ;
A9: len L = n + 1 by A7, FINSEQ_1:def_3;
A10: for k being Element of NAT st 1 <= k & k <= n + 1 holds
ex G being QC-formula of A ex k1 being Nat ex r1 being FinSequence st
( G = L . k & k + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) )
proof
let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= n + 1 implies ex G being QC-formula of A ex k1 being Nat ex r1 being FinSequence st
( G = L . k & k + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) ) )
assume ( 1 <= k & k <= n + 1 ) ; ::_thesis: ex G being QC-formula of A ex k1 being Nat ex r1 being FinSequence st
( G = L . k & k + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) )
then k in Seg (n + 1) by FINSEQ_1:1;
then ex G being QC-formula of A ex m, k1 being Nat ex r1 being FinSequence st
( G = L . k & m = k & m + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) ) by A8;
hence ex G being QC-formula of A ex k1 being Nat ex r1 being FinSequence st
( G = L . k & k + k1 = n + 1 & r1 = r | (Seg k1) & G = (tree_of_subformulae F) . (t ^ r1) ) ; ::_thesis: verum
end;
A11: for k being Element of NAT st 1 <= k & k < n + 1 holds
ex H1, G1 being Element of QC-WFF A st
( L . k = H1 & L . (k + 1) = G1 & H1 is_immediate_constituent_of G1 )
proof
let k be Element of NAT ; ::_thesis: ( 1 <= k & k < n + 1 implies ex H1, G1 being Element of QC-WFF A st
( L . k = H1 & L . (k + 1) = G1 & H1 is_immediate_constituent_of G1 ) )
assume that
A12: 1 <= k and
A13: k < n + 1 ; ::_thesis: ex H1, G1 being Element of QC-WFF A st
( L . k = H1 & L . (k + 1) = G1 & H1 is_immediate_constituent_of G1 )
consider H1 being QC-formula of A, k1 being Nat, r1 being FinSequence such that
A14: H1 = L . k and
A15: k + k1 = n + 1 and
A16: r1 = r | (Seg k1) and
A17: H1 = (tree_of_subformulae F) . (t ^ r1) by A10, A12, A13;
( 1 <= k + 1 & k + 1 <= n + 1 ) by A12, A13, NAT_1:13;
then consider G1 being QC-formula of A, k2 being Nat, r2 being FinSequence such that
A18: G1 = L . (k + 1) and
A19: (k + 1) + k2 = n + 1 and
A20: r2 = r | (Seg k2) and
A21: G1 = (tree_of_subformulae F) . (t ^ r2) by A10;
reconsider k1 = k1, k2 = k2 as Element of NAT by ORDINAL1:def_12;
k1 + 1 <= n + 1 by A12, A15, XREAL_1:6;
then k2 + 1 <= len r by A2, A15, A19, XREAL_1:6;
then consider m being Element of NAT such that
A22: r1 = r2 ^ <*m*> by A15, A16, A19, A20, TREES_9:33;
t ^ r2 in dom (tree_of_subformulae F)
proof
ex q being FinSequence st
( q = r | (Seg k2) & q is_a_prefix_of r ) by TREES_9:32;
hence t ^ r2 in dom (tree_of_subformulae F) by A1, A20, FINSEQ_6:13, TREES_1:20; ::_thesis: verum
end;
then reconsider t2 = t ^ r2 as Element of dom (tree_of_subformulae F) ;
A23: t2 ^ <*m*> = t ^ r1 by A22, FINSEQ_1:32;
t2 ^ <*m*> in dom (tree_of_subformulae F)
proof
ex q being FinSequence st
( q = r | (Seg k1) & q is_a_prefix_of r ) by TREES_9:32;
hence t2 ^ <*m*> in dom (tree_of_subformulae F) by A1, A16, A23, FINSEQ_6:13, TREES_1:20; ::_thesis: verum
end;
then H1 is_immediate_constituent_of G1 by A17, A21, A23, Th7;
hence ex H1, G1 being Element of QC-WFF A st
( L . k = H1 & L . (k + 1) = G1 & H1 is_immediate_constituent_of G1 ) by A14, A18; ::_thesis: verum
end;
0 < n + 1 by NAT_1:3;
then A24: 0 + 1 <= n + 1 by NAT_1:13;
then consider G being QC-formula of A, k1 being Nat, r1 being FinSequence such that
A25: G = L . 1 and
A26: 1 + k1 = n + 1 and
A27: r1 = r | (Seg k1) and
A28: G = (tree_of_subformulae F) . (t ^ r1) by A10;
A29: L . (n + 1) = (tree_of_subformulae F) . t
proof
consider G being QC-formula of A, k1 being Nat, r1 being FinSequence such that
A30: G = L . (n + 1) and
A31: ( (n + 1) + k1 = n + 1 & r1 = r | (Seg k1) ) and
A32: G = (tree_of_subformulae F) . (t ^ r1) by A24, A10;
r1 = {} by A31;
hence L . (n + 1) = (tree_of_subformulae F) . t by A30, A32, FINSEQ_1:34; ::_thesis: verum
end;
dom r = Seg k1 by A2, A26, FINSEQ_1:def_3;
then t9 = t ^ r1 by A1, A27, RELAT_1:69;
hence (tree_of_subformulae F) . t9 is_subformula_of (tree_of_subformulae F) . t by A24, A9, A25, A28, A29, A11, QC_LANG2:def_20; ::_thesis: verum
end;
theorem Th14: :: QC_LANG4:14
for A being QC-alphabet
for F being Element of QC-WFF A
for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t9 holds
len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t))
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t9 holds
len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t))
let F be Element of QC-WFF A; ::_thesis: for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t9 holds
len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t))
let t, t9 be Element of dom (tree_of_subformulae F); ::_thesis: ( t is_a_proper_prefix_of t9 implies len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t)) )
set G = (tree_of_subformulae F) . t;
set H = (tree_of_subformulae F) . t9;
assume A1: t is_a_proper_prefix_of t9 ; ::_thesis: len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t))
then A2: t is_a_prefix_of t9 by XBOOLE_0:def_8;
A3: now__::_thesis:_not_len_(@_((tree_of_subformulae_F)_._t9))_=_len_(@_((tree_of_subformulae_F)_._t))
consider r being FinSequence such that
A4: t9 = t ^ r by A2, TREES_1:1;
reconsider r = r as FinSequence of NAT by A4, FINSEQ_1:36;
A5: 1 <= len r
proof
reconsider t1 = {} as Element of dom (tree_of_subformulae F) by TREES_1:22;
( r <> {} & t1 is_a_prefix_of r ) by A1, A4, FINSEQ_1:34, XBOOLE_1:2;
then A6: t1 is_a_proper_prefix_of r by XBOOLE_0:def_8;
len t1 = 0 ;
then 0 < len r by A6, TREES_1:6;
then 0 + 1 <= len r by NAT_1:13;
hence 1 <= len r ; ::_thesis: verum
end;
defpred S1[ set , set ] means ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence ex m being Nat st
( m = $1 & r1 = r | (Seg m) & t1 = t ^ r1 & $2 = (tree_of_subformulae F) . t1 );
A7: for k being Nat st k in Seg (len r) holds
ex x being set st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg (len r) implies ex x being set st S1[k,x] )
assume A8: k in Seg (len r) ; ::_thesis: ex x being set st S1[k,x]
r | (Seg k) is FinSequence by FINSEQ_1:15;
then consider r1 being FinSequence such that
A9: r1 = r | (Seg k) ;
r1 is_a_prefix_of r by A8, A9, TREES_1:def_1;
then t ^ r1 in dom (tree_of_subformulae F) by A4, FINSEQ_6:13, TREES_1:20;
then consider t1 being Element of dom (tree_of_subformulae F) such that
A10: t1 = t ^ r1 ;
ex x being set st x = (tree_of_subformulae F) . t1 ;
hence ex x being set st S1[k,x] by A9, A10; ::_thesis: verum
end;
ex L being FinSequence st
( dom L = Seg (len r) & ( for k being Nat st k in Seg (len r) holds
S1[k,L . k] ) ) from FINSEQ_1:sch_1(A7);
then consider L being FinSequence such that
dom L = Seg (len r) and
A11: for k being Nat st k in Seg (len r) holds
ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence ex m being Nat st
( m = k & r1 = r | (Seg m) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 ) ;
for k being Element of NAT st 1 <= k & k <= len r holds
ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence st
( r1 = r | (Seg k) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 )
proof
let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= len r implies ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence st
( r1 = r | (Seg k) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 ) )
assume ( 1 <= k & k <= len r ) ; ::_thesis: ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence st
( r1 = r | (Seg k) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 )
then k in Seg (len r) by FINSEQ_1:1;
then ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence ex m being Nat st
( m = k & r1 = r | (Seg m) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 ) by A11;
hence ex t1 being Element of dom (tree_of_subformulae F) ex r1 being FinSequence st
( r1 = r | (Seg k) & t1 = t ^ r1 & L . k = (tree_of_subformulae F) . t1 ) ; ::_thesis: verum
end;
then consider t1 being Element of dom (tree_of_subformulae F), r1 being FinSequence such that
A12: r1 = r | (Seg 1) and
A13: t1 = t ^ r1 and
L . 1 = (tree_of_subformulae F) . t1 by A5;
set H1 = (tree_of_subformulae F) . t1;
A14: (tree_of_subformulae F) . t1 is_immediate_constituent_of (tree_of_subformulae F) . t
proof
ex m being Element of NAT st r1 = <*m*> by A5, A12, TREES_9:34;
hence (tree_of_subformulae F) . t1 is_immediate_constituent_of (tree_of_subformulae F) . t by A13, Th7; ::_thesis: verum
end;
r1 is_a_prefix_of r by A12, TREES_1:def_1;
then t1 is_a_prefix_of t9 by A4, A13, FINSEQ_6:13;
then A15: len (@ ((tree_of_subformulae F) . t9)) <= len (@ ((tree_of_subformulae F) . t1)) by Th1, Th13;
assume len (@ ((tree_of_subformulae F) . t9)) = len (@ ((tree_of_subformulae F) . t)) ; ::_thesis: contradiction
hence contradiction by A15, A14, QC_LANG2:51; ::_thesis: verum
end;
len (@ ((tree_of_subformulae F) . t9)) <= len (@ ((tree_of_subformulae F) . t)) by A2, Th1, Th13;
hence len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t)) by A3, XXREAL_0:1; ::_thesis: verum
end;
theorem Th15: :: QC_LANG4:15
for A being QC-alphabet
for F being Element of QC-WFF A
for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t9 holds
(tree_of_subformulae F) . t9 <> (tree_of_subformulae F) . t
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t9 holds
(tree_of_subformulae F) . t9 <> (tree_of_subformulae F) . t
let F be Element of QC-WFF A; ::_thesis: for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t9 holds
(tree_of_subformulae F) . t9 <> (tree_of_subformulae F) . t
let t, t9 be Element of dom (tree_of_subformulae F); ::_thesis: ( t is_a_proper_prefix_of t9 implies (tree_of_subformulae F) . t9 <> (tree_of_subformulae F) . t )
set G = (tree_of_subformulae F) . t;
set H = (tree_of_subformulae F) . t9;
assume t is_a_proper_prefix_of t9 ; ::_thesis: (tree_of_subformulae F) . t9 <> (tree_of_subformulae F) . t
then len (@ ((tree_of_subformulae F) . t9)) < len (@ ((tree_of_subformulae F) . t)) by Th14;
hence (tree_of_subformulae F) . t9 <> (tree_of_subformulae F) . t ; ::_thesis: verum
end;
theorem Th16: :: QC_LANG4:16
for A being QC-alphabet
for F being Element of QC-WFF A
for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t9 holds
(tree_of_subformulae F) . t9 is_proper_subformula_of (tree_of_subformulae F) . t
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t9 holds
(tree_of_subformulae F) . t9 is_proper_subformula_of (tree_of_subformulae F) . t
let F be Element of QC-WFF A; ::_thesis: for t, t9 being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t9 holds
(tree_of_subformulae F) . t9 is_proper_subformula_of (tree_of_subformulae F) . t
let t, t9 be Element of dom (tree_of_subformulae F); ::_thesis: ( t is_a_proper_prefix_of t9 implies (tree_of_subformulae F) . t9 is_proper_subformula_of (tree_of_subformulae F) . t )
set G = (tree_of_subformulae F) . t;
set H = (tree_of_subformulae F) . t9;
assume A1: t is_a_proper_prefix_of t9 ; ::_thesis: (tree_of_subformulae F) . t9 is_proper_subformula_of (tree_of_subformulae F) . t
then t is_a_prefix_of t9 by XBOOLE_0:def_8;
then A2: (tree_of_subformulae F) . t9 is_subformula_of (tree_of_subformulae F) . t by Th13;
(tree_of_subformulae F) . t9 <> (tree_of_subformulae F) . t by A1, Th15;
hence (tree_of_subformulae F) . t9 is_proper_subformula_of (tree_of_subformulae F) . t by A2, QC_LANG2:def_21; ::_thesis: verum
end;
theorem :: QC_LANG4:17
for A being QC-alphabet
for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) holds
( (tree_of_subformulae F) . t = F iff t = {} )
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) holds
( (tree_of_subformulae F) . t = F iff t = {} )
let F be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F) holds
( (tree_of_subformulae F) . t = F iff t = {} )
let t be Element of dom (tree_of_subformulae F); ::_thesis: ( (tree_of_subformulae F) . t = F iff t = {} )
now__::_thesis:_(_(tree_of_subformulae_F)_._t_=_F_implies_not_t_<>_{}_)
reconsider t1 = {} as Element of dom (tree_of_subformulae F) by TREES_1:22;
assume A1: (tree_of_subformulae F) . t = F ; ::_thesis: not t <> {}
A2: t1 is_a_prefix_of t by XBOOLE_1:2;
assume t <> {} ; ::_thesis: contradiction
then t1 is_a_proper_prefix_of t by A2, XBOOLE_0:def_8;
then (tree_of_subformulae F) . t is_proper_subformula_of (tree_of_subformulae F) . t1 by Th16;
hence contradiction by A1, Def2; ::_thesis: verum
end;
hence ( (tree_of_subformulae F) . t = F implies t = {} ) ; ::_thesis: ( t = {} implies (tree_of_subformulae F) . t = F )
assume t = {} ; ::_thesis: (tree_of_subformulae F) . t = F
hence (tree_of_subformulae F) . t = F by Def2; ::_thesis: verum
end;
theorem Th18: :: QC_LANG4:18
for A being QC-alphabet
for F being Element of QC-WFF A
for t, t9 being Element of dom (tree_of_subformulae F) st t <> t9 & (tree_of_subformulae F) . t = (tree_of_subformulae F) . t9 holds
not t,t9 are_c=-comparable
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for t, t9 being Element of dom (tree_of_subformulae F) st t <> t9 & (tree_of_subformulae F) . t = (tree_of_subformulae F) . t9 holds
not t,t9 are_c=-comparable
let F be Element of QC-WFF A; ::_thesis: for t, t9 being Element of dom (tree_of_subformulae F) st t <> t9 & (tree_of_subformulae F) . t = (tree_of_subformulae F) . t9 holds
not t,t9 are_c=-comparable
let t, t9 be Element of dom (tree_of_subformulae F); ::_thesis: ( t <> t9 & (tree_of_subformulae F) . t = (tree_of_subformulae F) . t9 implies not t,t9 are_c=-comparable )
assume that
A1: t <> t9 and
A2: (tree_of_subformulae F) . t = (tree_of_subformulae F) . t9 ; ::_thesis: not t,t9 are_c=-comparable
assume A3: t,t9 are_c=-comparable ; ::_thesis: contradiction
percases ( t is_a_prefix_of t9 or t9 is_a_prefix_of t ) by A3, XBOOLE_0:def_9;
suppose t is_a_prefix_of t9 ; ::_thesis: contradiction
then t is_a_proper_prefix_of t9 by A1, XBOOLE_0:def_8;
hence contradiction by A2, Th16; ::_thesis: verum
end;
suppose t9 is_a_prefix_of t ; ::_thesis: contradiction
then t9 is_a_proper_prefix_of t by A1, XBOOLE_0:def_8;
hence contradiction by A2, Th16; ::_thesis: verum
end;
end;
end;
definition
let A be QC-alphabet ;
let F, G be Element of QC-WFF A;
funcF -entry_points_in_subformula_tree_of G -> AntiChain_of_Prefixes of dom (tree_of_subformulae F) means :Def3: :: QC_LANG4:def 3
for t being Element of dom (tree_of_subformulae F) holds
( t in it iff (tree_of_subformulae F) . t = G );
existence
ex b1 being AntiChain_of_Prefixes of dom (tree_of_subformulae F) st
for t being Element of dom (tree_of_subformulae F) holds
( t in b1 iff (tree_of_subformulae F) . t = G )
proof
consider X being set such that
A1: X = { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } ;
A2: X is AntiChain_of_Prefixes of dom (tree_of_subformulae F)
proof
A3: for p1, p2 being FinSequence st p1 in X & p2 in X & p1 <> p2 holds
not p1,p2 are_c=-comparable
proof
let p1, p2 be FinSequence; ::_thesis: ( p1 in X & p2 in X & p1 <> p2 implies not p1,p2 are_c=-comparable )
assume that
A4: ( p1 in X & p2 in X ) and
A5: p1 <> p2 ; ::_thesis: not p1,p2 are_c=-comparable
( ex t1 being Element of dom (tree_of_subformulae F) st
( t1 = p1 & (tree_of_subformulae F) . t1 = G ) & ex t2 being Element of dom (tree_of_subformulae F) st
( t2 = p2 & (tree_of_subformulae F) . t2 = G ) ) by A1, A4;
hence not p1,p2 are_c=-comparable by A5, Th18; ::_thesis: verum
end;
for x being set st x in X holds
x is FinSequence
proof
let x be set ; ::_thesis: ( x in X implies x is FinSequence )
assume x in X ; ::_thesis: x is FinSequence
then ex t being Element of dom (tree_of_subformulae F) st
( t = x & (tree_of_subformulae F) . t = G ) by A1;
hence x is FinSequence ; ::_thesis: verum
end;
then reconsider X = X as AntiChain_of_Prefixes by A3, TREES_1:def_10;
X c= dom (tree_of_subformulae F)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in dom (tree_of_subformulae F) )
assume x in X ; ::_thesis: x in dom (tree_of_subformulae F)
then ex t being Element of dom (tree_of_subformulae F) st
( t = x & (tree_of_subformulae F) . t = G ) by A1;
hence x in dom (tree_of_subformulae F) ; ::_thesis: verum
end;
hence X is AntiChain_of_Prefixes of dom (tree_of_subformulae F) by TREES_1:def_11; ::_thesis: verum
end;
for t being Element of dom (tree_of_subformulae F) holds
( t in X iff (tree_of_subformulae F) . t = G )
proof
let t be Element of dom (tree_of_subformulae F); ::_thesis: ( t in X iff (tree_of_subformulae F) . t = G )
thus ( t in X iff (tree_of_subformulae F) . t = G ) ::_thesis: verum
proof
now__::_thesis:_(_t_in_X_implies_(tree_of_subformulae_F)_._t_=_G_)
assume t in X ; ::_thesis: (tree_of_subformulae F) . t = G
then ex t9 being Element of dom (tree_of_subformulae F) st
( t9 = t & (tree_of_subformulae F) . t9 = G ) by A1;
hence (tree_of_subformulae F) . t = G ; ::_thesis: verum
end;
hence ( t in X implies (tree_of_subformulae F) . t = G ) ; ::_thesis: ( (tree_of_subformulae F) . t = G implies t in X )
assume (tree_of_subformulae F) . t = G ; ::_thesis: t in X
hence t in X by A1; ::_thesis: verum
end;
end;
hence ex b1 being AntiChain_of_Prefixes of dom (tree_of_subformulae F) st
for t being Element of dom (tree_of_subformulae F) holds
( t in b1 iff (tree_of_subformulae F) . t = G ) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being AntiChain_of_Prefixes of dom (tree_of_subformulae F) st ( for t being Element of dom (tree_of_subformulae F) holds
( t in b1 iff (tree_of_subformulae F) . t = G ) ) & ( for t being Element of dom (tree_of_subformulae F) holds
( t in b2 iff (tree_of_subformulae F) . t = G ) ) holds
b1 = b2
proof
let P1, P2 be AntiChain_of_Prefixes of dom (tree_of_subformulae F); ::_thesis: ( ( for t being Element of dom (tree_of_subformulae F) holds
( t in P1 iff (tree_of_subformulae F) . t = G ) ) & ( for t being Element of dom (tree_of_subformulae F) holds
( t in P2 iff (tree_of_subformulae F) . t = G ) ) implies P1 = P2 )
assume A6: for t being Element of dom (tree_of_subformulae F) holds
( t in P1 iff (tree_of_subformulae F) . t = G ) ; ::_thesis: ( ex t being Element of dom (tree_of_subformulae F) st
( ( t in P2 implies (tree_of_subformulae F) . t = G ) implies ( (tree_of_subformulae F) . t = G & not t in P2 ) ) or P1 = P2 )
assume A7: for t being Element of dom (tree_of_subformulae F) holds
( t in P2 iff (tree_of_subformulae F) . t = G ) ; ::_thesis: P1 = P2
thus P1 c= P2 :: according to XBOOLE_0:def_10 ::_thesis: P2 c= P1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P1 or x in P2 )
assume A8: x in P1 ; ::_thesis: x in P2
P1 c= dom (tree_of_subformulae F) by TREES_1:def_11;
then reconsider t = x as Element of dom (tree_of_subformulae F) by A8;
(tree_of_subformulae F) . t = G by A6, A8;
hence x in P2 by A7; ::_thesis: verum
end;
thus P2 c= P1 ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P2 or x in P1 )
assume A9: x in P2 ; ::_thesis: x in P1
P2 c= dom (tree_of_subformulae F) by TREES_1:def_11;
then reconsider t = x as Element of dom (tree_of_subformulae F) by A9;
(tree_of_subformulae F) . t = G by A7, A9;
hence x in P1 by A6; ::_thesis: verum
end;
end;
end;
:: deftheorem Def3 defines -entry_points_in_subformula_tree_of QC_LANG4:def_3_:_
for A being QC-alphabet
for F, G being Element of QC-WFF A
for b4 being AntiChain_of_Prefixes of dom (tree_of_subformulae F) holds
( b4 = F -entry_points_in_subformula_tree_of G iff for t being Element of dom (tree_of_subformulae F) holds
( t in b4 iff (tree_of_subformulae F) . t = G ) );
theorem Th19: :: QC_LANG4:19
for A being QC-alphabet
for F, G being Element of QC-WFF A holds F -entry_points_in_subformula_tree_of G = { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G }
proof
let A be QC-alphabet ; ::_thesis: for F, G being Element of QC-WFF A holds F -entry_points_in_subformula_tree_of G = { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G }
let F, G be Element of QC-WFF A; ::_thesis: F -entry_points_in_subformula_tree_of G = { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G }
thus F -entry_points_in_subformula_tree_of G c= { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } :: according to XBOOLE_0:def_10 ::_thesis: { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } c= F -entry_points_in_subformula_tree_of G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F -entry_points_in_subformula_tree_of G or x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } )
assume A1: x in F -entry_points_in_subformula_tree_of G ; ::_thesis: x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G }
F -entry_points_in_subformula_tree_of G c= dom (tree_of_subformulae F) by TREES_1:def_11;
then reconsider t9 = x as Element of dom (tree_of_subformulae F) by A1;
(tree_of_subformulae F) . t9 = G by A1, Def3;
hence x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } ; ::_thesis: verum
end;
thus { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } c= F -entry_points_in_subformula_tree_of G ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } or x in F -entry_points_in_subformula_tree_of G )
assume x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } ; ::_thesis: x in F -entry_points_in_subformula_tree_of G
then ex t9 being Element of dom (tree_of_subformulae F) st
( t9 = x & (tree_of_subformulae F) . t9 = G ) ;
hence x in F -entry_points_in_subformula_tree_of G by Def3; ::_thesis: verum
end;
end;
theorem Th20: :: QC_LANG4:20
for A being QC-alphabet
for G, F being Element of QC-WFF A holds
( G is_subformula_of F iff F -entry_points_in_subformula_tree_of G <> {} )
proof
let A be QC-alphabet ; ::_thesis: for G, F being Element of QC-WFF A holds
( G is_subformula_of F iff F -entry_points_in_subformula_tree_of G <> {} )
let G, F be Element of QC-WFF A; ::_thesis: ( G is_subformula_of F iff F -entry_points_in_subformula_tree_of G <> {} )
now__::_thesis:_(_G_is_subformula_of_F_implies_F_-entry_points_in_subformula_tree_of_G_<>_{}_)
assume G is_subformula_of F ; ::_thesis: F -entry_points_in_subformula_tree_of G <> {}
then G in rng (tree_of_subformulae F) by Th10;
then ex x being set st
( x in dom (tree_of_subformulae F) & G = (tree_of_subformulae F) . x ) by FUNCT_1:def_3;
hence F -entry_points_in_subformula_tree_of G <> {} by Def3; ::_thesis: verum
end;
hence ( G is_subformula_of F implies F -entry_points_in_subformula_tree_of G <> {} ) ; ::_thesis: ( F -entry_points_in_subformula_tree_of G <> {} implies G is_subformula_of F )
assume F -entry_points_in_subformula_tree_of G <> {} ; ::_thesis: G is_subformula_of F
then consider x being set such that
A1: x in F -entry_points_in_subformula_tree_of G by XBOOLE_0:def_1;
x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } by A1, Th19;
then ex t being Element of dom (tree_of_subformulae F) st
( x = t & (tree_of_subformulae F) . t = G ) ;
then G in rng (tree_of_subformulae F) by FUNCT_1:def_3;
hence G is_subformula_of F by Th10; ::_thesis: verum
end;
theorem Th21: :: QC_LANG4:21
for A being QC-alphabet
for m being Element of NAT
for F being Element of QC-WFF A
for t9, t being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is negative holds
( (tree_of_subformulae F) . t9 = the_argument_of ((tree_of_subformulae F) . t) & m = 0 )
proof
let A be QC-alphabet ; ::_thesis: for m being Element of NAT
for F being Element of QC-WFF A
for t9, t being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is negative holds
( (tree_of_subformulae F) . t9 = the_argument_of ((tree_of_subformulae F) . t) & m = 0 )
let m be Element of NAT ; ::_thesis: for F being Element of QC-WFF A
for t9, t being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is negative holds
( (tree_of_subformulae F) . t9 = the_argument_of ((tree_of_subformulae F) . t) & m = 0 )
let F be Element of QC-WFF A; ::_thesis: for t9, t being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is negative holds
( (tree_of_subformulae F) . t9 = the_argument_of ((tree_of_subformulae F) . t) & m = 0 )
let t9, t be Element of dom (tree_of_subformulae F); ::_thesis: ( t9 = t ^ <*m*> & (tree_of_subformulae F) . t is negative implies ( (tree_of_subformulae F) . t9 = the_argument_of ((tree_of_subformulae F) . t) & m = 0 ) )
set G = (tree_of_subformulae F) . t;
set H = (tree_of_subformulae F) . t9;
assume that
A1: t9 = t ^ <*m*> and
A2: (tree_of_subformulae F) . t is negative ; ::_thesis: ( (tree_of_subformulae F) . t9 = the_argument_of ((tree_of_subformulae F) . t) & m = 0 )
A3: dom <*(the_argument_of ((tree_of_subformulae F) . t))*> = Seg 1 by FINSEQ_1:def_8;
A4: ( succ ((tree_of_subformulae F),t) = list_of_immediate_constituents ((tree_of_subformulae F) . t) & ex q being Element of dom (tree_of_subformulae F) st
( q = t & succ ((tree_of_subformulae F),t) = (tree_of_subformulae F) * (q succ) ) ) by Def2, TREES_9:def_6;
list_of_immediate_constituents ((tree_of_subformulae F) . t) = <*(the_argument_of ((tree_of_subformulae F) . t))*> by A2, Def1;
then dom <*(the_argument_of ((tree_of_subformulae F) . t))*> = dom (t succ) by A4, TREES_9:37;
then m + 1 in dom <*(the_argument_of ((tree_of_subformulae F) . t))*> by A1, TREES_9:39;
then A5: m + 1 = 0 + 1 by A3, FINSEQ_1:2, TARSKI:def_1;
(tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t by A1, Th7;
hence ( (tree_of_subformulae F) . t9 = the_argument_of ((tree_of_subformulae F) . t) & m = 0 ) by A2, A5, QC_LANG2:48; ::_thesis: verum
end;
theorem Th22: :: QC_LANG4:22
for A being QC-alphabet
for m being Element of NAT
for F being Element of QC-WFF A
for t9, t being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is conjunctive & not ( (tree_of_subformulae F) . t9 = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) holds
( (tree_of_subformulae F) . t9 = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 )
proof
let A be QC-alphabet ; ::_thesis: for m being Element of NAT
for F being Element of QC-WFF A
for t9, t being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is conjunctive & not ( (tree_of_subformulae F) . t9 = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) holds
( (tree_of_subformulae F) . t9 = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 )
let m be Element of NAT ; ::_thesis: for F being Element of QC-WFF A
for t9, t being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is conjunctive & not ( (tree_of_subformulae F) . t9 = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) holds
( (tree_of_subformulae F) . t9 = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 )
let F be Element of QC-WFF A; ::_thesis: for t9, t being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is conjunctive & not ( (tree_of_subformulae F) . t9 = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) holds
( (tree_of_subformulae F) . t9 = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 )
let t9, t be Element of dom (tree_of_subformulae F); ::_thesis: ( t9 = t ^ <*m*> & (tree_of_subformulae F) . t is conjunctive & not ( (tree_of_subformulae F) . t9 = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) implies ( (tree_of_subformulae F) . t9 = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 ) )
set G = (tree_of_subformulae F) . t;
set H = (tree_of_subformulae F) . t9;
assume that
A1: t9 = t ^ <*m*> and
A2: (tree_of_subformulae F) . t is conjunctive ; ::_thesis: ( ( (tree_of_subformulae F) . t9 = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) or ( (tree_of_subformulae F) . t9 = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 ) )
A3: list_of_immediate_constituents ((tree_of_subformulae F) . t) = <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> by A2, Def1;
len <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> = 2 by FINSEQ_1:44;
then A4: dom <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> = Seg 2 by FINSEQ_1:def_3;
A5: succ ((tree_of_subformulae F),t) = list_of_immediate_constituents ((tree_of_subformulae F) . t) by Def2;
ex q being Element of dom (tree_of_subformulae F) st
( q = t & succ ((tree_of_subformulae F),t) = (tree_of_subformulae F) * (q succ) ) by TREES_9:def_6;
then dom <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> = dom (t succ) by A5, A3, TREES_9:37;
then m + 1 in dom <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> by A1, TREES_9:39;
then A6: ( m + 1 = 0 + 1 or m + 1 = 1 + 1 ) by A4, FINSEQ_1:2, TARSKI:def_2;
percases ( m = 0 or m = 1 ) by A6;
supposeA7: m = 0 ; ::_thesis: ( ( (tree_of_subformulae F) . t9 = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) or ( (tree_of_subformulae F) . t9 = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 ) )
(tree_of_subformulae F) . t9 = (succ ((tree_of_subformulae F),t)) . (m + 1) by A1, TREES_9:40
.= the_left_argument_of ((tree_of_subformulae F) . t) by A5, A3, A7, FINSEQ_1:44 ;
hence ( ( (tree_of_subformulae F) . t9 = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) or ( (tree_of_subformulae F) . t9 = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 ) ) by A7; ::_thesis: verum
end;
supposeA8: m = 1 ; ::_thesis: ( ( (tree_of_subformulae F) . t9 = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) or ( (tree_of_subformulae F) . t9 = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 ) )
(tree_of_subformulae F) . t9 = (succ ((tree_of_subformulae F),t)) . (m + 1) by A1, TREES_9:40
.= the_right_argument_of ((tree_of_subformulae F) . t) by A5, A3, A8, FINSEQ_1:44 ;
hence ( ( (tree_of_subformulae F) . t9 = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) or ( (tree_of_subformulae F) . t9 = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 ) ) by A8; ::_thesis: verum
end;
end;
end;
theorem Th23: :: QC_LANG4:23
for A being QC-alphabet
for m being Element of NAT
for F being Element of QC-WFF A
for t9, t being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is universal holds
( (tree_of_subformulae F) . t9 = the_scope_of ((tree_of_subformulae F) . t) & m = 0 )
proof
let A be QC-alphabet ; ::_thesis: for m being Element of NAT
for F being Element of QC-WFF A
for t9, t being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is universal holds
( (tree_of_subformulae F) . t9 = the_scope_of ((tree_of_subformulae F) . t) & m = 0 )
let m be Element of NAT ; ::_thesis: for F being Element of QC-WFF A
for t9, t being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is universal holds
( (tree_of_subformulae F) . t9 = the_scope_of ((tree_of_subformulae F) . t) & m = 0 )
let F be Element of QC-WFF A; ::_thesis: for t9, t being Element of dom (tree_of_subformulae F) st t9 = t ^ <*m*> & (tree_of_subformulae F) . t is universal holds
( (tree_of_subformulae F) . t9 = the_scope_of ((tree_of_subformulae F) . t) & m = 0 )
let t9, t be Element of dom (tree_of_subformulae F); ::_thesis: ( t9 = t ^ <*m*> & (tree_of_subformulae F) . t is universal implies ( (tree_of_subformulae F) . t9 = the_scope_of ((tree_of_subformulae F) . t) & m = 0 ) )
set G = (tree_of_subformulae F) . t;
set H = (tree_of_subformulae F) . t9;
assume that
A1: t9 = t ^ <*m*> and
A2: (tree_of_subformulae F) . t is universal ; ::_thesis: ( (tree_of_subformulae F) . t9 = the_scope_of ((tree_of_subformulae F) . t) & m = 0 )
A3: dom <*(the_scope_of ((tree_of_subformulae F) . t))*> = Seg 1 by FINSEQ_1:def_8;
A4: ( succ ((tree_of_subformulae F),t) = list_of_immediate_constituents ((tree_of_subformulae F) . t) & ex q being Element of dom (tree_of_subformulae F) st
( q = t & succ ((tree_of_subformulae F),t) = (tree_of_subformulae F) * (q succ) ) ) by Def2, TREES_9:def_6;
not VERUM A is universal by QC_LANG1:20;
then A5: (tree_of_subformulae F) . t <> VERUM A by A2;
( not (tree_of_subformulae F) . t is atomic & not (tree_of_subformulae F) . t is negative & not (tree_of_subformulae F) . t is conjunctive ) by A2, QC_LANG1:20;
then list_of_immediate_constituents ((tree_of_subformulae F) . t) = <*(the_scope_of ((tree_of_subformulae F) . t))*> by Def1, A5;
then dom <*(the_scope_of ((tree_of_subformulae F) . t))*> = dom (t succ) by A4, TREES_9:37;
then m + 1 in dom <*(the_scope_of ((tree_of_subformulae F) . t))*> by A1, TREES_9:39;
then A6: m + 1 = 0 + 1 by A3, FINSEQ_1:2, TARSKI:def_1;
(tree_of_subformulae F) . t9 is_immediate_constituent_of (tree_of_subformulae F) . t by A1, Th7;
hence ( (tree_of_subformulae F) . t9 = the_scope_of ((tree_of_subformulae F) . t) & m = 0 ) by A2, A6, QC_LANG2:50; ::_thesis: verum
end;
theorem Th24: :: QC_LANG4:24
for A being QC-alphabet
for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . t is negative holds
( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_argument_of ((tree_of_subformulae F) . t) )
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . t is negative holds
( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_argument_of ((tree_of_subformulae F) . t) )
let F be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . t is negative holds
( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_argument_of ((tree_of_subformulae F) . t) )
let t be Element of dom (tree_of_subformulae F); ::_thesis: ( (tree_of_subformulae F) . t is negative implies ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_argument_of ((tree_of_subformulae F) . t) ) )
set G = (tree_of_subformulae F) . t;
consider H being Element of QC-WFF A such that
A1: H = the_argument_of ((tree_of_subformulae F) . t) ;
assume A2: (tree_of_subformulae F) . t is negative ; ::_thesis: ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_argument_of ((tree_of_subformulae F) . t) )
then H is_immediate_constituent_of (tree_of_subformulae F) . t by A1, QC_LANG2:48;
then consider m being Element of NAT such that
A3: t ^ <*m*> in dom (tree_of_subformulae F) and
H = (tree_of_subformulae F) . (t ^ <*m*>) by Th7;
m = 0 by A2, A3, Th21;
hence ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_argument_of ((tree_of_subformulae F) . t) ) by A2, A3, Th21; ::_thesis: verum
end;
Lm1: for x, y being set holds dom <*x,y*> = Seg 2
proof
let x, y be set ; ::_thesis: dom <*x,y*> = Seg 2
thus dom <*x,y*> = Seg (len <*x,y*>) by FINSEQ_1:def_3
.= Seg 2 by FINSEQ_1:44 ; ::_thesis: verum
end;
theorem Th25: :: QC_LANG4:25
for A being QC-alphabet
for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . t is conjunctive holds
( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_left_argument_of ((tree_of_subformulae F) . t) & t ^ <*1*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*1*>) = the_right_argument_of ((tree_of_subformulae F) . t) )
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . t is conjunctive holds
( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_left_argument_of ((tree_of_subformulae F) . t) & t ^ <*1*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*1*>) = the_right_argument_of ((tree_of_subformulae F) . t) )
let F be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . t is conjunctive holds
( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_left_argument_of ((tree_of_subformulae F) . t) & t ^ <*1*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*1*>) = the_right_argument_of ((tree_of_subformulae F) . t) )
let t be Element of dom (tree_of_subformulae F); ::_thesis: ( (tree_of_subformulae F) . t is conjunctive implies ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_left_argument_of ((tree_of_subformulae F) . t) & t ^ <*1*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*1*>) = the_right_argument_of ((tree_of_subformulae F) . t) ) )
set G = (tree_of_subformulae F) . t;
assume A1: (tree_of_subformulae F) . t is conjunctive ; ::_thesis: ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_left_argument_of ((tree_of_subformulae F) . t) & t ^ <*1*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*1*>) = the_right_argument_of ((tree_of_subformulae F) . t) )
(tree_of_subformulae F) * (t succ) = succ ((tree_of_subformulae F),t)
proof
ex q being Element of dom (tree_of_subformulae F) st
( q = t & succ ((tree_of_subformulae F),t) = (tree_of_subformulae F) * (q succ) ) by TREES_9:def_6;
hence (tree_of_subformulae F) * (t succ) = succ ((tree_of_subformulae F),t) ; ::_thesis: verum
end;
then A2: dom (t succ) = dom (succ ((tree_of_subformulae F),t)) by TREES_9:37
.= dom (list_of_immediate_constituents ((tree_of_subformulae F) . t)) by Def2
.= dom <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> by A1, Def1
.= {1,2} by Lm1, FINSEQ_1:2 ;
A3: 0 + 1 in {1,2} by TARSKI:def_2;
then t ^ <*0*> in dom (tree_of_subformulae F) by A2, TREES_9:39;
then (tree_of_subformulae F) . (t ^ <*0*>) = (succ ((tree_of_subformulae F),t)) . (0 + 1) by TREES_9:40
.= (list_of_immediate_constituents ((tree_of_subformulae F) . t)) . 1 by Def2
.= <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> . 1 by A1, Def1
.= the_left_argument_of ((tree_of_subformulae F) . t) by FINSEQ_1:44 ;
hence ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_left_argument_of ((tree_of_subformulae F) . t) ) by A2, A3, TREES_9:39; ::_thesis: ( t ^ <*1*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*1*>) = the_right_argument_of ((tree_of_subformulae F) . t) )
A4: 1 + 1 in {1,2} by TARSKI:def_2;
then t ^ <*1*> in dom (tree_of_subformulae F) by A2, TREES_9:39;
then (tree_of_subformulae F) . (t ^ <*1*>) = (succ ((tree_of_subformulae F),t)) . (1 + 1) by TREES_9:40
.= (list_of_immediate_constituents ((tree_of_subformulae F) . t)) . 2 by Def2
.= <*(the_left_argument_of ((tree_of_subformulae F) . t)),(the_right_argument_of ((tree_of_subformulae F) . t))*> . 2 by A1, Def1
.= the_right_argument_of ((tree_of_subformulae F) . t) by FINSEQ_1:44 ;
hence ( t ^ <*1*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*1*>) = the_right_argument_of ((tree_of_subformulae F) . t) ) by A2, A4, TREES_9:39; ::_thesis: verum
end;
theorem Th26: :: QC_LANG4:26
for A being QC-alphabet
for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . t is universal holds
( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_scope_of ((tree_of_subformulae F) . t) )
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . t is universal holds
( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_scope_of ((tree_of_subformulae F) . t) )
let F be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . t is universal holds
( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_scope_of ((tree_of_subformulae F) . t) )
let t be Element of dom (tree_of_subformulae F); ::_thesis: ( (tree_of_subformulae F) . t is universal implies ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_scope_of ((tree_of_subformulae F) . t) ) )
set G = (tree_of_subformulae F) . t;
consider H being Element of QC-WFF A such that
A1: H = the_scope_of ((tree_of_subformulae F) . t) ;
assume A2: (tree_of_subformulae F) . t is universal ; ::_thesis: ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_scope_of ((tree_of_subformulae F) . t) )
then H is_immediate_constituent_of (tree_of_subformulae F) . t by A1, QC_LANG2:50;
then consider m being Element of NAT such that
A3: t ^ <*m*> in dom (tree_of_subformulae F) and
H = (tree_of_subformulae F) . (t ^ <*m*>) by Th7;
m = 0 by A2, A3, Th23;
hence ( t ^ <*0*> in dom (tree_of_subformulae F) & (tree_of_subformulae F) . (t ^ <*0*>) = the_scope_of ((tree_of_subformulae F) . t) ) by A2, A3, Th23; ::_thesis: verum
end;
theorem Th27: :: QC_LANG4:27
for A being QC-alphabet
for F, G, H being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F)
for s being Element of dom (tree_of_subformulae G) st t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H holds
t ^ s in F -entry_points_in_subformula_tree_of H
proof
let A be QC-alphabet ; ::_thesis: for F, G, H being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F)
for s being Element of dom (tree_of_subformulae G) st t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H holds
t ^ s in F -entry_points_in_subformula_tree_of H
let F, G, H be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F)
for s being Element of dom (tree_of_subformulae G) st t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H holds
t ^ s in F -entry_points_in_subformula_tree_of H
let t be Element of dom (tree_of_subformulae F); ::_thesis: for s being Element of dom (tree_of_subformulae G) st t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H holds
t ^ s in F -entry_points_in_subformula_tree_of H
let s be Element of dom (tree_of_subformulae G); ::_thesis: ( t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H implies t ^ s in F -entry_points_in_subformula_tree_of H )
defpred S1[ Element of NAT ] means for F, G, H being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F)
for s being Element of dom (tree_of_subformulae G) st G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = $1 holds
t ^ s in F -entry_points_in_subformula_tree_of H;
A1: 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 A2: S1[k] ; ::_thesis: S1[k + 1]
thus S1[k + 1] ::_thesis: verum
proof
A3: 1 in {1} by TARSKI:def_1;
let F, G, H be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F)
for s being Element of dom (tree_of_subformulae G) st G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = k + 1 holds
t ^ s in F -entry_points_in_subformula_tree_of H
let t be Element of dom (tree_of_subformulae F); ::_thesis: for s being Element of dom (tree_of_subformulae G) st G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = k + 1 holds
t ^ s in F -entry_points_in_subformula_tree_of H
let s be Element of dom (tree_of_subformulae G); ::_thesis: ( G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = k + 1 implies t ^ s in F -entry_points_in_subformula_tree_of H )
assume that
A4: G = (tree_of_subformulae F) . t and
A5: H = (tree_of_subformulae G) . s and
A6: len s = k + 1 ; ::_thesis: t ^ s in F -entry_points_in_subformula_tree_of H
consider v being FinSequence, x being set such that
A7: s = v ^ <*x*> and
A8: len v = k by A6, TREES_2:3;
reconsider u = <*x*> as FinSequence of NAT by A7, FINSEQ_1:36;
A9: rng u c= NAT by FINSEQ_1:def_4;
( dom u = Seg 1 & u . 1 = x ) by FINSEQ_1:def_8;
then x in rng u by A3, FINSEQ_1:2, FUNCT_1:def_3;
then reconsider m = x as Element of NAT by A9;
reconsider v = v as FinSequence of NAT by A7, FINSEQ_1:36;
reconsider s9 = v as Element of dom (tree_of_subformulae G) by A7, TREES_1:21;
consider H9 being Element of QC-WFF A such that
A10: H9 = (tree_of_subformulae G) . s9 ;
A11: t ^ s9 in F -entry_points_in_subformula_tree_of H9 by A2, A4, A8, A10;
F -entry_points_in_subformula_tree_of H9 c= dom (tree_of_subformulae F) by TREES_1:def_11;
then consider t9 being Element of dom (tree_of_subformulae F) such that
A12: t9 = t ^ s9 by A11;
A13: H9 = (tree_of_subformulae F) . t9 by A11, A12, Def3;
A14: s = s9 ^ <*m*> by A7;
then A15: H is_immediate_constituent_of H9 by A5, A10, Th7;
A16: ( H = (tree_of_subformulae F) . (t9 ^ <*m*>) & t9 ^ <*m*> in dom (tree_of_subformulae F) )
proof
A17: H9 <> VERUM A by A15, QC_LANG2:41;
now__::_thesis:_(_H_=_(tree_of_subformulae_F)_._(t9_^_<*m*>)_&_t9_^_<*m*>_in_dom_(tree_of_subformulae_F)_)
percases ( H9 is negative or H9 is conjunctive or H9 is universal ) by A15, A17, QC_LANG1:9, QC_LANG2:47;
supposeA18: H9 is negative ; ::_thesis: ( H = (tree_of_subformulae F) . (t9 ^ <*m*>) & t9 ^ <*m*> in dom (tree_of_subformulae F) )
then ( H = the_argument_of H9 & m = 0 ) by A5, A14, A10, Th21;
hence ( H = (tree_of_subformulae F) . (t9 ^ <*m*>) & t9 ^ <*m*> in dom (tree_of_subformulae F) ) by A13, A18, Th24; ::_thesis: verum
end;
supposeA19: H9 is conjunctive ; ::_thesis: ( H = (tree_of_subformulae F) . (t9 ^ <*m*>) & t9 ^ <*m*> in dom (tree_of_subformulae F) )
then ( ( H = the_left_argument_of H9 & m = 0 ) or ( H = the_right_argument_of H9 & m = 1 ) ) by A5, A14, A10, Th22;
hence ( H = (tree_of_subformulae F) . (t9 ^ <*m*>) & t9 ^ <*m*> in dom (tree_of_subformulae F) ) by A13, A19, Th25; ::_thesis: verum
end;
supposeA20: H9 is universal ; ::_thesis: ( H = (tree_of_subformulae F) . (t9 ^ <*m*>) & t9 ^ <*m*> in dom (tree_of_subformulae F) )
then ( H = the_scope_of H9 & m = 0 ) by A5, A14, A10, Th23;
hence ( H = (tree_of_subformulae F) . (t9 ^ <*m*>) & t9 ^ <*m*> in dom (tree_of_subformulae F) ) by A13, A20, Th26; ::_thesis: verum
end;
end;
end;
hence ( H = (tree_of_subformulae F) . (t9 ^ <*m*>) & t9 ^ <*m*> in dom (tree_of_subformulae F) ) ; ::_thesis: verum
end;
t ^ s = t9 ^ <*m*> by A7, A12, FINSEQ_1:32;
hence t ^ s in F -entry_points_in_subformula_tree_of H by A16, Def3; ::_thesis: verum
end;
end;
A21: S1[ 0 ]
proof
let F, G, H be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F)
for s being Element of dom (tree_of_subformulae G) st G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = 0 holds
t ^ s in F -entry_points_in_subformula_tree_of H
let t be Element of dom (tree_of_subformulae F); ::_thesis: for s being Element of dom (tree_of_subformulae G) st G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = 0 holds
t ^ s in F -entry_points_in_subformula_tree_of H
let s be Element of dom (tree_of_subformulae G); ::_thesis: ( G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = 0 implies t ^ s in F -entry_points_in_subformula_tree_of H )
assume that
A22: G = (tree_of_subformulae F) . t and
A23: H = (tree_of_subformulae G) . s and
A24: len s = 0 ; ::_thesis: t ^ s in F -entry_points_in_subformula_tree_of H
A25: s = {} by A24;
then A26: t ^ s = t by FINSEQ_1:34;
H = G by A23, A25, Def2;
hence t ^ s in F -entry_points_in_subformula_tree_of H by A22, A26, Def3; ::_thesis: verum
end;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A21, A1);
then A27: ( G = (tree_of_subformulae F) . t & H = (tree_of_subformulae G) . s & len s = len s implies t ^ s in F -entry_points_in_subformula_tree_of H ) ;
assume ( t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H ) ; ::_thesis: t ^ s in F -entry_points_in_subformula_tree_of H
hence t ^ s in F -entry_points_in_subformula_tree_of H by A27, Def3; ::_thesis: verum
end;
theorem Th28: :: QC_LANG4:28
for A being QC-alphabet
for F, G, H being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F)
for s being FinSequence st t in F -entry_points_in_subformula_tree_of G & t ^ s in F -entry_points_in_subformula_tree_of H holds
s in G -entry_points_in_subformula_tree_of H
proof
let A be QC-alphabet ; ::_thesis: for F, G, H being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F)
for s being FinSequence st t in F -entry_points_in_subformula_tree_of G & t ^ s in F -entry_points_in_subformula_tree_of H holds
s in G -entry_points_in_subformula_tree_of H
let F, G, H be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F)
for s being FinSequence st t in F -entry_points_in_subformula_tree_of G & t ^ s in F -entry_points_in_subformula_tree_of H holds
s in G -entry_points_in_subformula_tree_of H
let t be Element of dom (tree_of_subformulae F); ::_thesis: for s being FinSequence st t in F -entry_points_in_subformula_tree_of G & t ^ s in F -entry_points_in_subformula_tree_of H holds
s in G -entry_points_in_subformula_tree_of H
let s be FinSequence; ::_thesis: ( t in F -entry_points_in_subformula_tree_of G & t ^ s in F -entry_points_in_subformula_tree_of H implies s in G -entry_points_in_subformula_tree_of H )
defpred S1[ Element of NAT ] means for F, G, H being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F)
for s being FinSequence st G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = $1 holds
s in G -entry_points_in_subformula_tree_of H;
A1: 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 A2: S1[k] ; ::_thesis: S1[k + 1]
thus S1[k + 1] ::_thesis: verum
proof
let F, G, H be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F)
for s being FinSequence st G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = k + 1 holds
s in G -entry_points_in_subformula_tree_of H
let t be Element of dom (tree_of_subformulae F); ::_thesis: for s being FinSequence st G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = k + 1 holds
s in G -entry_points_in_subformula_tree_of H
let s be FinSequence; ::_thesis: ( G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = k + 1 implies s in G -entry_points_in_subformula_tree_of H )
assume that
A3: G = (tree_of_subformulae F) . t and
A4: t ^ s in F -entry_points_in_subformula_tree_of H and
A5: len s = k + 1 ; ::_thesis: s in G -entry_points_in_subformula_tree_of H
consider v being FinSequence, x being set such that
A6: s = v ^ <*x*> and
A7: len v = k by A5, TREES_2:3;
F -entry_points_in_subformula_tree_of H = { t1 where t1 is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t1 = H } by Th19;
then consider t99 being Element of dom (tree_of_subformulae F) such that
A8: t99 = t ^ s and
A9: (tree_of_subformulae F) . t99 = H by A4;
reconsider s1 = s as FinSequence of NAT by A8, FINSEQ_1:36;
A10: s1 = v ^ <*x*> by A6;
then reconsider u = <*x*> as FinSequence of NAT by FINSEQ_1:36;
reconsider v = v as FinSequence of NAT by A10, FINSEQ_1:36;
A11: rng u c= NAT by FINSEQ_1:def_4;
A12: 1 in {1} by TARSKI:def_1;
( dom u = Seg 1 & u . 1 = x ) by FINSEQ_1:def_8;
then x in rng u by A12, FINSEQ_1:2, FUNCT_1:def_3;
then reconsider m = x as Element of NAT by A11;
consider t9 being FinSequence of NAT such that
A13: t9 = t ^ v ;
A14: t99 = t9 ^ <*m*> by A6, A8, A13, FINSEQ_1:32;
then t9 is_a_prefix_of t99 by TREES_1:1;
then reconsider t9 = t9 as Element of dom (tree_of_subformulae F) by TREES_1:20;
consider H9 being Element of QC-WFF A such that
A15: H9 = (tree_of_subformulae F) . t9 ;
t ^ v in F -entry_points_in_subformula_tree_of H9 by A13, A15, Def3;
then A16: v in G -entry_points_in_subformula_tree_of H9 by A2, A3, A7;
G -entry_points_in_subformula_tree_of H9 = { v1 where v1 is Element of dom (tree_of_subformulae G) : (tree_of_subformulae G) . v1 = H9 } by Th19;
then A17: ex v1 being Element of dom (tree_of_subformulae G) st
( v = v1 & (tree_of_subformulae G) . v1 = H9 ) by A16;
then reconsider v = v as Element of dom (tree_of_subformulae G) ;
A18: H is_immediate_constituent_of H9 by A9, A14, A15, Th7;
( H = (tree_of_subformulae G) . (v ^ <*m*>) & v ^ <*m*> in dom (tree_of_subformulae G) )
proof
A19: H9 <> VERUM A by A18, QC_LANG2:41;
now__::_thesis:_(_H_=_(tree_of_subformulae_G)_._(v_^_<*m*>)_&_v_^_<*m*>_in_dom_(tree_of_subformulae_G)_)
percases ( H9 is negative or H9 is conjunctive or H9 is universal ) by A18, A19, QC_LANG1:9, QC_LANG2:47;
supposeA20: H9 is negative ; ::_thesis: ( H = (tree_of_subformulae G) . (v ^ <*m*>) & v ^ <*m*> in dom (tree_of_subformulae G) )
then ( H = the_argument_of H9 & m = 0 ) by A9, A14, A15, Th21;
hence ( H = (tree_of_subformulae G) . (v ^ <*m*>) & v ^ <*m*> in dom (tree_of_subformulae G) ) by A17, A20, Th24; ::_thesis: verum
end;
supposeA21: H9 is conjunctive ; ::_thesis: ( H = (tree_of_subformulae G) . (v ^ <*m*>) & v ^ <*m*> in dom (tree_of_subformulae G) )
then ( ( H = the_left_argument_of H9 & m = 0 ) or ( H = the_right_argument_of H9 & m = 1 ) ) by A9, A14, A15, Th22;
hence ( H = (tree_of_subformulae G) . (v ^ <*m*>) & v ^ <*m*> in dom (tree_of_subformulae G) ) by A17, A21, Th25; ::_thesis: verum
end;
supposeA22: H9 is universal ; ::_thesis: ( H = (tree_of_subformulae G) . (v ^ <*m*>) & v ^ <*m*> in dom (tree_of_subformulae G) )
then ( H = the_scope_of H9 & m = 0 ) by A9, A14, A15, Th23;
hence ( H = (tree_of_subformulae G) . (v ^ <*m*>) & v ^ <*m*> in dom (tree_of_subformulae G) ) by A17, A22, Th26; ::_thesis: verum
end;
end;
end;
hence ( H = (tree_of_subformulae G) . (v ^ <*m*>) & v ^ <*m*> in dom (tree_of_subformulae G) ) ; ::_thesis: verum
end;
hence s in G -entry_points_in_subformula_tree_of H by A6, Def3; ::_thesis: verum
end;
end;
A23: S1[ 0 ]
proof
let F, G, H be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F)
for s being FinSequence st G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = 0 holds
s in G -entry_points_in_subformula_tree_of H
let t be Element of dom (tree_of_subformulae F); ::_thesis: for s being FinSequence st G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = 0 holds
s in G -entry_points_in_subformula_tree_of H
let s be FinSequence; ::_thesis: ( G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = 0 implies s in G -entry_points_in_subformula_tree_of H )
assume that
A24: G = (tree_of_subformulae F) . t and
A25: t ^ s in F -entry_points_in_subformula_tree_of H and
A26: len s = 0 ; ::_thesis: s in G -entry_points_in_subformula_tree_of H
A27: s = {} by A26;
then reconsider s9 = s as Element of dom (tree_of_subformulae G) by TREES_1:22;
A28: G = (tree_of_subformulae G) . s9 by A27, Def2;
F -entry_points_in_subformula_tree_of H = { t1 where t1 is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t1 = H } by Th19;
then ex t9 being Element of dom (tree_of_subformulae F) st
( t9 = t ^ s & (tree_of_subformulae F) . t9 = H ) by A25;
then H = G by A24, A27, FINSEQ_1:34;
hence s in G -entry_points_in_subformula_tree_of H by A28, Def3; ::_thesis: verum
end;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A23, A1);
then A29: ( G = (tree_of_subformulae F) . t & t ^ s in F -entry_points_in_subformula_tree_of H & len s = len s implies s in G -entry_points_in_subformula_tree_of H ) ;
assume ( t in F -entry_points_in_subformula_tree_of G & t ^ s in F -entry_points_in_subformula_tree_of H ) ; ::_thesis: s in G -entry_points_in_subformula_tree_of H
hence s in G -entry_points_in_subformula_tree_of H by A29, Def3; ::_thesis: verum
end;
theorem Th29: :: QC_LANG4:29
for A being QC-alphabet
for F, G, H being Element of QC-WFF A holds { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G) : ( t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H ) } c= F -entry_points_in_subformula_tree_of H
proof
let A be QC-alphabet ; ::_thesis: for F, G, H being Element of QC-WFF A holds { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G) : ( t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H ) } c= F -entry_points_in_subformula_tree_of H
let F, G, H be Element of QC-WFF A; ::_thesis: { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G) : ( t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H ) } c= F -entry_points_in_subformula_tree_of H
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G) : ( t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H ) } or x in F -entry_points_in_subformula_tree_of H )
assume x in { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G) : ( t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H ) } ; ::_thesis: x in F -entry_points_in_subformula_tree_of H
then ex t being Element of dom (tree_of_subformulae F) ex s being Element of dom (tree_of_subformulae G) st
( x = t ^ s & t in F -entry_points_in_subformula_tree_of G & s in G -entry_points_in_subformula_tree_of H ) ;
hence x in F -entry_points_in_subformula_tree_of H by Th27; ::_thesis: verum
end;
theorem Th30: :: QC_LANG4:30
for A being QC-alphabet
for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) holds (tree_of_subformulae F) | t = tree_of_subformulae ((tree_of_subformulae F) . t)
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) holds (tree_of_subformulae F) | t = tree_of_subformulae ((tree_of_subformulae F) . t)
let F be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F) holds (tree_of_subformulae F) | t = tree_of_subformulae ((tree_of_subformulae F) . t)
let t be Element of dom (tree_of_subformulae F); ::_thesis: (tree_of_subformulae F) | t = tree_of_subformulae ((tree_of_subformulae F) . t)
set T1 = (tree_of_subformulae F) | t;
set T2 = tree_of_subformulae ((tree_of_subformulae F) . t);
thus A1: dom ((tree_of_subformulae F) | t) = dom (tree_of_subformulae ((tree_of_subformulae F) . t)) :: according to TREES_4:def_1 ::_thesis: for b1 being Element of proj1 ((tree_of_subformulae F) | t) holds ((tree_of_subformulae F) | t) . b1 = (tree_of_subformulae ((tree_of_subformulae F) . t)) . b1
proof
let p be FinSequence of NAT ; :: according to TREES_2:def_1 ::_thesis: ( ( not p in dom ((tree_of_subformulae F) | t) or p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) ) & ( not p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) or p in dom ((tree_of_subformulae F) | t) ) )
now__::_thesis:_(_p_in_dom_((tree_of_subformulae_F)_|_t)_implies_p_in_dom_(tree_of_subformulae_((tree_of_subformulae_F)_._t))_)
consider G being Element of QC-WFF A such that
A2: G = (tree_of_subformulae F) . t ;
A3: t in F -entry_points_in_subformula_tree_of G by A2, Def3;
consider t9 being FinSequence of NAT such that
A4: t9 = t ^ p ;
assume p in dom ((tree_of_subformulae F) | t) ; ::_thesis: p in dom (tree_of_subformulae ((tree_of_subformulae F) . t))
then p in (dom (tree_of_subformulae F)) | t by TREES_2:def_10;
then reconsider t9 = t9 as Element of dom (tree_of_subformulae F) by A4, TREES_1:def_6;
consider H being Element of QC-WFF A such that
A5: H = (tree_of_subformulae F) . t9 ;
A6: G -entry_points_in_subformula_tree_of H c= dom (tree_of_subformulae ((tree_of_subformulae F) . t)) by A2, TREES_1:def_11;
t9 in F -entry_points_in_subformula_tree_of H by A5, Def3;
then p in G -entry_points_in_subformula_tree_of H by A3, A4, Th28;
hence p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) by A6; ::_thesis: verum
end;
hence ( p in dom ((tree_of_subformulae F) | t) implies p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) ) ; ::_thesis: ( not p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) or p in dom ((tree_of_subformulae F) | t) )
now__::_thesis:_(_p_in_dom_(tree_of_subformulae_((tree_of_subformulae_F)_._t))_implies_p_in_dom_((tree_of_subformulae_F)_|_t)_)
consider G being Element of QC-WFF A such that
A7: G = (tree_of_subformulae F) . t ;
assume p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) ; ::_thesis: p in dom ((tree_of_subformulae F) | t)
then reconsider s = p as Element of dom (tree_of_subformulae G) by A7;
consider H being Element of QC-WFF A such that
A8: H = (tree_of_subformulae G) . s ;
A9: s in G -entry_points_in_subformula_tree_of H by A8, Def3;
A10: F -entry_points_in_subformula_tree_of H c= dom (tree_of_subformulae F) by TREES_1:def_11;
t in F -entry_points_in_subformula_tree_of G by A7, Def3;
then t ^ s in F -entry_points_in_subformula_tree_of H by A9, Th27;
then s in (dom (tree_of_subformulae F)) | t by A10, TREES_1:def_6;
hence p in dom ((tree_of_subformulae F) | t) by TREES_2:def_10; ::_thesis: verum
end;
hence ( not p in dom (tree_of_subformulae ((tree_of_subformulae F) . t)) or p in dom ((tree_of_subformulae F) | t) ) ; ::_thesis: verum
end;
now__::_thesis:_for_p_being_Node_of_((tree_of_subformulae_F)_|_t)_holds_((tree_of_subformulae_F)_|_t)_._p_=_(tree_of_subformulae_((tree_of_subformulae_F)_._t))_._p
let p be Node of ((tree_of_subformulae F) | t); ::_thesis: ((tree_of_subformulae F) | t) . p = (tree_of_subformulae ((tree_of_subformulae F) . t)) . p
consider G being Element of QC-WFF A such that
A11: G = (tree_of_subformulae F) . t ;
reconsider s = p as Element of dom (tree_of_subformulae G) by A1, A11;
A12: dom ((tree_of_subformulae F) | t) = (dom (tree_of_subformulae F)) | t by TREES_2:def_10;
then reconsider t9 = t ^ s as Element of dom (tree_of_subformulae F) by TREES_1:def_6;
consider H being Element of QC-WFF A such that
A13: H = ((tree_of_subformulae F) | t) . p ;
A14: t in F -entry_points_in_subformula_tree_of G by A11, Def3;
((tree_of_subformulae F) | t) . p = (tree_of_subformulae F) . (t ^ p) by A12, TREES_2:def_10;
then t9 in F -entry_points_in_subformula_tree_of H by A13, Def3;
then s in G -entry_points_in_subformula_tree_of H by A14, Th28;
hence ((tree_of_subformulae F) | t) . p = (tree_of_subformulae ((tree_of_subformulae F) . t)) . p by A11, A13, Def3; ::_thesis: verum
end;
hence for p being Node of ((tree_of_subformulae F) | t) holds ((tree_of_subformulae F) | t) . p = (tree_of_subformulae ((tree_of_subformulae F) . t)) . p ; ::_thesis: verum
end;
theorem Th31: :: QC_LANG4:31
for A being QC-alphabet
for F, G being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) holds
( t in F -entry_points_in_subformula_tree_of G iff (tree_of_subformulae F) | t = tree_of_subformulae G )
proof
let A be QC-alphabet ; ::_thesis: for F, G being Element of QC-WFF A
for t being Element of dom (tree_of_subformulae F) holds
( t in F -entry_points_in_subformula_tree_of G iff (tree_of_subformulae F) | t = tree_of_subformulae G )
let F, G be Element of QC-WFF A; ::_thesis: for t being Element of dom (tree_of_subformulae F) holds
( t in F -entry_points_in_subformula_tree_of G iff (tree_of_subformulae F) | t = tree_of_subformulae G )
let t be Element of dom (tree_of_subformulae F); ::_thesis: ( t in F -entry_points_in_subformula_tree_of G iff (tree_of_subformulae F) | t = tree_of_subformulae G )
now__::_thesis:_(_t_in_F_-entry_points_in_subformula_tree_of_G_implies_(tree_of_subformulae_F)_|_t_=_tree_of_subformulae_G_)
assume t in F -entry_points_in_subformula_tree_of G ; ::_thesis: (tree_of_subformulae F) | t = tree_of_subformulae G
then (tree_of_subformulae F) . t = G by Def3;
hence (tree_of_subformulae F) | t = tree_of_subformulae G by Th30; ::_thesis: verum
end;
hence ( t in F -entry_points_in_subformula_tree_of G implies (tree_of_subformulae F) | t = tree_of_subformulae G ) ; ::_thesis: ( (tree_of_subformulae F) | t = tree_of_subformulae G implies t in F -entry_points_in_subformula_tree_of G )
now__::_thesis:_(_(tree_of_subformulae_F)_|_t_=_tree_of_subformulae_G_implies_t_in_F_-entry_points_in_subformula_tree_of_G_)
assume (tree_of_subformulae F) | t = tree_of_subformulae G ; ::_thesis: t in F -entry_points_in_subformula_tree_of G
then A1: (tree_of_subformulae F) . t = (tree_of_subformulae G) . {} by TREES_9:35;
(tree_of_subformulae G) . {} = G by Def2;
hence t in F -entry_points_in_subformula_tree_of G by A1, Def3; ::_thesis: verum
end;
hence ( (tree_of_subformulae F) | t = tree_of_subformulae G implies t in F -entry_points_in_subformula_tree_of G ) ; ::_thesis: verum
end;
theorem :: QC_LANG4:32
for A being QC-alphabet
for F, G being Element of QC-WFF A holds F -entry_points_in_subformula_tree_of G = { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) | t = tree_of_subformulae G }
proof
let A be QC-alphabet ; ::_thesis: for F, G being Element of QC-WFF A holds F -entry_points_in_subformula_tree_of G = { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) | t = tree_of_subformulae G }
let F, G be Element of QC-WFF A; ::_thesis: F -entry_points_in_subformula_tree_of G = { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) | t = tree_of_subformulae G }
thus F -entry_points_in_subformula_tree_of G c= { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) | t = tree_of_subformulae G } :: according to XBOOLE_0:def_10 ::_thesis: { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) | t = tree_of_subformulae G } c= F -entry_points_in_subformula_tree_of G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F -entry_points_in_subformula_tree_of G or x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) | t = tree_of_subformulae G } )
assume A1: x in F -entry_points_in_subformula_tree_of G ; ::_thesis: x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) | t = tree_of_subformulae G }
F -entry_points_in_subformula_tree_of G c= dom (tree_of_subformulae F) by TREES_1:def_11;
then reconsider t9 = x as Element of dom (tree_of_subformulae F) by A1;
(tree_of_subformulae F) | t9 = tree_of_subformulae G by A1, Th31;
hence x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) | t = tree_of_subformulae G } ; ::_thesis: verum
end;
thus { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) | t = tree_of_subformulae G } c= F -entry_points_in_subformula_tree_of G ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) | t = tree_of_subformulae G } or x in F -entry_points_in_subformula_tree_of G )
assume x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) | t = tree_of_subformulae G } ; ::_thesis: x in F -entry_points_in_subformula_tree_of G
then ex t9 being Element of dom (tree_of_subformulae F) st
( t9 = x & (tree_of_subformulae F) | t9 = tree_of_subformulae G ) ;
hence x in F -entry_points_in_subformula_tree_of G by Th31; ::_thesis: verum
end;
end;
theorem :: QC_LANG4:33
for A being QC-alphabet
for F, G, H being Element of QC-WFF A
for C being Chain of dom (tree_of_subformulae F) st G in { ((tree_of_subformulae F) . t) where t is Element of dom (tree_of_subformulae F) : t in C } & H in { ((tree_of_subformulae F) . t) where t is Element of dom (tree_of_subformulae F) : t in C } & not G is_subformula_of H holds
H is_subformula_of G
proof
let A be QC-alphabet ; ::_thesis: for F, G, H being Element of QC-WFF A
for C being Chain of dom (tree_of_subformulae F) st G in { ((tree_of_subformulae F) . t) where t is Element of dom (tree_of_subformulae F) : t in C } & H in { ((tree_of_subformulae F) . t) where t is Element of dom (tree_of_subformulae F) : t in C } & not G is_subformula_of H holds
H is_subformula_of G
let F, G, H be Element of QC-WFF A; ::_thesis: for C being Chain of dom (tree_of_subformulae F) st G in { ((tree_of_subformulae F) . t) where t is Element of dom (tree_of_subformulae F) : t in C } & H in { ((tree_of_subformulae F) . t) where t is Element of dom (tree_of_subformulae F) : t in C } & not G is_subformula_of H holds
H is_subformula_of G
let C be Chain of dom (tree_of_subformulae F); ::_thesis: ( G in { ((tree_of_subformulae F) . t) where t is Element of dom (tree_of_subformulae F) : t in C } & H in { ((tree_of_subformulae F) . t) where t is Element of dom (tree_of_subformulae F) : t in C } & not G is_subformula_of H implies H is_subformula_of G )
assume that
A1: G in { ((tree_of_subformulae F) . t) where t is Element of dom (tree_of_subformulae F) : t in C } and
A2: H in { ((tree_of_subformulae F) . t) where t is Element of dom (tree_of_subformulae F) : t in C } ; ::_thesis: ( G is_subformula_of H or H is_subformula_of G )
consider t9 being Element of dom (tree_of_subformulae F) such that
A3: G = (tree_of_subformulae F) . t9 and
A4: t9 in C by A1;
consider t99 being Element of dom (tree_of_subformulae F) such that
A5: H = (tree_of_subformulae F) . t99 and
A6: t99 in C by A2;
A7: t9,t99 are_c=-comparable by A4, A6, TREES_2:def_3;
percases ( t9 is_a_prefix_of t99 or t99 is_a_prefix_of t9 ) by A7, XBOOLE_0:def_9;
suppose t9 is_a_prefix_of t99 ; ::_thesis: ( G is_subformula_of H or H is_subformula_of G )
hence ( G is_subformula_of H or H is_subformula_of G ) by A3, A5, Th13; ::_thesis: verum
end;
suppose t99 is_a_prefix_of t9 ; ::_thesis: ( G is_subformula_of H or H is_subformula_of G )
hence ( G is_subformula_of H or H is_subformula_of G ) by A3, A5, Th13; ::_thesis: verum
end;
end;
end;
definition
let A be QC-alphabet ;
let F be Element of QC-WFF A;
mode Subformula of F -> Element of QC-WFF A means :Def4: :: QC_LANG4:def 4
it is_subformula_of F;
existence
ex b1 being Element of QC-WFF A st b1 is_subformula_of F ;
end;
:: deftheorem Def4 defines Subformula QC_LANG4:def_4_:_
for A being QC-alphabet
for F, b3 being Element of QC-WFF A holds
( b3 is Subformula of F iff b3 is_subformula_of F );
definition
let A be QC-alphabet ;
let F be Element of QC-WFF A;
let G be Subformula of F;
mode Entry_Point_in_Subformula_Tree of G -> Element of dom (tree_of_subformulae F) means :Def5: :: QC_LANG4:def 5
(tree_of_subformulae F) . it = G;
existence
ex b1 being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . b1 = G
proof
G is_subformula_of F by Def4;
then G in rng (tree_of_subformulae F) by Th10;
then ex x being set st
( x in dom (tree_of_subformulae F) & (tree_of_subformulae F) . x = G ) by FUNCT_1:def_3;
hence ex b1 being Element of dom (tree_of_subformulae F) st (tree_of_subformulae F) . b1 = G ; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines Entry_Point_in_Subformula_Tree QC_LANG4:def_5_:_
for A being QC-alphabet
for F being Element of QC-WFF A
for G being Subformula of F
for b4 being Element of dom (tree_of_subformulae F) holds
( b4 is Entry_Point_in_Subformula_Tree of G iff (tree_of_subformulae F) . b4 = G );
theorem :: QC_LANG4:34
for A being QC-alphabet
for F being Element of QC-WFF A
for G being Subformula of F
for t, t9 being Entry_Point_in_Subformula_Tree of G st t <> t9 holds
not t,t9 are_c=-comparable
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for G being Subformula of F
for t, t9 being Entry_Point_in_Subformula_Tree of G st t <> t9 holds
not t,t9 are_c=-comparable
let F be Element of QC-WFF A; ::_thesis: for G being Subformula of F
for t, t9 being Entry_Point_in_Subformula_Tree of G st t <> t9 holds
not t,t9 are_c=-comparable
let G be Subformula of F; ::_thesis: for t, t9 being Entry_Point_in_Subformula_Tree of G st t <> t9 holds
not t,t9 are_c=-comparable
let t, t9 be Entry_Point_in_Subformula_Tree of G; ::_thesis: ( t <> t9 implies not t,t9 are_c=-comparable )
assume A1: t <> t9 ; ::_thesis: not t,t9 are_c=-comparable
( (tree_of_subformulae F) . t = G & (tree_of_subformulae F) . t9 = G ) by Def5;
hence not t,t9 are_c=-comparable by A1, Th18; ::_thesis: verum
end;
definition
let A be QC-alphabet ;
let F be Element of QC-WFF A;
let G be Subformula of F;
func entry_points_in_subformula_tree G -> non empty AntiChain_of_Prefixes of dom (tree_of_subformulae F) equals :: QC_LANG4:def 6
F -entry_points_in_subformula_tree_of G;
coherence
F -entry_points_in_subformula_tree_of G is non empty AntiChain_of_Prefixes of dom (tree_of_subformulae F)
proof
G is_subformula_of F by Def4;
hence F -entry_points_in_subformula_tree_of G is non empty AntiChain_of_Prefixes of dom (tree_of_subformulae F) by Th20; ::_thesis: verum
end;
end;
:: deftheorem defines entry_points_in_subformula_tree QC_LANG4:def_6_:_
for A being QC-alphabet
for F being Element of QC-WFF A
for G being Subformula of F holds entry_points_in_subformula_tree G = F -entry_points_in_subformula_tree_of G;
theorem Th35: :: QC_LANG4:35
for A being QC-alphabet
for F being Element of QC-WFF A
for G being Subformula of F
for t being Entry_Point_in_Subformula_Tree of G holds t in entry_points_in_subformula_tree G
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for G being Subformula of F
for t being Entry_Point_in_Subformula_Tree of G holds t in entry_points_in_subformula_tree G
let F be Element of QC-WFF A; ::_thesis: for G being Subformula of F
for t being Entry_Point_in_Subformula_Tree of G holds t in entry_points_in_subformula_tree G
let G be Subformula of F; ::_thesis: for t being Entry_Point_in_Subformula_Tree of G holds t in entry_points_in_subformula_tree G
let t be Entry_Point_in_Subformula_Tree of G; ::_thesis: t in entry_points_in_subformula_tree G
(tree_of_subformulae F) . t = G by Def5;
hence t in entry_points_in_subformula_tree G by Def3; ::_thesis: verum
end;
theorem Th36: :: QC_LANG4:36
for A being QC-alphabet
for F being Element of QC-WFF A
for G being Subformula of F holds entry_points_in_subformula_tree G = { t where t is Entry_Point_in_Subformula_Tree of G : t = t }
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for G being Subformula of F holds entry_points_in_subformula_tree G = { t where t is Entry_Point_in_Subformula_Tree of G : t = t }
let F be Element of QC-WFF A; ::_thesis: for G being Subformula of F holds entry_points_in_subformula_tree G = { t where t is Entry_Point_in_Subformula_Tree of G : t = t }
let G be Subformula of F; ::_thesis: entry_points_in_subformula_tree G = { t where t is Entry_Point_in_Subformula_Tree of G : t = t }
thus entry_points_in_subformula_tree G c= { t where t is Entry_Point_in_Subformula_Tree of G : t = t } :: according to XBOOLE_0:def_10 ::_thesis: { t where t is Entry_Point_in_Subformula_Tree of G : t = t } c= entry_points_in_subformula_tree G
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in entry_points_in_subformula_tree G or x in { t where t is Entry_Point_in_Subformula_Tree of G : t = t } )
assume x in entry_points_in_subformula_tree G ; ::_thesis: x in { t where t is Entry_Point_in_Subformula_Tree of G : t = t }
then x in { t where t is Element of dom (tree_of_subformulae F) : (tree_of_subformulae F) . t = G } by Th19;
then consider t9 being Element of dom (tree_of_subformulae F) such that
A1: t9 = x and
A2: (tree_of_subformulae F) . t9 = G ;
reconsider t9 = t9 as Entry_Point_in_Subformula_Tree of G by A2, Def5;
t9 = t9 ;
hence x in { t where t is Entry_Point_in_Subformula_Tree of G : t = t } by A1; ::_thesis: verum
end;
thus { t where t is Entry_Point_in_Subformula_Tree of G : t = t } c= entry_points_in_subformula_tree G ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { t where t is Entry_Point_in_Subformula_Tree of G : t = t } or x in entry_points_in_subformula_tree G )
assume x in { t where t is Entry_Point_in_Subformula_Tree of G : t = t } ; ::_thesis: x in entry_points_in_subformula_tree G
then ex t being Entry_Point_in_Subformula_Tree of G st
( t = x & t = t ) ;
hence x in entry_points_in_subformula_tree G by Th35; ::_thesis: verum
end;
end;
theorem Th37: :: QC_LANG4:37
for A being QC-alphabet
for F being Element of QC-WFF A
for G1, G2 being Subformula of F
for t1 being Entry_Point_in_Subformula_Tree of G1
for s being Element of dom (tree_of_subformulae G1) st s in G1 -entry_points_in_subformula_tree_of G2 holds
t1 ^ s is Entry_Point_in_Subformula_Tree of G2
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for G1, G2 being Subformula of F
for t1 being Entry_Point_in_Subformula_Tree of G1
for s being Element of dom (tree_of_subformulae G1) st s in G1 -entry_points_in_subformula_tree_of G2 holds
t1 ^ s is Entry_Point_in_Subformula_Tree of G2
let F be Element of QC-WFF A; ::_thesis: for G1, G2 being Subformula of F
for t1 being Entry_Point_in_Subformula_Tree of G1
for s being Element of dom (tree_of_subformulae G1) st s in G1 -entry_points_in_subformula_tree_of G2 holds
t1 ^ s is Entry_Point_in_Subformula_Tree of G2
let G1, G2 be Subformula of F; ::_thesis: for t1 being Entry_Point_in_Subformula_Tree of G1
for s being Element of dom (tree_of_subformulae G1) st s in G1 -entry_points_in_subformula_tree_of G2 holds
t1 ^ s is Entry_Point_in_Subformula_Tree of G2
let t1 be Entry_Point_in_Subformula_Tree of G1; ::_thesis: for s being Element of dom (tree_of_subformulae G1) st s in G1 -entry_points_in_subformula_tree_of G2 holds
t1 ^ s is Entry_Point_in_Subformula_Tree of G2
let s be Element of dom (tree_of_subformulae G1); ::_thesis: ( s in G1 -entry_points_in_subformula_tree_of G2 implies t1 ^ s is Entry_Point_in_Subformula_Tree of G2 )
(tree_of_subformulae F) . t1 = G1 by Def5;
then A1: t1 in F -entry_points_in_subformula_tree_of G1 by Def3;
assume s in G1 -entry_points_in_subformula_tree_of G2 ; ::_thesis: t1 ^ s is Entry_Point_in_Subformula_Tree of G2
then A2: t1 ^ s in F -entry_points_in_subformula_tree_of G2 by A1, Th27;
F -entry_points_in_subformula_tree_of G2 c= dom (tree_of_subformulae F) by TREES_1:def_11;
then reconsider t9 = t1 ^ s as Element of dom (tree_of_subformulae F) by A2;
(tree_of_subformulae F) . t9 = G2 by A2, Def3;
hence t1 ^ s is Entry_Point_in_Subformula_Tree of G2 by Def5; ::_thesis: verum
end;
theorem :: QC_LANG4:38
for A being QC-alphabet
for F being Element of QC-WFF A
for G2, G1 being Subformula of F
for t1 being Entry_Point_in_Subformula_Tree of G1
for s being FinSequence st t1 ^ s is Entry_Point_in_Subformula_Tree of G2 holds
s in G1 -entry_points_in_subformula_tree_of G2
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for G2, G1 being Subformula of F
for t1 being Entry_Point_in_Subformula_Tree of G1
for s being FinSequence st t1 ^ s is Entry_Point_in_Subformula_Tree of G2 holds
s in G1 -entry_points_in_subformula_tree_of G2
let F be Element of QC-WFF A; ::_thesis: for G2, G1 being Subformula of F
for t1 being Entry_Point_in_Subformula_Tree of G1
for s being FinSequence st t1 ^ s is Entry_Point_in_Subformula_Tree of G2 holds
s in G1 -entry_points_in_subformula_tree_of G2
let G2, G1 be Subformula of F; ::_thesis: for t1 being Entry_Point_in_Subformula_Tree of G1
for s being FinSequence st t1 ^ s is Entry_Point_in_Subformula_Tree of G2 holds
s in G1 -entry_points_in_subformula_tree_of G2
let t1 be Entry_Point_in_Subformula_Tree of G1; ::_thesis: for s being FinSequence st t1 ^ s is Entry_Point_in_Subformula_Tree of G2 holds
s in G1 -entry_points_in_subformula_tree_of G2
let s be FinSequence; ::_thesis: ( t1 ^ s is Entry_Point_in_Subformula_Tree of G2 implies s in G1 -entry_points_in_subformula_tree_of G2 )
consider t9 being FinSequence such that
A1: t9 = t1 ^ s ;
(tree_of_subformulae F) . t1 = G1 by Def5;
then A2: t1 in F -entry_points_in_subformula_tree_of G1 by Def3;
assume t1 ^ s is Entry_Point_in_Subformula_Tree of G2 ; ::_thesis: s in G1 -entry_points_in_subformula_tree_of G2
then t9 in { t2 where t2 is Entry_Point_in_Subformula_Tree of G2 : t2 = t2 } by A1;
then t9 in entry_points_in_subformula_tree G2 by Th36;
hence s in G1 -entry_points_in_subformula_tree_of G2 by A2, A1, Th28; ::_thesis: verum
end;
theorem Th39: :: QC_LANG4:39
for A being QC-alphabet
for F being Element of QC-WFF A
for G1, G2 being Subformula of F holds { (t ^ s) where t is Entry_Point_in_Subformula_Tree of G1, s is Element of dom (tree_of_subformulae G1) : s in G1 -entry_points_in_subformula_tree_of G2 } = { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G1) : ( t in F -entry_points_in_subformula_tree_of G1 & s in G1 -entry_points_in_subformula_tree_of G2 ) }
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for G1, G2 being Subformula of F holds { (t ^ s) where t is Entry_Point_in_Subformula_Tree of G1, s is Element of dom (tree_of_subformulae G1) : s in G1 -entry_points_in_subformula_tree_of G2 } = { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G1) : ( t in F -entry_points_in_subformula_tree_of G1 & s in G1 -entry_points_in_subformula_tree_of G2 ) }
let F be Element of QC-WFF A; ::_thesis: for G1, G2 being Subformula of F holds { (t ^ s) where t is Entry_Point_in_Subformula_Tree of G1, s is Element of dom (tree_of_subformulae G1) : s in G1 -entry_points_in_subformula_tree_of G2 } = { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G1) : ( t in F -entry_points_in_subformula_tree_of G1 & s in G1 -entry_points_in_subformula_tree_of G2 ) }
let G1, G2 be Subformula of F; ::_thesis: { (t ^ s) where t is Entry_Point_in_Subformula_Tree of G1, s is Element of dom (tree_of_subformulae G1) : s in G1 -entry_points_in_subformula_tree_of G2 } = { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G1) : ( t in F -entry_points_in_subformula_tree_of G1 & s in G1 -entry_points_in_subformula_tree_of G2 ) }
thus { (t ^ s) where t is Entry_Point_in_Subformula_Tree of G1, s is Element of dom (tree_of_subformulae G1) : s in G1 -entry_points_in_subformula_tree_of G2 } c= { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G1) : ( t in F -entry_points_in_subformula_tree_of G1 & s in G1 -entry_points_in_subformula_tree_of G2 ) } :: according to XBOOLE_0:def_10 ::_thesis: { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G1) : ( t in F -entry_points_in_subformula_tree_of G1 & s in G1 -entry_points_in_subformula_tree_of G2 ) } c= { (t ^ s) where t is Entry_Point_in_Subformula_Tree of G1, s is Element of dom (tree_of_subformulae G1) : s in G1 -entry_points_in_subformula_tree_of G2 }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (t ^ s) where t is Entry_Point_in_Subformula_Tree of G1, s is Element of dom (tree_of_subformulae G1) : s in G1 -entry_points_in_subformula_tree_of G2 } or x in { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G1) : ( t in F -entry_points_in_subformula_tree_of G1 & s in G1 -entry_points_in_subformula_tree_of G2 ) } )
assume x in { (t ^ s) where t is Entry_Point_in_Subformula_Tree of G1, s is Element of dom (tree_of_subformulae G1) : s in G1 -entry_points_in_subformula_tree_of G2 } ; ::_thesis: x in { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G1) : ( t in F -entry_points_in_subformula_tree_of G1 & s in G1 -entry_points_in_subformula_tree_of G2 ) }
then consider t1 being Entry_Point_in_Subformula_Tree of G1, s1 being Element of dom (tree_of_subformulae G1) such that
A1: ( x = t1 ^ s1 & s1 in G1 -entry_points_in_subformula_tree_of G2 ) ;
(tree_of_subformulae F) . t1 = G1 by Def5;
then t1 in F -entry_points_in_subformula_tree_of G1 by Def3;
hence x in { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G1) : ( t in F -entry_points_in_subformula_tree_of G1 & s in G1 -entry_points_in_subformula_tree_of G2 ) } by A1; ::_thesis: verum
end;
thus { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G1) : ( t in F -entry_points_in_subformula_tree_of G1 & s in G1 -entry_points_in_subformula_tree_of G2 ) } c= { (t ^ s) where t is Entry_Point_in_Subformula_Tree of G1, s is Element of dom (tree_of_subformulae G1) : s in G1 -entry_points_in_subformula_tree_of G2 } ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G1) : ( t in F -entry_points_in_subformula_tree_of G1 & s in G1 -entry_points_in_subformula_tree_of G2 ) } or x in { (t ^ s) where t is Entry_Point_in_Subformula_Tree of G1, s is Element of dom (tree_of_subformulae G1) : s in G1 -entry_points_in_subformula_tree_of G2 } )
assume x in { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G1) : ( t in F -entry_points_in_subformula_tree_of G1 & s in G1 -entry_points_in_subformula_tree_of G2 ) } ; ::_thesis: x in { (t ^ s) where t is Entry_Point_in_Subformula_Tree of G1, s is Element of dom (tree_of_subformulae G1) : s in G1 -entry_points_in_subformula_tree_of G2 }
then consider t1 being Element of dom (tree_of_subformulae F), s1 being Element of dom (tree_of_subformulae G1) such that
A2: x = t1 ^ s1 and
A3: t1 in F -entry_points_in_subformula_tree_of G1 and
A4: s1 in G1 -entry_points_in_subformula_tree_of G2 ;
(tree_of_subformulae F) . t1 = G1 by A3, Def3;
then reconsider t1 = t1 as Entry_Point_in_Subformula_Tree of G1 by Def5;
x = t1 ^ s1 by A2;
hence x in { (t ^ s) where t is Entry_Point_in_Subformula_Tree of G1, s is Element of dom (tree_of_subformulae G1) : s in G1 -entry_points_in_subformula_tree_of G2 } by A4; ::_thesis: verum
end;
end;
theorem :: QC_LANG4:40
for A being QC-alphabet
for F being Element of QC-WFF A
for G1, G2 being Subformula of F holds { (t ^ s) where t is Entry_Point_in_Subformula_Tree of G1, s is Element of dom (tree_of_subformulae G1) : s in G1 -entry_points_in_subformula_tree_of G2 } c= entry_points_in_subformula_tree G2
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for G1, G2 being Subformula of F holds { (t ^ s) where t is Entry_Point_in_Subformula_Tree of G1, s is Element of dom (tree_of_subformulae G1) : s in G1 -entry_points_in_subformula_tree_of G2 } c= entry_points_in_subformula_tree G2
let F be Element of QC-WFF A; ::_thesis: for G1, G2 being Subformula of F holds { (t ^ s) where t is Entry_Point_in_Subformula_Tree of G1, s is Element of dom (tree_of_subformulae G1) : s in G1 -entry_points_in_subformula_tree_of G2 } c= entry_points_in_subformula_tree G2
let G1, G2 be Subformula of F; ::_thesis: { (t ^ s) where t is Entry_Point_in_Subformula_Tree of G1, s is Element of dom (tree_of_subformulae G1) : s in G1 -entry_points_in_subformula_tree_of G2 } c= entry_points_in_subformula_tree G2
{ (t ^ s) where t is Entry_Point_in_Subformula_Tree of G1, s is Element of dom (tree_of_subformulae G1) : s in G1 -entry_points_in_subformula_tree_of G2 } = { (t ^ s) where t is Element of dom (tree_of_subformulae F), s is Element of dom (tree_of_subformulae G1) : ( t in F -entry_points_in_subformula_tree_of G1 & s in G1 -entry_points_in_subformula_tree_of G2 ) } by Th39;
hence { (t ^ s) where t is Entry_Point_in_Subformula_Tree of G1, s is Element of dom (tree_of_subformulae G1) : s in G1 -entry_points_in_subformula_tree_of G2 } c= entry_points_in_subformula_tree G2 by Th29; ::_thesis: verum
end;
theorem :: QC_LANG4:41
for A being QC-alphabet
for F being Element of QC-WFF A
for G1, G2 being Subformula of F st ex t1 being Entry_Point_in_Subformula_Tree of G1 ex t2 being Entry_Point_in_Subformula_Tree of G2 st t1 is_a_prefix_of t2 holds
G2 is_subformula_of G1
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for G1, G2 being Subformula of F st ex t1 being Entry_Point_in_Subformula_Tree of G1 ex t2 being Entry_Point_in_Subformula_Tree of G2 st t1 is_a_prefix_of t2 holds
G2 is_subformula_of G1
let F be Element of QC-WFF A; ::_thesis: for G1, G2 being Subformula of F st ex t1 being Entry_Point_in_Subformula_Tree of G1 ex t2 being Entry_Point_in_Subformula_Tree of G2 st t1 is_a_prefix_of t2 holds
G2 is_subformula_of G1
let G1, G2 be Subformula of F; ::_thesis: ( ex t1 being Entry_Point_in_Subformula_Tree of G1 ex t2 being Entry_Point_in_Subformula_Tree of G2 st t1 is_a_prefix_of t2 implies G2 is_subformula_of G1 )
given t1 being Entry_Point_in_Subformula_Tree of G1, t2 being Entry_Point_in_Subformula_Tree of G2 such that A1: t1 is_a_prefix_of t2 ; ::_thesis: G2 is_subformula_of G1
( (tree_of_subformulae F) . t1 = G1 & (tree_of_subformulae F) . t2 = G2 ) by Def5;
hence G2 is_subformula_of G1 by A1, Th13; ::_thesis: verum
end;
theorem :: QC_LANG4:42
for A being QC-alphabet
for F being Element of QC-WFF A
for G2, G1 being Subformula of F st G2 is_subformula_of G1 holds
for t1 being Entry_Point_in_Subformula_Tree of G1 ex t2 being Entry_Point_in_Subformula_Tree of G2 st t1 is_a_prefix_of t2
proof
let A be QC-alphabet ; ::_thesis: for F being Element of QC-WFF A
for G2, G1 being Subformula of F st G2 is_subformula_of G1 holds
for t1 being Entry_Point_in_Subformula_Tree of G1 ex t2 being Entry_Point_in_Subformula_Tree of G2 st t1 is_a_prefix_of t2
let F be Element of QC-WFF A; ::_thesis: for G2, G1 being Subformula of F st G2 is_subformula_of G1 holds
for t1 being Entry_Point_in_Subformula_Tree of G1 ex t2 being Entry_Point_in_Subformula_Tree of G2 st t1 is_a_prefix_of t2
let G2, G1 be Subformula of F; ::_thesis: ( G2 is_subformula_of G1 implies for t1 being Entry_Point_in_Subformula_Tree of G1 ex t2 being Entry_Point_in_Subformula_Tree of G2 st t1 is_a_prefix_of t2 )
assume A1: G2 is_subformula_of G1 ; ::_thesis: for t1 being Entry_Point_in_Subformula_Tree of G1 ex t2 being Entry_Point_in_Subformula_Tree of G2 st t1 is_a_prefix_of t2
now__::_thesis:_for_t1_being_Entry_Point_in_Subformula_Tree_of_G1_ex_t2_being_Entry_Point_in_Subformula_Tree_of_G2_st_t1_is_a_prefix_of_t2
let t1 be Entry_Point_in_Subformula_Tree of G1; ::_thesis: ex t2 being Entry_Point_in_Subformula_Tree of G2 st t1 is_a_prefix_of t2
consider H being Element of QC-WFF A such that
A2: H = G2 ;
reconsider H = H as Subformula of G1 by A1, A2, Def4;
set s = the Entry_Point_in_Subformula_Tree of H;
(tree_of_subformulae G1) . the Entry_Point_in_Subformula_Tree of H = H by Def5;
then the Entry_Point_in_Subformula_Tree of H in G1 -entry_points_in_subformula_tree_of G2 by A2, Def3;
then t1 ^ the Entry_Point_in_Subformula_Tree of H is Entry_Point_in_Subformula_Tree of G2 by Th37;
then consider t2 being Entry_Point_in_Subformula_Tree of G2 such that
A3: t2 = t1 ^ the Entry_Point_in_Subformula_Tree of H ;
take t2 = t2; ::_thesis: t1 is_a_prefix_of t2
thus t1 is_a_prefix_of t2 by A3, TREES_1:1; ::_thesis: verum
end;
hence for t1 being Entry_Point_in_Subformula_Tree of G1 ex t2 being Entry_Point_in_Subformula_Tree of G2 st t1 is_a_prefix_of t2 ; ::_thesis: verum
end;