begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th4:
theorem
canceled;
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
begin
theorem
canceled;
theorem
canceled;
theorem Th28:
theorem
:: deftheorem Def1 defines list_of_immediate_constituents QC_LANG4:def 1 :
theorem Th30:
theorem Th31:
:: deftheorem Def2 defines tree_of_subformulae QC_LANG4:def 2 :
theorem
canceled;
theorem
canceled;
theorem Th34:
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem
theorem
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem
theorem Th47:
:: deftheorem Def3 defines -entry_points_in_subformula_tree_of QC_LANG4:def 3 :
theorem
canceled;
theorem Th49:
theorem Th50:
theorem Th51:
theorem Th52:
theorem Th53:
theorem Th54:
Lm1:
for x, y being set holds dom <*x,y*> = Seg 2
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem
theorem
:: deftheorem Def4 defines Subformula QC_LANG4:def 4 :
:: deftheorem Def5 defines Entry_Point_in_Subformula_Tree QC_LANG4:def 5 :
theorem
canceled;
theorem
:: deftheorem defines entry_points_in_subformula_tree QC_LANG4:def 6 :
theorem
canceled;
theorem Th67:
theorem Th68:
theorem Th69:
theorem
theorem Th71:
theorem
theorem
theorem