OAI/Computability/QuantumFactoring/NativeAIGExtend.lean
13 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ExactQuantumFactoring.NativeAIG.eraseVec_getDline 14 - lemma
OAI.ExactQuantumFactoring.NativeAIG.eraseVec_appendline 21 - def
OAI.ExactQuantumFactoring.NativeAIG.extendline 32 - lemma
OAI.ExactQuantumFactoring.NativeAIG.extend_lengthline 34 - lemma
OAI.ExactQuantumFactoring.NativeAIG.extend_refsline 35 - lemma
OAI.ExactQuantumFactoring.NativeAIG.extend_go_relline 41 - lemma
OAI.ExactQuantumFactoring.NativeAIG.extend_relline 63 - def
OAI.ExactQuantumFactoring.NativeAIG.shiftConcatline 68 - lemma
OAI.ExactQuantumFactoring.NativeAIG.shiftConcat_relline 69 - lemma
OAI.ExactQuantumFactoring.NativeAIG.shiftConcat_lengthline 75 - lemma
OAI.ExactQuantumFactoring.NativeAIG.shiftConcat_refsline 76 - def
OAI.ExactQuantumFactoring.NativeAIG.Emission.extendPline 86 - def
OAI.ExactQuantumFactoring.NativeAIG.Emission.shiftConcatPline 91