API tools faq
paste
Advertisement
Guest User

eqn_compiler debug output

a guest
Jan 11th, 2019
120
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 7.78 KB | None | 0 0
raw download clone embed print report
  1. [debug.eqn_compiler.elim_match] code:
  2. λ {l n m : ℕ} (a : bounded_preformula L n l) (a_1 : dvector (fin m) n),
  3. bounded_preformula.cases_on a
  4. (λ {a_1 : ℕ} (H_1 : n = a_1),
  5. eq.rec
  6. (λ (a_1 : l = 0),
  7. eq.rec
  8. (λ (a : bounded_preformula L n 0) (H_3 : a == ⊥), eq.rec (id_rhs (bounded_preformula L m 0) ⊥) _)
  9. _
  10. a)
  11. H_1)
  12. (λ {a_n : ℕ} (a_t₁ a_t₂ : bounded_term L a_n) (H_1 : n = a_n),
  13. eq.rec
  14. (λ (a_t₁ a_t₂ : bounded_term L n) (a_2 : l = 0),
  15. eq.rec
  16. (λ (a : bounded_preformula L n 0) (H_3 : a == a_t₁ ≃ a_t₂),
  17. eq.rec
  18. (id_rhs (bounded_preformula L m 0)
  19. (subst_var_bounded_term a_t₁ a_1 ≃ subst_var_bounded_term a_t₁ a_1))
  20. _)
  21. _
  22. a)
  23. H_1
  24. a_t₁
  25. a_t₂)
  26. (λ {a_n a_l : ℕ} (a_R : L.relations a_l) (H_1 : n = a_n),
  27. eq.rec
  28. (λ (H_2 : l = a_l),
  29. eq.rec
  30. (λ (a_R : L.relations l) (H_3 : a == bd_rel a_R),
  31. eq.rec (id_rhs (bounded_preformula L m l) (bd_rel a_R)) _)
  32. H_2
  33. a_R)
  34. H_1)
  35. (λ {a_n a_l : ℕ} (a_f : bounded_preformula L a_n (a_l + 1)) (a_t : bounded_term L a_n) (H_1 : n = a_n),
  36. eq.rec
  37. (λ (a_f : bounded_preformula L n (a_l + 1)) (a_t : bounded_term L n) (H_2 : l = a_l),
  38. eq.rec
  39. (λ (a_f : bounded_preformula L n (l + 1)) (H_3 : a == bd_apprel a_f a_t),
  40. eq.rec
  41. (id_rhs (bounded_preformula L m l)
  42. (bd_apprel ([fol.subst_var_bounded_formula._main._meta_aux] a_f a_1)
  43. (subst_var_bounded_term a_t a_1)))
  44. _)
  45. H_2
  46. a_f)
  47. H_1
  48. a_f
  49. a_t)
  50. (λ {a_n : ℕ} (a_f₁ a_f₂ : bounded_preformula L a_n 0) (H_1 : n = a_n),
  51. eq.rec
  52. (λ (a_f₁ a_f₂ : bounded_preformula L n 0) (a_2 : l = 0),
  53. eq.rec
  54. (λ (a : bounded_preformula L n 0) (H_3 : a == a_f₁ ⟹ a_f₂),
  55. eq.rec
  56. (id_rhs (bounded_preformula L m 0)
  57. ([fol.subst_var_bounded_formula._main._meta_aux] a_f₁ a_1 ⟹
  58. [fol.subst_var_bounded_formula._main._meta_aux] a_f₂ a_1))
  59. _)
  60. _
  61. a)
  62. H_1
  63. a_f₁
  64. a_f₂)
  65. (λ {a_n : ℕ} (a_f : bounded_preformula L (a_n + 1) 0) (H_1 : n = a_n),
  66. eq.rec
  67. (λ (a_f : bounded_preformula L (n + 1) 0) (a_2 : l = 0),
  68. eq.rec
  69. (λ (a : bounded_preformula L n 0) (H_3 : a == ∀' a_f),
  70. eq.rec
  71. (id_rhs (bounded_preformula L m 0)
  72. (∀'[fol.subst_var_bounded_formula._main._meta_aux] a_f (dvector_lift_var a_1)))
  73. _)
  74. _
  75. a)
  76. H_1
  77. a_f)
  78. _
  79. _
  80. _
  81. [debug.eqn_compiler.elim_match] code:
  82. λ {l n m : ℕ} (a : bounded_preformula L n l) (a_1 : dvector (fin m) n) (_F : bounded_preformula.below L a),
  83. bounded_preformula.cases_on a
  84. (λ {a_1 : ℕ} (H_1 : n = a_1),
  85. eq.rec
  86. (λ (a_1 : l = 0),
  87. eq.rec
  88. (λ (a : bounded_preformula L n 0) (_F : bounded_preformula.below L a) (H_3 : a == ⊥),
  89. eq.rec (λ (_F : bounded_preformula.below L ⊥), id_rhs (bounded_preformula L m 0) ⊥) _ _F)
  90. _
  91. a
  92. _F)
  93. H_1)
  94. (λ {a_n : ℕ} (a_t₁ a_t₂ : bounded_term L a_n) (H_1 : n = a_n),
  95. eq.rec
  96. (λ (a_t₁ a_t₂ : bounded_term L n) (a_2 : l = 0),
  97. eq.rec
  98. (λ (a : bounded_preformula L n 0) (_F : bounded_preformula.below L a) (H_3 : a == a_t₁ ≃ a_t₂),
  99. eq.rec
  100. (λ (_F : bounded_preformula.below L (a_t₁ ≃ a_t₂)),
  101. id_rhs (bounded_preformula L m 0)
  102. (subst_var_bounded_term a_t₁ a_1 ≃ subst_var_bounded_term a_t₁ a_1))
  103. _
  104. _F)
  105. _
  106. a
  107. _F)
  108. H_1
  109. a_t₁
  110. a_t₂)
  111. (λ {a_n a_l : ℕ} (a_R : L.relations a_l) (H_1 : n = a_n),
  112. eq.rec
  113. (λ (H_2 : l = a_l),
  114. eq.rec
  115. (λ (a_R : L.relations l) (H_3 : a == bd_rel a_R),
  116. eq.rec
  117. (λ (_F : bounded_preformula.below L (bd_rel a_R)), id_rhs (bounded_preformula L m l) (bd_rel a_R))
  118. _
  119. _F)
  120. H_2
  121. a_R)
  122. H_1)
  123. (λ {a_n a_l : ℕ} (a_f : bounded_preformula L a_n (a_l + 1)) (a_t : bounded_term L a_n) (H_1 : n = a_n),
  124. eq.rec
  125. (λ (a_f : bounded_preformula L n (a_l + 1)) (a_t : bounded_term L n) (H_2 : l = a_l),
  126. eq.rec
  127. (λ (a_f : bounded_preformula L n (l + 1)) (H_3 : a == bd_apprel a_f a_t),
  128. eq.rec
  129. (λ (_F : bounded_preformula.below L (bd_apprel a_f a_t)),
  130. id_rhs (bounded_preformula L m l) (bd_apprel ((_F.fst).fst a_1) (subst_var_bounded_term a_t a_1)))
  131. _
  132. _F)
  133. H_2
  134. a_f)
  135. H_1
  136. a_f
  137. a_t)
  138. (λ {a_n : ℕ} (a_f₁ a_f₂ : bounded_preformula L a_n 0) (H_1 : n = a_n),
  139. eq.rec
  140. (λ (a_f₁ a_f₂ : bounded_preformula L n 0) (a_2 : l = 0),
  141. eq.rec
  142. (λ (a : bounded_preformula L n 0) (_F : bounded_preformula.below L a) (H_3 : a == a_f₁ ⟹ a_f₂),
  143. eq.rec
  144. (λ (_F : bounded_preformula.below L (a_f₁ ⟹ a_f₂)),
  145. id_rhs (bounded_preformula L m 0) ((_F.fst).fst a_1 ⟹ ((_F.snd).fst).fst a_1))
  146. _
  147. _F)
  148. _
  149. a
  150. _F)
  151. H_1
  152. a_f₁
  153. a_f₂)
  154. (λ {a_n : ℕ} (a_f : bounded_preformula L (a_n + 1) 0) (H_1 : n = a_n),
  155. eq.rec
  156. (λ (a_f : bounded_preformula L (n + 1) 0) (a_2 : l = 0),
  157. eq.rec
  158. (λ (a : bounded_preformula L n 0) (_F : bounded_preformula.below L a) (H_3 : a == ∀' a_f),
  159. eq.rec
  160. (λ (_F : bounded_preformula.below L (∀' a_f)),
  161. id_rhs (bounded_preformula L m 0) (∀'(_F.fst).fst (dvector_lift_var a_1)))
  162. _
  163. _F)
  164. _
  165. a
  166. _F)
  167. H_1
  168. a_f)
  169. _
  170. _
  171. _
  172. [debug.eqn_compiler.structural_rec] elim_match equation rhs:
  173. ⊥
  174. [debug.eqn_compiler.structural_rec] elim_match equation rhs:
  175. subst_var_bounded_term t₁ v ≃ subst_var_bounded_term t₁ v
  176. [debug.eqn_compiler.structural_rec] elim_match equation rhs:
  177. bd_rel R
  178. [debug.eqn_compiler.structural_rec] elim_match equation rhs:
  179. bd_apprel ((_F.fst).fst v) (subst_var_bounded_term t v)
  180. [debug.eqn_compiler.structural_rec] decoded equation rhs term:
  181. (_F.fst).fst v
  182. ==>
  183. subst_var_bounded_formula._main f v
  184. [debug.eqn_compiler.structural_rec] elim_match equation rhs:
  185. (_F.fst).fst v ⟹ ((_F.snd).fst).fst v
  186. [debug.eqn_compiler.structural_rec] decoded equation rhs term:
  187. (_F.fst).fst v
  188. ==>
  189. subst_var_bounded_formula._main f₁ v
  190. [debug.eqn_compiler.structural_rec] decoded equation rhs term:
  191. ((_F.snd).fst).fst v
  192. ==>
  193. subst_var_bounded_formula._main f₂ v
  194. [debug.eqn_compiler.structural_rec] elim_match equation rhs:
  195. ∀'(_F.fst).fst (dvector_lift_var v)
  196. [debug.eqn_compiler.structural_rec] decoded equation rhs term:
  197. (_F.fst).fst (dvector_lift_var v)
  198. ==>
  199. subst_var_bounded_formula._main f (dvector_lift_var v)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!