let A be 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
let F, G, H be 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 t be 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 s be FinSequence; ( 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[ 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 Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A2:
S1[
k]
;
S1[k + 1]
thus
S1[
k + 1]
verumproof
let F,
G,
H be
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 = k + 1 holds
s in G -entry_points_in_subformula_tree_of Hlet t be
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 Hlet s be
FinSequence;
( 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
;
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) )
hence
s in G -entry_points_in_subformula_tree_of H
by A6, Def3;
verum
end;
end;
A23:
S1[ 0 ]
for k being Nat holds S1[k]
from NAT_1:sch 2(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 )
; s in G -entry_points_in_subformula_tree_of H
hence
s in G -entry_points_in_subformula_tree_of H
by A29, Def3; verum