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

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

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

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

theorem Th4: :: QC_LANG4:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for r being FinSequence ex q being FinSequence st
( q = r | (Seg n) & q is_a_prefix_of r )
proof end;

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

theorem Th6: :: QC_LANG4:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for r being FinSequence of D
for r1, r2 being FinSequence
for k being Nat st k + 1 <= len r & r1 = r | (Seg (k + 1)) & r2 = r | (Seg k) holds
ex x being Element of D st r1 = r2 ^ <*x*>
proof end;

theorem Th7: :: QC_LANG4:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for r being FinSequence of D
for r1 being FinSequence st 1 <= len r & r1 = r | (Seg 1) holds
ex x being Element of D st r1 = <*x*>
proof end;

registration
let D be non empty set ;
cluster finite ParametrizedSubset of D;
existence
ex b1 being DecoratedTree of D st b1 is finite
proof end;
end;

theorem Th8: :: QC_LANG4:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being DecoratedTree
for p being FinSequence of NAT holds T . p = (T | p) . {}
proof end;

theorem Th9: :: QC_LANG4:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being finite-branching DecoratedTree
for t being Element of dom T holds succ T,t = T * (t succ )
proof end;

theorem Th10: :: QC_LANG4:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being finite-branching DecoratedTree
for t being Element of dom T holds dom (T * (t succ )) = dom (t succ )
proof end;

theorem Th11: :: QC_LANG4:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being finite-branching DecoratedTree
for t being Element of dom T holds dom (succ T,t) = dom (t succ )
proof end;

theorem Th12: :: QC_LANG4:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being finite-branching DecoratedTree
for t being Element of dom T
for n being Nat holds
( t ^ <*n*> in dom T iff n + 1 in dom (t succ ) )
proof end;

theorem Th13: :: QC_LANG4:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being finite-branching DecoratedTree
for x being FinSequence
for n being Nat st x ^ <*n*> in dom T holds
T . (x ^ <*n*>) = (succ T,x) . (n + 1)
proof end;

theorem Th14: :: QC_LANG4:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being finite-branching DecoratedTree
for x', x being Element of dom T st x' in succ x holds
T . x' in rng (succ T,x)
proof end;

theorem Th15: :: QC_LANG4:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being finite-branching DecoratedTree
for x being Element of dom T
for y' being set st y' in rng (succ T,x) holds
ex x' being Element of dom T st
( y' = T . x' & x' in succ x )
proof end;

scheme :: QC_LANG4:sch 1
ExDecTrees{ F1() -> non empty set , F2() -> Element of F1(), F3( set ) -> FinSequence of F1() } :
ex T being finite-branching DecoratedTree of F1() st
( T . {} = F2() & ( for t being Element of dom T
for w being Element of F1() st w = T . t holds
succ T,t = F3(w) ) )
proof end;

theorem Th16: :: QC_LANG4:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree
for t being Element of T holds ProperPrefixes t is finite Chain of T
proof end;

theorem Th17: :: QC_LANG4:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree holds T -level 0 = {{} }
proof end;

theorem Th18: :: QC_LANG4:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for T being Tree holds T -level (n + 1) = union { (succ w) where w is Element of T : len w = n }
proof end;

theorem Th19: :: QC_LANG4:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being finite-branching Tree
for n being Nat holds T -level n is finite
proof end;

theorem Th20: :: QC_LANG4:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being finite-branching Tree holds
( T is finite iff ex n being Nat st T -level n = {} )
proof end;

theorem Th21: :: QC_LANG4:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being finite-branching Tree st not T is finite holds
ex C being Chain of T st not C is finite
proof end;

theorem Th22: :: QC_LANG4:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being finite-branching Tree st not T is finite holds
ex B being Branch of T st not B is finite
proof end;

theorem Th23: :: QC_LANG4:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree
for C being Chain of T
for t being Element of T st t in C & not C is finite holds
ex t' being Element of T st
( t' in C & t is_a_proper_prefix_of t' )
proof end;

theorem Th24: :: QC_LANG4:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for T being Tree
for B being Branch of T
for t being Element of T st t in B & not B is finite holds
ex t' being Element of T st
( t' in B & t' in succ t )
proof end;

theorem Th25: :: QC_LANG4:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being Function of NAT , NAT st ( for n being Nat holds f . (n + 1) <= f . n ) holds
ex m being Nat st
for n being Nat st m <= n holds
f . n = f . m
proof end;

scheme :: QC_LANG4:sch 2
FinDecTree{ F1() -> non empty set , F2() -> finite-branching DecoratedTree of F1(), F3( Element of F1()) -> Nat } :
F2() is finite
provided
A1: for t, t' being Element of dom F2()
for d being Element of F1() st t' in succ t & d = F2() . t' holds
F3(d) < F3((F2() . t))
proof end;

theorem Th26: :: QC_LANG4:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for T being DecoratedTree of D
for y being set st y in rng T holds
y is Element of D
proof end;

theorem Th27: :: QC_LANG4:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for T being DecoratedTree of D
for x being set st x in dom T holds
T . x is Element of D
proof end;

theorem Th28: :: QC_LANG4:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being Element of QC-WFF st F is_subformula_of G holds
len (@ F) <= len (@ G)
proof end;

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

definition
let p be Element of QC-WFF ;
func list_of_immediate_constituents p -> FinSequence of QC-WFF equals :Def1: :: QC_LANG4:def 1
<*> QC-WFF if ( p = VERUM 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 or p is atomic ) implies <*> QC-WFF is FinSequence of QC-WFF ) & ( p is negative implies <*(the_argument_of p)*> is FinSequence of QC-WFF ) & ( p is conjunctive implies <*(the_left_argument_of p),(the_right_argument_of p)*> is FinSequence of QC-WFF ) & ( p = VERUM or p is atomic or p is negative or p is conjunctive or <*(the_scope_of p)*> is FinSequence of QC-WFF ) )
;
consistency
for b1 being FinSequence of QC-WFF holds
( ( ( p = VERUM or p is atomic ) & p is negative implies ( b1 = <*> QC-WFF iff b1 = <*(the_argument_of p)*> ) ) & ( ( p = VERUM or p is atomic ) & p is conjunctive implies ( b1 = <*> QC-WFF 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:51;
end;

:: deftheorem Def1 defines list_of_immediate_constituents QC_LANG4:def 1 :
for p being Element of QC-WFF holds
( ( ( p = VERUM or p is atomic ) implies list_of_immediate_constituents p = <*> QC-WFF ) & ( 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 or p is atomic or p is negative or p is conjunctive or list_of_immediate_constituents p = <*(the_scope_of p)*> ) );

theorem Th30: :: QC_LANG4:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k being Nat
for F, G being Element of QC-WFF st k in dom (list_of_immediate_constituents F) & G = (list_of_immediate_constituents F) . k holds
G is_immediate_constituent_of F
proof end;

theorem Th31: :: QC_LANG4:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF holds rng (list_of_immediate_constituents F) = { G where G is Element of QC-WFF : G is_immediate_constituent_of F }
proof end;

definition
let p be Element of QC-WFF ;
func tree_of_subformulae p -> finite DecoratedTree of QC-WFF 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 st
( b1 . {} = p & ( for x being Element of dom b1 holds succ b1,x = list_of_immediate_constituents (b1 . x) ) )
proof end;
uniqueness
for b1, b2 being finite DecoratedTree of QC-WFF 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 end;
end;

:: deftheorem Def2 defines tree_of_subformulae QC_LANG4:def 2 :
for p being Element of QC-WFF
for b2 being finite DecoratedTree of QC-WFF holds
( b2 = tree_of_subformulae p iff ( b2 . {} = p & ( for x being Element of dom b2 holds succ b2,x = list_of_immediate_constituents (b2 . x) ) ) );

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

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

theorem Th34: :: QC_LANG4:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF holds F in rng (tree_of_subformulae F)
proof end;

theorem Th35: :: QC_LANG4:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for F being Element of QC-WFF
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 st
( G = (tree_of_subformulae F) . (t ^ <*n*>) & G is_immediate_constituent_of (tree_of_subformulae F) . t )
proof end;

theorem Th36: :: QC_LANG4:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for H, F being Element of QC-WFF
for t being Element of dom (tree_of_subformulae F) holds
( H is_immediate_constituent_of (tree_of_subformulae F) . t iff ex n being Nat st
( t ^ <*n*> in dom (tree_of_subformulae F) & H = (tree_of_subformulae F) . (t ^ <*n*>) ) )
proof end;

theorem Th37: :: QC_LANG4:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G, F, H being Element of QC-WFF st G in rng (tree_of_subformulae F) & H is_immediate_constituent_of G holds
H in rng (tree_of_subformulae F)
proof end;

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

theorem Th39: :: QC_LANG4:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G, F being Element of QC-WFF holds
( G in rng (tree_of_subformulae F) iff G is_subformula_of F )
proof end;

theorem :: QC_LANG4:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF holds rng (tree_of_subformulae F) = Subformulae F
proof end;

theorem :: QC_LANG4:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for t', t being Element of dom (tree_of_subformulae F) st t' in succ t holds
(tree_of_subformulae F) . t' is_immediate_constituent_of (tree_of_subformulae F) . t
proof end;

theorem Th42: :: QC_LANG4:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for t, t' being Element of dom (tree_of_subformulae F) st t is_a_prefix_of t' holds
(tree_of_subformulae F) . t' is_subformula_of (tree_of_subformulae F) . t
proof end;

theorem Th43: :: QC_LANG4:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for t, t' being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t' holds
len (@ ((tree_of_subformulae F) . t')) < len (@ ((tree_of_subformulae F) . t))
proof end;

theorem Th44: :: QC_LANG4:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for t, t' being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t' holds
(tree_of_subformulae F) . t' <> (tree_of_subformulae F) . t
proof end;

theorem Th45: :: QC_LANG4:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for t, t' being Element of dom (tree_of_subformulae F) st t is_a_proper_prefix_of t' holds
(tree_of_subformulae F) . t' is_proper_subformula_of (tree_of_subformulae F) . t
proof end;

theorem :: QC_LANG4:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for t being Element of dom (tree_of_subformulae F) holds
( (tree_of_subformulae F) . t = F iff t = {} )
proof end;

theorem Th47: :: QC_LANG4:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for t, t' being Element of dom (tree_of_subformulae F) st t <> t' & (tree_of_subformulae F) . t = (tree_of_subformulae F) . t' holds
not t,t' are_c=-comparable
proof end;

definition
let F, G be Element of QC-WFF ;
func F -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 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 end;
end;

:: deftheorem Def3 defines -entry_points_in_subformula_tree_of QC_LANG4:def 3 :
for F, G being Element of QC-WFF
for b3 being AntiChain_of_Prefixes of dom (tree_of_subformulae F) holds
( b3 = F -entry_points_in_subformula_tree_of G iff for t being Element of dom (tree_of_subformulae F) holds
( t in b3 iff (tree_of_subformulae F) . t = G ) );

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

theorem Th49: :: QC_LANG4:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being Element of QC-WFF holds F -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 end;

theorem Th50: :: QC_LANG4:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G, F being Element of QC-WFF holds
( G is_subformula_of F iff F -entry_points_in_subformula_tree_of G <> {} )
proof end;

theorem Th51: :: QC_LANG4:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat
for F being Element of QC-WFF
for t', t being Element of dom (tree_of_subformulae F) st t' = t ^ <*m*> & (tree_of_subformulae F) . t is negative holds
( (tree_of_subformulae F) . t' = the_argument_of ((tree_of_subformulae F) . t) & m = 0 )
proof end;

theorem Th52: :: QC_LANG4:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat
for F being Element of QC-WFF
for t', t being Element of dom (tree_of_subformulae F) st t' = t ^ <*m*> & (tree_of_subformulae F) . t is conjunctive & not ( (tree_of_subformulae F) . t' = the_left_argument_of ((tree_of_subformulae F) . t) & m = 0 ) holds
( (tree_of_subformulae F) . t' = the_right_argument_of ((tree_of_subformulae F) . t) & m = 1 )
proof end;

theorem Th53: :: QC_LANG4:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m being Nat
for F being Element of QC-WFF
for t', t being Element of dom (tree_of_subformulae F) st t' = t ^ <*m*> & (tree_of_subformulae F) . t is universal holds
( (tree_of_subformulae F) . t' = the_scope_of ((tree_of_subformulae F) . t) & m = 0 )
proof end;

theorem Th54: :: QC_LANG4:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for 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 end;

Lm1: for x, y being set holds dom <*x,y*> = Seg 2
proof end;

theorem Th55: :: QC_LANG4:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for 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 end;

theorem Th56: :: QC_LANG4:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for 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 end;

theorem Th57: :: QC_LANG4:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G, H being Element of QC-WFF
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 end;

theorem Th58: :: QC_LANG4:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G, H being Element of QC-WFF
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 end;

theorem Th59: :: QC_LANG4:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G, H being Element of QC-WFF holds { (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 end;

theorem Th60: :: QC_LANG4:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for t being Element of dom (tree_of_subformulae F) holds (tree_of_subformulae F) | t = tree_of_subformulae ((tree_of_subformulae F) . t)
proof end;

theorem Th61: :: QC_LANG4:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being Element of QC-WFF
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 end;

theorem :: QC_LANG4:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G being Element of QC-WFF holds F -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 end;

theorem :: QC_LANG4:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F, G, H being Element of QC-WFF
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 end;

definition
let F be Element of QC-WFF ;
mode Subformula of F -> Element of QC-WFF means :Def4: :: QC_LANG4:def 4
it is_subformula_of F;
existence
ex b1 being Element of QC-WFF st b1 is_subformula_of F
;
end;

:: deftheorem Def4 defines Subformula QC_LANG4:def 4 :
for F, b2 being Element of QC-WFF holds
( b2 is Subformula of F iff b2 is_subformula_of F );

definition
let F be Element of QC-WFF ;
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 end;
end;

:: deftheorem Def5 defines Entry_Point_in_Subformula_Tree QC_LANG4:def 5 :
for F being Element of QC-WFF
for G being Subformula of F
for b3 being Element of dom (tree_of_subformulae F) holds
( b3 is Entry_Point_in_Subformula_Tree of G iff (tree_of_subformulae F) . b3 = G );

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

theorem :: QC_LANG4:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for G being Subformula of F
for t, t' being Entry_Point_in_Subformula_Tree of G st t <> t' holds
not t,t' are_c=-comparable
proof end;

definition
let F be Element of QC-WFF ;
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 end;
end;

:: deftheorem defines entry_points_in_subformula_tree QC_LANG4:def 6 :
for F being Element of QC-WFF
for G being Subformula of F holds entry_points_in_subformula_tree G = F -entry_points_in_subformula_tree_of G;

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

theorem Th67: :: QC_LANG4:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for 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 end;

theorem Th68: :: QC_LANG4:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for 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 end;

theorem Th69: :: QC_LANG4:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for 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 end;

theorem :: QC_LANG4:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for 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 end;

theorem Th71: :: QC_LANG4:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for 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 end;

theorem :: QC_LANG4:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for 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 end;

theorem :: QC_LANG4:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for 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 end;

theorem :: QC_LANG4:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for F being Element of QC-WFF
for 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 end;