Logiweb dictionary of Frozen

Up Help

0 0 Frozen 1 1 ContainsEmpty(∗) 2 2 Dedu(∗, ∗) 3 2 Dedu_{0}(∗, ∗) 4 3 Dedu_{s}(∗, ∗, ∗) 5 3 Dedu_{1}(∗, ∗, ∗) 6 3 Dedu_{2}(∗, ∗, ∗) 7 4 Dedu_{3}(∗, ∗, ∗, ∗) 8 4 Dedu_{4}(∗, ∗, ∗, ∗) 9 4 Dedu_{4}^{∗}(∗, ∗, ∗, ∗) 10 3 Dedu_{5}(∗, ∗, ∗) 11 4 Dedu_{6}(∗, ∗, ∗, ∗) 12 4 Dedu_{6}^{∗}(∗, ∗, ∗, ∗) 13 1 Dedu_{7}(∗) 14 2 Dedu_{8}(∗, ∗) 15 2 Dedu_{8}^{∗}(∗, ∗) 16 0 (⋯)

17 0 Objekt-var
18 0 Ex-var
19 0 Ph-var
20 0 Værdi
21 0 Variabel

22 2 Op(∗, ∗) 23 1 Op(∗) 24 0 ph_{1} 25 0 ph_{2} 26 0 ph_{3} 27 1 ∗_{Ph} 28 1 ∗^{Ph} 29 4 ⟨∗≡ ∗ | ∗:=∗⟩_{Ph} 30 4 ⟨∗≡^{0} ∗ | ∗:=∗⟩_{Ph} 31 4 ⟨∗≡^{1} ∗ | ∗:=∗⟩_{Ph} 32 4 ⟨∗≡^{∗} ∗ | ∗:=∗⟩_{Ph} 33 1 ∗_{Ex} 34 1 ∗^{Ex} 35 0 Ex_{1} 36 0 Ex_{2} 37 0 Ex_{10} 38 0 Ex_{20} 39 4 ⟨∗≡ ∗ | ∗:=∗⟩_{Ex} 40 4 ⟨∗≡^{0} ∗ | ∗:=∗⟩_{Ex} 41 4 ⟨∗≡^{1} ∗ | ∗:=∗⟩_{Ex} 42 4 ⟨∗≡^{∗} ∗ | ∗:=∗⟩_{Ex}

43 0 var big set
44 0 OBS
45 0 BS

46 0 ZF ∗ 47 0 MP 48 0 Gen 49 0 Ded 50 0 Neg 51 0 Repetition 52 0 ExistIntro 53 0 Extensionality 54 0 SeparationDef 55 0 PairDef 56 0 UnionDef 57 0 PowerDef

58 0 axiom empty set

59 0 Cheat − AllDisjoint 60 0 Ø 61 0 Sep2Formula 62 0 Formula2Sep 63 0 HelperEqNecessary 64 0 EqNecessary 65 0 HelperTransSubset 66 0 TransSubset 67 0 ToSetEquality 68 0 Weakening 69 0 NegativeMT 70 0 MP2 71 0 MP3 72 0 MP4 73 0 MP5 74 0 Technicality 75 0 MT 76 0 AddDoubleNeg 77 0 RemoveDoubleNeg 78 0 AndCommutativity 79 0 FirstConjunct 80 0 SecondConjunct 81 0 JoinConjuncts 82 0 IffFirst 83 0 IffSecond 84 0 Contrapositive 85 0 FromContradiction

86 0 lemma er is reflexive

87 0 ERisSymmetric 88 0 ERisTransitive 89 0 HelperReflexivity 90 0 Reflexivity 91 0 HelperSymmetry 92 0 Symmetry 93 0 HelperTransitivity 94 0 Transitivity 95 0 AutoMember 96 0 HelperFromSetEquality 97 0 FromSetEquality 98 0 EmptySetSub 99 0 HelperUniqueEmptySet 100 0 UniqueEmptySet 101 0 HelperNoneEqNecessary 102 0 Helper(2)NoneEqNecessary 103 0 NoneEqNecessary 104 0 AutoImply 105 0 ImplyTransitivity 106 0 MemberNotEmpty 107 0 HelperMemberNotEmpty 108 0 = Reflexivity 109 0 = Symmetry 110 0 Helper = Transitivity 111 0 = Transitivity 112 0 Formula2Union 113 0 Union2Formula 114 0 SubsetTransitive 115 0 SubsetInPower 116 0 HelperPowerIsSub 117 0 Helper(Switch)PowerIsSub 118 0 PowerIsSub 119 0 PowerIsSub − Switch 120 0 EqClassIsSubset 121 0 BS − subset 122 0 Union(BS − R) − subset 123 0 Union − Identity 124 0 HelperEqSysNotØ 125 0 EqSysNotØ 126 0 WeakenOr1 127 0 WeakenOr2 128 0 FromDisjuncts 129 0 IffCommutativity 130 0 Pair2Formula

131 0 lemma set equality suff condition(t)0
132 0 lemma set equality suff condition(t)

133 0 Formula2Pair 134 0 HelperPairSubset 135 0 Helper(2)PairSubset 136 0 PairSubset 137 0 SamePair 138 0 SameSingleton 139 0 HelperSameUnion 140 0 SameUnion 141 0 SeparationSubset 142 0 SameBinaryUnion 143 0 SameSeparation 144 0 IntersectionSubset 145 0 SameIntersection 146 0 EqClassesAreDisjoint 147 0 HelperTransfer ≠ 148 0 Transfer ≠ 149 0 AllDisjoint 150 0 Imply − AllDisjoint 151 0 Eq − SystemIsPartition 152 2 ∗ ∩ ∗ 153 2 ∗ \ ∗ 154 1 ∪∗ 155 1 P(∗) 156 2 ∗ ∪ ∗ 157 1 {∗} 158 2 {∗, ∗} 159 2 ⟨∗, ∗⟩ 160 2 ∗ ∈ ∗ 161 2 ∗ ∉ ∗ 162 2 Partition(∗, ∗) 163 3 ∗(∗, ∗) 164 2 ReflRel(∗, ∗)

165 2 SymRel(∗, ∗) 166 2 TransRel(∗, ∗) 167 2 EqRel(∗, ∗) 168 3 [∗ ∈ ∗]_{∗} 169 2 ∗ = ∗ 170 2 ∗ ⊆ ∗ 171 1 ˙¬ ∗ 172 2 ∗ ≠ ∗ 173 2 ∗ ˙∧ ∗ 174 2 ∗ ˙∨ ∗ 175 2 ∗ ˙⇔ ∗ 176 2 {ph ∈ ∗ | ∗}

The pyk compiler, version 0.grue.20060417+ by Klaus Grue GRD-2006-06-21.UTC:07:04:17.579248 = MJD-53907.TAI:07:04:50.579248 = LGT-4657590290579248e-6