use(subst). use(int). use(pbeta). %use(int_lemmas). use(cd). use(comp_th). use(lemmaP2). lemmaP2(S,T,U,V,I). %noetig % Induktion ueber pbeta goal %Induktionsanfang comp_th(var(i),var(i)), % 1. Induktionsschritt ((comp_th(s,t) and pbeta(s,t)) => comp_th(abs(s),abs(t))), % 2. Induktionsschritt, in drei Faelle unterteilt ((comp_th(var(i),t) and comp_th(u,v) and pbeta(u,v) and pbeta(var(i),t)) => comp_th(app(var(i),u),app(t,v))), ((comp_th(app(x,y),t) and comp_th(u,v) and pbeta(u,v) and pbeta(app(x,y),t)) => comp_th(app(app(x,y),u),app(t,v))), % Bei folgender Induktionsvorraussetzung wird benutzt, dass bei pbeta(abs(s),x) % x immer aus abs(t) fuer ein t bestehen muss ((comp_th(s,t) and comp_th(u,v) and pbeta(s,t) and pbeta(u,v)) => comp_th(app(abs(s),u),app(abs(t),v))), % 3. Induktionsschritt ((comp_th(s,t) and comp_th(u,v) and pbeta(s,t) and pbeta(u,v)) => comp_th(app(abs(s),u),subst(t,0,v))) -> []. top_predicates_precedence([comp_th,lemmaP2]). option([var_overlaps(off),search_depth(0)]). :-sarp(+[15]),saci([2]). /* Proof: ====== 40 : pbeta(A,B) -> pbeta(abs(A),abs(B)) [input] 41 : pbeta(A,B) -> pbeta(C,D)=>pbeta(app(A,C),app(B,D)) [input] 42 : pbeta(A,B) -> pbeta(C,D)=>pbeta(app(abs(A),C),subst(B,0,D)) [input] 43 : pbeta(A,A) [input] 44 : cd(var(A))=var(A) [input] 45 : cd(app(var(A),B))=app(var(A),cd(B)) [input] 46 : cd(app(app(A,B),C))=app(cd(app(A,B)),cd(C)) [input] 47 : cd(app(abs(A),B))=subst(cd(A),0,cd(B)) [input] 48 : cd(abs(A))=abs(cd(A)) [input] 49 : comp_th(A,B)==(pbeta(A,B)=>pbeta(B,cd(A))) [input] 50 : lemmaP2(A,B,C,D,E)==(0=pbeta(subst(C,E,A),subst(D,E,B))) [input] 51 : lemmaP2(A,B,C,D,E) [input] 52 + comp_th(var(i),var(i)),comp_th(s,t)and pbeta(s,t)=>comp_th(abs(s),abs(t)),comp_th(var(i),t)and comp_th(u,v)and pbeta(u,v)and pbeta(var(i),t)=>comp_th(app(var(i),u),app(t,v)),comp_th(app(x,y),t)and comp_th(u,v)and pbeta(u,v)and pbeta(app(x,y),t)=>comp_th(app(app(x,y),u),app(t,v)),comp_th(s,t)and comp_th(u,v)and pbeta(s,t)and pbeta(u,v)=>comp_th(app(abs(s),u),app(abs(t),v)),comp_th(s,t)and comp_th(u,v)and pbeta(s,t)and pbeta(u,v)=>comp_th(app(abs(s),u),subst(t,0,v)) -> [input] 64 : pbeta(A,B),pbeta(C,D) -> pbeta(app(A,C),app(B,D)) [expansion from 41] 65 : pbeta(A,B),pbeta(C,D) -> pbeta(app(abs(A),C),subst(B,0,D)) [expansion from 42] 66 : 0=pbeta(subst(D,A,B),subst(E,A,C)) [reduction of 51 by [50]] 67 : pbeta(A,B),0= pbeta(subst(A,C,D),subst(B,C,E)) [expansion from 66] 68 : pbeta(A,B),pbeta(C,D) -> E<0,pbeta(subst(A,E,C),subst(B,E,D)) [totality resolution from 67] 69 + (pbeta(s,t)=>pbeta(t,cd(s)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(s,t)and pbeta(u,v)=>pbeta(app(abs(s),u),app(abs(t),v))=>pbeta(app(abs(t),v),subst(cd(s),0,cd(u))),(pbeta(app(x,y),t)=>pbeta(t,cd(app(x,y))))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(u,v)and pbeta(app(x,y),t)=>pbeta(app(app(x,y),u),app(t,v))=>pbeta(app(t,v),app(cd(app(x,y)),cd(u))),(pbeta(var(i),t)=>pbeta(t,var(i)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(u,v)and pbeta(var(i),t)=>pbeta(app(var(i),u),app(t,v))=>pbeta(app(t,v),app(var(i),cd(u))),(pbeta(s,t)=>pbeta(t,cd(s)))and pbeta(s,t)=>pbeta(abs(s),abs(t))=>pbeta(abs(t),abs(cd(s))),(pbeta(s,t)=>pbeta(t,cd(s)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(s,t)and pbeta(u,v)=>pbeta(app(abs(s),u),subst(t,0,v))=>pbeta(subst(t,0,v),subst(cd(s),0,cd(u))) -> [reduction of 52 by [49,44,43,43,L,49,48,49,49,45,49,49,44,49,46,49,49,49,47,49,49,49,47,49,49]] 70 + p$199,(pbeta(var(i),t)=>pbeta(t,var(i)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(u,v)and pbeta(var(i),t)=>pbeta(app(var(i),u),app(t,v))=>pbeta(app(t,v),app(var(i),cd(u))),(pbeta(s,t)=>pbeta(t,cd(s)))and pbeta(s,t)=>pbeta(abs(s),abs(t))=>pbeta(abs(t),abs(cd(s))),(pbeta(s,t)=>pbeta(t,cd(s)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(s,t)and pbeta(u,v)=>pbeta(app(abs(s),u),app(abs(t),v))=>pbeta(app(abs(t),v),subst(cd(s),0,cd(u))),(pbeta(app(x,y),t)=>pbeta(t,cd(app(x,y))))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(u,v)and pbeta(app(x,y),t)=>pbeta(app(app(x,y),u),app(t,v))=>pbeta(app(t,v),app(cd(app(x,y)),cd(u))) -> [expansion from 69] 71 + p$199,(pbeta(s,t)=>pbeta(t,cd(s)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(s,t)and pbeta(u,v) [expansion from 69] 72 + pbeta(app(abs(s),u),subst(t,0,v))=>pbeta(subst(t,0,v),subst(cd(s),0,cd(u))) -> p$199 [expansion from 69] 73 + p$198,(pbeta(s,t)=>pbeta(t,cd(s)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(s,t)and pbeta(u,v)=>pbeta(app(abs(s),u),app(abs(t),v))=>pbeta(app(abs(t),v),subst(cd(s),0,cd(u))),(pbeta(var(i),t)=>pbeta(t,var(i)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(u,v)and pbeta(var(i),t)=>pbeta(app(var(i),u),app(t,v))=>pbeta(app(t,v),app(var(i),cd(u))),(pbeta(s,t)=>pbeta(t,cd(s)))and pbeta(s,t)=>pbeta(abs(s),abs(t))=>pbeta(abs(t),abs(cd(s))),p$199 -> [expansion from 70] 74 + p$198,(pbeta(app(x,y),t)=>pbeta(t,cd(app(x,y))))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(u,v)and pbeta(app(x,y),t) [expansion from 70] 75 + pbeta(app(app(x,y),u),app(t,v))=>pbeta(app(t,v),app(cd(app(x,y)),cd(u))) -> p$198 [expansion from 70] 76 + p$197,p$199 [expansion from 71] 77 + p$197 -> (pbeta(s,t)=>pbeta(t,cd(s)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(s,t) [expansion from 71] 78 + p$197 -> pbeta(u,v) [expansion from 71] 79 + p$196 -> p$199 [expansion from 72] 81 + pbeta(subst(t,0,v),subst(cd(s),0,cd(u))) -> p$196 [expansion from 72] 82 + p$195,p$198 [expansion from 74] 83 + p$195 -> (pbeta(app(x,y),t)=>pbeta(t,cd(app(x,y))))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(u,v) [expansion from 74] 84 + p$195 -> pbeta(app(x,y),t) [expansion from 74] 85 + p$194 -> p$198 [expansion from 75] 87 + pbeta(app(t,v),app(cd(app(x,y)),cd(u))) -> p$194 [expansion from 75] 88 + p$199,pbeta(u,v) [negative chaining of 76 from 78] 89 + p$198,pbeta(app(x,y),t) [negative chaining of 82 from 84] 90 + p$199,(pbeta(s,t)=>pbeta(t,cd(s)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(s,t) [negative chaining of 76 from 77] 91 + p$199,(pbeta(s,t)=>pbeta(t,cd(s)))and pbeta(v,cd(u))and pbeta(s,t) [reduction of 90 by [88,L]] 92 + p$193,p$199 [expansion from 91] 93 + p$193 -> (pbeta(s,t)=>pbeta(t,cd(s)))and pbeta(v,cd(u)) [expansion from 91] 94 + p$193 -> pbeta(s,t) [expansion from 91] 95 + p$199,pbeta(s,t) [negative chaining of 92 from 94] 96 + p$199,(pbeta(s,t)=>pbeta(t,cd(s)))and pbeta(v,cd(u)) [negative chaining of 92 from 93] 97 + p$199,pbeta(t,cd(s))and pbeta(v,cd(u)) [reduction of 96 by [95,L]] 98 + p$192,p$199 [expansion from 97] 99 + p$192 -> pbeta(t,cd(s)) [expansion from 97] 100 + p$192 -> pbeta(v,cd(u)) [expansion from 97] 101 + p$199,pbeta(t,cd(s)) [negative chaining of 98 from 99] 102 + p$199,pbeta(v,cd(u)) [negative chaining of 98 from 100] 103 + p$198,(pbeta(app(x,y),t)=>pbeta(t,cd(app(x,y))))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(u,v) [negative chaining of 82 from 83] 104 + p$198,pbeta(t,cd(app(x,y)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(u,v) [reduction of 103 by [89,L]] 105 + p$191,p$198 [expansion from 104] 106 + p$191 -> pbeta(t,cd(app(x,y)))and(pbeta(u,v)=>pbeta(v,cd(u))) [expansion from 104] 107 + p$191 -> pbeta(u,v) [expansion from 104] 108 + p$198,pbeta(u,v) [negative chaining of 105 from 107] 109 + p$198,pbeta(t,cd(app(x,y)))and(pbeta(u,v)=>pbeta(v,cd(u))) [negative chaining of 105 from 106] 110 + p$198,pbeta(t,cd(app(x,y)))and pbeta(v,cd(u)) [reduction of 109 by [108,L]] 111 + p$190,p$198 [expansion from 110] 112 + p$190 -> pbeta(t,cd(app(x,y))) [expansion from 110] 113 + p$190 -> pbeta(v,cd(u)) [expansion from 110] 114 + p$198,pbeta(v,cd(u)) [negative chaining of 111 from 113] 115 + p$198,pbeta(t,cd(app(x,y))) [negative chaining of 111 from 112] 116 + pbeta(t,cd(app(x,y))),pbeta(v,cd(u)) -> p$194 [negative chaining of 64 from 87] 118 + pbeta(t,cd(app(x,y))) -> p$198,p$194 [negative chaining of 114 from 116] 119 + p$198 [reduction of 118 by [115,85,L]] 120 + (pbeta(s,t)=>pbeta(t,cd(s)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(s,t)and pbeta(u,v)=>pbeta(app(abs(s),u),app(abs(t),v))=>pbeta(app(abs(t),v),subst(cd(s),0,cd(u))),(pbeta(var(i),t)=>pbeta(t,var(i)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(u,v)and pbeta(var(i),t)=>pbeta(app(var(i),u),app(t,v))=>pbeta(app(t,v),app(var(i),cd(u))),(pbeta(s,t)=>pbeta(t,cd(s)))and pbeta(s,t)=>pbeta(abs(s),abs(t))=>pbeta(abs(t),abs(cd(s))),p$199 -> [reduction of 73 by [119]] 121 + pbeta(t,cd(s)),pbeta(v,cd(u)) -> p$196 [negative chaining of 68 from 81] 122 + pbeta(t,cd(s)) -> p$199,p$196 [negative chaining of 102 from 121] 123 + p$199 [reduction of 122 by [101,79,L]] 124 + (pbeta(s,t)=>pbeta(t,cd(s)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(s,t)and pbeta(u,v)=>pbeta(app(abs(s),u),app(abs(t),v))=>pbeta(app(abs(t),v),subst(cd(s),0,cd(u))),(pbeta(var(i),t)=>pbeta(t,var(i)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(u,v)and pbeta(var(i),t)=>pbeta(app(var(i),u),app(t,v))=>pbeta(app(t,v),app(var(i),cd(u))),(pbeta(s,t)=>pbeta(t,cd(s)))and pbeta(s,t)=>pbeta(abs(s),abs(t))=>pbeta(abs(t),abs(cd(s))) -> [reduction of 120 by [123]] 125 + p$189,(pbeta(var(i),t)=>pbeta(t,var(i)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(u,v)and pbeta(var(i),t)=>pbeta(app(var(i),u),app(t,v))=>pbeta(app(t,v),app(var(i),cd(u))),(pbeta(s,t)=>pbeta(t,cd(s)))and pbeta(s,t)=>pbeta(abs(s),abs(t))=>pbeta(abs(t),abs(cd(s))) -> [expansion from 124] 126 + p$189,(pbeta(s,t)=>pbeta(t,cd(s)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(s,t)and pbeta(u,v) [expansion from 124] 127 + pbeta(app(abs(s),u),app(abs(t),v))=>pbeta(app(abs(t),v),subst(cd(s),0,cd(u))) -> p$189 [expansion from 124] 128 + p$188,(pbeta(s,t)=>pbeta(t,cd(s)))and pbeta(s,t)=>pbeta(abs(s),abs(t))=>pbeta(abs(t),abs(cd(s))),p$189 -> [expansion from 125] 129 + p$188,(pbeta(var(i),t)=>pbeta(t,var(i)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(u,v)and pbeta(var(i),t) [expansion from 125] 130 + pbeta(app(var(i),u),app(t,v))=>pbeta(app(t,v),app(var(i),cd(u))) -> p$188 [expansion from 125] 131 + p$197,p$189 [expansion from 126] 132 + p$187,p$188,p$189 -> [expansion from 128] 133 + p$187,(pbeta(s,t)=>pbeta(t,cd(s)))and pbeta(s,t) [expansion from 128] 134 + pbeta(abs(s),abs(t))=>pbeta(abs(t),abs(cd(s))) -> p$187 [expansion from 128] 135 + p$186,p$188 [expansion from 129] 136 + p$186 -> (pbeta(var(i),t)=>pbeta(t,var(i)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(u,v) [expansion from 129] 137 + p$186 -> pbeta(var(i),t) [expansion from 129] 138 + p$185 -> p$188 [expansion from 130] 140 + pbeta(app(t,v),app(var(i),cd(u))) -> p$185 [expansion from 130] 141 + p$184,p$187 [expansion from 133] 142 + p$184 -> pbeta(s,t)=>pbeta(t,cd(s)) [expansion from 133] 143 + p$184 -> pbeta(s,t) [expansion from 133] 144 + p$184,pbeta(s,t) -> pbeta(t,cd(s)) [expansion from 142] 145 + p$183 -> p$187 [expansion from 134] 147 + pbeta(abs(t),abs(cd(s))) -> p$183 [expansion from 134] 148 + p$187,pbeta(s,t) [negative chaining of 141 from 143] 149 + p$188,pbeta(var(i),t) [negative chaining of 135 from 137] 150 + pbeta(t,cd(s)) -> p$183 [negative chaining of 40 from 147] 151 + pbeta(t,var(i)),pbeta(v,cd(u)) -> p$185 [negative chaining of 64 from 140] 152 + p$184 -> p$187,pbeta(t,cd(s)) [negative chaining of 148 from 144] 153 + p$187 [reduction of 152 by [141,150,145,L,L]] 154 + p$189,p$188 -> [reduction of 132 by [153]] 155 + p$188,(pbeta(var(i),t)=>pbeta(t,var(i)))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(u,v) [negative chaining of 135 from 136] 156 + p$188,pbeta(t,var(i))and(pbeta(u,v)=>pbeta(v,cd(u)))and pbeta(u,v) [reduction of 155 by [149,L]] 157 + p$182,p$188 [expansion from 156] 158 + p$182 -> pbeta(t,var(i))and(pbeta(u,v)=>pbeta(v,cd(u))) [expansion from 156] 159 + p$182 -> pbeta(u,v) [expansion from 156] 160 + pbeta(u,v) [reduction of 159 by [157,154,131,78,L,L]] 161 + p$197 -> (pbeta(s,t)=>pbeta(t,cd(s)))and pbeta(v,cd(u))and pbeta(s,t) [reduction of 77 by [160,L]] 165 + p$182 -> pbeta(t,var(i))and pbeta(v,cd(u)) [reduction of 158 by [160,L]] 166 + p$188,pbeta(t,var(i))and pbeta(v,cd(u)) [negative chaining of 157 from 165] 167 + p$181,p$188 [expansion from 166] 168 + p$181 -> pbeta(t,var(i)) [expansion from 166] 169 + p$181 -> pbeta(v,cd(u)) [expansion from 166] 170 + p$188,pbeta(t,var(i)) [negative chaining of 167 from 168] 171 + p$188,pbeta(v,cd(u)) [negative chaining of 167 from 169] 172 + p$188 [reduction of 171 by [151,138,L,170,L]] 173 + p$189 -> [reduction of 154 by [172]] 174 + pbeta(app(abs(s),u),app(abs(t),v))=>pbeta(app(abs(t),v),subst(cd(s),0,cd(u))) -> [reduction of 127 by [173,L]] 175 + p$197 [reduction of 131 by [173,L]] 176 + (pbeta(s,t)=>pbeta(t,cd(s)))and pbeta(v,cd(u))and pbeta(s,t) [reduction of 161 by [175]] 178 + pbeta(app(abs(t),v),subst(cd(s),0,cd(u))) -> [expansion from 174] 179 + (pbeta(s,t)=>pbeta(t,cd(s)))and pbeta(v,cd(u)) [expansion from 176] 180 + pbeta(s,t) [expansion from 176] 183 + pbeta(t,cd(s))and pbeta(v,cd(u)) [reduction of 179 by [180,L]] 184 + pbeta(t,cd(s)) [expansion from 183] 185 + pbeta(v,cd(u)) [expansion from 183] 196 + pbeta(t,cd(s)),pbeta(v,cd(u)) -> [negative chaining of 65 from 178] 197 + false [reduction of 196 by [184,185]] Length = 126, Depth = 37 Total time: 157610 milliseconds Number of forward inferences: 27 Number of tableau inferences: 64 Number of kept clauses: 160 */