Library hydras.MoreAck.expressibleExamples
From hydras.Ackermann Require Import expressible.
From hydras.Ackermann Require Import NN NewNotations NNtheory.
Import NNnotations.
From Coq Require Import Lia.
Goal ∀ n, RepresentableHalf1 NN 0 n (v#0 = natToTerm n)%fol.
Lemma L1: RepresentableHalf1 NN 1 (fun n ⇒ n + n)
(v#0 = v#1 + v#1)%fol.
Lemma L2: RepresentableHalf2 NN 1 (fun n ⇒ n + n)
(v#0 = v#1 + v#1)%fol.
Lemma L3: Representable NN 1 (fun n ⇒ n + n) (v#0 = v#1 + v#1)%fol.
Lemma L4 : Representable NN 1 (fun n ⇒ n × 2) (v#0 = v#1 + v#1)%fol.
From hydras.Ackermann Require Import NN NewNotations NNtheory.
Import NNnotations.
From Coq Require Import Lia.
Goal ∀ n, RepresentableHalf1 NN 0 n (v#0 = natToTerm n)%fol.
Lemma L1: RepresentableHalf1 NN 1 (fun n ⇒ n + n)
(v#0 = v#1 + v#1)%fol.
Lemma L2: RepresentableHalf2 NN 1 (fun n ⇒ n + n)
(v#0 = v#1 + v#1)%fol.
Lemma L3: Representable NN 1 (fun n ⇒ n + n) (v#0 = v#1 + v#1)%fol.
Lemma L4 : Representable NN 1 (fun n ⇒ n × 2) (v#0 = v#1 + v#1)%fol.
Mind the order of variables v#1 ... v#n
f v#n ... v#1 = v#0
v#2 is bound to n
Lemma L5: RepresentableHalf1 NN 2 (fun n p ⇒ n) (v#0 = v#2)%fol.
Search substT . Search (SysPrf _ (?A → ?A)%fol).
Search freeVarT (S_ _).
Qed.
v#1 is bound to p