:: The Subformula Tree of a Formula of the First Order Language
:: by Oleg Okhotnikov
::
:: Received October 2, 1995
:: Copyright (c) 1995 Association of Mizar Users
theorem :: QC_LANG4:1
canceled;
theorem :: QC_LANG4:2
canceled;
theorem :: QC_LANG4:3
canceled;
theorem Th4: :: QC_LANG4:4
theorem :: QC_LANG4:5
canceled;
theorem Th6: :: QC_LANG4:6
theorem Th7: :: QC_LANG4:7
theorem Th8: :: QC_LANG4:8
theorem Th9: :: QC_LANG4:9
theorem Th10: :: QC_LANG4:10
theorem Th11: :: QC_LANG4:11
theorem Th12: :: QC_LANG4:12
theorem Th13: :: QC_LANG4:13
theorem Th14: :: QC_LANG4:14
theorem Th15: :: QC_LANG4:15
theorem Th16: :: QC_LANG4:16
theorem Th17: :: QC_LANG4:17
theorem Th18: :: QC_LANG4:18
theorem Th19: :: QC_LANG4:19
theorem Th20: :: QC_LANG4:20
theorem Th21: :: QC_LANG4:21
theorem Th22: :: QC_LANG4:22
theorem Th23: :: QC_LANG4:23
theorem Th24: :: QC_LANG4:24
theorem Th25: :: QC_LANG4:25
theorem Th26: :: QC_LANG4:26
theorem Th27: :: QC_LANG4:27
theorem Th28: :: QC_LANG4:28
theorem :: QC_LANG4:29
:: deftheorem Def1 defines list_of_immediate_constituents QC_LANG4:def 1 :
theorem Th30: :: QC_LANG4:30
theorem Th31: :: QC_LANG4:31
:: deftheorem Def2 defines tree_of_subformulae QC_LANG4:def 2 :
theorem :: QC_LANG4:32
canceled;
theorem :: QC_LANG4:33
canceled;
theorem Th34: :: QC_LANG4:34
theorem Th35: :: QC_LANG4:35
theorem Th36: :: QC_LANG4:36
theorem Th37: :: QC_LANG4:37
theorem Th38: :: QC_LANG4:38
theorem Th39: :: QC_LANG4:39
theorem :: QC_LANG4:40
theorem :: QC_LANG4:41
theorem Th42: :: QC_LANG4:42
theorem Th43: :: QC_LANG4:43
theorem Th44: :: QC_LANG4:44
theorem Th45: :: QC_LANG4:45
theorem :: QC_LANG4:46
theorem Th47: :: QC_LANG4:47
:: deftheorem Def3 defines -entry_points_in_subformula_tree_of QC_LANG4:def 3 :
theorem :: QC_LANG4:48
canceled;
theorem Th49: :: QC_LANG4:49
theorem Th50: :: QC_LANG4:50
theorem Th51: :: QC_LANG4:51
theorem Th52: :: QC_LANG4:52
theorem Th53: :: QC_LANG4:53
theorem Th54: :: QC_LANG4:54
Lm1:
for x, y being set holds dom <*x,y*> = Seg 2
theorem Th55: :: QC_LANG4:55
theorem Th56: :: QC_LANG4:56
theorem Th57: :: QC_LANG4:57
theorem Th58: :: QC_LANG4:58
theorem Th59: :: QC_LANG4:59
theorem Th60: :: QC_LANG4:60
theorem Th61: :: QC_LANG4:61
theorem :: QC_LANG4:62
theorem :: QC_LANG4:63
:: deftheorem Def4 defines Subformula QC_LANG4:def 4 :
:: deftheorem Def5 defines Entry_Point_in_Subformula_Tree QC_LANG4:def 5 :
theorem :: QC_LANG4:64
canceled;
theorem :: QC_LANG4:65
:: deftheorem defines entry_points_in_subformula_tree QC_LANG4:def 6 :
theorem :: QC_LANG4:66
canceled;
theorem Th67: :: QC_LANG4:67
theorem Th68: :: QC_LANG4:68
theorem Th69: :: QC_LANG4:69
theorem :: QC_LANG4:70
theorem Th71: :: QC_LANG4:71
theorem :: QC_LANG4:72
theorem :: QC_LANG4:73
theorem :: QC_LANG4:74